From 935c2a03a31a46e0713ab4f52a3bcccd1420f352 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 19:10:21 -0800 Subject: [PATCH] feat(*): change name conventions for Lean builtin libraries Signed-off-by: Leonardo de Moura --- doc/lean/calc.md | 20 +- examples/lean/even.lean | 30 +- examples/lean/ex1.lean | 12 +- examples/lean/ex2.lean | 15 +- examples/lean/ex3.lean | 22 +- examples/lean/ex4.lean | 6 +- examples/lean/ex5.lean | 65 +-- examples/lean/set.lean | 41 +- examples/lean/tactic1.lean | 4 +- examples/lean/tactic_in_lua.lean | 2 +- src/builtin/Nat.lean | 310 +++++++------ src/builtin/cast.lean | 10 +- src/builtin/kernel.lean | 416 +++++++++--------- src/builtin/macros.lua | 20 +- src/builtin/obj/Nat.olean | Bin 15911 -> 15943 bytes src/builtin/obj/cast.olean | Bin 739 -> 743 bytes src/builtin/obj/kernel.olean | Bin 17140 -> 17184 bytes src/frontends/lean/parser_calc.cpp | 10 +- src/kernel/builtin.cpp | 82 ++-- src/tests/frontends/lean/frontend.cpp | 2 +- src/tests/library/rewriter/rewriter.cpp | 10 +- tests/lean/abst.lean | 4 +- tests/lean/abst.lean.expected.out | 4 +- tests/lean/apply_tac1.lean | 4 +- tests/lean/apply_tac1.lean.expected.out | 4 +- tests/lean/apply_tac2.lean | 8 +- tests/lean/apply_tac2.lean.expected.out | 2 +- tests/lean/bad10.lean | 2 +- tests/lean/bad10.lean.expected.out | 2 +- tests/lean/bad5.lean | 2 +- tests/lean/bad5.lean.expected.out | 2 +- tests/lean/bad9.lean | 2 +- tests/lean/bad9.lean.expected.out | 2 +- tests/lean/bug.lean | 2 +- tests/lean/bug.lean.expected.out | 2 +- tests/lean/cast1.lean | 2 +- tests/lean/cast2.lean | 8 +- tests/lean/cast2.lean.expected.out | 6 +- tests/lean/cast3.lean | 4 +- tests/lean/cast3.lean.expected.out | 4 +- tests/lean/cast4.lean | 22 +- tests/lean/cast4.lean.expected.out | 22 +- tests/lean/discharge.lean | 8 +- tests/lean/discharge.lean.expected.out | 2 +- tests/lean/disj1.lean | 2 +- tests/lean/disj1.lean.expected.out | 2 +- tests/lean/disjcases.lean | 8 +- tests/lean/elab1.lean | 8 +- tests/lean/elab1.lean.expected.out | 32 +- tests/lean/elab7.lean | 20 +- tests/lean/elab7.lean.expected.out | 29 +- tests/lean/eq3.lean | 4 +- tests/lean/eq3.lean.expected.out | 4 +- tests/lean/errmsg1.lean | 2 +- tests/lean/exists1.lean | 2 +- tests/lean/exists1.lean.expected.out | 2 +- tests/lean/exists2.lean | 16 +- tests/lean/exists2.lean.expected.out | 16 +- tests/lean/exists3.lean | 34 +- tests/lean/exists4.lean | 12 +- tests/lean/exists4.lean.expected.out | 10 +- tests/lean/exists5.lean | 2 +- tests/lean/exists5.lean.expected.out | 2 +- tests/lean/exists6.lean | 6 +- tests/lean/exists7.lean | 2 +- tests/lean/exists7.lean.expected.out | 2 +- tests/lean/exists8.lean | 34 +- tests/lean/find.lean.expected.out | 8 +- tests/lean/forall1.lean | 2 +- tests/lean/forall1.lean.expected.out | 2 +- tests/lean/ho.lean | 2 +- tests/lean/ho.lean.expected.out | 2 +- tests/lean/interactive/elab6.lean | 4 +- .../lean/interactive/elab6.lean.expected.out | 2 +- tests/lean/interactive/t10.lean | 2 +- tests/lean/interactive/t12.lean | 2 +- tests/lean/interactive/t12.lean.expected.out | 2 +- tests/lean/interactive/t13.lean.expected.out | 2 +- tests/lean/interactive/t3.lean.expected.out | 2 +- tests/lean/interactive/t6.lean | 2 +- tests/lean/interactive/t8.lean | 4 +- tests/lean/interactive/t9.lean | 6 +- tests/lean/let2.lean | 10 +- tests/lean/let2.lean.expected.out | 12 +- tests/lean/lua11.lean | 6 +- tests/lean/norm_bug1.lean | 14 +- tests/lean/norm_bug1.lean.expected.out | 14 +- tests/lean/norm_tac.lean.expected.out | 2 +- tests/lean/ns1.lean | 2 +- tests/lean/refute1.lean | 2 +- tests/lean/scope.lean | 14 +- tests/lean/scope.lean.expected.out | 13 +- tests/lean/slow/tactic1.lean | 2 +- tests/lean/subst.lean | 2 +- tests/lean/subst.lean.expected.out | 2 +- tests/lean/subst2.lean | 14 +- tests/lean/subst2.lean.expected.out | 12 +- tests/lean/subst3.lean | 6 +- tests/lean/subst3.lean.expected.out | 11 +- tests/lean/tactic1.lean.expected.out | 2 +- tests/lean/tactic10.lean | 4 +- tests/lean/tactic10.lean.expected.out | 2 +- tests/lean/tactic11.lean | 2 +- tests/lean/tactic12.lean | 4 +- tests/lean/tactic13.lean | 8 +- tests/lean/tactic13.lean.expected.out | 4 +- tests/lean/tactic14.lean | 4 +- tests/lean/tactic14.lean.expected.out | 2 +- tests/lean/tactic2.lean | 8 +- tests/lean/tactic2.lean.expected.out | 17 +- tests/lean/tactic3.lean.expected.out | 6 +- tests/lean/tactic4.lean.expected.out | 2 +- tests/lean/tactic5.lean.expected.out | 2 +- tests/lean/tactic6.lean | 12 +- tests/lean/tactic8.lean | 4 +- tests/lean/tactic8.lean.expected.out | 2 +- tests/lean/tactic9.lean | 4 +- tests/lean/tactic9.lean.expected.out | 2 +- tests/lean/tst10.lean | 8 +- tests/lean/tst10.lean.expected.out | 6 +- tests/lean/tst11.lean | 4 +- tests/lean/tst11.lean.expected.out | 2 +- tests/lean/tst3.lean.expected.out | 5 + tests/lean/tst4.lean | 4 +- tests/lean/tst4.lean.expected.out | 8 +- tests/lean/tst6.lean | 32 +- tests/lean/tst6.lean.expected.out | 52 ++- tests/lean/type_inf_bug1.lean | 24 +- tests/lean/type_inf_bug1.lean.expected.out | 24 +- tests/lua/env4.lua | 2 +- 130 files changed, 927 insertions(+), 965 deletions(-) diff --git a/doc/lean/calc.md b/doc/lean/calc.md index 9f42a3b0d..c502c9133 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 f76c20bec..2496d8258 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 8e14b78cb..d600ae759 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 5a0e3a0c1..c813ea2cd 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 d5d8aec11..2030cf415 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 23bcde8d6..e470b12d3 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 b2866682c..11c574612 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 1ebbc059c..48fd4358b 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 4de6d4bbb..50e1dcd20 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 c3d10e86d..e2f86d5a1 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 6e2e3feaa..3e40671d7 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 6d9813024..8bc01e02f 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 92cfbbe21..3fa7175ba 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 05484ba44..db0ae3aec 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 5da36280d2c2e475a414ad3e22c49692e63be644..c120b1d2af57025bc22af2bbe95ce1f8e0e8906b 100644 GIT binary patch literal 15943 zcmb7LdyHj8ojz4{Z+G9$1`}llSeKq=db(#8A`ZCOS%{8Vk@0E>uS7tU$DQsw^ksUw zd+xmrBWt4UD(;9Q!OcqWfjoEB#kcr};%1HDIEorKG1*lU1sMTdcV(39GjZ$tzH?92 zse5kEFoEi-`n@0ZtEzL(U0G_kmiKg)+FAb3boQ;Tbo<%fc6YhGl-<e;WE=#za}#t>s+AL%b=$YJ{Z9k+IzAZO}e3-joB6m zGBaj(t7Gl!R#uig4-6Y<47-!;Zb4gzAaXQiK|6CD=$MH_!KV&B6tp;rT7b>?QXhY^ ziTXg5`aqQ#YnQ#pGYUNkNK~Rx7W!&&rOcDE!1spHe8K7^GG!Fkoe|fUMO-@z!DpbA zb53O!O-VUx-;w$M#{K*b>UT=kI*`?BKpgL_&Ch4cw*+>x-rV+nz&u-O=g@61sm?(+ zvk7@;`NlwBgmBC@GtaDo7yUN{PMc=YZboAePO3Ng#(k@p$)^4P)|en|b!n}a-O}!^ zbc4KzL!>Rp$*hr3!`_Ix(6*8d72PDZfw{sD2~&YN7R_-qtAT{MOwA%Mg7`!gBbOn? z!Yl<$2F3gmMK%sEu`Ski_UwU9S+>Cs+6OwleotdlxAW|oO22S22m{RB`B~i_z*y|A zK(FDGe4*2uUu<=KDN7|P)F&#@*8QTvzqf9&HM^&^)N5z$rOrOiW!K_QqdxFk9e%^V zE2#X{Y=f=zosA^}mlSbSF`1`0x@0mnP-A|ZSHrJ1=|I?KV9}WzT8eoICOa=y76Uuw z>uWnVu;b;n_iqQYtTX3D=Q-I~?sr!>n^(HySwT1}jNN8!Z*6x^Wmt+cCcEljNEOTk zHFuaGOts19QMbLvZ$kJ-i*K6q%-+5)*OpUcKq4QQ=5l*`ngH_B)?iGCr(b2e#XRvW zv#%Ms6IgvO9EFj%A(n1|<4qW*fR| zXlOl`YMo4|N9@T3VC9}f_w8t+9fgTQcw=ZahsBIt1ph9NEL_)Zv(%;q8d*mdUrw9f zLze{KsTu+G{u##bb?E2&`=H=l?`KqS02^Ou_xfF5>AZ@<9xInQj3{O^(CMX6^Jmk_ zH-t-4#UJ#_(l)wdb+miX$gmsGeVDTybU(}BETYTtjp#8ftMR&`-zjF0vA}!RRp<`#P8dd!MbRXQ;;lru>${{^tggrW{%*cf;dS>gBeDB^=XeJKQ;+R1-p?!bbo z(3K6^+{L7!#H%<#6)5*HfEo?E*t)5GUHialH;XG?!jgQgwf%1ArcNtg?%vLPcPgsv zW4@B~yRGHH7MZY_(Kwl9hH2@@mwyb^WXoi-n7#{$_8gg#m!*UyointqK>Iy3@nV8& zajuA5yZ(WP0i%y!NtfONj>0F@rpzThKwZLiVcQ8&10KGrtyRb0*_5d=< z&C>Eiw4+h*CxA;mw56%$U~+~WLTVnxEz7-Frj{i-jkJ9>;8_(7%1tEPX%>N0+Dgang=U(;-#U-7$hRFHRrvb6d!K0ByNEwt#~ z1(1^cR(7dHTw5kEy)z-Eo${1297speFkD>K|CSh}rLNT0U2AgP{KHZ*8ySrt;{_=a z)S*23CeJh|!Svddk^%x(8*DXZg5Z!n$1ph+#~Bk`i0Qgwyc%Wm%rww9so-%5$`!kk zs^9AMR^}_BHFo^VM;^goJEK4cXm_~HtB?oty`lTp>{8oOTmv8EgV|n;%|=j=?`-75 z0 zLNyvZe~BDD@|;8=G_gU}4)S)OQQ`R@y4pqlhTRd>hI|%)k@F!p&Qg2os3!7aK%xq| z-jhgPBpfQ4+rc^w!238!ur{ApU?M#n<+PAsm`lmI-n<`>+o=H#Pv-V=eo+6-9>Bws zc@H}8tu$gUkcJOWG>9vkGH6=Z(#&0?iWow`hh+Lt8+efoxr!mE?p}`z5IzD~*bh~} z?l}>BRTUPQe>Ex4AAmmaoq4DliJWOUJxtET|2seo&whfCzS#NA z-vj(W-M88>1{eCkkhF|&my-^-%u|iSQu_oUvs{MAfn0A@>_qN^0N*!4t_ns}Hk#l@ z9oTTl5}ce)%tKUcsN_l-7iMuIF!w=)2f@&M0SzM`Vv?MN72{*0GzNo5&|K-8EIs%W zB&P`!oOZuT;5$Ke9O6igyeHh@ogVtRCTEnd2H4o3mQN))Pd)dlz^g;J zKbof&i;6_WI+Rcyh-)6J@>a@y-JtMT$S^-4=OQ#L$o7mn$n($u>xYtuS$d6!`}|=u z;NX{D1NhRyZU&{D09-nvm|!&SU+4IzfxFlGQ6(u3gd=aKq@|1E+i94E5OW*#|0KjH zsGkbme_(ewzR**e!NTZvYEScHy8+<%<`(d|qIiYe&q-|7iv40aY?iOXaA-ICs~}`_ z7;DV_k#92Ic#o6=#CwQYO#+mGX_g$rIcbx%C;G*N-mC@9`4WddIFO|7B7`Wc)Gv8{ z%cvBIYtIAn`H`K$V=&QNP>8fc#hIx>e&O<*W7VJp>rfmG$huezBes~m1o&WOFN<`+ zcnBZ5NBD0(9{w4HD6W-=^vV+_6&2SSwY+*g(n6p;qtG>wUQLHI2|!U9g8Ch+B&y|xZYYEoUx%|#w=E-LhA8Og`RxlB)_8gK(ohtyhJ73-o* z+3P%xecK4Bs*6!|1jkG@izaeRZJU6gXRfAhL6__204h$d_HBM-uM4_G0iZ{NZf^x< zY44EPh4D7Oq63fHfwUOH@^F>g2B_u;=$YPn@)$ID3m{jF@(zGO13uxA8kK(F z8*haJCg+)+n9P+kGfH4&I5@!CTwr1{t&Kq;95~|JvyzxxhRHXFn6Pwe!6yn{3e3w# zC|L7Az0gpOI3P1Hay-Y{;;3-Y>as+k%RzZ5kiv?|W-GQle3{YmXg-W5w&$7cKn_ns zcrM6x(4xzHo8}ud^36XN_l>=_&`UXRN#f}9>C-QP09#YO6Nik49l1Ah zt_4FKX~Ynb)SXkF43Yd|B4D!o;Oa#`MXy02Iv|`l?W-`UCs;H^hm%JztL~TCWl{|n z5VC~z_Ej_vW4co(t9Uys;CgJi0|FL{Nj>08&aL)`kc|+U#ToRt#e>qmiCIuMyZQ)1 zrgj5`6mB((p!Z+8Ec?GO5?|BME2tPe;MyPfj{RqfNN;XB7r@SZ7br~N;Wd9w4LDCF zrSlmke@6VU5pdU}eEUYCzLmZedtqS#%b=?1 zvr-de46nw86YVbuVOE6w=t)0mpVpfD3=m`-vp?M}N0jFpsO|u5bZOx7N;ez|J1Z;+ zek16=NQ^!R8!ltC>audQRVsFtCzZci7hi=sS`3ed?$_8IS{IcP@JPhGbOIC=AV}ftyX637oSel{()%fD0PmVVEUyPy z;Q@}C%vGssriq36l^=eI6--gw2l{Vp*o)3d-^iM)#3OJb4^k$t#s{bnN2I;JRw*r@kxjmPnV%(I*-!c?LF-AOHy*K7`-Sh-5{LhN>; zE93O-n6f(1(fWhQ_z<+opE{y<5Dh&}vC+e!L9trz$d!Kq=PbC)(No_<*RadmwYuL5 zvqyZ_**Q$adix=7PI{p+Cv(37EF}Q-R=F8`ul2ZxIWzRZR(pT+$#_&>(=AjF3aEOA z`aS_+(w9X`-S0ulHTuSOA)5dWbs^!bFCFJ#N}sjGS9?ECJcR`)^zbHpJKEaaTk9@V ze!9vlUuF|h#!?dfXRrR_)BTx$lpKHZ<@xKjxCx@tmut}#l0HOXGU;+pkeL6jvkm-; z$}Jhwe#+fQNI2h6$BNqw=$Tv4D}R0#Jz5|QnGbdCSteGolHg^Y?%DE|e((vtK}<5$I1KBMmb1Aj2fZ5*M* zR-nw%hfkp^XZ$>LpGJ2Bv~((Y#HA^dF@K=tJ_N4#0>OO%AQ7Nfn8ZU|Tx7gO{Pw!A zi2Nx}&S3XhFfl3{@QMzpx`yf4{R}6=>Cp4VuQWov4Sc!sb<+D4sQ5z2J&dkE=tUp( zL}lD_RhcN%jY{G?=x~=-5p(zP8(=@>?hC>hCHel}iB9|eBXoZgy3doA2*=o^gKrH8 zN7g@S_;*u~e3mO{nGm z5%8j3`J}TqpNlD-{~D6D?Ws^gx7+KLh_#E@Bm zzX}pM?#?;14;SuKOo7dxbLCH1(r`TkT2+kvc_=2B4h)*;lgLFk(dgV(;JaV0gYUWX zcIT4sFde=AEaiQn&_TwMT@iDU|Edn8Qp_=d%;dSs{ZkU?Ut_Fus<0mQODKBQ46LD#6pIV66Bu zy9~>tx-2rxE>rVZwTU#lCj4x^J^GIOMOCG_Ga{nwqaZS~XjRaB$9)yUgXE`50=ROv z2@of%DogF8sw=3@#8#Wh<6z(pqeY1=9rcPZ1h_k#OeROe+Q|i6Wem=AhZ%P*4nH0s z6{zCRYy*C6Bk_xrteuR>Q|rDRN=X(kg($hy)lP<+RN-i!_$RDS0n>xStb=a!5dBPk zNrkJO3I>3ruU=~#{G8*P#OxV%bxT9{2JJ@lh;}1!DErAh5wzfK0)cjq9|s9JT6@Ku zZ^N~^b~Y%Vn874p|b&A?a(}BvWUfT^6XE n4{P+2)mBzRf876)FdF$ECr2aylj3OPe+q0aTwd6PACLb(s}VXM literal 15911 zcmb7LeUOz^8Gp}t?_KupO!|j|__@F?yONm-Izy$di^9$&0TE0^6uiscg$v6r+`Wr9 z>GYvQMv7^TW~qs2HKt~nGkrLz8G(g0SvFJID3gd<&Lry8f1Tg&dG9&rJ@>uWm8s+T zc)p+KJm)#@Jv%m1E{zUXM#@q0PgOQ;9;?=(jpgcSc_i9esz!QgsTNI9kschYMWvBS zX*|*gZ~8{01!ZueGE%FIj+bjuJZd1%jFK4+*OZ2aqNQWCQmryJ3IwG;M$Gvb#3|5C z6C(lWsRSJWXf6e61Wpq@_q<3MsJQ^mr)`zIe18QK*x_gsFh$ z?bQ0xYGrGsWRizPkqBQ_Ef1aI%mQm{+B{Mz8w&)K#9OmK`8<-h$-pxX7N(==$fFg& zUJ7wml-JuZDS};rUcu~z1(or&>q}LW@j{Lg8k6Oy^JZ`1-_=Hmfzrr$dErQ96KA4p z@Sj4yZt6Ttjel2A^sCr9o6+3b=L^^i(D;FXak3lGC6Ug$5arp_Y{P}6acj#ifYB?2 z)#P(DCO3XqW(IXH|PPt?B=`6`##{SF8!zR}7kNR#i60NvyQ{oLyQ3E0wzZ6HyXNKMv z8=X>D#W~aL%0VGbkS@!GfmifQiIuH}^%Aoa3F~|;>;u^CKp>!z=~@gT!>lO1n|d*3 zX82%RLd7<~(<0ro(Ipw`&aIu#W3nHOZ^vOwBz8pivuL~%he5;jLdI5hI~gYp{$1+n z*wS!4l;<+wh<=w7om%gpQJnQ8e_?%3H+^_6`biB?Pf?#SGhT{XP#&*UO>Q(IUO?!! zbYjGaY@9>g0nroY$_7}XN(6wqMCq02wo$QF=!#-jq5CLjSEKtl-LnDRjc6FT1L#%# zT}8{2O+8`(^2Jlo-iU_2-Hu*y7Oesc7*Wt<1r$BQ)ec(u1^`NcptlQ6p>EBUW?;^J z>vLp$oc+$@6itjr%5GcIjs+?_45EtcuH-~NC(!IgQz+>5rLE;P9GO%RNhzY5bB$tk07rg++a?bRlTi-F zW;6!^&?s0GCLMwuqNM$RQtfCdhn!-PX)xK%_;BHP2$LNodzjs{w>|4%^;I+nGqs>y zQVKW=3;@mfzf)F%b;{7`(FW2xAt>26Qtxs74*-=F;=6SGU#z_ATP7sPLy&4_2GajP zK>X&YzKhBCn^ARo6#?gHXEJz?VYV);K7>W!toK3hU8l0Ms|$66`GsTVJoZxXAn;OK z9^=!Upp-%O8!ti<>Q!P<20x*+W4bRurj~wu1LzPMI*S|n-+?-^%O$YO05w}aRmYL2 z>`kmk?^zso*PS2Y*>PN#}rDAl$T}5vd z((0+1z?mVrj)#w!V!-BkxN83R_*m90txc~5qmgPLRMs%fA@x;>r+?YgA!(*fj#6rEdu-PH+PBC6X%5*DF#aotwOkhIHLAgxYn z6&h+DKt7QvU6PX^1EZqH3a(~g(i_8Lk*}i}s)YjYuvm%E1K7|ih^hv7T23thX~Hi8 zCB@PLHc$)FhEbo!WYITFAb=-vR5ZY%R#tLR7hyS!OISfUDU|3FNHGIIGn+|ajUm~M zQc!>ax5AtvW9v#akeTh2a0APan#Mc0Q3{#w1}>S=?vfJ7DhGH?B=#ur_2@Q+I3_n> zsn94zK#UaGG^v5q1{%ye%bg@lHv7Rydq8HWHj_;pFymGrv;C4SP6cjeWu%y%brZih z5ojioJeACx2bk2U|8kp%P#&eM+_X9(2kPe)IM{rq3P$^RG;(@;fnDar)agNaNM{%j z2^}{}(J7!bo(UZgMUZ*{A^D19@OO^-wktDN}Q)2`&70v7&fukrm?G zGf909%X?aFt{P}DLTluLV3UuXGIsmy`&{Ya9-Kg5IMGG;#j$ zcIh-jAqv&IFEBc`vbx6wrN|NheG5Q$JE^(1{AN)kD#%V|cl(^@98aT)CvO2YsULXuHkuav)Q$j|G6uKL zSkdGwS)5C4u0a)J6!kc?9wSs>O%iV>S?XERbpQ-! z(sS431S$sxAdvEg8S0BYD)4~>p!uQ3fMO_?ltTgI26$TD!C&Udo(bP249yzv!t(1Z zSzR%CRKeobCF-hHsFtCIokP^s*{FbAV;Z#py;3$1Dd!A;`)(lcgIIAJIQ(wF??rk| z9+>@TQY9G)LM^p~4Y|NKOe1Ou$2N`VA+8V})gYx#zMfEOo2K+NSiZUmSILWBb_7N9 z3kupC8jfl5B8KRxRe>y}bnxq|4UoRZ$>upAknJi!u52b77L)rpx;zd<3JQ?OPAJnz zx(z;O=+yvK&jX0zDmmU+2R~Bj%O@uRzvYM+nRZx}Rym3EKxOWnSwd1?-T-PaG+1<^ce#L`@``%RK$_ilD+ z2bc36r2R_Y3w+ z4%5Kqn08>0jnt9s%9AWBO!NYPeoat9;ROb!;*ZdLHf0JSLQ5(ORuI6^3u*U6oa}+& znn|eGKqZAQp`0q>^}77i3VQLJ)DL*zyHaR4N~A%| z;K%PeDA*AQ-z?+s2Aa?#kR!^gI*7(6rLE`_9R?DCT5u*191_a~##-H{%Epx@slX`5jUe2e~NtauE@IW*$rZXuOjq*+_I0pW3(&bJRCE zzU|hInc-N+Nj~Td1fV%7Met)zIjrQxkbXWhR>0^r4fCl8aWv;Vk>#o7Sn6Jw9^kjQ?dJq>ptqbkC|>9GlYDpfwcfoN6_?&viGAe?x)m} zZ0c{Y9yV*S@*ZJ9;)UkbWmb6@Ua{o^fd>7Jl=g9SMerZFF0NAXYI!odGHS;HB_U#u zNgK?|@=(pc(wlk0iA#V+>rOY%ALkE_PgIBG0c9G77rjWQCndUtpLxTzaLdxN|BlO0 zmiyrhFbRJ?lS?AqL)#%8sc@4AK#cl$1Gj?99K3@v+&88-iOAQT2m5|B{-$PJAq=&o z8@owF)o^ES1o}+qFFTVmPjY7(q?p$3W58QZF^I;W42aSj$pftu4S;zyQV**invwss zZ*f`P?Pf*QTA<<@0v)61e6pq~$Uq)({tQbJSwDB(U%2j5=$?;f!dvh*mPF2T%X8Un z=QLeOW>RgKrFc6x6Z3H!$7pVqJI2R>o9rNBtW!Su`V(+i$K`~WIbncg$FagRe+PQ9 z1JScjA%AKHscpDeo_c55OUyKN5+ck753%1f=!*TGb=_Z~I~6j&e# zm3v*N?gI{QH8HcPERj$*R!(5oqbaGuirQFQnowoRig)u3ufdOZJJv{6HgcL$ZcY{cfCS;4@Dp(S76{ms`l1=6Q|kQDT7`dul9j8Hs>;Nc z`I9WFL#3UekK_1n;32{Fch`LxT?wv#m|m_B23I=(Y)HkgXJwh&JtXpa4oJa^-`T|dnDM^ZAZ@F>I#580wgP-kUh>)$l$(ml<7uFN)Ab{giA#21f%I(N$xVfsB)d_5 zp-)j9>El3eXCrAR+g?Bv(U4w{-Ezm*SHd4xbNJvH@9W0;VRq#%hVFVfiBJQ2w3FB5 z)=u#OCk2i{Iy&A<4VnWX8|6;#1w4y291*!QOcNh)vK&a8Az}*K)o2DFb3bS+N{$Cs zXzVl63?(K>RZfR`+51;R&}`9*H5H+sA%HEyK}`w7=gm<%0Pla21GEi zfk@HG6B!+ad4VhzMj!y{VM@u*&CJW1cwb`jUq)47DP*al#5|~!FOw&u)a2<*a(e0@ hW5hv(5r_cU!ocL2TL7XN6o43Puxnn5TV_rw0{}YbAW{GT delta 122 zcmaFP`j~Y>IUAF6VsVM<#QFdMHURAyR#U@G`iVmoSEu$@-hnNG1&TP*zvSdljVR86O?O5f*s&d+zh zy_=wSCMWNC&wJkU{-5)m?@K1eI<4`M(Xmbues2Hx=z-4URHyL6g>yyW3s?B|#B`Ad zu1N!&bf7g^_$?C?W5q(Fx1Ve8A03+>9WNTwllwbG>W#FJRhr!QJ#^B$=2AIh0|u)vd_RP8EBYK8&^W?OdwY< z+Li-c$+5vcKZBlZr*QAgj808Y5qnmjF~@I3pRvYoWl)v!pFz|>;-N9N@&)DWyqz+F zb_LP^zrmOUr0b_xuf>2QJeM@Yt^r7@CCE(t&apqP7C9GNNhpd96zd!X&bTd%-y14Q zgw@fTHrkl4 zuXNEYow=K&8*A}#1CpqwT9OEE56M!9b=Oo)|M&0$+W zUEB%B&$+Vrq)a-PWPIV5U7&x9r_(GgE|U!4zK>A#Kbq z3>YG?ge;{{RA9_TGRx`7);Mg4|`89tHdo)o4n7*PIG|hepBeae8LdG>B0c zd>%v1l2xImN{2byQmAcXWGn`{5nv)aKO}M5 z*(F?vHW|oBQb`2NPKD?m>!89xODjdDrn&2<(R3DUKS`141*!KCumXQ4gC7Pc^&SQ| zy9(`LG{H*UYCWDtq!zlLjius4*2x-}^go%eDEFr*_ea22!hSS^AIsp!0nVm4+;#%7 zw}QOx4eBzVH-671WL421#j{)qbx4X;0*D$~`kjqTdC&oQ1 z%`=#zO7j_jvdA9*e1=Oro@HRY7+B#k_z5(%4fNB7QAOR0W5e9k3B_648|E*|%!la} zhJ|GKEC>YtA;3)}_#=SJvM(4T-n;~SF}#Yxp&nT$Cq(v3iIMK2@q}TlXrO5Bny{_8 zwQoXCham0Roq;Ge;H)WYsQ5z&cQ=*~Z&J@vcW|_7U$QJi| zK;0*n&lyINH)Fl8?Q^v0WM0aa};1s z(^P1lG;}O8h(DGZi$5GedxS-i!(bCQN~$jblvH2N;9nW&7D*HYoKc_T_p}alZs^SH zn=D*rbu3$)x*|$sT#X#fj-(1DAN2p)VS%N2uEtUw7?xw8VKv_sQos!cHc1f2Gn+g| zf>_M{(t5#tO4Dej$$89V^llMYEbBx2G#VM`D;fMd1Kpx5KNrrr4{!vIb4y>I!eE`G zcdw4p|E-}z+Dvw)CdLkQ&g(69c>Fr8n@@u(`~#3u;U6=IqU6>mlOIzevu%(H4gI35 zLAOLBF{6ZEHB3qmyDB*0xf`d{4d7Gg!E8Ce;D3Psj7HM_O9uZHpz`G32+H=g=t?07 z5~peaFNE}|)v6aT!k9{j)@Kb<)drb9Up{edN}n7TlIrVVEEWDegWoXF4XJn{D$SfV zYb%N{g8axwis!9Um+E-o%Q`J%y$D7UB`9cXK=YIpMY(5N-yK|X@(`Fr0;rm9A<(PMq z*ab#mw_prWloCkgMwD1dVd=6ln9~L=FOCdaR%l|ywc`V7ya1@fJa|;dW-lrQ4urm@g z@~)0zvq0F)7?vc+QM!z_1fQZrvnELAWNsXL>QC{Kidwy!R0Meu=uQR?C3J>Fbw?|KJt1*KwT z4M17tbpU0RwE$(6bq2YoIc+__uk^BtwkPFD%_=lNkBq@9g=7G`EwTsRInSj`InH%P z9c0@GP&M)O2D#@LsC>W{RW?57Ge##bAX8jc@_5TK8=JJZq{O4itP$ff9JR`67UdgNp&)Obr=PV+8pSb_>B01bjAk6k}Ff(G?~Z_sF6} z?k$kf(2B`EzXup!NRAwiJ5>BRiCEam@r08q$uAlz#)z!2p{EtNC_8Rpsq73y0dsmyU1K$&A3K-r5X747AQ^e59YZw3Lk5BFn$lqPB)Y$NSU3{%FL zy7r*=e56a-Uuvjs?RzRe0;amr2T%OsxkOi&; zsDOA2Kn28A02L6w3Xql2T@CO$+T|L6v#<5|Ym!g)s*|+4z|w|1DvV!|qlZYx@N$>( zthNyRSakgc(0M9Ri82f;@-z*BBPx#?p)p#cL^s}7^9f=Bum5=!>ce~6P>D8!7G;$u5j|f%xa7w&1FXIDh!-{AXQYk zAdwD8E|}!sVHkVn={|IvY1tN!96Rcl+;`loQB2&<<4Djs*1uj#8*wp~H80UuM(hMA zrD=aDO-qkKJ@*(0xG``-@oVUpXlCeCa%JD;x(#~Ipb8It&@&o@%u4iWrGc}dZLu2- z8T&NbUmahL1iPP4BBtb;SY}bU<6~oZy*{t|w{X60{B`lPikK3ucHTJ!m?;&ifl)c8 zt1NaSrpaP^0BTnmHOTK`@Z1EjqnM$!EG9hjuBhHzF&tYYfX#~*ELk+rz(fuYRrGq{ z_zdl|S;1j`ZwyUM;xiBF+f?mvn%@oweD_k0$eaR%;thrC*sOR0^ueg}#}@;K=Cf(` zSOWg4yH)$5nrNs zlB%#B09MbGr;xS{1k;gCQvU6Rwt%`~pM6y{8a^>n4;P?<>{8k|lWi2l5D@l10r7*qWM}*kwCr-GcE9-JdUj!n)b2r7<#5(cWcEu5q{i9h|^@D-^BhoeVuf$n5vStDQc(xMbO^?jF3B?;s_Bj1HlT`!58OLFlKXMGFxY40?t_@bmvZi?LH=p<2eYNrkCu8m>qevG1`cpcnVh#=%s(9_ zi>tgXi()Cf^Kasgk)IV*Ernqa=VkXmlIEpz!bk zFRqFb{cHs(^6YUH@m-2ku97Q?NC)z!@qZU!KjnLjpf&zQG*UrZ>2G4F&|Kb}xd(|! zuEuw$y)EZJ$lTC@`J?DlApbV|5KpK5e#80iVT2a}#eL`>L;p}}y4LEgoR+~1t%V$$ zqZ}?*wU&dmJz_2hDAhg!M2_O=*8b_rCr1#qxEGDq_yoY955Rk|)w$mWD2cIQ9dBzI zV%{z11T@;5KM7D<)29fg%ISuz-{?=V7WyGF+>oBG={=pe!$$N?uu)hk^t3-cKL-uO zVf)j7s%|JSZZO&#G;wJIDsYXH38E>{Fkl-$1CWc9fU+ItR)nlKIV-!cdL_FW+P9O& zp&tc14Fi=mgLdFSMqu1HEoBZ2DK$taY7l2JU*<-*JbSJL1F`Bxn*D6VeGcPt=jSu{ z1%k=5jn&p~oRjrbKkB(UOFj(3v$Njl>%B7V;4Va8;^avsk(@-YX_6ruYZJ0MGs|%f zh*n2A&Pgl-b?S#>PPbeQTn$zOqePzv6-AGf0aDRJ;Y#$OLE{2eHDnQr%$&r}0i;UP zXLHVH8=;b=Yh zA?F&jh-6m%7HB#d#`zLvRg6>r zpileZauT6A9gU2`!$!q8H*qK%NBwA=n>cV3Gz#ck`IZ4$31}K3BUPFpbmOMu8&7j+ zJUkBZUwl-)Zel=Dd4(Tn^nGN7h~uQpM98SQXZ<`$Z;}hvUdq6)HQm>smnzvm5k&SE z`D?1opdmAp0WGYLcZ~EFOey*+r1_NIn86t7D|>%jWbVv1V-1TmZtXP_IG*tIod~q9 zUz@ia8`u7;(>$hC%s!2EWb;lrDem#fsNBsMLK1#6^jQA&@RBj~FIi zqrho)06nfd^a#5gj4JMU0e!iH8$3g|r#t*X>O}@8aEJe1BK-;7;a|)%UyeIW=@WS4 zp~SH2jqhZ&znj7TGO+Pb%^Q3`YoA+=BW?zUJEgz_c{{VgY z;26OetqkQ9=bXl3JV206(5I(!a)JcfD*(z1oO{Bg;8YJe_$EeKQJ;$8N>)JIHCn_y#BS_66rI27w%sd9goFrOLD9nmmjBmshkh6FDg}VZY7^zZc*K3+YHb$bl(hTgvtG=11A{LcgA&8w%B8;M2zZl1gv1m`UP1)dpo zc+RReIRUCRp;A--Hc*S=NbTQh4JY}_FfJnCk|~y2C*CU47Cmp4=dlHNo=g+utK}x+ zs?uLfeSQI}O5rmAO5rmBN?`b1W8l#H}@N4Yg%=ltAiyqDr z*)jPa@)?in6*)s@E#+Q?A<50~UkR7wb9i$d{c=h#rW(Qg*V&)udOl1u_KN0OV9w`r zxQ7cArcDyQAzpc~@VmnprH@|^XbssuN06)D1CZnEaRSsCCKw@%p+^XWhpWW8u6A_+Bxz!S=Y#HfZjxY=IO>FBFsct2HwhkeczeX=MY!Ud=P;tjoCw!CwZb z7NT8%?B}(Vi<378O_ayk=ztT{+R_`xXW4vIQxeI zqt~C=<7sO~vi5Y)@%+OTm^%G7y}1+3Ay~v;V@*idYXQpGI{<2#p9~SZ{(LiH&J+5b#|Qy(*wFETkuL_{yy#!;SH5hOe92_Ny4U5kS_>rmGE{$^HVg z6@sN%t?yPhC+ZW!%~9Z-Kl>a~y^5j_%36{8cE3+p&>kjrhGiWYi*q-^@5k$s8bh(NN_!b3XR~Fxf)lW@VJt9OGCAjpqY# z*gUke(R5P&nro=tv6OgZo9>sKA|#lPZZ&$}_4k)>RHQz-8HAmDCmo~@NP3b|ZO&Y< zfMVxSpFe2R=afr?gowHA`rKE-QJ@x5|CK~wZ<5G$phrxNwwz&Z3 z6W812cc3TVDcu`8hQ}wyIl7?BgyT1_%S7Whzc7{hzlK9SQHF4A6$|Rw*hU>eI}ghM zzuvG2NY_oZP6R?4oSbSDr?8YL^EymKe@E2U+J0 zk8irHKDMP1!`C7*j?xc3Nq!FbJwf2>lECG4t7=FG{AN-shJ{(-s89-%4^io!2Pam* z(+joMHind67)h~H=8!5(eXjLn${V+D9G}=s$8|?2yCjyAUP(E;8seLK{?b1{kL@y=?fo)+zE0eCEF)8!0WfMOJ*(%|XCSkAm0RNRb^jSO4h5@c7kNMu{!yAzPNw zZ7DaXCk1Z^%3hLW_P0d|0nDAi+MFewzF&$w$V+7x< zeB;$uLj8V_z!#b@CRI;ZLI$iP%`A$P6~TaE!z7XG#_FTkS*OZeP6<(X9)ugPi6{e# z6xd0(VQ?oWWW?ecZQA$@iLBaKT3=7}e(C=PAmb0^vDHL`aP`AdW7xFmcz{qe*j;sWY zc84AceLMOpx9=c|JM--=(y0Tb6Y7C(sEQ@QPcN;NSfZ5z?%|yGr$$3 zy@g<(FKrPR$qI3PrPQf2j`u_i?dnN`wTQ_9#VYe>)ME*V1W!lIz zCaJ*pgFxWz0A<=9fIIupK8j|FNz9CQ10|e{Lie$dDetpR(0^dt?-V6!{Sj*YSCA?F z?nodrLZf$LbZ5+>75h;dlpW*n1TZx;G89mZ!(Un_*l}KS`^FKgAt=C#Zg=-QQ1g&` z3?MD24*~4%u!6q}L|c7`Qajg(XThQxaW6pG{nr4WRX$7ZUa@zhKqr0Sz6mA^>b?XAPA)XLkWBs;IgFi z94b~J0h$~Q6?bNccJ-oOLN_xDO^&AZ5b}VH6q>70x5s!Rc#4A-AZ)Ta_q>Fzl>R6{ zDZMv=j{sC+d<@`A+V*w<&T<;_0zm54s@6wrSb1R2GPX8P?VJo*3jQ)kk~WV4ls1ni z@Z$!$L!|=J%&2Gj%j%PjOB*}3j%6;1dMWvtHX=9VQej?5;gehW;Qa}Q364sT(Bz)erg4waxkJG^rwi?;(a15MN#JJrlUi_{gn06BDuV?%JOqcGCi@(g~-C60RIt<40$4fUjV3l z`yxTv)E2E6QjoYaqIE?Ya$zw)xZM}HJK`W48P z1y3gMs|LDdsz9twS>CqL6&!FN-BLZ*hnUYkY1momq3r=tBD~G*aWA0BWE5XO1e402w^H zc?jzf-f_PV46}pY$Flbs?%xe8tox4y?laI0$IA7R)*v7-JmD#Wc74z7gLmzg7HAk~3XvZCdPYdnO^U{i@UB_Vj z9E`fo`vpK-@Eh?jXC*LeA^y1(4P&1Jk~Ql9>VAPD2cb}Q3rEr9Xkw23%sRnms~gj3 z7HS4B7#RO^AS6d4^V1;J;h+v9FM~+7{0gAz+W!KSz6|_*6!0k9*8^7)gKpf8-Gj`Q zdoZ|x7&JY~H5gNzEpk8<5>5Rd8wsWkY+Kz3&ujf4E#1+TtldNu7Tl>>n{GK!TAj)G zl&GqWbW;tK!gLwr(3M9VVS2=QjM5{n0+8NwRfF7PWMlJqihB)Iw6G3T#<4i|SJRK@jH2#380oEI+ z#P0!=?mTHq_rox1HKItMSRK-X@XiD2O;6My2X?k@E$$E-iP~DA+Milh>W+q-OfvbA z2WnP29va+pTue_uzNk`?aC)v|Vkqg>;H)FTz*=T=UtkY>%~)JgHe&SiS7X3DOpBA&UC37`>dMuLgJp!Pfx1ir{eo2MNvvxKrB;E-`nYpVj8E zMMF1pN;^zlh7n(t9(8nbG#9C$lZm5njze{eW!>Sh6Z3;!z{zi_7s!uAx)JPIUcP9j z8mrpe!9WahZh~5rOe4ADc*v1E76Me_od8g@CmQ5u(H)C0%7vio-5UDA`ocG|J_m-% zPPSVQdVe_Zq0+lP>$FAoI7IR)g7ItxE=8w}D@e~}h7jB@HOnsN&I^1y2W z$^(3wQ$mni39$qON{G_|vVOaz05?$B831>l=&)QgJ{Q^wzECZy zP(LWKU0g_DK2nHLI|+TJ4K}1&_^2&oiPSnmv zb69eiW}1+L@Iz5ULxuQ58!1la(md3#PO5|bill#zzOwpkfKr{?o>X6k(JSOm)afi+ zkA^JS#Q<|OlMD^zvhPyu1-<9#rg-e6fa1xSyBaxYZO`#c6NZR_{aXUJe^YolQTPvq z(I!R{j-~D_>lCgS;M?nIgLp3Z!cz(-?c+#}R{Q*vBDxAVWg5du8S>b2pyaXh0BUC# zFvxEq?FxXyy0F6G83n|zB~ZSHVp7$>k+I;^Sd1#@!$F=9)pdNZpv6jTzbzz~m~a#o zeZ3F-*olh1?L-*y6$XqJr9>ta?nfMQD4sLv(&@8HVT1D^JzE6no^`3@G&)gETMa5X zZ4E%>A=lX=sZ9OollTHw<(k2#sCbz6H<0Irc@U)uDU=(t!y*aA=?w%)H=8XL@5Lya zXgs7?I<47i-|P$*kNN72+NUjo?6VXB_$)+F@j(V_$(pg{O}_AybJF!O!s&)-Aj=eI zmIvMpO_V`Me_idnpBUtZt?_$eJd1u2PdB^}G`CrkSClO|Q_06Pv;nzRQR`#Uh0qk&_I)|5HXcO?v<90&I` zWBudf%}uuBwfir=Zc8^%#jMGvxrs4F(QdS+@ad)mZYIcD1^4=g&^#R7TlB+nc}SKf z`7|SkjM8-z2HWiSk0c+_4n4*)?&$kRAOr4_m0Yl%{-_a?rWCtT(ja@mVR$;$KL$!Z zGKrIv3Z0SDXkBuNoKtf0dy~BnL)t^Z-iMRcGAgPeg&FRowRC~j)Wv@S3R#uY^`0AV zm6qj68dc9h4ryh}?utZN4S0EmiA4K2*k+`%i8N5#e+i6yH@;@yyRWyrq$8sfEx2lr=) zY@qBe%yl)uZs_MPA_(Y3G%`WQr#AtWiI;a-T5}=LHsd;c;MvJ@4xEg(JZW83j-!ldZ_y8G9S1~dMlGpG z&8Sw6i)$tsLBhBIqmr+1`t~t;pVCJarptKTd%;~wpYzeDbY->r z!JzY#!t|L0Me~(D=TDbDsj%HzXgW<9q^5~liOv$yUYgdLwiW59x_d43*9BXziqoHS zB&@3G_N?R_4|-4MU~4Qp=VGFwxfS(;b1tTH(h{ej^OKH>Ps6VJVGUtCwNjnedfoF99*50i#@ z$SYXNYEYV#ndJni%SnddS4%e zPFV&d(5?Vb?kDd7*8y2QCgz)x3jN>C3UpWq1KalR|H9yx$iuw<6hImL=>&cT;F)c% z&v0I@JS*4Z?AX!upS0oRdfcYQhlNy(jK;n*g9Iio7m>=)KVVS$e2!q}0Fd`E5GV>s z7W>mwq{O9oBrf(}S#e526qzK1{dOVHF@(pwvH$p#osxr7b?S=%<&-Za5QlnqXnT-W z*l6W93esmmoaJa*>(m!)Bn62te>#LITsi7*1(-C_=SfJEK3`4XQvmtZfnOR&b@R?d zW|IR$Wo844l@lL(6&e*U3bwUgiFTFV6}$ng*%Ig%UXbM&*`WvdlK>BfN6ta?RxwH) z5WHe{Uk8oe(tHD;u1~)Sa0!>mw+yNtzR+5~bOwg;_@~n_{XjFT+!A4C^$0Xakw}vs zZv+01ts#^DBj81ZvFL`cS*P`4*uJ|iUY_=YGMmN^hN&K|=hGpO!RqP}usYopSC67C z&j2rDzYS2veg~k8{a1s6u>fIK6?t7Ut0eW+;g!kLMiP|AStb1iogqq!7e|Q{lJqxj zAS~T*Gf@^(>+ezq!G8ldf2JQi)vi$J><`(oBqNOIl{%~xHfZPcD zhIX+zXZ{y(=fWlNlYGc_Na3uy49$7E9!E5_{`jh%nVM89!B9OtiLuK@?S45B{dB|+ zK%^Y{AwcEOa|TsUhi%yt0CO~NQ7wAb;EuHj2B%u27fiOS+Z8LtN!B4Zs;5EdDOBmd z07|7F0SpOZV6_qblf4#(>02kdzR{8f?HHL_yi=NXO{(i8s#VZ!lUmMe!{T z`5j)NmDjY~-{3s7>qP?#yM7E%uKtNZ)rMT1l$K|5!ztlL^23X`=NEThj&+P-#IcUhvM9k4$MdSV(px#^k z44{nrIY3>J{lcK?HGF}|w`QTTVfcEG+1>V4_!kAg_~dmJ;^S`P)UOAshK98yz2~al z9QF6dCjDzvi+f#-1j&NZ=Tfl6SKxPE0akCex%Kz3)tfP`zl$-c8JN|f4Zp)nujTbV zpPPo;MKQZTq-9DdYUFkm9(B9g^eMfluNhAjx67lAjAqm07%j}EQh3&`-ihXR)hBEc z`U#YyWT^Q+#kjunDQ8g2rzD*+h_)bk%H=*)nl@9l(Fe!!*MO$pg9i8;f!9Jo3RU@x5i{7ttYj`%KN(eF2&#W! z#NkG*Ejmo=dP+C;<9XuOm~U!$Vtp-tfdP$*Su!r0ZtGUBL9-XG_A{-KtNpRvIyn5j%fCVFUFyj5=KZ|vQ` L=;jspKVAGE1Ou^1 diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 60edd4dbb..1b4462902 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 bee7e12e5..629e59b69 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 f1073fd06..e77a6e46b 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 f72605900..2deb348d4 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 1c0fcd506..7712c8b52 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 a241ab3c3..48717adad 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 e7022ea00..467e3f229 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 d184b1342..4aa254fdf 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 f77fc8d5b..32ab828b0 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 c9da3cd33..08e2efc27 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 675736312..3861cee14 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 36e79f708..294ea7e02 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 017e71f63..97df31599 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 deea5aa7d..58fbbad0a 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 6d72f6d12..9c25a26e8 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 079e9bcd4..3c9fee4c2 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 6e093e983..53adf653f 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 4354e0ad8..0ff4396c6 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 33a9d76e8..3519518ae 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 4bedf9335..3eefa3d49 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 a9f6edf00..8ff44375a 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 4d29fd438..5013dcce0 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 834fb095e..d78ef34af 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 f26a279d3..ce6035a78 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 0682944e7..f76e10055 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 a5d17eab4..69e6baca4 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 f62895544..c61b7f7e9 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 13102b87e..ba0fb3e83 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 1aefd3eed..e5ffd0e1d 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 36ed7d8b4..56b81a478 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 24e6ed3e8..a49b1b786 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 6d824836d..07e8341f4 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 74d48d06a..b68550b08 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 4c4ed2ec6..0e80da44f 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 148fc260d..925df762f 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 d5542ebab..783843fc4 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 294ba9370..ce0c79e3c 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 11f4c165f..ccee5ea9f 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 453b01627..93e414f68 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 a1106e415..0b172240f 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 f9024920b..7f50c23f2 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 5d83250d1..d9c2f324d 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 3a1d5934e..887be720b 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 1bb871e20..63c0c0069 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 fcfe6454f..44a71e9e8 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 675ac2754..315e87637 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 b04aa3b73..e34270ba4 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 491dc4fe4..d901ef092 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 620a488be..7a003b38e 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 587132870..a31cf7c47 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 9ba9e80c1..2cdffce2d 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 6a07ee752..8d6659565 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 74eb17558..1bea43e06 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 368987e8c..7071cdb9c 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 653a0d365..e41967743 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 7db433aa8..d0eae73d1 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 0ff7de0f8..385206a41 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 c2c1d340b..d5143352d 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 af5fc8b62..a56720c61 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 035beb6eb..a895f6f3e 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 c34bb68de..bb7cda099 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 0e61a9c31..74cab7ec4 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 ba666b779..f9bc99ebe 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 c09f14d21..97bc0c79b 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 48fb412e1..b4b7b1a41 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 0653180f0..34352789b 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 de9904e32..9681b9ddc 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 e56e34452..ff70caccc 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 9a89a4d96..36a183450 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 3e94ea090..b5eb5ea11 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 67fd0fabb..77c67417f 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 56512ebcb..b684ae620 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 bb9d4a83a..20c8cd9d7 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 d3261f262..902f1e0a6 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 6d51cb115..79224d990 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 397612aca..4b61f0dfb 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 112bf8870..a8e9a9cf7 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 c69a7aa25..4712d4829 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 5d70ee285..cf01df570 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 325242d3b..105c51865 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 b9ae590fd..3c011904c 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 5ad8b09d0..1314ef553 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 3710f2536..e3b118305 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 f9a722c93..43d61479a 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 48eb3b860..f5abe8d09 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 742f9640b..f44ce4cec 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 b3218dfbe..b254ddc7f 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 5cab16f8b..68b44ead7 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 fea2a706b..8a1f240c7 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 9fced163c..d4b5ee029 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 d21bf7293..a62e0479e 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 a4ed118b2..3fc564fdb 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 e71265514..fad00475d 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 362e992e9..ac015c76a 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 3da2c3c0c..ea948013c 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 88cdafaf7..15c9d9b11 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 83723cdb4..d61430d25 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 0bfc64bca..ead518c71 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 98cc50f82..c053ca4f6 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 c151f757e..4fdb20b89 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 d7e9fc32b..fbbaf838f 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 88f5af685..d2af22553 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 f57a72c9a..4c1d64f48 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 99b88af75..67e2da3cd 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 175020fcd..d161d3388 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 c51f19fa0..aafd87e47 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 113b5942a..410364323 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 1ac314f31..54af34420 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 ff99e839a..fceff6dcf 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 ed6ea0e2e..2d830f6fb 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 5145d4b02..399b6f4dd 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 e77b6502b..2947a7c3c 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 6176bb7a6..d2323b8f7 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))