max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/spredProofMode.lean
Garmelon 08eb78a5b2
chore: switch to new test/bench suite (#12590) 
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.

For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
2026-02-25 13:51:53 +00:00

390 lines
8.7 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Graf
-/
import Std.Do
import Std.Tactic.Do
open Std.Do
variable (σs : List Type)
theorem start_stop (Q : SPred σs) (H : Q ⊢ₛ Q) : Q ⊢ₛ Q := by
mstart
mintro HQ
mstop
exact H
theorem exact (Q : SPred σs) : Q ⊢ₛ Q := by
mstart
mintro HQ
mexact HQ
theorem exact_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by
mintro -
mexact hP
theorem clear (P Q : SPred σs) : P ⊢ₛ Q → Q := by
mintro HP
mintro HQ
mclear HP
mexact HQ
/--
trace: σs : List Type
P Q : SPred σs
⊢ ⏎
h✝¹ : Q
h✝ : P
⊢ₛ Q
-/
#guard_msgs in
theorem assumption (P Q : SPred σs) : Q ⊢ₛ P → Q := by
mintro _
mintro _
-- NB: We want
-- h✝¹ : Q
-- h✝ : P
-- Not
-- h✝ : Q
-- h✝¹ : P
-- just like for `intro _ _`.
trace_state
massumption
theorem assumption_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by
mintro _
massumption
namespace pure
theorem move (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
mintro Hφ
mpure Hφ
mexact (ψ Hφ)
/--
trace: σs : List Type
φ₁ φ₂ : Prop
Q : SPred σs
⊢ ⏎
Hφ1 : ⌜φ₁⌝
Hφ2 : ⌜φ₂⌝
HQ : Q
⊢ₛ Q
-/
#guard_msgs in
theorem move_multiple (Q : SPred σs) : ⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝ → Q → Q := by
mintro Hφ1
mintro Hφ2
mintro HQ
trace_state
mpure Hφ1
mpure Hφ2
mexact HQ
theorem move_conjunction (Q : SPred σs) : (⌜φ₁⌝ ∧ ⌜φ₂⌝) ⊢ₛ Q → Q := by
mintro Hφ
mintro HQ
mpure Hφ
mexact HQ
theorem rename_i1 (P Q R : SPred σs) : ⊢ₛ P → Q → R → Q := by
mintro _ _ _
mrename_i HQ _
mexact HQ
theorem rename_i2 (P Q R : SPred σs) : ⊢ₛ P → Q → R → R → Q := by
mintro H H H H
mrename_i _ HQ _
mexact HQ
end pure
namespace pureintro
theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
mpure_intro
exact True.intro
theorem or : ⊢ₛ ⌜True⌝ ∨ (⌜False⌝ : SPred σs) := by
mpure_intro
left
exact True.intro
theorem with_proof (H : A → B) (P Q : SPred σs) : P ⊢ₛ Q → ⌜A⌝ → ⌜B⌝ := by
mintro _HP _HQ
mpure_intro
exact H
end pureintro
namespace emptyhyp
/--
trace: σs : List Type
⊢ ⏎
h : ⌜True⌝
⊢ₛ ⌜True⌝
-/
#guard_msgs in
theorem true_named : ⊢ₛ (⌜True⌝ : SPred σs) → ⌜True⌝ := by
mintro h
trace_state
mexact h
/--
trace: σs : List Type
⊢ ⏎
⊢ₛ ⌜True⌝
-/
#guard_msgs in
theorem true_unnamed_hidden : ⊢ₛ (⌜True⌝ : SPred σs) → ⌜True⌝ := by
mintro _
trace_state
mpure_intro
exact True.intro
theorem or : ⊢ₛ ⌜True⌝ ∨ (⌜False⌝ : SPred σs) := by
mpure_intro
left
exact True.intro
theorem with_proof (H : A → B) (P Q : SPred σs) : P ⊢ₛ Q → ⌜A⌝ → ⌜B⌝ := by
mintro _HP _HQ
mpure_intro
exact H
end emptyhyp
namespace frame
theorem move (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
mintro _
mframe
mrename_i HQ H
mcases H with HP
mexact HQ
theorem move_multiple (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
mintro h
mcases h with ⟨hp, hQ, hq, rest⟩
mframe
mexact hQ
theorem move_all : ⊢ₛ ⌜p⌝ ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ ⌜s⌝ ∧ ⌜t⌝ → (⌜t⌝ : SPred []) := by
mintro h
mframe
mpure_intro
grind
end frame
theorem revert (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ R := by
mintro ⟨HP, HQ, HR⟩
mrevert HR
mrevert HP
mintro HP'
mintro HR'
mexact HR'
theorem revert_forall (H : SPred σs) (T : SPred (α::β::σs))
(h : (fun _ _ => H) ∧ (fun s₁ s₂ => ⌜s₁ = e₁ ∧ s₂ = e₂⌝) ⊢ₛ T) :
H ⊢ₛ T e₁ e₂ := by
mintro h
mrevert ∀2
exact h
namespace constructor
theorem and (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
mintro HQ
mconstructor <;> mexact HQ
end constructor
theorem exfalso (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
mintro HP
mexfalso
mexact HP
namespace leftright
theorem left (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
mintro HP
mleft
mexact HP
theorem right (P Q : SPred σs) : Q ⊢ₛ P ∨ Q := by
mintro HQ
mright
mexact HQ
theorem complex (P Q R : SPred σs) : ⊢ₛ P → Q → P ∧ (R ∨ Q ∨ R) := by
mintro HP HQ
mconstructor
· massumption
mright
mleft
mexact HQ
end leftright
namespace specialize
theorem simple (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
mintro HP HPQ
mspecialize HPQ HP
mexact HPQ
theorem multiple (P Q R : SPred σs) : ⊢ₛ P → Q → (P → Q → R) → R := by
mintro HP HQ HPQR
mspecialize HPQR HP HQ
mexact HPQR
theorem pure_imp (P Q R : SPred σs) : (⊢ₛ P) → ⊢ₛ Q → (P → Q → R) → R := by
intro HP
mintro HQ HPQR
mspecialize HPQR HP HQ
mexact HPQR
theorem forall' (y : Nat) (Q : Nat → SPred σs) : ⊢ₛ (∀ x, Q x) → Q (y + 1) := by
mintro HQ
mspecialize HQ (y + 1)
mexact HQ
theorem mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
mintro HQ HΨ
mspecialize HΨ (y + 1) hP HQ
mexact HΨ
theorem pure_mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
mintro HQ
mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
mexact HΨ
theorem pure_with_local (P : SPred σs) (hc : c) : (⌜c⌝ → P) ⊢ₛ P := by
mintro HP
mspecialize HP hc
mexact HP
end specialize
namespace havereplace
theorem mrepl (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
mintro HP HPQ
mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
mexact HPQ
theorem mhave (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
mintro HP HPQ
mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
mhave HQ := by mspecialize HPQ HP; mexact HPQ
mexact HQ
theorem mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
mintro HQ HΨ
mhave H := by mspecialize HΨ (y + 1) hP HQ; mexact HΨ
mexact H
end havereplace
namespace cases
theorem rename (P : SPred σs) : P ⊢ₛ P := by
mintro HP
mcases HP with HP'
mexact HP'
theorem clear (P Q : SPred σs) : ⊢ₛ P → Q → P := by
mintro HP HQ
mcases HQ with -
mexact HP
theorem pure (P : SPred σs) (Q : Prop) : φ → (⊢ₛ P → ⌜Q⌝ → P) := by
intro hφ
mintro HP HQ
mcases HQ with ⌜hQ⌝
mexact HP
theorem pure_exact (P : SPred σs) (Q : Prop) (hqr : Q → ⊢ₛ R) : ⊢ₛ P → ⌜Q⌝ → R := by
mintro HP HQ
mcases HQ with ⌜hQ⌝
mexact hqr hQ
theorem and (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ R := by
mintro HPQR
mcases HPQR with ⟨HP, HQ, HR⟩
mexact HR
theorem and_clear_pure (P Q R : SPred σs) (φ : Prop) : (P ∧ Q ∧ ⌜φ⌝ ∧ R) ⊢ₛ R := by
mintro HPQR
mcases HPQR with ⟨_, -, ⌜hφ⌝, HR⟩
mexact HR
theorem or (P Q R : SPred σs) : P ∧ (Q ∨ R) ∧ (Q → R) ⊢ₛ R := by
mintro H
mcases H with ⟨-, ⟨HQ | HR⟩, HQR⟩
· mspecialize HQR HQ
mexact HQR
· mexact HR
theorem and_persistent (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ R := by
mintro HPQR
mcases HPQR with ⟨#HP, HQ, □HR⟩
mexact HR
theorem and_pure (P Q R : Prop) : (⌜P⌝ ∧ ⌜Q⌝ ∧ ⌜R⌝) ⊢ₛ (⌜R⌝ : SPred σs) := by
mintro HPQR
mcases HPQR with ⟨%HP, ⌜HQ⌝, HR⟩
mpure_intro
exact HR
end cases
namespace introforall
theorem beta_conj (P Q R : SPred (Nat::σs)) (H : ∀ n, P n ∧ Q n ⊢ₛ R n) : P ∧ Q ⊢ₛ R := by
mintro ⟨HP, HQ⟩ ∀s
mstop
exact H s
end introforall
namespace refine
theorem and (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
mintro ⟨HP, HQ, HR⟩
mrefine ⟨HP, HR⟩
theorem exists_1 (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
mintro H
mrefine ⟨⌜42⌝, H⟩
theorem exists_2 (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
mintro H
mexists 42
end refine
theorem mosel1 {α : Type} (P : SPred σs) (Φ Ψ : α → SPred σs) :
P ∧ (∃ a, Φ a ∨ Ψ a) ⊢ₛ ∃ a, (P ∧ Φ a) ∨ (P ∧ Ψ a) := by
mintro ⟨HP, ⟨a, ⟨HΦ | HΨ⟩⟩⟩
· mexists a
mleft
mrefine ⟨HP, HΦ⟩
· mexists a
mright
mrefine ⟨HP, HΨ⟩
theorem mosel3 {α : Type} (P : SPred σs) (Φ Ψ : α → SPred σs) :
P ∧ (∃ a, Φ a ∨ Ψ a) ⊢ₛ ∃ a, Φ a ∨ (P ∧ P ∧ Ψ a) := by
mintro ⟨HP, ⟨a, ⟨HΦ | HΨ⟩⟩⟩
· mexists a
mleft
mexact HΦ
· mexists a
mright
mrefine ⟨HP, HP, HΨ⟩
Reference in a new issue View git blame Copy permalink