diff --git a/doc/lean/calc.md b/doc/lean/calc.md index 9f42a3b0d5..c502c91339 100644 --- a/doc/lean/calc.md +++ b/doc/lean/calc.md @@ -17,7 +17,7 @@ may also be of the form `{ }`, where `` is a proof for some equality `a = b`. The form `{ }` is just syntax sugar for - Subst (Refl _{i-1}) + subst (refl _{i-1}) That is, we are claiming we can obtain `_i` by replacing `a` with `b` in `_{i-1}`. @@ -35,8 +35,8 @@ Here is an example := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : Nat::PlusComm d 1 - ... = e : Symm Ax4. + ... = 1 + d : Nat::plus::comm d 1 + ... = e : symm Ax4. ``` The proof expressions `_i` do not need to be explicitly provided. @@ -45,7 +45,7 @@ proof expression using the given tactic or solver. Even when tactics and solvers are not used, we can still use the elaboration engine to fill gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the -`Nat::PlusComm` theorem. The Lean elaboration engine will infer `d` and `1` for us. +`Nat::plus::comm` theorem. The Lean elaboration engine will infer `d` and `1` for us. Here is the same example using placeholders. ```lean @@ -53,8 +53,8 @@ Here is the same example using placeholders. := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : Nat::PlusComm _ _ - ... = e : Symm Ax4. + ... = 1 + d : Nat::plus::comm _ _ + ... = e : symm Ax4. ``` We can also use the operators `=>`, `⇒`, `<=>`, `⇔` and `≠` in calculational proofs. @@ -64,7 +64,7 @@ Here is an example. theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 := calc a = b : H1 ... = c + 1 : H2 - ... ≠ 0 : Nat::SuccNeZero _. + ... ≠ 0 : Nat::succ::nz _. ``` The Lean `let` construct can also be used to build calculational-like proofs. @@ -75,9 +75,9 @@ The Lean `let` construct can also be used to build calculational-like proofs. axiom Axf (a : Nat) : f (f a) = a. theorem T3 (a b : Nat) (H : P (f (f (f (f a)))) (f (f b))) : P a b - := let s1 : P (f (f a)) (f (f b)) := Subst H (Axf a), - s2 : P a (f (f b)) := Subst s1 (Axf a), - s3 : P a b := Subst s2 (Axf b) + := let s1 : P (f (f a)) (f (f b)) := subst H (Axf a), + s2 : P a (f (f b)) := subst s1 (Axf a), + s3 : P a b := subst s2 (Axf b) in s3. ``` diff --git a/examples/lean/even.lean b/examples/lean/even.lean index f76c20beca..2496d8258e 100644 --- a/examples/lean/even.lean +++ b/examples/lean/even.lean @@ -8,19 +8,19 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1. -- Prove that the sum of two even numbers is even. -- -- Notes: we use the macro --- Obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2 +-- obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2 -- -- It is syntax sugar for existential elimination. -- It expands to -- --- ExistsElim [expr]_1 (fun [binding], [expr]_2) +-- exists::elim [expr]_1 (fun [binding], [expr]_2) -- -- It is defined in the file macros.lua. -- -- We also use the calculational proof style. -- See doc/lean/calc.md for more information. -- --- We use the first two Obtain-expressions to extract the +-- We use the first two obtain-expressions to extract the -- witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2. -- We can do that because H1 and H2 are evidence/proof for the -- fact that 'a' and 'b' are even. @@ -29,12 +29,12 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1. -- the witness w1+w2 for the fact that a+b is also even. -- That is, we provide a derivation showing that a+b = 2*(w1 + w2) theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) -:= Obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1, - Obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2, - ExistsIntro (w1 + w2) - (calc a + b = 2*w1 + b : { Hw1 } - ... = 2*w1 + 2*w2 : { Hw2 } - ... = 2*(w1 + w2) : Symm (Nat::Distribute 2 w1 w2)). +:= obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1, + obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2, + exists::intro (w1 + w2) + (calc a + b = 2*w1 + b : { Hw1 } + ... = 2*w1 + 2*w2 : { Hw2 } + ... = 2*(w1 + w2) : symm (Nat::distribute 2 w1 w2)). -- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute. -- Lean can infer them automatically. @@ -50,12 +50,12 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) -- is left associative. Moreover, Lean normalizer does not use -- any theorems such as + associativity. theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) -:= Obtain (w : Nat) (Hw : a = 2*w + 1), from H, - ExistsIntro (w + 1) - (calc a + 1 = 2*w + 1 + 1 : { Hw } - ... = 2*w + (1 + 1) : Symm (Nat::PlusAssoc _ _ _) - ... = 2*w + 2*1 : Refl _ - ... = 2*(w + 1) : Symm (Nat::Distribute _ _ _)). +:= obtain (w : Nat) (Hw : a = 2*w + 1), from H, + exists::intro (w + 1) + (calc a + 1 = 2*w + 1 + 1 : { Hw } + ... = 2*w + (1 + 1) : symm (Nat::plus::assoc _ _ _) + ... = 2*w + 2*1 : refl _ + ... = 2*(w + 1) : symm (Nat::distribute _ _ _)). -- The following command displays the proof object produced by Lean after -- expanding macros, and infering implicit/missing arguments. diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean index 8e14b78cb6..d600ae7599 100644 --- a/examples/lean/ex1.lean +++ b/examples/lean/ex1.lean @@ -2,8 +2,8 @@ variable N : Type variable h : N -> N -> N -- Specialize congruence theorem for h-applications -theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := - Congr (Congr (Refl h) H1) H2 +theorem congrh {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := + congr (congr (refl h) H1) H2 -- Declare some variables variable a : N @@ -18,13 +18,13 @@ axiom H2 : b = e -- Proof that (h a b) = (h c e) theorem T1 : (h a b) = (h c e) := - DisjCases H1 - (λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) - (λ C2, CongrH (Trans (Conjunct2 C2) (Conjunct1 C2)) H2) + or::elim H1 + (λ C1, congrh ((and::eliml C1) ⋈ (and::elimr C1)) H2) + (λ C2, congrh ((and::elimr C2) ⋈ (and::eliml C2)) H2) -- We can use theorem T1 to prove other theorems theorem T2 : (h a (h a b)) = (h a (h c e)) := - CongrH (Refl a) T1 + congrh (refl a) T1 -- Display the last two objects (i.e., theorems) added to the environment print environment 2 diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean index 5a0e3a0c1d..c813ea2cdb 100644 --- a/examples/lean/ex2.lean +++ b/examples/lean/ex2.lean @@ -1,19 +1,16 @@ import macros. theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r -:= Assume H_pq_qr H_p, - let P_pq := Conjunct1 H_pq_qr, - P_qr := Conjunct2 H_pq_qr, - P_q := MP P_pq H_p - in MP P_qr P_q. +:= assume H_pq_qr H_p, + let P_pq := and::eliml H_pq_qr, + P_qr := and::elimr H_pq_qr + in P_qr ◂ (P_pq ◂ H_p) setoption pp::implicit true. print environment 1. theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c -:= Assume H_abc H_ab H_a, - let P_b := (MP H_ab H_a), - P_bc := (MP H_abc H_a) - in MP P_bc P_b. +:= assume H_abc H_ab H_a, + (H_abc ◂ H_a) ◂ (H_ab ◂ H_a) print environment 1. diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean index d5d8aec115..2030cf415d 100644 --- a/examples/lean/ex3.lean +++ b/examples/lean/ex3.lean @@ -1,28 +1,28 @@ import macros. theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) -:= Assume H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab). +:= assume H_ab, and::intro (and::elimr H_ab) (and::eliml H_ab). theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) -:= Assume H_ab, - DisjCases H_ab - (λ H_a, Disj2 b H_a) - (λ H_b, Disj1 H_b a). +:= assume H_ab, + or::elim H_ab + (λ H_a, or::intror b H_a) + (λ H_b, or::introl H_b a). --- (EM a) is the excluded middle a ∨ ¬a --- (MT H H_na) is Modus Tollens with +-- (em a) is the excluded middle a ∨ ¬a +-- (mt H H_na) is Modus Tollens with -- H : (a ⇒ b) ⇒ a) -- H_na : ¬a -- produces -- ¬(a ⇒ b) -- --- NotImp1 applied to +-- not::imp::eliml applied to -- (MT H H_na) : ¬(a ⇒ b) -- produces -- a theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a -:= Assume H, DisjCases (EM a) - (λ H_a, H_a) - (λ H_na, NotImp1 (MT H H_na)). +:= assume H, or::elim (em a) + (λ H_a, H_a) + (λ H_na, not::imp::eliml (mt H H_na)). print environment 3. \ No newline at end of file diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean index 23bcde8d69..e470b12d38 100644 --- a/examples/lean/ex4.lean +++ b/examples/lean/ex4.lean @@ -2,7 +2,7 @@ import Int import tactic definition a : Nat := 10 -- Trivial indicates a "proof by evaluation" -theorem T1 : a > 0 := Trivial -theorem T2 : a - 5 > 3 := Trivial +theorem T1 : a > 0 := trivial +theorem T2 : a - 5 > 3 := trivial -- The next one is commented because it fails --- theorem T3 : a > 11 := Trivial +-- theorem T3 : a > 11 := trivial diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean index b2866682c0..11c5746127 100644 --- a/examples/lean/ex5.lean +++ b/examples/lean/ex5.lean @@ -1,72 +1,49 @@ +import macros + scope theorem ReflIf (A : Type) (R : A → A → Bool) - (Symmetry : Π x y, R x y → R y x) - (Transitivity : Π x y z, R x y → R y z → R x z) + (Symm : Π x y, R x y → R y x) + (Trans : Π x y z, R x y → R y z → R x z) (Linked : Π x, ∃ y, R x y) : Π x, R x x := - fun x, ExistsElim (Linked x) - (fun (w : A) (H : R x w), - let L1 : R w x := Symmetry x w H - in Transitivity x w x H L1) + λ x, obtain (w : A) (H : R x w), from (Linked x), + let L1 : R w x := Symm x w H + in Trans x w x H L1 + pop::scope scope - -- Same example but using ∀ instead of Π and ⇒ instead of → + -- Same example but using ∀ instead of Π and ⇒ instead of →. + -- Remark: H ↓ x is syntax sugar for forall::elim H x + -- Remark: H1 ◂ H2 is syntax sugar for mp H1 H2 theorem ReflIf (A : Type) (R : A → A → Bool) - (Symmetry : ∀ x y, R x y ⇒ R y x) - (Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z) + (Symm : ∀ x y, R x y ⇒ R y x) + (Trans : ∀ x y z, R x y ⇒ R y z ⇒ R x z) (Linked : ∀ x, ∃ y, R x y) : ∀ x, R x x := - ForallIntro (fun x, - ExistsElim (ForallElim Linked x) - (fun (w : A) (H : R x w), - let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H) - in (MP (MP (ForallElim (ForallElim (ForallElim Transitivity x) w) x) H) L1))) + take x, obtain (w : A) (H : R x w), from (Linked ↓ x), + let L1 : R w x := Symm ↓ x ↓ w ◂ H + in Trans ↓ x ↓ w ↓ x ◂ H ◂ L1 - -- We can make the previous example less verbose by using custom notation - - infixl 50 ! : ForallElim - infixl 30 << : MP - - theorem ReflIf2 (A : Type) - (R : A → A → Bool) - (Symmetry : ∀ x y, R x y ⇒ R y x) - (Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z) - (Linked : ∀ x, ∃ y, R x y) - : - ∀ x, R x x := - ForallIntro (fun x, - ExistsElim (Linked ! x) - (fun (w : A) (H : R x w), - let L1 : R w x := Symmetry ! x ! w << H - in Transitivity ! x ! w ! x << H << L1)) - - print environment 1 pop::scope scope -- Same example again. variable A : Type variable R : A → A → Bool - axiom Symmetry {x y : A} : R x y → R y x - axiom Transitivity {x y z : A} : R x y → R y z → R x z + axiom Symm {x y : A} : R x y → R y x + axiom Trans {x y z : A} : R x y → R y z → R x z axiom Linked (x : A) : ∃ y, R x y theorem ReflIf (x : A) : R x x := - ExistsElim (Linked x) (fun (w : A) (H : R x w), - let L1 : R w x := Symmetry H - in Transitivity H L1) + obtain (w : A) (H : R x w), from (Linked x), + let L1 : R w x := Symm H + in Trans H L1 - -- Even more compact proof of the same theorem - theorem ReflIf2 (x : A) : R x x := - ExistsElim (Linked x) (fun w H, Transitivity H (Symmetry H)) - - -- The command Endscope exports both theorem to the main scope - -- The variables and axioms in the scope become parameters to both theorems. end -- Display the last two theorems diff --git a/examples/lean/set.lean b/examples/lean/set.lean index 1ebbc059c1..48fd4358b9 100644 --- a/examples/lean/set.lean +++ b/examples/lean/set.lean @@ -8,31 +8,30 @@ infix 60 ∈ : element definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 ⇒ x ∈ s2 infix 50 ⊆ : subset -theorem SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 := - take s1 s2 s3, Assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3), +theorem subset::trans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 := + take s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3), have s1 ⊆ s3 : - take x, Assume Hin : x ∈ s1, + take x, assume Hin : x ∈ s1, have x ∈ s3 : - let L1 : x ∈ s2 := MP (Instantiate H1 x) Hin - in MP (Instantiate H2 x) L1 + let L1 : x ∈ s2 := H1 ↓ x ◂ Hin + in H2 ↓ x ◂ L1 -theorem SubsetExt (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 := - take s1 s2, Assume (H : ∀ x, x ∈ s1 = x ∈ s2), - Abst (fun x, Instantiate H x) +theorem subset::ext (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 := + take s1 s2, assume (H : ∀ x, x ∈ s1 = x ∈ s2), + abst (λ x, H ↓ x) -theorem SubsetAntiSymm (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := - take s1 s2, Assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1), +theorem subset::antisym (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := + take s1 s2, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1), have s1 = s2 : - MP (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 : - Instantiate (SubsetExt A) s1 s2) - (have (∀ x, x ∈ s1 = x ∈ s2) : - take x, have x ∈ s1 = x ∈ s2 : - let L1 : x ∈ s1 ⇒ x ∈ s2 := Instantiate H1 x, - L2 : x ∈ s2 ⇒ x ∈ s1 := Instantiate H2 x - in ImpAntisym L1 L2) + (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 : + (subset::ext A) ↓ s1 ↓ s2) + ◂ (have (∀ x, x ∈ s1 = x ∈ s2) : + take x, have x ∈ s1 = x ∈ s2 : + iff::intro (have x ∈ s1 ⇒ x ∈ s2 : H1 ↓ x) + (have x ∈ s2 ⇒ x ∈ s1 : H2 ↓ x)) + -- Compact (but less readable) version of the previous theorem -theorem SubsetAntiSymm2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := - take s1 s2, Assume H1 H2, - MP (Instantiate (SubsetExt A) s1 s2) - (take x, ImpAntisym (Instantiate H1 x) (Instantiate H2 x)) +theorem subset::antisym2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := + take s1 s2, assume H1 H2, + (subset::ext A) ↓ s1 ↓ s2 ◂ (take x, iff::intro (H1 ↓ x) (H2 ↓ x)) diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean index 4de6d4bbbb..50e1dcd208 100644 --- a/examples/lean/tactic1.lean +++ b/examples/lean/tactic1.lean @@ -1,10 +1,8 @@ -- This example demonstrates how to specify a proof skeleton that contains -- "holes" that must be filled using user-defined tactics. +import tactic (* --- import useful macros for creating tactics -import("tactic.lua") - -- Define a simple tactic using Lua auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac())) diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean index c3d10e86d9..e2f86d5a1a 100644 --- a/examples/lean/tactic_in_lua.lean +++ b/examples/lean/tactic_in_lua.lean @@ -42,7 +42,7 @@ local pb = s:proof_builder() local new_pb = function(m, a) - local Conj = Const("Conj") + local Conj = Const({"and", "intro"}) local new_m = proof_map(m) -- Copy proof map m for _, p in ipairs(proof_info) do local n = p[1] -- n is the name of the goal splitted by this tactic diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 6e2e3feaab..3e40671d7a 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -30,219 +30,217 @@ infix 50 > : gt definition id (a : Nat) := a notation 55 | _ | : id -axiom SuccNeZero (a : Nat) : a + 1 ≠ 0 -axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b -axiom PlusZero (a : Nat) : a + 0 = a -axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1 -axiom MulZero (a : Nat) : a * 0 = 0 -axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a -axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b -axiom Induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : Π (n : Nat) (iH : P n), P (n + 1)) : P a +axiom succ::nz (a : Nat) : a + 1 ≠ 0 +axiom succ::inj {a b : Nat} (H : a + 1 = b + 1) : a = b +axiom plus::zeror (a : Nat) : a + 0 = a +axiom plus::succr (a b : Nat) : a + (b + 1) = (a + b) + 1 +axiom mul::zeror (a : Nat) : a * 0 = 0 +axiom mul::succr (a b : Nat) : a * (b + 1) = a * b + a +axiom le::def (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b +axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : Π (n : Nat) (iH : P n), P (n + 1)) : P a -theorem ZeroNeOne : 0 ≠ 1 := Trivial - -theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a -:= Induction a - (Assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) +theorem pred::nz' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a +:= induction a + (assume H : 0 ≠ 0, false::elim (∃ b, b + 1 = 0) H) (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), - Assume H : n + 1 ≠ 0, - DisjCases (EM (n = 0)) - (λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) + assume H : n + 1 ≠ 0, + or::elim (em (n = 0)) + (λ Heq0 : n = 0, exists::intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 })) (λ Hne0 : n ≠ 0, - Obtain (w : Nat) (Hw : w + 1 = n), from (MP iH Hne0), - ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))) + obtain (w : Nat) (Hw : w + 1 = n), from (iH ◂ Hne0), + exists::intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))) -theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a -:= MP (NeZeroPred' a) H +theorem pred::nz {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a +:= (pred::nz' a) ◂ H -theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B -:= DisjCases (EM (a = 0)) +theorem destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B +:= or::elim (em (a = 0)) (λ Heq0 : a = 0, H1 Heq0) - (λ Hne0 : a ≠ 0, Obtain (w : Nat) (Hw : w + 1 = a), from (NeZeroPred Hne0), - H2 w (Symm Hw)) + (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred::nz Hne0), + H2 w (symm Hw)) -theorem ZeroPlus (a : Nat) : 0 + a = a -:= Induction a - (have 0 + 0 = 0 : Trivial) +theorem plus::zerol (a : Nat) : 0 + a = a +:= induction a + (have 0 + 0 = 0 : trivial) (λ (n : Nat) (iH : 0 + n = n), - calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n + calc 0 + (n + 1) = (0 + n) + 1 : plus::succr 0 n ... = n + 1 : { iH }) -theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 -:= Induction b - (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) - ... = (a + 0) + 1 : { Symm (PlusZero a) }) +theorem plus::succl (a b : Nat) : (a + 1) + b = (a + b) + 1 +:= induction b + (calc (a + 1) + 0 = a + 1 : plus::zeror (a + 1) + ... = (a + 0) + 1 : { symm (plus::zeror a) }) (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), - calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n + calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : plus::succr (a + 1) n ... = ((a + n) + 1) + 1 : { iH } - ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : Symm (PlusSucc a n) }) + ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (plus::succr a n) }) -theorem PlusComm (a b : Nat) : a + b = b + a -:= Induction b - (calc a + 0 = a : PlusZero a - ... = 0 + a : Symm (ZeroPlus a)) +theorem plus::comm (a b : Nat) : a + b = b + a +:= induction b + (calc a + 0 = a : plus::zeror a + ... = 0 + a : symm (plus::zerol a)) (λ (n : Nat) (iH : a + n = n + a), - calc a + (n + 1) = (a + n) + 1 : PlusSucc a n + calc a + (n + 1) = (a + n) + 1 : plus::succr a n ... = (n + a) + 1 : { iH } - ... = (n + 1) + a : Symm (SuccPlus n a)) + ... = (n + 1) + a : symm (plus::succl n a)) -theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c -:= Induction a - (calc 0 + (b + c) = b + c : ZeroPlus (b + c) - ... = (0 + b) + c : { Symm (ZeroPlus b) }) +theorem plus::assoc (a b c : Nat) : a + (b + c) = (a + b) + c +:= induction a + (calc 0 + (b + c) = b + c : plus::zerol (b + c) + ... = (0 + b) + c : { symm (plus::zerol b) }) (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), - calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) + calc (n + 1) + (b + c) = (n + (b + c)) + 1 : plus::succl n (b + c) ... = ((n + b) + c) + 1 : { iH } - ... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) - ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : Symm (SuccPlus n b) }) + ... = ((n + b) + 1) + c : symm (plus::succl (n + b) c) + ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (plus::succl n b) }) -theorem ZeroMul (a : Nat) : 0 * a = 0 -:= Induction a - (have 0 * 0 = 0 : Trivial) +theorem mul::zerol (a : Nat) : 0 * a = 0 +:= induction a + (have 0 * 0 = 0 : trivial) (λ (n : Nat) (iH : 0 * n = 0), - calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n + calc 0 * (n + 1) = (0 * n) + 0 : mul::succr 0 n ... = 0 + 0 : { iH } - ... = 0 : Trivial) + ... = 0 : trivial) -theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b -:= Induction b - (calc (a + 1) * 0 = 0 : MulZero (a + 1) - ... = a * 0 : Symm (MulZero a) - ... = a * 0 + 0 : Symm (PlusZero (a * 0))) +theorem mul::succl (a b : Nat) : (a + 1) * b = a * b + b +:= induction b + (calc (a + 1) * 0 = 0 : mul::zeror (a + 1) + ... = a * 0 : symm (mul::zeror a) + ... = a * 0 + 0 : symm (plus::zeror (a * 0))) (λ (n : Nat) (iH : (a + 1) * n = a * n + n), - calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n + calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul::succr (a + 1) n ... = a * n + n + (a + 1) : { iH } - ... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1 - ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : Symm (PlusAssoc (a * n) n a) } - ... = a * n + (a + n) + 1 : { PlusComm n a } - ... = a * n + a + n + 1 : { PlusAssoc (a * n) a n } - ... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) } - ... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)) + ... = a * n + n + a + 1 : plus::assoc (a * n + n) a 1 + ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (plus::assoc (a * n) n a) } + ... = a * n + (a + n) + 1 : { plus::comm n a } + ... = a * n + a + n + 1 : { plus::assoc (a * n) a n } + ... = a * (n + 1) + n + 1 : { symm (mul::succr a n) } + ... = a * (n + 1) + (n + 1) : symm (plus::assoc (a * (n + 1)) n 1)) -theorem OneMul (a : Nat) : 1 * a = a -:= Induction a - (have 1 * 0 = 0 : Trivial) +theorem mul::lhs::one (a : Nat) : 1 * a = a +:= induction a + (have 1 * 0 = 0 : trivial) (λ (n : Nat) (iH : 1 * n = n), - calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n + calc 1 * (n + 1) = 1 * n + 1 : mul::succr 1 n ... = n + 1 : { iH }) -theorem MulOne (a : Nat) : a * 1 = a -:= Induction a - (have 0 * 1 = 0 : Trivial) +theorem mul::rhs::one (a : Nat) : a * 1 = a +:= induction a + (have 0 * 1 = 0 : trivial) (λ (n : Nat) (iH : n * 1 = n), - calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 + calc (n + 1) * 1 = n * 1 + 1 : mul::succl n 1 ... = n + 1 : { iH }) -theorem MulComm (a b : Nat) : a * b = b * a -:= Induction b - (calc a * 0 = 0 : MulZero a - ... = 0 * a : Symm (ZeroMul a)) +theorem mul::comm (a b : Nat) : a * b = b * a +:= induction b + (calc a * 0 = 0 : mul::zeror a + ... = 0 * a : symm (mul::zerol a)) (λ (n : Nat) (iH : a * n = n * a), - calc a * (n + 1) = a * n + a : MulSucc a n + calc a * (n + 1) = a * n + a : mul::succr a n ... = n * a + a : { iH } - ... = (n + 1) * a : Symm (SuccMul n a)) + ... = (n + 1) * a : symm (mul::succl n a)) -theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c -:= Induction a - (calc 0 * (b + c) = 0 : ZeroMul (b + c) - ... = 0 + 0 : Trivial - ... = 0 * b + 0 : { Symm (ZeroMul b) } - ... = 0 * b + 0 * c : { Symm (ZeroMul c) }) +theorem distribute (a b c : Nat) : a * (b + c) = a * b + a * c +:= induction a + (calc 0 * (b + c) = 0 : mul::zerol (b + c) + ... = 0 + 0 : trivial + ... = 0 * b + 0 : { symm (mul::zerol b) } + ... = 0 * b + 0 * c : { symm (mul::zerol c) }) (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), - calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c) + calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul::succl n (b + c) ... = n * b + n * c + (b + c) : { iH } - ... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c - ... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) } - ... = n * b + (b + n * c) + c : { PlusComm (n * c) b } - ... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) } - ... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) } - ... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c) - ... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }) + ... = n * b + n * c + b + c : plus::assoc (n * b + n * c) b c + ... = n * b + (n * c + b) + c : { symm (plus::assoc (n * b) (n * c) b) } + ... = n * b + (b + n * c) + c : { plus::comm (n * c) b } + ... = n * b + b + n * c + c : { plus::assoc (n * b) b (n * c) } + ... = (n + 1) * b + n * c + c : { symm (mul::succl n b) } + ... = (n + 1) * b + (n * c + c) : symm (plus::assoc ((n + 1) * b) (n * c) c) + ... = (n + 1) * b + (n + 1) * c : { symm (mul::succl n c) }) -theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c -:= calc (a + b) * c = c * (a + b) : MulComm (a + b) c - ... = c * a + c * b : Distribute c a b - ... = a * c + c * b : { MulComm c a } - ... = a * c + b * c : { MulComm c b } +theorem distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c +:= calc (a + b) * c = c * (a + b) : mul::comm (a + b) c + ... = c * a + c * b : distribute c a b + ... = a * c + c * b : { mul::comm c a } + ... = a * c + b * c : { mul::comm c b } -theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c -:= Induction a - (calc 0 * (b * c) = 0 : ZeroMul (b * c) - ... = 0 * c : Symm (ZeroMul c) - ... = (0 * b) * c : { Symm (ZeroMul b) }) +theorem mul::assoc (a b c : Nat) : a * (b * c) = a * b * c +:= induction a + (calc 0 * (b * c) = 0 : mul::zerol (b * c) + ... = 0 * c : symm (mul::zerol c) + ... = (0 * b) * c : { symm (mul::zerol b) }) (λ (n : Nat) (iH : n * (b * c) = n * b * c), - calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) + calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul::succl n (b * c) ... = n * b * c + (b * c) : { iH } - ... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) - ... = (n + 1) * b * c : { Symm (SuccMul n b) }) + ... = (n * b + b) * c : symm (distribute2 (n * b) b c) + ... = (n + 1) * b * c : { symm (mul::succl n b) }) -theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c -:= Induction a - (Assume H : 0 + b = 0 + c, - calc b = 0 + b : Symm (ZeroPlus b) +theorem plus::inj' (a b c : Nat) : a + b = a + c ⇒ b = c +:= induction a + (assume H : 0 + b = 0 + c, + calc b = 0 + b : symm (plus::zerol b) ... = 0 + c : H - ... = c : ZeroPlus c) + ... = c : plus::zerol c) (λ (n : Nat) (iH : n + b = n + c ⇒ b = c), - Assume H : n + 1 + b = n + 1 + c, + assume H : n + 1 + b = n + 1 + c, let L1 : n + b + 1 = n + c + 1 - := (calc n + b + 1 = n + (b + 1) : Symm (PlusAssoc n b 1) - ... = n + (1 + b) : { PlusComm b 1 } - ... = n + 1 + b : PlusAssoc n 1 b + := (calc n + b + 1 = n + (b + 1) : symm (plus::assoc n b 1) + ... = n + (1 + b) : { plus::comm b 1 } + ... = n + 1 + b : plus::assoc n 1 b ... = n + 1 + c : H - ... = n + (1 + c) : Symm (PlusAssoc n 1 c) - ... = n + (c + 1) : { PlusComm 1 c } - ... = n + c + 1 : PlusAssoc n c 1), - L2 : n + b = n + c := SuccInj L1 - in MP iH L2) + ... = n + (1 + c) : symm (plus::assoc n 1 c) + ... = n + (c + 1) : { plus::comm 1 c } + ... = n + c + 1 : plus::assoc n c 1), + L2 : n + b = n + c := succ::inj L1 + in iH ◂ L2) -theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c -:= MP (PlusInj' a b c) H +theorem plus::inj {a b c : Nat} (H : a + b = a + c) : b = c +:= (plus::inj' a b c) ◂ H -theorem PlusEq0 {a b : Nat} (H : a + b = 0) : a = 0 -:= Destruct (λ H1 : a = 0, H1) +theorem plus::eqz {a b : Nat} (H : a + b = 0) : a = 0 +:= destruct (λ H1 : a = 0, H1) (λ (n : Nat) (H1 : a = n + 1), - AbsurdElim (a = 0) - H (calc a + b = n + 1 + b : { H1 } - ... = n + (1 + b) : Symm (PlusAssoc n 1 b) - ... = n + (b + 1) : { PlusComm 1 b } - ... = n + b + 1 : PlusAssoc n b 1 - ... ≠ 0 : SuccNeZero (n + b))) + absurd::elim (a = 0) + H (calc a + b = n + 1 + b : { H1 } + ... = n + (1 + b) : symm (plus::assoc n 1 b) + ... = n + (b + 1) : { plus::comm 1 b } + ... = n + b + 1 : plus::assoc n b 1 + ... ≠ 0 : succ::nz (n + b))) -theorem LeIntro {a b c : Nat} (H : a + c = b) : a ≤ b -:= EqMP (Symm (LeDef a b)) (have (∃ x, a + x = b) : ExistsIntro c H) +theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b +:= (symm (le::def a b)) ◆ (have (∃ x, a + x = b) : exists::intro c H) -theorem LeElim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b -:= EqMP (LeDef a b) H +theorem le::elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b +:= (le::def a b) ◆ H -theorem LeRefl (a : Nat) : a ≤ a := LeIntro (PlusZero a) +theorem le::refl (a : Nat) : a ≤ a := le::intro (plus::zeror a) -theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a) +theorem le::zero (a : Nat) : 0 ≤ a := le::intro (plus::zerol a) -theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c -:= Obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), - Obtain (w2 : Nat) (Hw2 : b + w2 = c), from (LeElim H2), - LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 - ... = b + w2 : { Hw1 } - ... = c : Hw2) +theorem le::trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c +:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1), + obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le::elim H2), + le::intro (calc a + (w1 + w2) = a + w1 + w2 : plus::assoc a w1 w2 + ... = b + w2 : { Hw1 } + ... = c : Hw2) -theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c -:= Obtain (w : Nat) (Hw : a + w = b), from (LeElim H), - LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) - ... = a + (w + c) : { PlusComm c w } - ... = a + w + c : PlusAssoc a w c +theorem le::plus {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c +:= obtain (w : Nat) (Hw : a + w = b), from (le::elim H), + le::intro (calc a + c + w = a + (c + w) : symm (plus::assoc a c w) + ... = a + (w + c) : { plus::comm c w } + ... = a + w + c : plus::assoc a w c ... = b + c : { Hw }) -theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b -:= Obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), - Obtain (w2 : Nat) (Hw2 : b + w2 = a), from (LeElim H2), +theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b +:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1), + obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le::elim H2), let L1 : w1 + w2 = 0 - := PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } - ... = b + w2 : { Hw1 } - ... = a : Hw2 - ... = a + 0 : Symm (PlusZero a)), - L2 : w1 = 0 := PlusEq0 L1 - in calc a = a + 0 : Symm (PlusZero a) - ... = a + w1 : { Symm L2 } + := plus::inj (calc a + (w1 + w2) = a + w1 + w2 : { plus::assoc a w1 w2 } + ... = b + w2 : { Hw1 } + ... = a : Hw2 + ... = a + 0 : symm (plus::zeror a)), + L2 : w1 = 0 := plus::eqz L1 + in calc a = a + 0 : symm (plus::zeror a) + ... = a + w1 : { symm L2 } ... = b : Hw1 setopaque ge true diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index 6d98130247..8bc01e02fe 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -5,20 +5,20 @@ variable cast {A B : (Type U)} : A == B → A → B. -- The CastEq axiom states that for any cast of x is equal to x. -axiom CastEq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x. +axiom cast::eq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x. -- The CastApp axiom "propagates" the cast over application -axiom CastApp {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} +axiom cast::app {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : A == A') (f : Π x : A, B x) (x : A) : cast H1 f (cast H2 x) == f x. -- If two (dependent) function spaces are equal, then their domains are equal. -axiom DomInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} +axiom dominj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} (H : (Π x : A, B x) == (Π x : A', B' x)) : A == A'. -- If two (dependent) function spaces are equal, then their ranges are equal. -axiom RanInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} +axiom raninj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} (H : (Π x : A, B x) == (Π x : A', B' x)) (a : A) : - B a == B' (cast (DomInj H) a). + B a == B' (cast (dominj H) a). diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 92cfbbe218..3fa7175bad 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -64,172 +64,176 @@ definition neq {A : TypeU} (a b : A) : Bool infix 50 ≠ : neq -axiom MP {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b +axiom mp {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b -axiom Discharge {a b : Bool} (H : a → b) : a ⇒ b +infixl 100 <| : mp +infixl 100 ◂ : mp -axiom Case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a +axiom discharge {a b : Bool} (H : a → b) : a ⇒ b -axiom Refl {A : TypeU} (a : A) : a == a +axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a -axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b +axiom refl {A : TypeU} (a : A) : a == a -definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b -:= Subst H1 H2 +axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b -axiom Eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f +definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b +:= subst H1 H2 -axiom ImpAntisym {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : a == b +axiom eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f -axiom Abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g +axiom iff::intro {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : iff a b -axiom HSymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a +axiom abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g -axiom HTrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c +axiom hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a -theorem Trivial : true -:= Refl true +axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c -theorem TrueNeFalse : not (true == false) -:= Trivial +theorem trivial : true +:= refl true -theorem EM (a : Bool) : a ∨ ¬ a -:= Case (λ x, x ∨ ¬ x) Trivial Trivial a +theorem em (a : Bool) : a ∨ ¬ a +:= case (λ x, x ∨ ¬ x) trivial trivial a -theorem FalseElim (a : Bool) (H : false) : a -:= Case (λ x, x) Trivial H a +theorem false::elim (a : Bool) (H : false) : a +:= case (λ x, x) trivial H a -theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false -:= MP H2 H1 +theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false +:= H2 ◂ H1 -theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b -:= Subst H2 H1 +theorem eq::mp {a b : Bool} (H1 : a == b) (H2 : a) : b +:= subst H2 H1 --- Assume is a 'macro' that expands into a Discharge +infixl 100 <|> : eq::mp +infixl 100 ◆ : eq::mp -theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c -:= Assume Ha, MP H2 (MP H1 Ha) +-- assume is a 'macro' that expands into a discharge -theorem ImpEqTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c -:= Assume Ha, EqMP H2 (MP H1 Ha) +theorem imp::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c +:= assume Ha, H2 ◂ (H1 ◂ Ha) -theorem EqImpTrans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c -:= Assume Ha, MP H2 (EqMP H1 Ha) +theorem imp::eq::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c +:= assume Ha, H2 ◆ (H1 ◂ Ha) -theorem DoubleNeg (a : Bool) : (¬ ¬ a) == a -:= Case (λ x, (¬ ¬ x) == x) Trivial Trivial a +theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c +:= assume Ha, H2 ◂ (H1 ◆ Ha) -theorem DoubleNegElim {a : Bool} (H : ¬ ¬ a) : a -:= EqMP (DoubleNeg a) H +theorem not::not::eq (a : Bool) : (¬ ¬ a) == a +:= case (λ x, (¬ ¬ x) == x) trivial trivial a -theorem MT {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a -:= Assume H : a, Absurd (MP H1 H) H2 +theorem not::not::elim {a : Bool} (H : ¬ ¬ a) : a +:= (not::not::eq a) ◆ H -theorem Contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a -:= Assume H1 : ¬ b, MT H H1 +theorem mt {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a +:= assume H : a, absurd (H1 ◂ H) H2 -theorem AbsurdElim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b -:= FalseElim b (Absurd H1 H2) +theorem contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a +:= assume H1 : ¬ b, mt H H1 -theorem NotImp1 {a b : Bool} (H : ¬ (a ⇒ b)) : a -:= DoubleNegElim +theorem absurd::elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b +:= false::elim b (absurd H1 H2) + +theorem not::imp::eliml {a b : Bool} (H : ¬ (a ⇒ b)) : a +:= not::not::elim (have ¬ ¬ a : - Assume H1 : ¬ a, Absurd (have a ⇒ b : Assume H2 : a, AbsurdElim b H2 H1) + assume H1 : ¬ a, absurd (have a ⇒ b : assume H2 : a, absurd::elim b H2 H1) (have ¬ (a ⇒ b) : H)) -theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b -:= Assume H1 : b, Absurd (have a ⇒ b : Assume H2 : a, H1) +theorem not::imp::elimr {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b +:= assume H1 : b, absurd (have a ⇒ b : assume H2 : a, H1) (have ¬ (a ⇒ b) : H) +theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b +:= H1 ◂ H2 + -- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean -theorem Conj {a b : Bool} (H1 : a) (H2 : b) : a ∧ b -:= Assume H : a ⇒ ¬ b, Absurd H2 (MP H H1) +theorem and::intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b +:= assume H : a ⇒ ¬ b, absurd H2 (H ◂ H1) -theorem Conjunct1 {a b : Bool} (H : a ∧ b) : a -:= NotImp1 H +theorem and::eliml {a b : Bool} (H : a ∧ b) : a +:= not::imp::eliml H -theorem Conjunct2 {a b : Bool} (H : a ∧ b) : b -:= DoubleNegElim (NotImp2 H) +theorem and::elimr {a b : Bool} (H : a ∧ b) : b +:= not::not::elim (not::imp::elimr H) -- Remark: disjunction is defined as ¬ a ⇒ b in Lean -theorem Disj1 {a : Bool} (H : a) (b : Bool) : a ∨ b -:= Assume H1 : ¬ a, AbsurdElim b H H1 +theorem or::introl {a : Bool} (H : a) (b : Bool) : a ∨ b +:= assume H1 : ¬ a, absurd::elim b H H1 -theorem Disj2 {b : Bool} (a : Bool) (H : b) : a ∨ b -:= Assume H1 : ¬ a, H +theorem or::intror {b : Bool} (a : Bool) (H : b) : a ∨ b +:= assume H1 : ¬ a, H -theorem ArrowToImplies {a b : Bool} (H : a → b) : a ⇒ b -:= Assume H1 : a, H H1 - -theorem Resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b -:= MP H1 H2 - -theorem DisjCases {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c -:= DoubleNegElim - (Assume H : ¬ c, - Absurd (have c : H3 (have b : Resolve1 H1 (have ¬ a : (MT (ArrowToImplies H2) H)))) +theorem or::elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c +:= not::not::elim + (assume H : ¬ c, + absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H)))) H) -theorem Refute {a : Bool} (H : ¬ a → false) : a -:= DisjCases (EM a) (λ H1 : a, H1) (λ H1 : ¬ a, FalseElim a (H H1)) +theorem refute {a : Bool} (H : ¬ a → false) : a +:= or::elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false::elim a (H H1)) -theorem Symm {A : TypeU} {a b : A} (H : a == b) : b == a -:= Subst (Refl a) H +theorem symm {A : TypeU} {a b : A} (H : a == b) : b == a +:= subst (refl a) H -theorem NeSymm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a -:= Assume H1 : b = a, MP H (Symm H1) +theorem trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c +:= subst H1 H2 -theorem EqNeTrans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c -:= Subst H2 (Symm H1) +infixl 100 ⋈ : trans -theorem NeEqTrans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c -:= Subst H1 H2 +theorem ne::symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a +:= assume H1 : b = a, H ◂ (symm H1) -theorem Trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c -:= Subst H1 H2 +theorem eq::ne::trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c +:= subst H2 (symm H1) -theorem EqTElim {a : Bool} (H : a == true) : a -:= EqMP (Symm H) Trivial +theorem ne::eq::trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c +:= subst H1 H2 -theorem EqTIntro {a : Bool} (H : a) : a == true -:= ImpAntisym (Assume H1 : a, Trivial) - (Assume H2 : true, H) +theorem eqt::elim {a : Bool} (H : a == true) : a +:= (symm H) ◆ trivial -theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a -:= SubstP (fun h : (Π x : A, B x), f a == h a) (Refl (f a)) H +theorem eqt::intro {a : Bool} (H : a) : a == true +:= iff::intro (assume H1 : a, trivial) + (assume H2 : true, H) + +theorem congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a +:= substp (fun h : (Π x : A, B x), f a == h a) (refl (f a)) H -- Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b) -- are not "definitionally equal" They are (B a) and (B b) -- They are provably equal, we just have to apply Congr1 -theorem Congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b -:= SubstP (fun x : A, f a == f x) (Refl (f a)) H +theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b +:= substp (fun x : A, f a == f x) (refl (f a)) H -- Remark: like the previous theorem we use heterogeneous equality We cannot use Trans theorem -- because the types are not definitionally equal -theorem Congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b -:= HTrans (Congr2 f H2) (Congr1 b H1) +theorem congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b +:= htrans (congr2 f H2) (congr1 b H1) -theorem ForallElim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a -:= EqTElim (Congr1 a H) +theorem forall::elim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a +:= eqt::elim (congr1 a H) -theorem ForallIntro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A P -:= Trans (Symm (Eta P)) - (Abst (λ x, EqTIntro (H x))) +infixl 100 ! : forall::elim +infixl 100 ↓ : forall::elim + +theorem forall::intro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A P +:= (symm (eta P)) ⋈ (abst (λ x, eqt::intro (H x))) -- Remark: the existential is defined as (¬ (forall x : A, ¬ P x)) -theorem ExistsElim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B -:= Refute (λ R : ¬ B, - Absurd (ForallIntro (λ a : A, MT (Assume H : P a, H2 a H) R)) +theorem exists::elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B +:= refute (λ R : ¬ B, + absurd (forall::intro (λ a : A, mt (assume H : P a, H2 a H) R)) H1) -theorem ExistsIntro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P -:= Assume H1 : (∀ x : A, ¬ P x), - Absurd H (ForallElim H1 a) +theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P +:= assume H1 : (∀ x : A, ¬ P x), + absurd H (forall::elim H1 a) -- At this point, we have proved the theorems we need using the -- definitions of forall, exists, and, or, =>, not We mark (some of) @@ -242,155 +246,151 @@ setopaque or true setopaque and true setopaque forall true -theorem OrComm (a b : Bool) : (a ∨ b) == (b ∨ a) -:= ImpAntisym (Assume H, DisjCases H (λ H1, Disj2 b H1) (λ H2, Disj1 H2 a)) - (Assume H, DisjCases H (λ H1, Disj2 a H1) (λ H2, Disj1 H2 b)) +theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a) +:= iff::intro (assume H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a)) + (assume H, or::elim H (λ H1, or::intror a H1) (λ H2, or::introl H2 b)) +theorem or::assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) +:= iff::intro (assume H : (a ∨ b) ∨ c, + or::elim H (λ H1 : a ∨ b, or::elim H1 (λ Ha : a, or::introl Ha (b ∨ c)) (λ Hb : b, or::intror a (or::introl Hb c))) + (λ Hc : c, or::intror a (or::intror b Hc))) + (assume H : a ∨ (b ∨ c), + or::elim H (λ Ha : a, (or::introl (or::introl Ha b) c)) + (λ H1 : b ∨ c, or::elim H1 (λ Hb : b, or::introl (or::intror a Hb) c) + (λ Hc : c, or::intror (a ∨ b) Hc))) -theorem OrAssoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) -:= ImpAntisym (Assume H : (a ∨ b) ∨ c, - DisjCases H (λ H1 : a ∨ b, DisjCases H1 (λ Ha : a, Disj1 Ha (b ∨ c)) (λ Hb : b, Disj2 a (Disj1 Hb c))) - (λ Hc : c, Disj2 a (Disj2 b Hc))) - (Assume H : a ∨ (b ∨ c), - DisjCases H (λ Ha : a, (Disj1 (Disj1 Ha b) c)) - (λ H1 : b ∨ c, DisjCases H1 (λ Hb : b, Disj1 (Disj2 a Hb) c) - (λ Hc : c, Disj2 (a ∨ b) Hc))) +theorem or::id (a : Bool) : (a ∨ a) == a +:= iff::intro (assume H, or::elim H (λ H1, H1) (λ H2, H2)) + (assume H, or::introl H a) -theorem OrId (a : Bool) : (a ∨ a) == a -:= ImpAntisym (Assume H, DisjCases H (λ H1, H1) (λ H2, H2)) - (Assume H, Disj1 H a) +theorem or::falsel (a : Bool) : (a ∨ false) == a +:= iff::intro (assume H, or::elim H (λ H1, H1) (λ H2, false::elim a H2)) + (assume H, or::introl H false) -theorem OrRhsFalse (a : Bool) : (a ∨ false) == a -:= ImpAntisym (Assume H, DisjCases H (λ H1, H1) (λ H2, FalseElim a H2)) - (Assume H, Disj1 H false) +theorem or::falser (a : Bool) : (false ∨ a) == a +:= (or::comm false a) ⋈ (or::falsel a) -theorem OrLhsFalse (a : Bool) : (false ∨ a) == a -:= Trans (OrComm false a) (OrRhsFalse a) +theorem or::truel (a : Bool) : (true ∨ a) == true +:= eqt::intro (case (λ x : Bool, true ∨ x) trivial trivial a) -theorem OrLhsTrue (a : Bool) : (true ∨ a) == true -:= EqTIntro (Case (λ x : Bool, true ∨ x) Trivial Trivial a) +theorem or::truer (a : Bool) : (a ∨ true) == true +:= (or::comm a true) ⋈ (or::truel a) -theorem OrRhsTrue (a : Bool) : (a ∨ true) == true -:= Trans (OrComm a true) (OrLhsTrue a) +theorem or::tauto (a : Bool) : (a ∨ ¬ a) == true +:= eqt::intro (em a) -theorem OrAnotA (a : Bool) : (a ∨ ¬ a) == true -:= EqTIntro (EM a) +theorem and::comm (a b : Bool) : (a ∧ b) == (b ∧ a) +:= iff::intro (assume H, and::intro (and::elimr H) (and::eliml H)) + (assume H, and::intro (and::elimr H) (and::eliml H)) -theorem AndComm (a b : Bool) : (a ∧ b) == (b ∧ a) -:= ImpAntisym (Assume H, Conj (Conjunct2 H) (Conjunct1 H)) - (Assume H, Conj (Conjunct2 H) (Conjunct1 H)) +theorem and::id (a : Bool) : (a ∧ a) == a +:= iff::intro (assume H, and::eliml H) + (assume H, and::intro H H) -theorem AndId (a : Bool) : (a ∧ a) == a -:= ImpAntisym (Assume H, Conjunct1 H) - (Assume H, Conj H H) +theorem and::assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c)) +:= iff::intro (assume H, and::intro (and::eliml (and::eliml H)) (and::intro (and::elimr (and::eliml H)) (and::elimr H))) + (assume H, and::intro (and::intro (and::eliml H) (and::eliml (and::elimr H))) (and::elimr (and::elimr H))) -theorem AndAssoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c)) -:= ImpAntisym (Assume H, Conj (Conjunct1 (Conjunct1 H)) (Conj (Conjunct2 (Conjunct1 H)) (Conjunct2 H))) - (Assume H, Conj (Conj (Conjunct1 H) (Conjunct1 (Conjunct2 H))) (Conjunct2 (Conjunct2 H))) +theorem and::truer (a : Bool) : (a ∧ true) == a +:= iff::intro (assume H : a ∧ true, and::eliml H) + (assume H : a, and::intro H trivial) -theorem AndRhsTrue (a : Bool) : (a ∧ true) == a -:= ImpAntisym (Assume H : a ∧ true, Conjunct1 H) - (Assume H : a, Conj H Trivial) +theorem and::truel (a : Bool) : (true ∧ a) == a +:= trans (and::comm true a) (and::truer a) -theorem AndLhsTrue (a : Bool) : (true ∧ a) == a -:= Trans (AndComm true a) (AndRhsTrue a) +theorem and::falsel (a : Bool) : (a ∧ false) == false +:= iff::intro (assume H, and::elimr H) + (assume H, false::elim (a ∧ false) H) -theorem AndRhsFalse (a : Bool) : (a ∧ false) == false -:= ImpAntisym (Assume H, Conjunct2 H) - (Assume H, FalseElim (a ∧ false) H) +theorem and::falser (a : Bool) : (false ∧ a) == false +:= (and::comm false a) ⋈ (and::falsel a) -theorem AndLhsFalse (a : Bool) : (false ∧ a) == false -:= Trans (AndComm false a) (AndRhsFalse a) +theorem and::absurd (a : Bool) : (a ∧ ¬ a) == false +:= iff::intro (assume H, absurd (and::eliml H) (and::elimr H)) + (assume H, false::elim (a ∧ ¬ a) H) -theorem AndAnotA (a : Bool) : (a ∧ ¬ a) == false -:= ImpAntisym (Assume H, Absurd (Conjunct1 H) (Conjunct2 H)) - (Assume H, FalseElim (a ∧ ¬ a) H) +theorem not::true : (¬ true) == false +:= trivial -theorem NotTrue : (¬ true) == false -:= Trivial +theorem not::false : (¬ false) == true +:= trivial -theorem NotFalse : (¬ false) == true -:= Trivial - -theorem NotAnd (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) -:= Case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b)) - (Case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) Trivial Trivial b) - (Case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) Trivial Trivial b) +theorem not::and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) +:= case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b)) + (case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) trivial trivial b) + (case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) trivial trivial b) a -theorem NotAndElim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b -:= EqMP (NotAnd a b) H +theorem not::and::elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b +:= (not::and a b) ◆ H -theorem NotOr (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b) -:= Case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b)) - (Case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) Trivial Trivial b) - (Case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) Trivial Trivial b) +theorem not::or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b) +:= case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b)) + (case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) trivial trivial b) + (case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) trivial trivial b) a -theorem NotOrElim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b -:= EqMP (NotOr a b) H +theorem not::or::elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b +:= (not::or a b) ◆ H -theorem NotEq (a b : Bool) : (¬ (a == b)) == ((¬ a) == b) -:= Case (λ x, (¬ (x == b)) == ((¬ x) == b)) - (Case (λ y, (¬ (true == y)) == ((¬ true) == y)) Trivial Trivial b) - (Case (λ y, (¬ (false == y)) == ((¬ false) == y)) Trivial Trivial b) +theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b) +:= case (λ x, (¬ (x == b)) == ((¬ x) == b)) + (case (λ y, (¬ (true == y)) == ((¬ true) == y)) trivial trivial b) + (case (λ y, (¬ (false == y)) == ((¬ false) == y)) trivial trivial b) a -theorem NotEqElim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b -:= EqMP (NotEq a b) H +theorem not::iff::elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b +:= (not::iff a b) ◆ H -theorem NotImp (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b) -:= Case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b)) - (Case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) Trivial Trivial b) - (Case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) Trivial Trivial b) +theorem not::implies (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b) +:= case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b)) + (case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) trivial trivial b) + (case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) trivial trivial b) a -theorem NotImpElim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b -:= EqMP (NotImp a b) H +theorem not::implies::elim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b +:= (not::implies a b) ◆ H -theorem NotCongr {a b : Bool} (H : a == b) : (¬ a) == (¬ b) -:= Congr2 not H +theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b) +:= congr2 not H -theorem ForallEqIntro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∀ x : A, P x) == (∀ x : A, Q x) -:= Congr2 (Forall A) (Abst H) +theorem eq::forall::intro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∀ x : A, P x) == (∀ x : A, Q x) +:= congr2 (Forall A) (abst H) -theorem ExistsEqIntro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x) -:= Congr2 (Exists A) (Abst H) +theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x) +:= congr2 (Exists A) (abst H) -theorem NotForall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) -:= let L1 : (¬ ∀ x : A, ¬ ¬ P x) == (∃ x : A, ¬ P x) := Refl (∃ x : A, ¬ P x), - L2 : (¬ ∀ x : A, P x) == (¬ ∀ x : A, ¬ ¬ P x) := - NotCongr (ForallEqIntro (λ x : A, (Symm (DoubleNeg (P x))))) - in Trans L2 L1 +theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) +:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (eq::forall::intro (λ x : A, (symm (not::not::eq (P x))))) + ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x) -theorem NotForallElim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x -:= EqMP (NotForall A P) H +theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x +:= (not::forall A P) ◆ H -theorem NotExists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x) -:= let L1 : (¬ ∃ x : A, P x) == (¬ ¬ ∀ x : A, ¬ P x) := Refl (¬ ∃ x : A, P x), - L2 : (¬ ¬ ∀ x : A, ¬ P x) == (∀ x : A, ¬ P x) := DoubleNeg (∀ x : A, ¬ P x) - in Trans L1 L2 +theorem not::exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x) +:= calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x) + ... = (∀ x : A, ¬ P x) : not::not::eq (∀ x : A, ¬ P x) -theorem NotExistsElim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x -:= EqMP (NotExists A P) H +theorem not::exists::elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x +:= (not::exists A P) ◆ H -theorem UnfoldExists1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) -:= ExistsElim H +theorem exists::unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) +:= exists::elim H (λ (w : A) (H1 : P w), - DisjCases (EM (w = a)) - (λ Heq : w = a, Disj1 (Subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) - (λ Hne : w ≠ a, Disj2 (P a) (ExistsIntro w (Conj Hne H1)))) + or::elim (em (w = a)) + (λ Heq : w = a, or::introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) + (λ Hne : w ≠ a, or::intror (P a) (exists::intro w (and::intro Hne H1)))) -theorem UnfoldExists2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x -:= DisjCases H - (λ H1 : P a, ExistsIntro a H1) +theorem exists::unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x +:= or::elim H + (λ H1 : P a, exists::intro a H1) (λ H2 : (∃ x : A, x ≠ a ∧ P x), - ExistsElim H2 + exists::elim H2 (λ (w : A) (Hw : w ≠ a ∧ P w), - ExistsIntro w (Conjunct2 Hw))) + exists::intro w (and::elimr Hw))) -theorem UnfoldExists {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) -:= ImpAntisym (Assume H : (∃ x : A, P x), UnfoldExists1 a H) - (Assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H) +theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) +:= iff::intro (assume H : (∃ x : A, P x), exists::unfold1 a H) + (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H) setopaque exists true diff --git a/src/builtin/macros.lua b/src/builtin/macros.lua index 05484ba440..db0ae3aec1 100644 --- a/src/builtin/macros.lua +++ b/src/builtin/macros.lua @@ -83,11 +83,9 @@ function nary_macro(name, f, farity) end) end -binder_macro("take", Const("ForallIntro"), 3, 1, 3) -binder_macro("Assume", Const("Discharge"), 3, 1, 3) -nary_macro("Instantiate", Const("ForallElim"), 4) -nary_macro("MP'", Const("MP"), 4) -nary_macro("Subst'", Const("Subst"), 6) +binder_macro("take", Const({"forall", "intro"}), 3, 1, 3) +binder_macro("assume", Const("discharge"), 3, 1, 3) +nary_macro("instantiate", Const({"forall", "elim"}), 4) -- ExistsElim syntax-sugar -- Example: @@ -96,14 +94,14 @@ nary_macro("Subst'", Const("Subst"), 6) -- Axiom Ax2: forall x y, not P x y -- Now, the following macro expression -- obtain (a b : Nat) (H : P a b) from Ax1, --- show false, Absurd H (instantiate Ax2 a b) +-- have false : absurd H (instantiate Ax2 a b) -- expands to --- ExistsElim Ax1 +-- exists::elim Ax1 -- (fun (a : Nat) (Haux : ...), --- ExistsElim Haux +-- exists::elim Haux -- (fun (b : Na) (H : P a b), --- show false, Absurd H (instantiate Ax2 a b) -macro("Obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr }, +-- have false : absurd H (instantiate Ax2 a b) +macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr }, function (env, bindings, fromid, exPr, body) local n = #bindings if n < 2 then @@ -112,7 +110,7 @@ macro("Obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg if fromid ~= name("from") then error("invalid 'obtain' expression, 'from' keyword expected, got '" .. tostring(fromid) .. "'") end - local exElim = mk_constant("ExistsElim") + local exElim = mk_constant({"exists", "elim"}) local H_name = bindings[n][1] local H_type = bindings[n][2] local a_name = bindings[n-1][1] diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 5da36280d2..c120b1d2af 100644 Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index 52eac2499b..f65b61fe78 100644 Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index fb4339ac39..0e2cfd6910 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 60edd4dbb6..1b44629022 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -44,11 +44,11 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } -static name g_eq_imp_trans("EqImpTrans"); -static name g_imp_eq_trans("ImpEqTrans"); -static name g_imp_trans("ImpTrans"); -static name g_eq_ne_trans("EqNeTrans"); -static name g_ne_eq_trans("NeEqTrans"); +static name g_eq_imp_trans({"eq", "imp", "trans"}); +static name g_imp_eq_trans({"imp", "eq", "trans"}); +static name g_imp_trans({"imp", "trans"}); +static name g_eq_ne_trans({"eq", "ne", "trans"}); +static name g_ne_eq_trans({"ne", "eq", "trans"}); static name g_neq("neq"); calc_proof_parser::calc_proof_parser() { diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index bee7e12e54..629e59b698 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -127,49 +127,47 @@ MK_CONSTANT(forall_fn, name("forall")); MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(homo_eq_fn, name("eq")); // Axioms -MK_CONSTANT(mp_fn, name("MP")); -MK_CONSTANT(discharge_fn, name("Discharge")); -MK_CONSTANT(case_fn, name("Case")); -MK_CONSTANT(refl_fn, name("Refl")); -MK_CONSTANT(subst_fn, name("Subst")); -MK_CONSTANT(eta_fn, name("Eta")); -MK_CONSTANT(imp_antisym_fn, name("ImpAntisym")); -MK_CONSTANT(abst_fn, name("Abst")); -MK_CONSTANT(htrans_fn, name("HTrans")); -MK_CONSTANT(hsymm_fn, name("HSymm")); +MK_CONSTANT(mp_fn, name("mp")); +MK_CONSTANT(discharge_fn, name("discharge")); +MK_CONSTANT(case_fn, name("case")); +MK_CONSTANT(refl_fn, name("refl")); +MK_CONSTANT(subst_fn, name("subst")); +MK_CONSTANT(eta_fn, name("eta")); +MK_CONSTANT(imp_antisym_fn, name({"iff", "intro"})); +MK_CONSTANT(abst_fn, name("abst")); +MK_CONSTANT(htrans_fn, name("htrans")); +MK_CONSTANT(hsymm_fn, name("hsymm")); // Theorems -MK_CONSTANT(trivial, name("Trivial")); -MK_CONSTANT(true_neq_false, name("TrueNeFalse")); -MK_CONSTANT(false_elim_fn, name("FalseElim")); -MK_CONSTANT(absurd_fn, name("Absurd")); -MK_CONSTANT(em_fn, name("EM")); -MK_CONSTANT(double_neg_fn, name("DoubleNeg")); -MK_CONSTANT(double_neg_elim_fn, name("DoubleNegElim")); -MK_CONSTANT(mt_fn, name("MT")); -MK_CONSTANT(contrapos_fn, name("Contrapos")); -MK_CONSTANT(false_imp_any_fn, name("FalseImpAny")); -MK_CONSTANT(absurd_elim_fn, name("AbsurdElim")); -MK_CONSTANT(eq_mp_fn, name("EqMP")); -MK_CONSTANT(not_imp1_fn, name("NotImp1")); -MK_CONSTANT(not_imp2_fn, name("NotImp2")); -MK_CONSTANT(conj_fn, name("Conj")); -MK_CONSTANT(conjunct1_fn, name("Conjunct1")); -MK_CONSTANT(conjunct2_fn, name("Conjunct2")); -MK_CONSTANT(disj1_fn, name("Disj1")); -MK_CONSTANT(disj2_fn, name("Disj2")); -MK_CONSTANT(disj_cases_fn, name("DisjCases")); -MK_CONSTANT(refute_fn, name("Refute")); -MK_CONSTANT(symm_fn, name("Symm")); -MK_CONSTANT(trans_fn, name("Trans")); -MK_CONSTANT(congr1_fn, name("Congr1")); -MK_CONSTANT(congr2_fn, name("Congr2")); -MK_CONSTANT(congr_fn, name("Congr")); -MK_CONSTANT(eqt_elim_fn, name("EqTElim")); -MK_CONSTANT(eqt_intro_fn, name("EqTIntro")); -MK_CONSTANT(forall_elim_fn, name("ForallElim")); -MK_CONSTANT(forall_intro_fn, name("ForallIntro")); -MK_CONSTANT(exists_elim_fn, name("ExistsElim")); -MK_CONSTANT(exists_intro_fn, name("ExistsIntro")); +MK_CONSTANT(trivial, name("trivial")); +MK_CONSTANT(false_elim_fn, name({"false", "elim"})); +MK_CONSTANT(absurd_fn, name("absurd")); +MK_CONSTANT(em_fn, name("em")); +MK_CONSTANT(double_neg_fn, name("doubleneg")); +MK_CONSTANT(double_neg_elim_fn, name({"doubleneg", "elim"})); +MK_CONSTANT(mt_fn, name("mt")); +MK_CONSTANT(contrapos_fn, name("contrapos")); +MK_CONSTANT(absurd_elim_fn, name({"absurd", "elim"})); +MK_CONSTANT(eq_mp_fn, name({"eq", "mp"})); +MK_CONSTANT(not_imp1_fn, name({"not", "imp", "eliml"})); +MK_CONSTANT(not_imp2_fn, name({"not", "imp", "elimr"})); +MK_CONSTANT(conj_fn, name({"and", "intro"})); +MK_CONSTANT(conjunct1_fn, name({"and", "eliml"})); +MK_CONSTANT(conjunct2_fn, name({"and", "elimr"})); +MK_CONSTANT(disj1_fn, name({"or", "introl"})); +MK_CONSTANT(disj2_fn, name({"or", "intror"})); +MK_CONSTANT(disj_cases_fn, name({"or", "elim"})); +MK_CONSTANT(refute_fn, name("refute")); +MK_CONSTANT(symm_fn, name("symm")); +MK_CONSTANT(trans_fn, name("trans")); +MK_CONSTANT(congr1_fn, name("congr1")); +MK_CONSTANT(congr2_fn, name("congr2")); +MK_CONSTANT(congr_fn, name("congr")); +MK_CONSTANT(eqt_elim_fn, name({"eqt", "elim"})); +MK_CONSTANT(eqt_intro_fn, name({"eqt", "intro"})); +MK_CONSTANT(forall_elim_fn, name({"forall", "elim"})); +MK_CONSTANT(forall_intro_fn, name({"forall", "intro"})); +MK_CONSTANT(exists_elim_fn, name({"exists", "elim"})); +MK_CONSTANT(exists_intro_fn, name({"exists", "intro"})); void import_kernel(environment const & env, io_state const & ios) { env->import("kernel", ios); diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index f1073fd062..e77a6e46b7 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -120,7 +120,7 @@ static void tst8() { environment env; io_state ios = init_frontend(env); formatter fmt = mk_pp_formatter(env); add_infixl(env, ios, "<-$->", 10, mk_refl_fn()); - std::cout << fmt(*(env->find_object("Trivial"))) << "\n"; + std::cout << fmt(*(env->find_object("trivial"))) << "\n"; } static void tst9() { diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index f726059006..2deb348d4e 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -341,7 +341,7 @@ static void try_rewriter1_tst() { cout << " " << concl << " := " << proof << std::endl; lean_assert_eq(concl, mk_eq(a_plus_b, a_plus_b)); - lean_assert_eq(proof, Const("Refl")(Nat, a_plus_b)); + lean_assert_eq(proof, Const("refl")(Nat, a_plus_b)); env->add_theorem("New_theorem6", concl, proof); } @@ -451,7 +451,7 @@ static void app_rewriter1_tst() { << "Proof = " << proof << std::endl; lean_assert_eq(concl, mk_eq(v, f1(b_plus_a))); lean_assert_eq(proof, - Const("Congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b))); + Const("congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b))); env->add_theorem("app_rewriter2", concl, proof); cout << "====================================================" << std::endl; v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a); @@ -464,11 +464,11 @@ static void app_rewriter1_tst() { // Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a) lean_assert_eq(proof, - Const("Congr")(Nat, Fun(name("_"), Nat, Nat), f4(zero, a_plus_b, zero), f4(zero, b_plus_a, zero), + Const("congr")(Nat, Fun(name("_"), Nat, Nat), f4(zero, a_plus_b, zero), f4(zero, b_plus_a, zero), b_plus_a, a_plus_b, - Const("Congr1")(Nat, Fun(name("_"), Nat, Nat >> Nat), f4(zero, a_plus_b), + Const("congr1")(Nat, Fun(name("_"), Nat, Nat >> Nat), f4(zero, a_plus_b), f4(zero, b_plus_a), zero, - Const("Congr2")(Nat, Fun(name("_"), Nat, Nat >> (Nat >> Nat)), + Const("congr2")(Nat, Fun(name("_"), Nat, Nat >> (Nat >> Nat)), a_plus_b, b_plus_a, f4(zero), Const("ADD_COMM")(a, b))), Const("ADD_COMM")(b, a))); diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean index 1c0fcd506f..7712c8b52e 100644 --- a/tests/lean/abst.lean +++ b/tests/lean/abst.lean @@ -1,6 +1,6 @@ import Int. axiom PlusComm(a b : Int) : a + b == b + a. variable a : Int. -check (Abst (fun x : Int, (PlusComm a x))). +check (abst (fun x : Int, (PlusComm a x))). setoption pp::implicit true. -check (Abst (fun x : Int, (PlusComm a x))). +check (abst (fun x : Int, (PlusComm a x))). diff --git a/tests/lean/abst.lean.expected.out b/tests/lean/abst.lean.expected.out index a241ab3c32..48717adadf 100644 --- a/tests/lean/abst.lean.expected.out +++ b/tests/lean/abst.lean.expected.out @@ -3,7 +3,7 @@ Imported 'Int' Assumed: PlusComm Assumed: a -Abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a) +abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a) Set: lean::pp::implicit -@Abst ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) : +@abst ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a) diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean index e7022ea00f..467e3f229f 100644 --- a/tests/lean/apply_tac1.lean +++ b/tests/lean/apply_tac1.lean @@ -5,7 +5,7 @@ variable f : Int -> Int -> Bool variable P : Int -> Int -> Bool axiom Ax1 (x y : Int) (H : P x y) : (f x y) theorem T1 (a : Int) : (P a a) => (f a a). - apply Discharge. + apply discharge. apply Ax1. exact. done. @@ -19,7 +19,7 @@ theorem T2 (a : Int) : (P a a) => (f a a). done. theorem T3 (a : Int) : (P a a) => (f a a). - Repeat (OrElse (apply Discharge) exact (apply Ax2) (apply Ax1)). + Repeat (OrElse (apply discharge) exact (apply Ax2) (apply Ax1)). done. print environment 2. \ No newline at end of file diff --git a/tests/lean/apply_tac1.lean.expected.out b/tests/lean/apply_tac1.lean.expected.out index d184b13428..4aa254fdfe 100644 --- a/tests/lean/apply_tac1.lean.expected.out +++ b/tests/lean/apply_tac1.lean.expected.out @@ -10,5 +10,5 @@ Assumed: Ax2 Proved: T2 Proved: T3 -theorem T2 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H) -theorem T3 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H) +theorem T2 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H) +theorem T3 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H) diff --git a/tests/lean/apply_tac2.lean b/tests/lean/apply_tac2.lean index f77fc8d5be..32ab828b01 100644 --- a/tests/lean/apply_tac2.lean +++ b/tests/lean/apply_tac2.lean @@ -1,8 +1,8 @@ (* import("tactic.lua") *) -check @Discharge +check @discharge theorem T (a b : Bool) : a => b => b => a. - apply Discharge. - apply Discharge. - apply Discharge. + apply discharge. + apply discharge. + apply discharge. exact. done. \ No newline at end of file diff --git a/tests/lean/apply_tac2.lean.expected.out b/tests/lean/apply_tac2.lean.expected.out index c9da3cd332..08e2efc271 100644 --- a/tests/lean/apply_tac2.lean.expected.out +++ b/tests/lean/apply_tac2.lean.expected.out @@ -1,4 +1,4 @@ Set: pp::colors Set: pp::unicode -@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b) +@discharge : Π (a b : Bool), (a → b) → (a ⇒ b) Proved: T diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean index 675736312a..3861cee142 100644 --- a/tests/lean/bad10.lean +++ b/tests/lean/bad10.lean @@ -3,6 +3,6 @@ setoption pp::colors false. variable N : Type. definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ := -SubstP (fun x : N, f (f a) == _) (Refl (f (f _))) H. +substp (fun x : N, f (f a) == _) (refl (f (f _))) H. print environment 1. diff --git a/tests/lean/bad10.lean.expected.out b/tests/lean/bad10.lean.expected.out index 36e79f708f..294ea7e027 100644 --- a/tests/lean/bad10.lean.expected.out +++ b/tests/lean/bad10.lean.expected.out @@ -5,4 +5,4 @@ Assumed: N Defined: T definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) := - @SubstP N (f a) a (λ x : N, f (f a) == f (f a)) (@Refl N (f (f a))) H + @substp N (f a) a (λ x : N, f (f a) == f (f a)) (@refl N (f (f a))) H diff --git a/tests/lean/bad5.lean b/tests/lean/bad5.lean index 017e71f63f..97df31599d 100644 --- a/tests/lean/bad5.lean +++ b/tests/lean/bad5.lean @@ -4,5 +4,5 @@ variable a : Int variable b : Int axiom H1 : a = b axiom H2 : (g a) > 0 -theorem T1 : (g b) > 0 := SubstP (λ x, (g x) > 0) H2 H1 +theorem T1 : (g b) > 0 := substp (λ x, (g x) > 0) H2 H1 print environment 2 diff --git a/tests/lean/bad5.lean.expected.out b/tests/lean/bad5.lean.expected.out index deea5aa7d5..58fbbad0a3 100644 --- a/tests/lean/bad5.lean.expected.out +++ b/tests/lean/bad5.lean.expected.out @@ -8,4 +8,4 @@ Assumed: H2 Proved: T1 axiom H2 : g a > 0 -theorem T1 : g b > 0 := SubstP (λ x : ℤ, g x > 0) H2 H1 +theorem T1 : g b > 0 := substp (λ x : ℤ, g x > 0) H2 H1 diff --git a/tests/lean/bad9.lean b/tests/lean/bad9.lean index 6d72f6d127..9c25a26e88 100644 --- a/tests/lean/bad9.lean +++ b/tests/lean/bad9.lean @@ -4,5 +4,5 @@ variable N : Type. check fun (a : N) (f : N -> N) (H : f a == a), -let calc1 : f a == a := SubstP (fun x : N, f a == _) (Refl (f a)) H +let calc1 : f a == a := substp (fun x : N, f a == _) (refl (f a)) H in calc1. \ No newline at end of file diff --git a/tests/lean/bad9.lean.expected.out b/tests/lean/bad9.lean.expected.out index 079e9bcd40..3c9fee4c27 100644 --- a/tests/lean/bad9.lean.expected.out +++ b/tests/lean/bad9.lean.expected.out @@ -4,5 +4,5 @@ Set: pp::colors Assumed: N λ (a : N) (f : N → N) (H : f a == a), - let calc1 : f a == a := @SubstP N (f a) a (λ x : N, f a == x) (@Refl N (f a)) H in calc1 : + let calc1 : f a == a := @substp N (f a) a (λ x : N, f a == x) (@refl N (f a)) H in calc1 : Π (a : N) (f : N → N), f a == a → f a == a diff --git a/tests/lean/bug.lean b/tests/lean/bug.lean index 6e093e983a..53adf653f0 100644 --- a/tests/lean/bug.lean +++ b/tests/lean/bug.lean @@ -1 +1 @@ -check fun (A A' : (Type U)) (H : A == A'), Symm H +check fun (A A' : (Type U)) (H : A == A'), symm H diff --git a/tests/lean/bug.lean.expected.out b/tests/lean/bug.lean.expected.out index 4354e0ad89..0ff4396c6d 100644 --- a/tests/lean/bug.lean.expected.out +++ b/tests/lean/bug.lean.expected.out @@ -3,7 +3,7 @@ Failed to solve A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU (line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of - @Symm + @symm with arguments: ?M::0 A diff --git a/tests/lean/cast1.lean b/tests/lean/cast1.lean index 33a9d76e84..3519518aee 100644 --- a/tests/lean/cast1.lean +++ b/tests/lean/cast1.lean @@ -4,7 +4,7 @@ import Int. variable vector : Type -> Nat -> Type axiom N0 (n : Nat) : n + 0 = n theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) := - Congr (Refl (vector T)) (N0 n) + congr (refl (vector T)) (N0 n) variable f (n : Nat) (v : vector Int n) : Int variable m : Nat variable v1 : vector Int (m + 0) diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean index 4bedf9335c..3eefa3d495 100644 --- a/tests/lean/cast2.lean +++ b/tests/lean/cast2.lean @@ -5,8 +5,8 @@ variable A' : Type variable B' : Type axiom H : (A -> B) = (A' -> B') variable a : A -check DomInj H -theorem BeqB' : B = B' := RanInj H a +check dominj H +theorem BeqB' : B = B' := raninj H a setoption pp::implicit true -print DomInj H -print RanInj H a +print dominj H +print raninj H a diff --git a/tests/lean/cast2.lean.expected.out b/tests/lean/cast2.lean.expected.out index a9f6edf001..8ff44375a8 100644 --- a/tests/lean/cast2.lean.expected.out +++ b/tests/lean/cast2.lean.expected.out @@ -7,8 +7,8 @@ Assumed: B' Assumed: H Assumed: a -DomInj H : A == A' +dominj H : A == A' Proved: BeqB' Set: lean::pp::implicit -@DomInj A A' (λ x : A, B) (λ x : A', B') H -@RanInj A A' (λ x : A, B) (λ x : A', B') H a +@dominj A A' (λ x : A, B) (λ x : A', B') H +@raninj A A' (λ x : A, B) (λ x : A', B') H a diff --git a/tests/lean/cast3.lean b/tests/lean/cast3.lean index 4d29fd4383..5013dcce00 100644 --- a/tests/lean/cast3.lean +++ b/tests/lean/cast3.lean @@ -2,8 +2,8 @@ import cast variables A A' B B' : Type variable x : A -eval cast (Refl A) x -eval x = (cast (Refl A) x) +eval cast (refl A) x +eval x = (cast (refl A) x) variable b : B definition f (x : A) : B := b axiom H : (A -> B) = (A' -> B) diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out index 834fb095ee..d78ef34af6 100644 --- a/tests/lean/cast3.lean.expected.out +++ b/tests/lean/cast3.lean.expected.out @@ -6,8 +6,8 @@ Assumed: B Assumed: B' Assumed: x -cast (Refl A) x -x == cast (Refl A) x +cast (refl A) x +x == cast (refl A) x Assumed: b Defined: f Assumed: H diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean index f26a279d3f..ce6035a786 100644 --- a/tests/lean/cast4.lean +++ b/tests/lean/cast4.lean @@ -12,16 +12,16 @@ check fun (A A': TypeM) (H2 : f == g) (H3 : a == b), let - S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1, - L2 : A' == A := DomInj S1, + S1 : (Pi x : A', B' x) == (Pi x : A, B x) := symm H1, + L2 : A' == A := dominj S1, b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b, - L4 : a == b' := HTrans H3 L3, - L5 : f a == f b' := Congr2 f L4, + L3 : b == b' := cast::eq L2 b, + L4 : a == b' := htrans H3 L3, + L5 : f a == f b' := congr2 f L4, g' : (Pi x : A, B x) := cast S1 g, - L6 : g == g' := CastEq S1 g, - L7 : f == g' := HTrans H2 L6, - L8 : f b' == g' b' := Congr1 b' L7, - L9 : f a == g' b' := HTrans L5 L8, - L10 : g' b' == g b := CastApp S1 L2 g b - in HTrans L9 L10 + L6 : g == g' := cast::eq S1 g, + L7 : f == g' := htrans H2 L6, + L8 : f b' == g' b' := congr1 b' L7, + L9 : f a == g' b' := htrans L5 L8, + L10 : g' b' == g b := cast::app S1 L2 g b + in htrans L9 L10 diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out index 0682944e71..f76e100551 100644 --- a/tests/lean/cast4.lean.expected.out +++ b/tests/lean/cast4.lean.expected.out @@ -12,18 +12,18 @@ (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : f == g) (H3 : a == b), - let S1 : (Π x : A', B' x) == (Π x : A, B x) := Symm H1, - L2 : A' == A := DomInj S1, + let S1 : (Π x : A', B' x) == (Π x : A, B x) := symm H1, + L2 : A' == A := dominj S1, b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b, - L4 : a == b' := HTrans H3 L3, - L5 : f a == f b' := Congr2 f L4, + L3 : b == b' := cast::eq L2 b, + L4 : a == b' := htrans H3 L3, + L5 : f a == f b' := congr2 f L4, g' : Π x : A, B x := cast S1 g, - L6 : g == g' := CastEq S1 g, - L7 : f == g' := HTrans H2 L6, - L8 : f b' == g' b' := Congr1 b' L7, - L9 : f a == g' b' := HTrans L5 L8, - L10 : g' b' == g b := CastApp S1 L2 g b - in HTrans L9 L10 : + L6 : g == g' := cast::eq S1 g, + L7 : f == g' := htrans H2 L6, + L8 : f b' == g' b' := congr1 b' L7, + L9 : f a == g' b' := htrans L5 L8, + L10 : g' b' == g b := cast::app S1 L2 g b + in htrans L9 L10 : Π (A A' : TypeM) (B : A → TypeM) (B' : A' → TypeM) (f : Π x : A, B x) (g : Π x : A', B' x) (a : A) (b : A'), (Π x : A, B x) == (Π x : A', B' x) → f == g → a == b → f a == g b diff --git a/tests/lean/discharge.lean b/tests/lean/discharge.lean index a5d17eab41..69e6baca48 100644 --- a/tests/lean/discharge.lean +++ b/tests/lean/discharge.lean @@ -1,8 +1,8 @@ import tactic -check @Discharge +check @discharge theorem T (a b : Bool) : a => b => b => a. - apply Discharge. - apply Discharge. - apply Discharge. + apply discharge. + apply discharge. + apply discharge. exact. done. \ No newline at end of file diff --git a/tests/lean/discharge.lean.expected.out b/tests/lean/discharge.lean.expected.out index f628955447..c61b7f7e96 100644 --- a/tests/lean/discharge.lean.expected.out +++ b/tests/lean/discharge.lean.expected.out @@ -1,5 +1,5 @@ Set: pp::colors Set: pp::unicode Imported 'tactic' -@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b) +@discharge : Π (a b : Bool), (a → b) → (a ⇒ b) Proved: T diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean index 13102b87e1..ba0fb3e830 100644 --- a/tests/lean/disj1.lean +++ b/tests/lean/disj1.lean @@ -1,7 +1,7 @@ import tactic theorem T1 (a b : Bool) : a \/ b => b \/ a. - apply Discharge. + apply discharge. (* disj_hyp_tac() *) (* disj_tac() *) back diff --git a/tests/lean/disj1.lean.expected.out b/tests/lean/disj1.lean.expected.out index 1aefd3eedc..e5ffd0e1d6 100644 --- a/tests/lean/disj1.lean.expected.out +++ b/tests/lean/disj1.lean.expected.out @@ -4,4 +4,4 @@ Proved: T1 Proved: T2 theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a := - Discharge (λ H : a ∨ b, DisjCases H (λ H : a, Disj2 b H) (λ H : b, Disj1 H a)) + discharge (λ H : a ∨ b, or::elim H (λ H : a, or::intror b H) (λ H : b, or::introl H a)) diff --git a/tests/lean/disjcases.lean b/tests/lean/disjcases.lean index 36ed7d8b47..56b81a4789 100644 --- a/tests/lean/disjcases.lean +++ b/tests/lean/disjcases.lean @@ -2,10 +2,10 @@ variables a b c : Bool axiom H : a \/ b theorem T (a b : Bool) : a \/ b => b \/ a. - apply Discharge. - apply (DisjCases H). - apply Disj2. + apply discharge. + apply (or::elim H). + apply or::intror. exact. - apply Disj1. + apply or::introl. exact. done. \ No newline at end of file diff --git a/tests/lean/elab1.lean b/tests/lean/elab1.lean index 24e6ed3e86..a49b1b786a 100644 --- a/tests/lean/elab1.lean +++ b/tests/lean/elab1.lean @@ -1,5 +1,3 @@ - - variable f {A : Type} (a b : A) : A. check f 10 true @@ -17,13 +15,13 @@ check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b. variable a : Bool variable b : Bool variable H : a /\ b -theorem t1 : b := Discharge (fun H1, Conj H1 (Conjunct1 H)). +theorem t1 : b := discharge (fun H1, and::intro H1 (and::eliml H)). -theorem t2 : a = b := Trans (Refl a) (Refl b). +theorem t2 : a = b := trans (refl a) (refl b). check f Bool Bool. theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a := - Discharge (λ H, DisjCases (EM a) + discharge (λ H, or::elim (EM a) (λ H_a, H) (λ H_na, NotImp1 (MT H H_na))) diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 6d824836d7..07e8341f44 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -3,19 +3,19 @@ Assumed: f Failed to solve ⊢ Bool ≺ ℕ - (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of + (line: 2: pos: 6) Type of argument 3 must be convertible to the expected type in the application of @f with arguments: ℕ 10 ⊤ Assumed: g -Error (line: 7, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: +Error (line: 5, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: Type Assumed: h Failed to solve x : ?M::0, A : Type ⊢ ?M::0 ≺ A - (line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of + (line: 9: pos: 27) Type of argument 2 must be convertible to the expected type in the application of h with arguments: A @@ -23,7 +23,7 @@ x : ?M::0, A : Type ⊢ ?M::0 ≺ A Assumed: my_eq Failed to solve A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C - (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of + (line: 13: pos: 51) Type of argument 2 must be convertible to the expected type in the application of my_eq with arguments: C @@ -34,34 +34,24 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C Assumed: H Failed to solve ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b - (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. + (line: 18: pos: 18) Type of definition 't1' must be convertible to expected type. Failed to solve ⊢ b == b ≺ a == b - (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of - @Trans + (line: 20: pos: 22) Type of argument 6 must be convertible to the expected type in the application of + @trans with arguments: ?M::1 a a b - Refl a - Refl b + refl a + refl b Failed to solve ⊢ ?M::1 ≺ Type - (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of + (line: 22: pos: 6) Type of argument 1 must be convertible to the expected type in the application of @f with arguments: ?M::0 Bool Bool -Failed to solve -a : Bool, b : Bool, H : (a ⇒ b) ⇒ a ⊢ a → (a ⇒ b) ⇒ a ≺ a → a - (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of - @DisjCases - with arguments: - a - ¬ a - a - EM a - λ H_a : a, H - λ H_na : ¬ a, NotImp1 (MT H H_na) +Error (line: 25, pos: 31) unknown identifier 'EM' diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean index 74d48d06a6..b68550b085 100644 --- a/tests/lean/elab7.lean +++ b/tests/lean/elab7.lean @@ -4,18 +4,18 @@ variable F1 : A -> B -> C variable F2 : A -> B -> C variable H : Pi (a : A) (b : B), (F1 a b) == (F2 a b) variable a : A -check Eta (F2 a) -check Abst (fun a : A, - (Trans (Symm (Eta (F1 a))) - (Trans (Abst (fun (b : B), H a b)) - (Eta (F2 a))))) +check eta (F2 a) +check abst (fun a : A, + (trans (symm (eta (F1 a))) + (trans (abst (fun (b : B), H a b)) + (eta (F2 a))))) -check Abst (fun a, (Abst (fun b, H a b))) +check abst (fun a, (abst (fun b, H a b))) -theorem T1 : F1 = F2 := Abst (fun a, (Abst (fun b, H a b))) -theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (fun a, (Abst (fun b, H a b))) -theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b))) -theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b))) +theorem T1 : F1 = F2 := abst (fun a, (abst (fun b, H a b))) +theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (fun a, (abst (fun b, H a b))) +theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b))) +theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b))) print environment 4 setoption pp::implicit true print environment 4 \ No newline at end of file diff --git a/tests/lean/elab7.lean.expected.out b/tests/lean/elab7.lean.expected.out index 4c4ed2ec6f..0e80da44f1 100644 --- a/tests/lean/elab7.lean.expected.out +++ b/tests/lean/elab7.lean.expected.out @@ -8,37 +8,36 @@ Assumed: F2 Assumed: H Assumed: a -Eta (F2 a) : (λ x : B, F2 a x) == F2 a -Abst (λ a : A, Trans (Symm (Eta (F1 a))) (Trans (Abst (λ b : B, H a b)) (Eta (F2 a)))) : - (λ x : A, F1 x) == (λ x : A, F2 x) -Abst (λ a : A, Abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1) +eta (F2 a) : (λ x : B, F2 a x) == F2 a +abst (λ a : A, symm (eta (F1 a)) ⋈ (abst (λ b : B, H a b) ⋈ eta (F2 a))) : (λ x : A, F1 x) == (λ x : A, F2 x) +abst (λ a : A, abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1) Proved: T1 Proved: T2 Proved: T3 Proved: T4 -theorem T1 : F1 = F2 := Abst (λ a : A, Abst (λ b : B, H a b)) -theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (λ a : A, Abst (λ b : B, H a b)) -theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := Abst (λ a : A, Abst (λ b : B, H a b)) +theorem T1 : F1 = F2 := abst (λ a : A, abst (λ b : B, H a b)) +theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (λ a : A, abst (λ b : B, H a b)) +theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := abst (λ a : A, abst (λ b : B, H a b)) theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) := - Abst (λ a : A, Abst (λ b : B, H a b)) + abst (λ a : A, abst (λ b : B, H a b)) Set: lean::pp::implicit theorem T1 : @eq (A → B → C) F1 F2 := - @Abst A (λ x : A, B → C) F1 F2 (λ a : A, @Abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b)) + @abst A (λ x : A, B → C) F1 F2 (λ a : A, @abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b)) theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 := - @Abst A + @abst A (λ x : A, B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 - (λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b)) + (λ a : A, @abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b)) theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) := - @Abst A + @abst A (λ x : A, B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) - (λ a : A, @Abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b)) + (λ a : A, @abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b)) theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) := - @Abst A + @abst A (λ x : A, B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) - (λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b)) + (λ a : A, @abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b)) diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean index 148fc260d2..925df762f2 100644 --- a/tests/lean/eq3.lean +++ b/tests/lean/eq3.lean @@ -5,6 +5,6 @@ variable v2 : Vector (n + 0) variable v3 : Vector (0 + n) axiom H1 : v1 == v2 axiom H2 : v2 == v3 -check HTrans H1 H2 +check htrans H1 H2 setoption pp::implicit true -check HTrans H1 H2 +check htrans H1 H2 diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out index d5542ebabc..783843fc47 100644 --- a/tests/lean/eq3.lean.expected.out +++ b/tests/lean/eq3.lean.expected.out @@ -7,6 +7,6 @@ Assumed: v3 Assumed: H1 Assumed: H2 -HTrans H1 H2 : v1 == v3 +htrans H1 H2 : v1 == v3 Set: lean::pp::implicit -@HTrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3 +@htrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3 diff --git a/tests/lean/errmsg1.lean b/tests/lean/errmsg1.lean index 294ba9370f..ce0c79e3c3 100644 --- a/tests/lean/errmsg1.lean +++ b/tests/lean/errmsg1.lean @@ -5,4 +5,4 @@ check fun x, x theorem T (A : Type) (x : A) : Pi (y : A), A := _. -theorem T (x : _) : x = x := Refl x. +theorem T (x : _) : x = x := refl x. diff --git a/tests/lean/exists1.lean b/tests/lean/exists1.lean index 11f4c165f4..ccee5ea9ff 100644 --- a/tests/lean/exists1.lean +++ b/tests/lean/exists1.lean @@ -2,5 +2,5 @@ import Int. variable a : Int variable P : Int -> Int -> Bool axiom H : P a a -theorem T : exists x : Int, P a a := ExistsIntro a H. +theorem T : exists x : Int, P a a := exists::intro a H. print environment 1. \ No newline at end of file diff --git a/tests/lean/exists1.lean.expected.out b/tests/lean/exists1.lean.expected.out index 453b016274..93e414f680 100644 --- a/tests/lean/exists1.lean.expected.out +++ b/tests/lean/exists1.lean.expected.out @@ -5,4 +5,4 @@ Assumed: P Assumed: H Proved: T -theorem T : ∃ x : ℤ, P a a := ExistsIntro a H +theorem T : ∃ x : ℤ, P a a := exists::intro a H diff --git a/tests/lean/exists2.lean b/tests/lean/exists2.lean index a1106e415a..0b172240fe 100644 --- a/tests/lean/exists2.lean +++ b/tests/lean/exists2.lean @@ -6,13 +6,13 @@ variable g : Int -> Int axiom H1 : P (f a (g a)) (f a (g a)) axiom H2 : P (f (g a) (g a)) (f (g a) (g a)) axiom H3 : P (f (g a) (g a)) (g a) -theorem T1 : exists x y : Int, P (f y x) (f y x) := ExistsIntro _ (ExistsIntro _ H1) -theorem T2 : exists x : Int, P (f x (g x)) (f x (g x)) := ExistsIntro _ H1 -theorem T3 : exists x : Int, P (f x x) (f x x) := ExistsIntro _ H2 -theorem T4 : exists x : Int, P (f (g a) x) (f x x) := ExistsIntro _ H2 -theorem T5 : exists x : Int, P x x := ExistsIntro _ H2 -theorem T6 : exists x y : Int, P x y := ExistsIntro _ (ExistsIntro _ H3) -theorem T7 : exists x : Int, P (f x x) x := ExistsIntro _ H3 -theorem T8 : exists x y : Int, P (f x x) y := ExistsIntro _ (ExistsIntro _ H3) +theorem T1 : exists x y : Int, P (f y x) (f y x) := exists::intro _ (exists::intro _ H1) +theorem T2 : exists x : Int, P (f x (g x)) (f x (g x)) := exists::intro _ H1 +theorem T3 : exists x : Int, P (f x x) (f x x) := exists::intro _ H2 +theorem T4 : exists x : Int, P (f (g a) x) (f x x) := exists::intro _ H2 +theorem T5 : exists x : Int, P x x := exists::intro _ H2 +theorem T6 : exists x y : Int, P x y := exists::intro _ (exists::intro _ H3) +theorem T7 : exists x : Int, P (f x x) x := exists::intro _ H3 +theorem T8 : exists x y : Int, P (f x x) y := exists::intro _ (exists::intro _ H3) print environment 8. \ No newline at end of file diff --git a/tests/lean/exists2.lean.expected.out b/tests/lean/exists2.lean.expected.out index f9024920b7..7f50c23f25 100644 --- a/tests/lean/exists2.lean.expected.out +++ b/tests/lean/exists2.lean.expected.out @@ -16,11 +16,11 @@ Proved: T6 Proved: T7 Proved: T8 -theorem T1 : ∃ x y : ℤ, P (f y x) (f y x) := ExistsIntro (g a) (ExistsIntro a H1) -theorem T2 : ∃ x : ℤ, P (f x (g x)) (f x (g x)) := ExistsIntro a H1 -theorem T3 : ∃ x : ℤ, P (f x x) (f x x) := ExistsIntro (g a) H2 -theorem T4 : ∃ x : ℤ, P (f (g a) x) (f x x) := ExistsIntro (g a) H2 -theorem T5 : ∃ x : ℤ, P x x := ExistsIntro (f (g a) (g a)) H2 -theorem T6 : ∃ x y : ℤ, P x y := ExistsIntro (f (g a) (g a)) (ExistsIntro (g a) H3) -theorem T7 : ∃ x : ℤ, P (f x x) x := ExistsIntro (g a) H3 -theorem T8 : ∃ x y : ℤ, P (f x x) y := ExistsIntro (g a) (ExistsIntro (g a) H3) +theorem T1 : ∃ x y : ℤ, P (f y x) (f y x) := exists::intro (g a) (exists::intro a H1) +theorem T2 : ∃ x : ℤ, P (f x (g x)) (f x (g x)) := exists::intro a H1 +theorem T3 : ∃ x : ℤ, P (f x x) (f x x) := exists::intro (g a) H2 +theorem T4 : ∃ x : ℤ, P (f (g a) x) (f x x) := exists::intro (g a) H2 +theorem T5 : ∃ x : ℤ, P x x := exists::intro (f (g a) (g a)) H2 +theorem T6 : ∃ x y : ℤ, P x y := exists::intro (f (g a) (g a)) (exists::intro (g a) H3) +theorem T7 : ∃ x : ℤ, P (f x x) x := exists::intro (g a) H3 +theorem T8 : ∃ x y : ℤ, P (f x x) y := exists::intro (g a) (exists::intro (g a) H3) diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean index 5d83250d11..d9c2f324d6 100644 --- a/tests/lean/exists3.lean +++ b/tests/lean/exists3.lean @@ -4,26 +4,26 @@ variable P : Int -> Int -> Bool setopaque exists false. theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := - ForallIntro (fun a, - ForallIntro (fun b, - ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R1) a)) b)) + forall::intro (fun a, + forall::intro (fun b, + forall::elim (not::not::elim (forall::elim (not::not::elim R1) a)) b)) axiom Ax : forall x, exists y, P x y theorem T2 : exists x y, P x y := - Refute (fun R : not (exists x y, P x y), - let L1 : forall x y, not (P x y) := ForallIntro (fun a, - ForallIntro (fun b, - ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R) a)) b)), - L2 : exists y, P 0 y := ForallElim Ax 0 - in ExistsElim L2 (fun (w : Int) (H : P 0 w), - Absurd H (ForallElim (ForallElim L1 0) w))). + refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := forall::intro (fun a, + forall::intro (fun b, + forall::elim (not::not::elim (forall::elim (not::not::elim R) a)) b)), + L2 : exists y, P 0 y := forall::elim Ax 0 + in exists::elim L2 (fun (w : Int) (H : P 0 w), + absurd H (forall::elim (forall::elim L1 0) w))). theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := - Refute (fun R : not (exists x y, P x y), - let L1 : forall x y, not (P x y) := ForallIntro (fun a, - ForallIntro (fun b, - ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R) a)) b)), - L2 : exists y, P a y := ForallElim H1 a - in ExistsElim L2 (fun (w : A) (H : P a w), - Absurd H (ForallElim (ForallElim L1 a) w))). + refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := forall::intro (fun a, + forall::intro (fun b, + forall::elim (not::not::elim (forall::elim (not::not::elim R) a)) b)), + L2 : exists y, P a y := forall::elim H1 a + in exists::elim L2 (fun (w : A) (H : P a w), + absurd H (forall::elim (forall::elim L1 a) w))). diff --git a/tests/lean/exists4.lean b/tests/lean/exists4.lean index 3a1d5934e0..887be720bd 100644 --- a/tests/lean/exists4.lean +++ b/tests/lean/exists4.lean @@ -3,14 +3,14 @@ variables a b c : N variables P : N -> N -> N -> Bool axiom H3 : P a b c -theorem T1 : exists x y z : N, P x y z := @ExistsIntro N (fun x : N, exists y z : N, P x y z) a - (@ExistsIntro N _ b - (@ExistsIntro N (fun z : N, P a b z) c H3)) +theorem T1 : exists x y z : N, P x y z := exists::@intro N (fun x : N, exists y z : N, P x y z) a + (exists::@intro N _ b + (exists::@intro N (fun z : N, P a b z) c H3)) -theorem T2 : exists x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) +theorem T2 : exists x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3)) -theorem T3 : exists x y z : N, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H3)) +theorem T3 : exists x y z : N, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H3)) -theorem T4 (H : P a a b) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H)) +theorem T4 (H : P a a b) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H)) print environment 4 \ No newline at end of file diff --git a/tests/lean/exists4.lean.expected.out b/tests/lean/exists4.lean.expected.out index 1bb871e202..63c0c00698 100644 --- a/tests/lean/exists4.lean.expected.out +++ b/tests/lean/exists4.lean.expected.out @@ -11,11 +11,11 @@ Proved: T3 Proved: T4 theorem T1 : ∃ x y z : N, P x y z := - @ExistsIntro + exists::@intro N (λ x : N, ∃ y z : N, P x y z) a - (@ExistsIntro N (λ y : N, ∃ z : N, P a y z) b (@ExistsIntro N (λ z : N, P a b z) c H3)) -theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) -theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) -theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H)) + (exists::@intro N (λ y : N, ∃ z : N, P a y z) b (exists::@intro N (λ z : N, P a b z) c H3)) +theorem T2 : ∃ x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3)) +theorem T3 : ∃ x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3)) +theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := exists::intro a (exists::intro a (exists::intro b H)) diff --git a/tests/lean/exists5.lean b/tests/lean/exists5.lean index fcfe6454fb..44a71e9e80 100644 --- a/tests/lean/exists5.lean +++ b/tests/lean/exists5.lean @@ -2,6 +2,6 @@ variable N : Type variables a b c : N variables P : N -> N -> N -> Bool -theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H)) +theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H)) print environment 1. diff --git a/tests/lean/exists5.lean.expected.out b/tests/lean/exists5.lean.expected.out index 675ac27544..315e876378 100644 --- a/tests/lean/exists5.lean.expected.out +++ b/tests/lean/exists5.lean.expected.out @@ -7,4 +7,4 @@ Assumed: P Proved: T1 theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z := - ExistsIntro (f a) (ExistsIntro b (ExistsIntro (f (f c)) H)) + exists::intro (f a) (exists::intro b (exists::intro (f (f c)) H)) diff --git a/tests/lean/exists6.lean b/tests/lean/exists6.lean index b04aa3b734..e34270ba4d 100644 --- a/tests/lean/exists6.lean +++ b/tests/lean/exists6.lean @@ -3,6 +3,6 @@ variable P : Int -> Int -> Int -> Bool axiom Ax1 : exists x y z, P x y z axiom Ax2 : forall x y z, not (P x y z) theorem T : false := - ExistsElim Ax1 (fun a H1, ExistsElim H1 (fun b H2, ExistsElim H2 (fun (c : Int) (H3 : P a b c), - let notH3 : not (P a b c) := ForallElim (ForallElim (ForallElim Ax2 a) b) c - in Absurd H3 notH3))) + exists::elim Ax1 (fun a H1, exists::elim H1 (fun b H2, exists::elim H2 (fun (c : Int) (H3 : P a b c), + let notH3 : not (P a b c) := forall::elim (forall::elim (forall::elim Ax2 a) b) c + in absurd H3 notH3))) diff --git a/tests/lean/exists7.lean b/tests/lean/exists7.lean index 491dc4fe4c..d901ef092f 100644 --- a/tests/lean/exists7.lean +++ b/tests/lean/exists7.lean @@ -7,6 +7,6 @@ setopaque forall false. setopaque exists false. setopaque not false. -theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H)) +theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H)) print environment 1. diff --git a/tests/lean/exists7.lean.expected.out b/tests/lean/exists7.lean.expected.out index 620a488be5..7a003b38e9 100644 --- a/tests/lean/exists7.lean.expected.out +++ b/tests/lean/exists7.lean.expected.out @@ -8,4 +8,4 @@ Assumed: P Proved: T1 theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z := - ExistsIntro (f a) (ExistsIntro b (ExistsIntro (f (f c)) H)) + exists::intro (f a) (exists::intro b (exists::intro (f (f c)) H)) diff --git a/tests/lean/exists8.lean b/tests/lean/exists8.lean index 5871328702..a31cf7c479 100644 --- a/tests/lean/exists8.lean +++ b/tests/lean/exists8.lean @@ -2,26 +2,26 @@ import Int. variable P : Int -> Int -> Bool theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := - ForallIntro (fun a, - ForallIntro (fun b, - ForallElim (NotExistsElim (ForallElim (NotExistsElim R1) a)) b)) + forall::intro (fun a, + forall::intro (fun b, + forall::elim (not::exists::elim (forall::elim (not::exists::elim R1) a)) b)) axiom Ax : forall x, exists y, P x y theorem T2 : exists x y, P x y := - Refute (fun R : not (exists x y, P x y), - let L1 : forall x y, not (P x y) := ForallIntro (fun a, - ForallIntro (fun b, - ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)), - L2 : exists y, P 0 y := ForallElim Ax 0 - in ExistsElim L2 (fun (w : Int) (H : P 0 w), - Absurd H (ForallElim (ForallElim L1 0) w))). + refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := forall::intro (fun a, + forall::intro (fun b, + forall::elim (not::exists::elim (forall::elim (not::exists::elim R) a)) b)), + L2 : exists y, P 0 y := forall::elim Ax 0 + in exists::elim L2 (fun (w : Int) (H : P 0 w), + absurd H (forall::elim (forall::elim L1 0) w))). theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := - Refute (fun R : not (exists x y, P x y), - let L1 : forall x y, not (P x y) := ForallIntro (fun a, - ForallIntro (fun b, - ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)), - L2 : exists y, P a y := ForallElim H1 a - in ExistsElim L2 (fun (w : A) (H : P a w), - Absurd H (ForallElim (ForallElim L1 a) w))). + refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := forall::intro (fun a, + forall::intro (fun b, + forall::elim (not::exists::elim (forall::elim (not::exists::elim R) a)) b)), + L2 : exists y, P a y := forall::elim H1 a + in exists::elim L2 (fun (w : A) (H : P a w), + absurd H (forall::elim (forall::elim L1 a) w))). diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out index 9ba9e80c1d..2cdffce2df 100644 --- a/tests/lean/find.lean.expected.out +++ b/tests/lean/find.lean.expected.out @@ -1,8 +1,8 @@ Set: pp::colors Set: pp::unicode Imported 'find' -theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a -theorem Congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b -theorem Congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b +theorem congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a +theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b +theorem congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b Error (line: 3, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo' -Error (line: 4, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression '(ab' +Error (line: 4, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture diff --git a/tests/lean/forall1.lean b/tests/lean/forall1.lean index 6a07ee752d..8d66595654 100644 --- a/tests/lean/forall1.lean +++ b/tests/lean/forall1.lean @@ -1,4 +1,4 @@ import Int. variable P : Int -> Bool axiom Ax (x : Int) : P x -check ForallIntro Ax \ No newline at end of file +check forall::intro Ax \ No newline at end of file diff --git a/tests/lean/forall1.lean.expected.out b/tests/lean/forall1.lean.expected.out index 74eb175588..1bea43e06a 100644 --- a/tests/lean/forall1.lean.expected.out +++ b/tests/lean/forall1.lean.expected.out @@ -3,4 +3,4 @@ Imported 'Int' Assumed: P Assumed: Ax -ForallIntro Ax : ∀ x : ℤ, P x +forall::intro Ax : ∀ x : ℤ, P x diff --git a/tests/lean/ho.lean b/tests/lean/ho.lean index 368987e8c1..7071cdb9c9 100644 --- a/tests/lean/ho.lean +++ b/tests/lean/ho.lean @@ -4,5 +4,5 @@ variable a : Int variable b : Int axiom H1 : a = b axiom H2 : (g a) > 0 -theorem T1 : (g b) > 0 := Subst H2 H1 +theorem T1 : (g b) > 0 := subst H2 H1 print environment 2 diff --git a/tests/lean/ho.lean.expected.out b/tests/lean/ho.lean.expected.out index 653a0d3650..e41967743d 100644 --- a/tests/lean/ho.lean.expected.out +++ b/tests/lean/ho.lean.expected.out @@ -8,4 +8,4 @@ Assumed: H2 Proved: T1 axiom H2 : g a > 0 -theorem T1 : g b > 0 := Subst H2 H1 +theorem T1 : g b > 0 := subst H2 H1 diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean index 7db433aa8e..d0eae73d10 100644 --- a/tests/lean/interactive/elab6.lean +++ b/tests/lean/interactive/elab6.lean @@ -5,5 +5,5 @@ local env = get_environment() env:set_opaque("forall", false) *) -theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := - Abst (fun x, EqTIntro (H x)) +theorem forall::intro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := + abst (fun x, eqt::intro (H x)) diff --git a/tests/lean/interactive/elab6.lean.expected.out b/tests/lean/interactive/elab6.lean.expected.out index 0ff7de0f88..385206a419 100644 --- a/tests/lean/interactive/elab6.lean.expected.out +++ b/tests/lean/interactive/elab6.lean.expected.out @@ -1,3 +1,3 @@ # Set: pp::colors Set: pp::unicode - Proved: ForallIntro2 + Proved: forall::intro2 diff --git a/tests/lean/interactive/t10.lean b/tests/lean/interactive/t10.lean index c2c1d340b0..d5143352df 100644 --- a/tests/lean/interactive/t10.lean +++ b/tests/lean/interactive/t10.lean @@ -3,7 +3,7 @@ simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac())) *) theorem T2 (A B : Bool) : A /\ B => B /\ A := - Discharge (fun H : A /\ B, + discharge (fun H : A /\ B, let H1 : A := _, H2 : B := _, main : B /\ A := _ diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean index af5fc8b62d..a56720c61f 100644 --- a/tests/lean/interactive/t12.lean +++ b/tests/lean/interactive/t12.lean @@ -28,7 +28,7 @@ theorem T3 (A B : Bool) : A /\ B -> B /\ A := in _. conj_hyp. exact. done. conj_hyp. exact. done. - apply Conj. exact. done. + apply and::intro. exact. done. theorem T4 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, diff --git a/tests/lean/interactive/t12.lean.expected.out b/tests/lean/interactive/t12.lean.expected.out index 035beb6eb2..a895f6f3e4 100644 --- a/tests/lean/interactive/t12.lean.expected.out +++ b/tests/lean/interactive/t12.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Proved: T1 theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := - let lemma1 : A := Conjunct1 assumption, lemma2 : B := Conjunct2 assumption in Conj lemma2 lemma1 + let lemma1 : A := and::eliml assumption, lemma2 : B := and::elimr assumption in and::intro lemma2 lemma1 # Proof state: A : Bool, B : Bool, assumption : A ∧ B ⊢ A ## Proof state: diff --git a/tests/lean/interactive/t13.lean.expected.out b/tests/lean/interactive/t13.lean.expected.out index c34bb68dea..bb7cda099c 100644 --- a/tests/lean/interactive/t13.lean.expected.out +++ b/tests/lean/interactive/t13.lean.expected.out @@ -2,5 +2,5 @@ Set: pp::unicode Proved: T1 theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := - let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1 + let lemma1 := and::eliml assumption, lemma2 := and::elimr assumption in and::intro lemma2 lemma1 # \ No newline at end of file diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out index 0e61a9c31e..74cab7ec48 100644 --- a/tests/lean/interactive/t3.lean.expected.out +++ b/tests/lean/interactive/t3.lean.expected.out @@ -14,5 +14,5 @@ H : b, a : Bool, b : Bool ⊢ b ## Proof state: no goals ## Proved: T2 -# theorem T2 (a b : Bool) : b ⇒ a ∨ b := Discharge (λ H : b, Disj2 a H) +# theorem T2 (a b : Bool) : b ⇒ a ∨ b := discharge (λ H : b, or::intror a H) # \ No newline at end of file diff --git a/tests/lean/interactive/t6.lean b/tests/lean/interactive/t6.lean index ba666b779a..f9bc99ebef 100644 --- a/tests/lean/interactive/t6.lean +++ b/tests/lean/interactive/t6.lean @@ -2,6 +2,6 @@ theorem T1 (a b : Bool) : a => b => a /\ b. (* imp_tac() *). (* imp_tac() *). - apply Conj. + apply and::intro. exact. done. diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean index c09f14d213..97bc0c79bd 100644 --- a/tests/lean/interactive/t8.lean +++ b/tests/lean/interactive/t8.lean @@ -1,7 +1,7 @@ (* import("tactic.lua") *) setoption tactic::proof_state::goal_names true. theorem T (a : Bool) : a => a /\ a. - apply Discharge. - apply Conj. + apply discharge. + apply and::intro. exact. done. diff --git a/tests/lean/interactive/t9.lean b/tests/lean/interactive/t9.lean index 48fb412e16..b4b7b1a41e 100644 --- a/tests/lean/interactive/t9.lean +++ b/tests/lean/interactive/t9.lean @@ -1,6 +1,6 @@ (* import("tactic.lua") *) theorem T1 (A B : Bool) : A /\ B => B /\ A := - Discharge (fun H : A /\ B, + discharge (fun H : A /\ B, let main : B /\ A := (let H1 : B := _, H2 : A := _ @@ -12,7 +12,7 @@ theorem T1 (A B : Bool) : A /\ B => B /\ A := conj_hyp. exact. done. - apply Conj. + apply and::intro. exact. done. @@ -21,7 +21,7 @@ simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac())) *) theorem T2 (A B : Bool) : A /\ B => B /\ A := - Discharge (fun H : A /\ B, + discharge (fun H : A /\ B, let H1 : A := _, H2 : B := _, main : B /\ A := _ diff --git a/tests/lean/let2.lean b/tests/lean/let2.lean index 0653180f08..34352789bf 100644 --- a/tests/lean/let2.lean +++ b/tests/lean/let2.lean @@ -1,10 +1,10 @@ -- Annotating lemmas theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := - Discharge (λ H_pq_qr, Discharge (λ H_p, - let P_pq : (p ⇒ q) := Conjunct1 H_pq_qr, - P_qr : (q ⇒ r) := Conjunct2 H_pq_qr, - P_q : q := MP P_pq H_p - in MP P_qr P_q)) + discharge (λ H_pq_qr, discharge (λ H_p, + let P_pq : (p ⇒ q) := and::eliml H_pq_qr, + P_qr : (q ⇒ r) := and::elimr H_pq_qr, + P_q : q := mp P_pq H_p + in mp P_qr P_q)) print environment 1 \ No newline at end of file diff --git a/tests/lean/let2.lean.expected.out b/tests/lean/let2.lean.expected.out index de9904e323..9681b9ddc2 100644 --- a/tests/lean/let2.lean.expected.out +++ b/tests/lean/let2.lean.expected.out @@ -2,11 +2,11 @@ Set: pp::unicode Proved: simple theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := - Discharge + discharge (λ H_pq_qr : (p ⇒ q) ∧ (q ⇒ r), - Discharge + discharge (λ H_p : p, - let P_pq : p ⇒ q := Conjunct1 H_pq_qr, - P_qr : q ⇒ r := Conjunct2 H_pq_qr, - P_q : q := MP P_pq H_p - in MP P_qr P_q)) + let P_pq : p ⇒ q := and::eliml H_pq_qr, + P_qr : q ⇒ r := and::elimr H_pq_qr, + P_q : q := P_pq ◂ H_p + in P_qr ◂ P_q)) diff --git a/tests/lean/lua11.lean b/tests/lean/lua11.lean index e56e344525..ff70caccce 100644 --- a/tests/lean/lua11.lean +++ b/tests/lean/lua11.lean @@ -44,9 +44,9 @@ import Int. assert(env:find_object("val"):get_value() == Const("x")) assert(env:find_object("val"):get_weight() == 1) assert(not pcall(function() M:get_weight() end)) - assert(env:find_object("Congr"):is_opaque()) - assert(env:find_object("Congr"):is_theorem()) - assert(env:find_object("Refl"):is_axiom()) + assert(env:find_object("congr"):is_opaque()) + assert(env:find_object("congr"):is_theorem()) + assert(env:find_object("refl"):is_axiom()) assert(env:find_object(name("Int", "sub")):is_definition()) assert(env:find_object("x"):is_var_decl()) *) diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean index 9a89a4d966..36a183450d 100644 --- a/tests/lean/norm_bug1.lean +++ b/tests/lean/norm_bug1.lean @@ -5,8 +5,8 @@ check fun (A A': TypeM) (a : A) (b : A') (L2 : A' == A), - let b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b + let b' : A := cast L2 b, + L3 : b == b' := cast::eq L2 b in L3 check fun (A A': TypeM) @@ -19,10 +19,10 @@ check fun (A A': TypeM) (H1 : (Pi x : A, B x) == (Pi x : A', B' x)) (H2 : f == g) (H3 : a == b), - let L1 : A == A' := DomInj H1, - L2 : A' == A := Symm L1, + let L1 : A == A' := dominj H1, + L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b, - L4 : a == b' := HTrans H3 L3, - L5 : f a == f b' := Congr2 f L4 + L3 : b == b' := cast::eq L2 b, + L4 : a == b' := htrans H3 L3, + L5 : f a == f b' := congr2 f L4 in L5 diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out index 3e94ea090f..b5eb5ea118 100644 --- a/tests/lean/norm_bug1.lean.expected.out +++ b/tests/lean/norm_bug1.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Imported 'cast' Set: pp::colors -λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 : +λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 : Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b λ (A A' : TypeM) (B : A → TypeM) @@ -14,12 +14,12 @@ (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : f == g) (H3 : a == b), - let L1 : A == A' := DomInj H1, - L2 : A' == A := Symm L1, + let L1 : A == A' := dominj H1, + L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b, - L4 : a == b' := HTrans H3 L3, - L5 : f a == f b' := Congr2 f L4 + L3 : b == b' := cast::eq L2 b, + L4 : a == b' := htrans H3 L3, + L5 : f a == f b' := congr2 f L4 in L5 : Π (A A' : TypeM) (B : A → TypeM) @@ -29,4 +29,4 @@ (a : A) (b : A') (H1 : (Π x : A, B x) == (Π x : A', B' x)), - f == g → a == b → f a == f (cast (Symm (DomInj H1)) b) + f == g → a == b → f a == f (cast (symm (dominj H1)) b) diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out index 67fd0fabb5..77c67417f6 100644 --- a/tests/lean/norm_tac.lean.expected.out +++ b/tests/lean/norm_tac.lean.expected.out @@ -9,7 +9,7 @@ Assumed: read Assumed: V1 Defined: D -definition D : ℤ := @read ℤ 10 V1 1 Trivial +definition D : ℤ := @read ℤ 10 V1 1 trivial Assumed: b Defined: a Proved: T diff --git a/tests/lean/ns1.lean b/tests/lean/ns1.lean index 56512ebcbc..b684ae620e 100644 --- a/tests/lean/ns1.lean +++ b/tests/lean/ns1.lean @@ -3,7 +3,7 @@ import Int. namespace foo. variable a : Nat. definition b := a. - theorem T : a = b := Refl a. + theorem T : a = b := refl a. axiom H : b >= a. namespace bla. variables a c d : Int. diff --git a/tests/lean/refute1.lean b/tests/lean/refute1.lean index bb9d4a83a9..20c8cd9d7f 100644 --- a/tests/lean/refute1.lean +++ b/tests/lean/refute1.lean @@ -1,3 +1,3 @@ variables a b : Bool axiom H : a /\ b -theorem T : a := Refute (fun R, Absurd (Conjunct1 H) R) +theorem T : a := refute (fun R, absurd (and::eliml H) R) diff --git a/tests/lean/scope.lean b/tests/lean/scope.lean index d3261f2626..902f1e0a69 100644 --- a/tests/lean/scope.lean +++ b/tests/lean/scope.lean @@ -9,18 +9,18 @@ scope variable hinv : B -> A axiom Inv (x : A) : hinv (h x) = x axiom H1 (x y : A) : f x y = f y x - theorem f_eq_g : f = g := Abst (fun x, (Abst (fun y, + theorem f_eq_g : f = g := abst (fun x, (abst (fun y, let L1 : f x y = f y x := H1 x y, - L2 : f y x = g x y := Refl (g x y) - in Trans L1 L2))) + L2 : f y x = g x y := refl (g x y) + in trans L1 L2))) theorem Inj (x y : A) (H : h x = h y) : x = y := - let L1 : hinv (h x) = hinv (h y) := Congr2 hinv H, + let L1 : hinv (h x) = hinv (h y) := congr2 hinv H, L2 : hinv (h x) = x := Inv x, L3 : hinv (h y) = y := Inv y, - L4 : x = hinv (h x) := Symm L2, - L5 : x = hinv (h y) := Trans L4 L1 - in Trans L5 L3. + L4 : x = hinv (h x) := symm L2, + L5 : x = hinv (h y) := trans L4 L1 + in trans L5 L3. end print environment 3. diff --git a/tests/lean/scope.lean.expected.out b/tests/lean/scope.lean.expected.out index 6d51cb1156..79224d990c 100644 --- a/tests/lean/scope.lean.expected.out +++ b/tests/lean/scope.lean.expected.out @@ -13,15 +13,14 @@ Proved: Inj definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x theorem f_eq_g (A : Type) (f : A → A → A) (H1 : Π x y : A, f x y = f y x) : f = g A f := - Abst (λ x : A, - Abst (λ y : A, - let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := Refl (g A f x y) in Trans L1 L2)) + abst (λ x : A, + abst (λ y : A, let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := refl (g A f x y) in L1 ⋈ L2)) theorem Inj (A B : Type) (h : A → B) (hinv : B → A) (Inv : Π x : A, hinv (h x) = x) (x y : A) (H : h x = h y) : x = y := - let L1 : hinv (h x) = hinv (h y) := Congr2 hinv H, + let L1 : hinv (h x) = hinv (h y) := congr2 hinv H, L2 : hinv (h x) = x := Inv x, L3 : hinv (h y) = y := Inv y, - L4 : x = hinv (h x) := Symm L2, - L5 : x = hinv (h y) := Trans L4 L1 - in Trans L5 L3 + L4 : x = hinv (h x) := symm L2, + L5 : x = hinv (h y) := L4 ⋈ L1 + in L5 ⋈ L3 10 diff --git a/tests/lean/slow/tactic1.lean b/tests/lean/slow/tactic1.lean index 397612acaa..4b61f0dfb3 100644 --- a/tests/lean/slow/tactic1.lean +++ b/tests/lean/slow/tactic1.lean @@ -5,7 +5,7 @@ definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (doub (* -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions -local congr_tac = Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac())) +local congr_tac = Repeat(OrElse(apply_tac("refl"), apply_tac("congr"), assumption_tac())) -- Create an eager tactic that only tries to prove goal after unfolding everything eager_tac = Then(-- unfold homogeneous equality diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean index 112bf8870e..a8e9a9cf78 100644 --- a/tests/lean/subst.lean +++ b/tests/lean/subst.lean @@ -3,7 +3,7 @@ variable a : Int variable n : Nat axiom H1 : a + a + a = 10 axiom H2 : a = n -theorem T : a + n + a = 10 := Subst H1 H2 +theorem T : a + n + a = 10 := subst H1 H2 setoption pp::coercion true setoption pp::notation false setoption pp::implicit true diff --git a/tests/lean/subst.lean.expected.out b/tests/lean/subst.lean.expected.out index c69a7aa252..4712d4829a 100644 --- a/tests/lean/subst.lean.expected.out +++ b/tests/lean/subst.lean.expected.out @@ -10,4 +10,4 @@ Set: lean::pp::notation Set: lean::pp::implicit theorem T : @eq ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) := - @Subst ℤ a (nat_to_int n) (λ x : ℤ, @eq ℤ (Int::add (Int::add a x) a) (nat_to_int 10)) H1 H2 + @subst ℤ a (nat_to_int n) (λ x : ℤ, @eq ℤ (Int::add (Int::add a x) a) (nat_to_int 10)) H1 H2 diff --git a/tests/lean/subst2.lean b/tests/lean/subst2.lean index 5d70ee285a..cf01df5704 100644 --- a/tests/lean/subst2.lean +++ b/tests/lean/subst2.lean @@ -1,15 +1,15 @@ (* import("tactic.lua") *) theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z). - apply ForallIntro. + apply forall::intro. beta. - apply ForallIntro. + apply forall::intro. beta. - apply ForallIntro. + apply forall::intro. beta. - apply Discharge. - apply Discharge. - apply Discharge. - apply (Subst (Subst H H::1) H::2) + apply discharge. + apply discharge. + apply discharge. + apply (subst (subst H H::1) H::2) done. print environment 1. \ No newline at end of file diff --git a/tests/lean/subst2.lean.expected.out b/tests/lean/subst2.lean.expected.out index 325242d3b0..105c518650 100644 --- a/tests/lean/subst2.lean.expected.out +++ b/tests/lean/subst2.lean.expected.out @@ -3,13 +3,13 @@ Proved: T theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A, p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) := - ForallIntro + forall::intro (λ x : A, - ForallIntro + forall::intro (λ x::1 : A, - ForallIntro + forall::intro (λ x::2 : A, - Discharge + discharge (λ H : p (f x x), - Discharge - (λ H::1 : x = x::1, Discharge (λ H::2 : x = x::2, Subst (Subst H H::1) H::2)))))) + discharge + (λ H::1 : x = x::1, discharge (λ H::2 : x = x::2, subst (subst H H::1) H::2)))))) diff --git a/tests/lean/subst3.lean b/tests/lean/subst3.lean index b9ae590fda..3c011904c8 100644 --- a/tests/lean/subst3.lean +++ b/tests/lean/subst3.lean @@ -1,7 +1,7 @@ -(* import("macros.lua") *) +import macros theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z) := - take x y z, Assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z), - Subst' H1 H2 H3. + take x y z, assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z), + subst (subst H1 H2) H3 print environment 1. \ No newline at end of file diff --git a/tests/lean/subst3.lean.expected.out b/tests/lean/subst3.lean.expected.out index 5ad8b09d0f..1314ef5537 100644 --- a/tests/lean/subst3.lean.expected.out +++ b/tests/lean/subst3.lean.expected.out @@ -1,14 +1,15 @@ Set: pp::colors Set: pp::unicode + Imported 'macros' Proved: T theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A, p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) := - ForallIntro + forall::intro (λ x : A, - ForallIntro + forall::intro (λ y : A, - ForallIntro + forall::intro (λ z : A, - Discharge + discharge (λ H1 : p (f x x), - Discharge (λ H2 : x = y, Discharge (λ H3 : x = z, Subst (Subst H1 H2) H3)))))) + discharge (λ H2 : x = y, discharge (λ H3 : x = z, subst (subst H1 H2) H3)))))) diff --git a/tests/lean/tactic1.lean.expected.out b/tests/lean/tactic1.lean.expected.out index 3710f25367..e3b118305f 100644 --- a/tests/lean/tactic1.lean.expected.out +++ b/tests/lean/tactic1.lean.expected.out @@ -3,4 +3,4 @@ Assumed: p Assumed: q Assumed: r -theorem T1 : p ⇒ q ⇒ p ∧ q := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H H::1)) +theorem T1 : p ⇒ q ⇒ p ∧ q := discharge (λ H : p, discharge (λ H::1 : q, and::intro H H::1)) diff --git a/tests/lean/tactic10.lean b/tests/lean/tactic10.lean index f9a722c935..43d61479ad 100644 --- a/tests/lean/tactic10.lean +++ b/tests/lean/tactic10.lean @@ -4,8 +4,8 @@ definition g(a b : Bool) : Bool := a \/ b. theorem T1 (a b : Bool) : (g a b) => (f b) => a := _. unfold_all - apply Discharge - apply Discharge + apply discharge + apply discharge disj_hyp exact absurd diff --git a/tests/lean/tactic10.lean.expected.out b/tests/lean/tactic10.lean.expected.out index 48eb3b8601..f5abe8d09c 100644 --- a/tests/lean/tactic10.lean.expected.out +++ b/tests/lean/tactic10.lean.expected.out @@ -6,4 +6,4 @@ Defined: h Proved: T2 theorem T2 (a b : Bool) : h a b ⇒ f b ⇒ a := - Discharge (λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdElim a H H::1))) + discharge (λ H : a ∨ b, discharge (λ H::1 : ¬ b, or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1))) diff --git a/tests/lean/tactic11.lean b/tests/lean/tactic11.lean index 742f9640b4..f44ce4cec0 100644 --- a/tests/lean/tactic11.lean +++ b/tests/lean/tactic11.lean @@ -1,7 +1,7 @@ (* import("tactic.lua") *) theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a) := _ . beta. - apply Discharge. + apply discharge. conj_hyp. exact. done. diff --git a/tests/lean/tactic12.lean b/tests/lean/tactic12.lean index b3218dfbe4..b254ddc7f5 100644 --- a/tests/lean/tactic12.lean +++ b/tests/lean/tactic12.lean @@ -1,14 +1,14 @@ (* import("tactic.lua") *) theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a). beta. - apply Discharge. + apply discharge. conj_hyp. exact. done. variables p q : Bool. theorem T2 : p /\ q => q. - apply Discharge. + apply discharge. conj_hyp. exact. done. \ No newline at end of file diff --git a/tests/lean/tactic13.lean b/tests/lean/tactic13.lean index 5cab16f8b1..68b44ead70 100644 --- a/tests/lean/tactic13.lean +++ b/tests/lean/tactic13.lean @@ -3,10 +3,10 @@ import Int. variable f : Int -> Int -> Int (* -refl_tac = apply_tac("Refl") -congr_tac = apply_tac("Congr") -symm_tac = apply_tac("Symm") -trans_tac = apply_tac("Trans") +refl_tac = apply_tac("refl") +congr_tac = apply_tac("congr") +symm_tac = apply_tac("symm") +trans_tac = apply_tac("trans") unfold_homo_eq_tac = unfold_tac("eq") auto = unfold_homo_eq_tac .. Repeat(OrElse(refl_tac, congr_tac, assumption_tac(), Then(symm_tac, assumption_tac(), now_tac()))) *) diff --git a/tests/lean/tactic13.lean.expected.out b/tests/lean/tactic13.lean.expected.out index fea2a706b4..8a1f240c76 100644 --- a/tests/lean/tactic13.lean.expected.out +++ b/tests/lean/tactic13.lean.expected.out @@ -5,6 +5,6 @@ Proved: T1 Proved: T2 theorem T1 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : f (f a a) b = f (f b c) a := - Congr (Congr (Refl f) (Congr (Congr (Refl f) H1) H2)) (Symm H1) + congr (congr (refl f) (congr (congr (refl f) H1) H2)) (symm H1) theorem T2 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : f (f a c) = f (f b a) := - Congr (Refl f) (Congr (Congr (Refl f) H1) (Symm H2)) + congr (refl f) (congr (congr (refl f) H1) (symm H2)) diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean index 9fced163c1..d4b5ee029c 100644 --- a/tests/lean/tactic14.lean +++ b/tests/lean/tactic14.lean @@ -1,8 +1,8 @@ import Int. (* --- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions -congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac())) +-- Tactic for trying to prove goal using reflexivity, congruence and available assumptions +congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("refl"), apply_tac("congr"), assumption_tac())) *) diff --git a/tests/lean/tactic14.lean.expected.out b/tests/lean/tactic14.lean.expected.out index d21bf72938..a62e0479e2 100644 --- a/tests/lean/tactic14.lean.expected.out +++ b/tests/lean/tactic14.lean.expected.out @@ -3,4 +3,4 @@ Imported 'Int' Proved: T1 theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : f (f a) = f (f b) := - Congr (Refl f) (Congr (Refl f) assumption) + congr (refl f) (congr (refl f) assumption) diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean index a4ed118b2c..3fc564fdb5 100644 --- a/tests/lean/tactic2.lean +++ b/tests/lean/tactic2.lean @@ -2,11 +2,11 @@ variables p q r : Bool theorem T1 : p => q => p /\ q := - Discharge (fun H1, - Discharge (fun H2, + discharge (fun H1, + discharge (fun H2, let H1 : p := _, H2 : q := _ - in Conj H1 H2 + in and::intro H1 H2 )). exact -- solve first metavar done @@ -31,7 +31,7 @@ theorem T3 : p => p /\ q => r => q /\ r /\ p := _. print environment 1 theorem T4 : p => p /\ q => r => q /\ r /\ p := _. - Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact) + Repeat (OrElse (apply discharge) (apply and::intro) conj_hyp exact) done -- Display proof term generated by previous tac -- diff --git a/tests/lean/tactic2.lean.expected.out b/tests/lean/tactic2.lean.expected.out index e712655148..fad00475d1 100644 --- a/tests/lean/tactic2.lean.expected.out +++ b/tests/lean/tactic2.lean.expected.out @@ -5,16 +5,21 @@ Assumed: r Proved: T1 Proved: T2 -theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H (Conj H::1 H))) +theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := + discharge (λ H : p, discharge (λ H::1 : q, and::intro H (and::intro H::1 H))) Proved: T3 theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p := - Discharge + discharge (λ H : p, - Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1))))) + discharge + (λ H::1 : p ∧ q, + discharge (λ H::2 : r, and::intro (and::elimr H::1) (and::intro H::2 (and::eliml H::1))))) Proved: T4 theorem T4 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p := - Discharge + discharge (λ H : p, - Discharge + discharge (λ H::1 : p ∧ q, - Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (let H::1::1 := Conjunct1 H::1 in Conj H::2 H::1::1)))) + discharge + (λ H::2 : r, + and::intro (and::elimr H::1) (let H::1::1 := and::eliml H::1 in and::intro H::2 H::1::1)))) diff --git a/tests/lean/tactic3.lean.expected.out b/tests/lean/tactic3.lean.expected.out index 362e992e9a..ac015c76a1 100644 --- a/tests/lean/tactic3.lean.expected.out +++ b/tests/lean/tactic3.lean.expected.out @@ -5,6 +5,8 @@ Assumed: r Proved: T1 theorem T1 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p := - Discharge + discharge (λ H : p, - Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1))))) + discharge + (λ H::1 : p ∧ q, + discharge (λ H::2 : r, and::intro (and::elimr H::1) (and::intro H::2 (and::eliml H::1))))) diff --git a/tests/lean/tactic4.lean.expected.out b/tests/lean/tactic4.lean.expected.out index 3da2c3c0c1..ea948013ce 100644 --- a/tests/lean/tactic4.lean.expected.out +++ b/tests/lean/tactic4.lean.expected.out @@ -1,4 +1,4 @@ Set: pp::colors Set: pp::unicode Proved: T4 -theorem T4 (a b : Bool) : a ⇒ b ⇒ a ∧ b := Discharge (λ H : a, Discharge (λ H::1 : b, Conj H H::1)) +theorem T4 (a b : Bool) : a ⇒ b ⇒ a ∧ b := discharge (λ H : a, discharge (λ H::1 : b, and::intro H H::1)) diff --git a/tests/lean/tactic5.lean.expected.out b/tests/lean/tactic5.lean.expected.out index 88cdafaf70..15c9d9b115 100644 --- a/tests/lean/tactic5.lean.expected.out +++ b/tests/lean/tactic5.lean.expected.out @@ -2,4 +2,4 @@ Set: pp::unicode Proved: T4 theorem T4 (a b : Bool) : a ⇒ b ⇒ a ∧ b ∧ a := - Discharge (λ H : a, Discharge (λ H::1 : b, Conj H (Conj H::1 H))) + discharge (λ H : a, discharge (λ H::1 : b, and::intro H (and::intro H::1 H))) diff --git a/tests/lean/tactic6.lean b/tests/lean/tactic6.lean index 83723cdb4c..d61430d257 100644 --- a/tests/lean/tactic6.lean +++ b/tests/lean/tactic6.lean @@ -1,18 +1,18 @@ (* import("tactic.lua") *) theorem T (a b c : Bool): a => b /\ c => c /\ a /\ b := _. - apply Discharge - apply Discharge + apply discharge + apply discharge conj_hyp - apply Conj + apply and::intro (* Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) *) exact done theorem T2 (a b c : Bool): a => b /\ c => c /\ a /\ b := _. - apply Discharge - apply Discharge + apply discharge + apply discharge conj_hyp - apply Conj + apply and::intro (* show_tac() *) (* Focus(Then(show_tac(), conj_tac(), Focus(assumption_tac(), 1)), 2) *) (* show_tac() *) diff --git a/tests/lean/tactic8.lean b/tests/lean/tactic8.lean index 0bfc64bcac..ead518c712 100644 --- a/tests/lean/tactic8.lean +++ b/tests/lean/tactic8.lean @@ -1,7 +1,7 @@ (* import("tactic.lua") *) theorem T (a b : Bool) : a \/ b => (not b) => a := _. - apply Discharge - apply Discharge + apply discharge + apply discharge disj_hyp exact absurd diff --git a/tests/lean/tactic8.lean.expected.out b/tests/lean/tactic8.lean.expected.out index 98cc50f826..c053ca4f64 100644 --- a/tests/lean/tactic8.lean.expected.out +++ b/tests/lean/tactic8.lean.expected.out @@ -2,4 +2,4 @@ Set: pp::unicode Proved: T theorem T (a b : Bool) : a ∨ b ⇒ ¬ b ⇒ a := - Discharge (λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdElim a H H::1))) + discharge (λ H : a ∨ b, discharge (λ H::1 : ¬ b, or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1))) diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean index c151f757e9..4fdb20b892 100644 --- a/tests/lean/tactic9.lean +++ b/tests/lean/tactic9.lean @@ -2,8 +2,8 @@ definition f(a : Bool) : Bool := not a. theorem T (a b : Bool) : a \/ b => (f b) => a := _. - apply Discharge - apply Discharge + apply discharge + apply discharge disj_hyp unfold f exact diff --git a/tests/lean/tactic9.lean.expected.out b/tests/lean/tactic9.lean.expected.out index d7e9fc32bd..fbbaf838fa 100644 --- a/tests/lean/tactic9.lean.expected.out +++ b/tests/lean/tactic9.lean.expected.out @@ -3,4 +3,4 @@ Defined: f Proved: T theorem T (a b : Bool) : a ∨ b ⇒ f b ⇒ a := - Discharge (λ H : a ∨ b, Discharge (λ H::1 : f b, DisjCases H (λ H : a, H) (λ H : b, AbsurdElim a H H::1))) + discharge (λ H : a ∨ b, discharge (λ H::1 : f b, or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1))) diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean index 88f5af685f..d2af225532 100644 --- a/tests/lean/tst10.lean +++ b/tests/lean/tst10.lean @@ -1,6 +1,6 @@ variable a : Bool variable b : Bool --- Conjunctions +-- and::introunctions print a && b print a && b && a print a /\ b @@ -21,6 +21,6 @@ eval true => a -- Simple proof axiom H1 : a axiom H2 : a => b -check @MP -print MP H2 H1 -check MP H2 H1 +check @mp +print mp H2 H1 +check mp H2 H1 diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out index f57a72c9ae..4c1d64f48e 100644 --- a/tests/lean/tst10.lean.expected.out +++ b/tests/lean/tst10.lean.expected.out @@ -19,6 +19,6 @@ if a a ⊤ if ⊤ a ⊤ Assumed: H1 Assumed: H2 -@MP : Π (a b : Bool), (a ⇒ b) → a → b -MP H2 H1 -MP H2 H1 : b +@mp : Π (a b : Bool), (a ⇒ b) → a → b +H2 ◂ H1 +H2 ◂ H1 : b diff --git a/tests/lean/tst11.lean b/tests/lean/tst11.lean index 99b88af754..67e2da3cdf 100644 --- a/tests/lean/tst11.lean +++ b/tests/lean/tst11.lean @@ -5,8 +5,8 @@ eval xor true true eval xor true false variable a : Bool print a ⊕ a ⊕ a -check @Subst +check @subst theorem EM2 (a : Bool) : a \/ (not a) := - Case (fun x : Bool, x \/ (not x)) Trivial Trivial a + case (fun x : Bool, x \/ (not x)) trivial trivial a check EM2 check EM2 a diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out index 175020fcdc..d161d3388f 100644 --- a/tests/lean/tst11.lean.expected.out +++ b/tests/lean/tst11.lean.expected.out @@ -6,7 +6,7 @@ ⊤ Assumed: a a ⊕ a ⊕ a -@Subst : Π (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b +@subst : Π (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b Proved: EM2 EM2 : Π a : Bool, a ∨ ¬ a EM2 a : a ∨ ¬ a diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out index c51f19fa0a..aafd87e474 100644 --- a/tests/lean/tst3.lean.expected.out +++ b/tests/lean/tst3.lean.expected.out @@ -7,6 +7,11 @@ implies ⊤ (implies a ⊥) notation 100 _ |- _ ; _ : f f c d e c |- d ; e +Notation has been redefined, the existing notation: + infixl 100 ! +has been replaced with: + notation 20 _ ! +because they conflict with each other. (c !) ! fact (fact c) The precedence of ';' changed from 100 to 30. diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean index 113b5942af..4103643233 100644 --- a/tests/lean/tst4.lean +++ b/tests/lean/tst4.lean @@ -9,7 +9,7 @@ variable EqNice {A : Type} (lhs rhs : A) : Bool infix 50 === : EqNice print n1 === n2 check f n1 n2 -check @Congr +check @congr print f n1 n2 variable a : N variable b : N @@ -17,5 +17,5 @@ variable c : N variable g : N -> N axiom H1 : a = b && b = c theorem Pr : (g a) = (g c) := - Congr (Refl g) (Trans (Conjunct1 H1) (Conjunct2 H1)) + congr (refl g) (trans (and::eliml H1) (and::elimr H1)) print environment 2 diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out index 1ac314f31f..54af344208 100644 --- a/tests/lean/tst4.lean.expected.out +++ b/tests/lean/tst4.lean.expected.out @@ -10,7 +10,7 @@ Assumed: EqNice @EqNice N n1 n2 @f N n1 n2 : N -@Congr : Π (A : TypeU) (B : A → TypeU) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b +@congr : Π (A : TypeU) (B : A → TypeU) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b @f N n1 n2 Assumed: a Assumed: b @@ -20,11 +20,11 @@ Proved: Pr axiom H1 : @eq N a b ∧ @eq N b c theorem Pr : @eq N (g a) (g c) := - @Congr N + @congr N (λ x : N, N) g g a c - (@Refl (N → N) g) - (@Trans N a b c (@Conjunct1 (@eq N a b) (@eq N b c) H1) (@Conjunct2 (@eq N a b) (@eq N b c) H1)) + (@refl (N → N) g) + (@trans N a b c (and::@eliml (@eq N a b) (@eq N b c) H1) (and::@elimr (@eq N a b) (@eq N b c) H1)) diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean index ff99e839a7..fceff6dcfc 100644 --- a/tests/lean/tst6.lean +++ b/tests/lean/tst6.lean @@ -1,8 +1,8 @@ variable N : Type variable h : N -> N -> N -theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := - Congr (Congr (Refl h) H1) H2 +theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := + congr (congr (refl h) H1) H2 -- Display the theorem showing implicit arguments setoption lean::pp::implicit true @@ -13,11 +13,11 @@ setoption lean::pp::implicit false print environment 2 theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := - DisjCases H + or::elim H (fun H1 : a = b ∧ b = c, - CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) (fun H1 : a = d ∧ d = c, - CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) -- print proof of the last theorem with all implicit arguments setoption lean::pp::implicit true @@ -25,34 +25,34 @@ print environment 1 -- Using placeholders to hide the type of H1 theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := - DisjCases H + or::elim H (fun H1 : _, - CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) (fun H1 : _, - CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) setoption lean::pp::implicit true print environment 1 -- Same example but the first conjuct has unnecessary stuff theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := - DisjCases H + or::elim H (fun H1 : _, - CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b)) + congrH (trans (and::eliml H1) (and::elimr (and::elimr H1))) (refl b)) (fun H1 : _, - CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) setoption lean::pp::implicit false print environment 1 theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) := - DisjCases H + or::elim H (fun H1 : _, - let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) - in CongrH AeqC (Symm AeqC)) + let AeqC := trans (and::eliml H1) (and::elimr (and::elimr H1)) + in congrH AeqC (symm AeqC)) (fun H1 : _, - let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) - in CongrH AeqC (Symm AeqC)) + let AeqC := trans (and::eliml H1) (and::elimr H1) + in congrH AeqC (symm AeqC)) setoption lean::pp::implicit false print environment 1 diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index ed6ea0e2e9..2d830f6fb8 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -2,70 +2,68 @@ Set: pp::unicode Assumed: N Assumed: h - Proved: CongrH + Proved: congrH Set: lean::pp::implicit variable h : N → N → N -theorem CongrH {a1 a2 b1 b2 : N} (H1 : @eq N a1 b1) (H2 : @eq N a2 b2) : @eq N (h a1 a2) (h b1 b2) := - @Congr N (λ x : N, N) (h a1) (h b1) a2 b2 (@Congr N (λ x : N, N → N) h h a1 b1 (@Refl (N → N → N) h) H1) H2 +theorem congrH {a1 a2 b1 b2 : N} (H1 : @eq N a1 b1) (H2 : @eq N a2 b2) : @eq N (h a1 a2) (h b1 b2) := + @congr N (λ x : N, N) (h a1) (h b1) a2 b2 (@congr N (λ x : N, N → N) h h a1 b1 (@refl (N → N → N) h) H1) H2 Set: lean::pp::implicit variable h : N → N → N -theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := Congr (Congr (Refl h) H1) H2 +theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := congr (congr (refl h) H1) H2 Proved: Example1 Set: lean::pp::implicit theorem Example1 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) := - @DisjCases + or::@elim (@eq N a b ∧ @eq N b c) (@eq N a d ∧ @eq N d c) (h a b == h c b) H (λ H1 : @eq N a b ∧ @eq N b c, - @CongrH a + @congrH a b c b - (@Trans N a b c (@Conjunct1 (@eq N a b) (@eq N b c) H1) (@Conjunct2 (@eq N a b) (@eq N b c) H1)) - (@Refl N b)) + (@trans N a b c (and::@eliml (@eq N a b) (@eq N b c) H1) (and::@elimr (@eq N a b) (@eq N b c) H1)) + (@refl N b)) (λ H1 : @eq N a d ∧ @eq N d c, - @CongrH a + @congrH a b c b - (@Trans N a d c (@Conjunct1 (@eq N a d) (@eq N d c) H1) (@Conjunct2 (@eq N a d) (@eq N d c) H1)) - (@Refl N b)) + (@trans N a d c (and::@eliml (@eq N a d) (@eq N d c) H1) (and::@elimr (@eq N a d) (@eq N d c) H1)) + (@refl N b)) Proved: Example2 Set: lean::pp::implicit theorem Example2 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) := - @DisjCases + or::@elim (@eq N a b ∧ @eq N b c) (@eq N a d ∧ @eq N d c) (@eq N (h a b) (h c b)) H (λ H1 : @eq N a b ∧ @eq N b c, - @CongrH a + @congrH a b c b - (@Trans N a b c (@Conjunct1 (a == b) (@eq N b c) H1) (@Conjunct2 (@eq N a b) (b == c) H1)) - (@Refl N b)) + (@trans N a b c (and::@eliml (a == b) (@eq N b c) H1) (and::@elimr (@eq N a b) (b == c) H1)) + (@refl N b)) (λ H1 : @eq N a d ∧ @eq N d c, - @CongrH a + @congrH a b c b - (@Trans N a d c (@Conjunct1 (a == d) (@eq N d c) H1) (@Conjunct2 (@eq N a d) (d == c) H1)) - (@Refl N b)) + (@trans N a d c (and::@eliml (a == d) (@eq N d c) H1) (and::@elimr (@eq N a d) (d == c) H1)) + (@refl N b)) Proved: Example3 Set: lean::pp::implicit theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a b = h c b := - DisjCases - H - (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b)) - (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b)) + or::elim H + (λ H1 : a = b ∧ b = e ∧ b = c, congrH (and::eliml H1 ⋈ and::elimr (and::elimr H1)) (refl b)) + (λ H1 : a = d ∧ d = c, congrH (and::eliml H1 ⋈ and::elimr H1) (refl b)) Proved: Example4 Set: lean::pp::implicit theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a c = h c a := - DisjCases - H - (λ H1 : a = b ∧ b = e ∧ b = c, - let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC)) - (λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC)) + or::elim H + (λ H1 : a = b ∧ b = e ∧ b = c, + let AeqC := and::eliml H1 ⋈ and::elimr (and::elimr H1) in congrH AeqC (symm AeqC)) + (λ H1 : a = d ∧ d = c, let AeqC := and::eliml H1 ⋈ and::elimr H1 in congrH AeqC (symm AeqC)) diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean index 5145d4b02b..399b6f4dd8 100644 --- a/tests/lean/type_inf_bug1.lean +++ b/tests/lean/type_inf_bug1.lean @@ -5,8 +5,8 @@ check fun (A A': TypeM) (a : A) (b : A') (L2 : A' == A), - let b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b + let b' : A := cast L2 b, + L3 : b == b' := cast::eq L2 b in L3 check fun (A A': TypeM) @@ -19,16 +19,16 @@ check fun (A A': TypeM) (H1 : (Pi x : A, B x) == (Pi x : A', B' x)) (H2 : f == g) (H3 : a == b), - let L1 : A == A' := DomInj H1, - L2 : A' == A := Symm L1, + let L1 : A == A' := dominj H1, + L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b, - L4 : a == b' := HTrans H3 L3, - L5 : f a == f b' := Congr2 f L4, - S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1, + L3 : b == b' := cast::eq L2 b, + L4 : a == b' := htrans H3 L3, + L5 : f a == f b' := congr2 f L4, + S1 : (Pi x : A', B' x) == (Pi x : A, B x) := symm H1, g' : (Pi x : A, B x) := cast S1 g, - L6 : g == g' := CastEq S1 g, - L7 : f == g' := HTrans H2 L6, - L8 : f b' == g' b' := Congr1 b' L7, - L9 : f a == g' b' := HTrans L5 L8 + L6 : g == g' := cast::eq S1 g, + L7 : f == g' := htrans H2 L6, + L8 : f b' == g' b' := congr1 b' L7, + L9 : f a == g' b' := htrans L5 L8 in L9 diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out index e77b6502b6..2947a7c3ce 100644 --- a/tests/lean/type_inf_bug1.lean.expected.out +++ b/tests/lean/type_inf_bug1.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Imported 'cast' Set: pp::colors -λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 : +λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 : Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b λ (A A' : TypeM) (B : A → TypeM) @@ -14,18 +14,18 @@ (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : f == g) (H3 : a == b), - let L1 : A == A' := DomInj H1, - L2 : A' == A := Symm L1, + let L1 : A == A' := dominj H1, + L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := CastEq L2 b, - L4 : a == b' := HTrans H3 L3, - L5 : f a == f b' := Congr2 f L4, - S1 : (Π x : A', B' x) == (Π x : A, B x) := Symm H1, + L3 : b == b' := cast::eq L2 b, + L4 : a == b' := htrans H3 L3, + L5 : f a == f b' := congr2 f L4, + S1 : (Π x : A', B' x) == (Π x : A, B x) := symm H1, g' : Π x : A, B x := cast S1 g, - L6 : g == g' := CastEq S1 g, - L7 : f == g' := HTrans H2 L6, - L8 : f b' == g' b' := Congr1 b' L7, - L9 : f a == g' b' := HTrans L5 L8 + L6 : g == g' := cast::eq S1 g, + L7 : f == g' := htrans H2 L6, + L8 : f b' == g' b' := congr1 b' L7, + L9 : f a == g' b' := htrans L5 L8 in L9 : Π (A A' : TypeM) (B : A → TypeM) @@ -35,4 +35,4 @@ (a : A) (b : A') (H1 : (Π x : A, B x) == (Π x : A', B' x)), - f == g → a == b → f a == cast (Symm H1) g (cast (Symm (DomInj H1)) b) + f == g → a == b → f a == cast (symm H1) g (cast (symm (dominj H1)) b) diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index 6176bb7a6a..d2323b8f7d 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -23,7 +23,7 @@ local ok, msg = pcall(function() child:add_definition("val3", Const("Int"), Cons assert(not ok) print(msg) assert(child:normalize(Const("val2")) == Const("val2")) -child:add_theorem("Th1", Eq(iVal(0), iVal(0)), Const("Trivial")) +child:add_theorem("Th1", Eq(iVal(0), iVal(0)), Const("trivial")) child:add_axiom("H1", Eq(Const("x"), iVal(0))) assert(child:has_object("H1")) local ctx = context(context(), "x", Const("Int"), iVal(10))