diff --git a/examples/lean/abelian.lean b/examples/lean/abelian.lean deleted file mode 100644 index cf3d35dc4..000000000 --- a/examples/lean/abelian.lean +++ /dev/null @@ -1,145 +0,0 @@ -import macros - -definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z) -definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x -definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id - -universe s ≥ 1 - -definition group := sig A : (Type s), sig mul : A → A → A, sig one : A, (associative mul) # (is_identity mul one) # (inverse_ex mul one) -definition to_group (A : (Type s)) (mul : A → A → A) (one : A) (H1 : associative mul) (H2 : is_identity mul one) (H3 : inverse_ex mul one) : group -:= pair A (pair mul (pair one (pair H1 (pair H2 H3)))) - --- The following definitions can be generated automatically. -definition carrier (g : group) := proj1 g -definition G_mul {g : group} : carrier g → carrier g → carrier g -:= proj1 (proj2 g) -infixl 70 * : G_mul -definition one {g : group} : carrier g -:= proj1 (proj2 (proj2 g)) -theorem G_assoc {g : group} (x y z : carrier g) : (x * y) * z = x * (y * z) -:= (proj1 (proj2 (proj2 (proj2 g)))) x y z -theorem G_id {g : group} (x : carrier g) : x * one = x -:= (proj1 (proj2 (proj2 (proj2 (proj2 g))))) x -theorem G_inv {g : group} (x : carrier g) : ∃ y, x * y = one -:= (proj2 (proj2 (proj2 (proj2 (proj2 g))))) x - -set_opaque group true -set_opaque carrier true -set_opaque G_mul true -set_opaque one true - --- First example: the pairwise product of two groups is a group -definition product (g1 g2 : group) : group -:= let S := carrier g1 # carrier g2, - -- It would be nice to be able to define local notation, and write _*_ instead of f - f := λ x y, pair (proj1 x * proj1 y) (proj2 x * proj2 y), - o := pair one one -- this is actually (pair (@one g1) (@one g2)) - in have assoc : associative f, - -- The elaborator failed to infer the type of the pairs. - -- I had to annotate the pairs with their types. - from take x y z : S, -- We don't really need to provide S, but it will make the elaborator to work much harder - -- since * is an overloaded operator, we also have * as notation for Nat::mul in the context. - calc f (f x y) z = (pair ((proj1 x * proj1 y) * proj1 z) ((proj2 x * proj2 y) * proj2 z) : S) : refl (f (f x y) z) - ... = (pair (proj1 x * (proj1 y * proj1 z)) ((proj2 x * proj2 y) * proj2 z) : S) : { G_assoc (proj1 x) (proj1 y) (proj1 z) } - ... = (pair (proj1 x * (proj1 y * proj1 z)) (proj2 x * (proj2 y * proj2 z)) : S) : { G_assoc (proj2 x) (proj2 y) (proj2 z) } - ... = f x (f y z) : refl (f x (f y z)), - have id : is_identity f o, - from take x : S, - calc f x o = (pair (proj1 x * one) (proj2 x * one) : S) : refl (f x o) - ... = (pair (proj1 x) (proj2 x * one) : S) : { G_id (proj1 x) } - ... = (pair (proj1 x) (proj2 x) : S) : { G_id (proj2 x) } - ... = x : pair_proj_eq x, - have inv : inverse_ex f o, - from take x : S, - obtain (y1 : carrier g1) (Hy1 : proj1 x * y1 = one), from G_inv (proj1 x), - obtain (y2 : carrier g2) (Hy2 : proj2 x * y2 = one), from G_inv (proj2 x), - show ∃ y, f x y = o, - from exists_intro (pair y1 y2 : S) - (calc f x (pair y1 y2 : S) = (pair (proj1 x * y1) (proj2 x * y2) : S) : refl (f x (pair y1 y2 : S)) - ... = (pair one (proj2 x * y2) : S) : { Hy1 } - ... = (pair one one : S) : { Hy2 } - ... = o : refl o), - to_group S f o assoc id inv - -set_opaque product true - --- It would be nice to be able to write x.first and x.second instead of (proj1 x) and (proj2 x) - --- Remark: * is overloaded since Lean loads Nat.lean by default. --- The type errors related to * are quite cryptic because of that - --- Use 'star' for creating products -infixr 50 ⋆ : product - --- It would be nice to be able to write (p1 p2 : g1 ⋆ g2 ⋆ g3) -check λ (g1 g2 g3 : group) (p1 p2 : carrier (g1 ⋆ g2 ⋆ g3)), p1 * p2 = p2 * p1 - -theorem group_inhab (g : group) : inhabited (carrier g) -:= inhabited_intro (@one g) - -definition inv {g : group} (a : carrier g) : carrier g -:= ε (group_inhab g) (λ x : carrier g, a * x = one) - -theorem G_idl {g : group} (x : carrier g) : x * one = x -:= G_id x - -theorem G_invl {g : group} (x : carrier g) : x * inv x = one -:= obtain (y : carrier g) (Hy : x * y = one), from G_inv x, - eps_ax (group_inhab g) y Hy -set_opaque inv true - -theorem G_inv_aux {g : group} (x : carrier g) : inv x = (inv x * x) * inv x -:= symm (calc (inv x * x) * inv x = inv x * (x * inv x) : G_assoc (inv x) x (inv x) - ... = inv x * one : { G_invl x } - ... = inv x : G_idl (inv x)) - -theorem G_invr {g : group} (x : carrier g) : inv x * x = one -:= calc inv x * x = (inv x * x) * one : symm (G_idl (inv x * x)) - ... = (inv x * x) * (inv x * inv (inv x)) : { symm (G_invl (inv x)) } - ... = ((inv x * x) * inv x) * inv (inv x) : symm (G_assoc (inv x * x) (inv x) (inv (inv x))) - ... = (inv x * (x * inv x)) * inv (inv x) : { G_assoc (inv x) x (inv x) } - ... = (inv x * one) * inv (inv x) : { G_invl x } - ... = (inv x) * inv (inv x) : { G_idl (inv x) } - ... = one : G_invl (inv x) - -theorem G_idr {g : group} (x : carrier g) : one * x = x -:= calc one * x = (x * inv x) * x : { symm (G_invl x) } - ... = x * (inv x * x) : G_assoc x (inv x) x - ... = x * one : { G_invr x } - ... = x : G_idl x - -theorem G_inv_inv {g : group} (x : carrier g) : inv (inv x) = x -:= calc inv (inv x) = inv (inv x) * one : symm (G_idl (inv (inv x))) - ... = inv (inv x) * (inv x * x) : { symm (G_invr x) } - ... = (inv (inv x) * inv x) * x : symm (G_assoc (inv (inv x)) (inv x) x) - ... = one * x : { G_invr (inv x) } - ... = x : G_idr x - - -definition commutative {A : (Type U)} (f : A → A → A) := ∀ x y, f x y = f y x - -definition abelian_group := sig g : group, commutative (@G_mul g) -definition ab_to_g (ag : abelian_group) : group -:= proj1 ag --- Coercions currently only work with opaque types --- We must first define "extract" the information we want, and then --- mark abelian_group as opaque -definition AG_comm {g : abelian_group} (x y : carrier (ab_to_g g)) : x * y = y * x -:= (proj2 g) x y - -set_opaque abelian_group true -set_opaque ab_to_g true -set_opaque AG_comm true - -coercion ab_to_g --- Now, we can use abelian groups where groups are expected. - -theorem AG_left_comm {g : abelian_group} (x y z : carrier g) : x * (y * z) = y * (x * z) -:= calc x * (y * z) = (x * y) * z : symm (G_assoc x y z) - ... = (y * x) * z : { AG_comm x y } - ... = y * (x * z) : G_assoc y x z - - - - diff --git a/examples/lean/alg.lean b/examples/lean/alg.lean deleted file mode 100644 index 9cf80db18..000000000 --- a/examples/lean/alg.lean +++ /dev/null @@ -1,83 +0,0 @@ -import macros - -definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z) -definition commutative {A : (Type U)} (f : A → A → A) := ∀ x y, f x y = f y x -definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x -definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id - -definition struct := Type -definition carrier (s : struct) := s - -definition mul_struct -:= sig s : struct, carrier s → carrier s → carrier s - -definition mul_to_s (m : mul_struct) : struct := proj1 m -coercion mul_to_s - -definition mul {m : mul_struct} : carrier m → carrier m → carrier m -:= proj2 m - -infixl 70 * : mul - -definition semi_group -:= sig m : mul_struct, associative (@mul m) - -definition sg_to_mul (sg : semi_group) : mul_struct := proj1 sg -definition sg_to_s (sg : semi_group) : struct := mul_to_s (sg_to_mul sg) -coercion sg_to_s -coercion sg_to_mul - -theorem sg_assoc {m : semi_group} (x y z : carrier m) : (x * y) * z = x * (y * z) -:= proj2 m x y z - -definition monoid -:= sig sg : semi_group, sig id : carrier sg, is_identity (@mul sg) id - -definition monoid_to_sg (m : monoid) : semi_group := proj1 m -definition monoid_to_mul (m : monoid) : mul_struct := sg_to_mul (monoid_to_sg m) -definition monoid_to_s (m : monoid) : struct := mul_to_s (monoid_to_mul m) -coercion monoid_to_sg -coercion monoid_to_mul -coercion monoid_to_s - -definition one {m : monoid} : carrier m -:= proj1 (proj2 m) -theorem monoid_id {m : monoid} (x : carrier m) : x * one = x -:= proj2 (proj2 m) x - -definition group -:= sig m : monoid, inverse_ex (@mul m) (@one m) - -definition group_to_monoid (g : group) : monoid := proj1 g -definition group_to_sg (g : group) : semi_group := monoid_to_sg (group_to_monoid g) -definition group_to_mul (g : group) : mul_struct := sg_to_mul (group_to_sg g) -definition group_to_s (g : group) : struct := mul_to_s (group_to_mul g) -coercion group_to_monoid -coercion group_to_sg -coercion group_to_mul -coercion group_to_s - -theorem group_inv {g : group} (x : carrier g) : ∃ y, x * y = one -:= proj2 g x - -definition abelian_group -:= sig g : group, commutative (@mul g) - -definition abelian_to_group (ag : abelian_group) : group := proj1 ag -definition abelian_to_monoid (ag : abelian_group) : monoid := group_to_monoid (abelian_to_group ag) -definition abelian_to_sg (ag : abelian_group) : semi_group := monoid_to_sg (abelian_to_monoid ag) -definition abelian_to_mul (ag : abelian_group) : mul_struct := sg_to_mul (abelian_to_sg ag) -definition abelian_to_s (ag : abelian_group) : struct := mul_to_s (abelian_to_mul ag) -coercion abelian_to_group -coercion abelian_to_monoid -coercion abelian_to_sg -coercion abelian_to_mul -coercion abelian_to_s - -theorem abelian_comm {ag : abelian_group} (x y : carrier ag) : x * y = y * x -:= proj2 ag x y - -theorem abelian_left_comm {ag : abelian_group} (x y z : carrier ag) : x * (y * z) = y * (x * z) -:= calc x * (y * z) = (x * y) * z : symm (sg_assoc x y z) - ... = (y * x) * z : { abelian_comm x y } - ... = y * (x * z) : sg_assoc y x z diff --git a/examples/lean/dep_if.lean b/examples/lean/dep_if.lean deleted file mode 100644 index d01d9445d..000000000 --- a/examples/lean/dep_if.lean +++ /dev/null @@ -1,99 +0,0 @@ -import macros -import tactic - --- "Dependent" if-then-else (dep_if c t e) --- The then-branch t gets a proof for c, and the else-branch e gets a proof for ¬ c --- We also prove that --- 1) given H : c, (dep_if c t e) = t H --- 2) given H : ¬ c, (dep_if c t e) = e H - --- We define the "dependent" if-then-else using Hilbert's choice operator ε. --- Note that ε is only applicable to non-empty types. Thus, we first --- prove the following auxiliary theorem. -theorem inhabited_resolve {A : (Type U)} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A -:= or_elim (em c) - (λ Hc, inhabited_range (inhabited_intro t) Hc) - (λ Hnc, inhabited_range (inhabited_intro e) Hnc) - --- The actual definition -definition dep_if {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) : A -:= ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) - -theorem then_simp (A : (Type U)) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c) - : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H -:= let s1 : (∀ Hc : c, r = t Hc) ↔ r = t H - := iff_intro - (assume Hl : (∀ Hc : c, r = t Hc), - Hl H) - (assume Hr : r = t H, - λ Hc : c, subst Hr (proof_irrel H Hc)), - s2 : (∀ Hnc : ¬ c, r = e Hnc) ↔ true - := eqt_intro (λ Hnc : ¬ c, absurd_elim (r = e Hnc) H Hnc) - in by simp - --- Given H : c, (dep_if c t e) = t H -theorem dep_if_elim_then {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c) : dep_if c t e = t H -:= let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = t H) - := funext (λ r, then_simp A c r t e H) - in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) - ... = ε (inhabited_resolve t e) (λ r, r = t H) : { s1 } - ... = t H : eps_singleton (inhabited_resolve t e) (t H) - -theorem dep_if_true {A : (Type U)} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial -:= dep_if_elim_then true t e trivial - -theorem else_simp (A : (Type U)) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : ¬ c) - : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H -:= let s1 : (∀ Hc : c, r = t Hc) ↔ true - := eqt_intro (λ Hc : c, absurd_elim (r = t Hc) Hc H), - s2 : (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H - := iff_intro - (assume Hl : (∀ Hnc : ¬ c, r = e Hnc), - Hl H) - (assume Hr : r = e H, - λ Hnc : ¬ c, subst Hr (proof_irrel H Hnc)) - in by simp - --- Given H : ¬ c, (dep_if c t e) = e H -theorem dep_if_elim_else {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H -:= let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = e H) - := funext (λ r, else_simp A c r t e H) - in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) - ... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 } - ... = e H : eps_singleton (inhabited_resolve t e) (e H) - -theorem dep_if_false {A : (Type U)} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial -:= dep_if_elim_else false t e not_false_trivial - -set_option simplifier::heq true -- enable heterogeneous equality support - -universe M >= 1 - -theorem dep_if_congr {A : (Type M)} (c1 c2 : Bool) - (t1 : c1 → A) (t2 : c2 → A) - (e1 : ¬ c1 → A) (e2 : ¬ c2 → A) - (Hc : c1 = c2) - (Ht : t1 = cast (by simp) t2) - (He : e1 = cast (by simp) e2) - : dep_if c1 t1 e1 = dep_if c2 t2 e2 -:= by simp - -scope - -- Here is an example where dep_if is useful - -- Suppose we have a (div s t H) where H is a proof for t ≠ 0 - variable div (s : Nat) (t : Nat) (H : t ≠ 0) : Nat - -- Now, we want to define a function that - -- returns 0 if x = 0 - -- and div 10 x _ otherwise - -- We can't use the standard if-the-else, because we don't have a way to synthesize the proof for x ≠ 0 - check λ x, dep_if (x = 0) (λ H, 0) (λ H : ¬ x = 0, div 10 x H) -pop_scope - --- If the dependent then/else branches do not use the proofs Hc : c and Hn : ¬ c, then we --- can reduce the dependent-if to a regular if -theorem dep_if_if {A : (Type U)} (c : Bool) (t e : A) : dep_if c (λ Hc, t) (λ Hn, e) = if c then t else e -:= or_elim (em c) - (assume Hc : c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hc, t) Hc : dep_if_elim_then _ _ _ Hc - ... = if c then t else e : by simp) - (assume Hn : ¬ c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hn, e) Hn : dep_if_elim_else _ _ _ Hn - ... = if c then t else e : by simp) diff --git a/examples/lean/even.lean b/examples/lean/even.lean deleted file mode 100644 index 15081fa68..000000000 --- a/examples/lean/even.lean +++ /dev/null @@ -1,72 +0,0 @@ -import macros -using Nat - --- In this example, we prove two simple theorems about even/odd numbers. --- First, we define the predicates even and odd. -definition even (a : Nat) := ∃ b, a = 2*b -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 --- --- It is syntax sugar for existential elimination. --- It expands to --- --- 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 --- 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. --- --- We use a calculational proof 'calc' expression to derive --- 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, - exists_intro (w1 + w2) - (calc a + b = 2*w1 + b : { Hw1 } - ... = 2*w1 + 2*w2 : { Hw2 } - ... = 2*(w1 + w2) : symm (distributer 2 w1 w2)) - --- In the following example, we omit the arguments for add_assoc, refl and distribute. --- Lean can infer them automatically. --- --- refl is the reflexivity proof. (refl a) is a proof that two --- definitionally equal terms are indeed equal. --- "definitionally equal" means that they have the same normal form. --- We can also view it as "Proof by computation". --- The normal form of (1+1), and 2*1 is 2. --- --- Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'. --- The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since + --- 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, - exists_intro (w + 1) - (calc a + 1 = 2*w + 1 + 1 : { Hw } - ... = 2*w + (1 + 1) : add_assoc _ _ _ - ... = 2*w + 2*1 : refl _ - ... = 2*(w + 1) : symm (distributer _ _ _)) - --- The following command displays the proof object produced by Lean after --- expanding macros, and infering implicit/missing arguments. -print environment 2 - --- By default, Lean does not display implicit arguments. --- The following command will force it to display them. -set_option pp::implicit true - -print environment 2 - --- As an exercise, prove that the sum of two odd numbers is even, --- and other similar theorems. diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean deleted file mode 100644 index cb1b66123..000000000 --- a/examples/lean/ex1.lean +++ /dev/null @@ -1,35 +0,0 @@ -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 - --- Declare some variables -variable a : N -variable b : N -variable c : N -variable d : N -variable e : N - --- Add axioms stating facts about these variables -axiom H1 : (a = b ∧ b = c) ∨ (d = c ∧ a = d) -axiom H2 : b = e - --- Proof that (h a b) = (h c e) -theorem T1 : (h a b) = (h c e) := - or_elim H1 - (λ C1, congrh (trans (and_eliml C1) (and_elimr C1)) H2) - (λ C2, congrh (trans (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 - --- Display the last two objects (i.e., theorems) added to the environment -print environment 2 - --- print implicit arguments -set_option lean::pp::implicit true -set_option pp::width 150 -print environment 2 diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean deleted file mode 100644 index 8ab3b057e..000000000 --- a/examples/lean/ex2.lean +++ /dev/null @@ -1,16 +0,0 @@ -import macros. - -theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r -:= 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) - -set_option 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, - (H_abc H_a) (H_ab H_a) - -print environment 1. diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean deleted file mode 100644 index 0f0825c07..000000000 --- a/examples/lean/ex3.lean +++ /dev/null @@ -1,28 +0,0 @@ -import macros. - -theorem my_and_comm (a b : Bool) : (a ∧ b) → (b ∧ a) -:= assume H_ab, and_intro (and_elimr H_ab) (and_eliml H_ab). - -theorem my_or_comm (a b : Bool) : (a ∨ b) → (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 --- H : (a → b) → a) --- H_na : ¬a --- produces --- ¬(a → b) --- --- not_imp_eliml applied to --- (MT H H_na) : ¬(a → b) --- produces --- a -theorem pierce (a b : Bool) : ((a → b) → a) → a -:= 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 deleted file mode 100644 index adc9f50e3..000000000 --- a/examples/lean/ex4.lean +++ /dev/null @@ -1,5 +0,0 @@ -import Int -import tactic -set_option simplifier::unfold true -- allow the simplifier to unfold definitions -definition a : Nat := 10 -theorem T1 : a > 0 := (by simp) diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean deleted file mode 100644 index 17822db67..000000000 --- a/examples/lean/ex5.lean +++ /dev/null @@ -1,34 +0,0 @@ -import macros - -scope - theorem ReflIf (A : Type) - (R : A → A → Bool) - (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 := - 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 - -pop_scope - -scope - -- Same example again. - variable A : Type - variable R : A → A → Bool - 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 := - obtain (w : A) (H : R x w), from (Linked x), - let L1 : R w x := Symm H - in Trans H L1 - -end - --- Display the last two theorems -print environment 2 \ No newline at end of file diff --git a/examples/lean/group.lean b/examples/lean/group.lean deleted file mode 100644 index b113cec92..000000000 --- a/examples/lean/group.lean +++ /dev/null @@ -1,111 +0,0 @@ -import macros - -definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z) -definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x -definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id - -universe s ≥ 1 - -definition group := sig A : (Type s), sig mul : A → A → A, sig one : A, (associative mul) # (is_identity mul one) # (inverse_ex mul one) -definition to_group (A : (Type s)) (mul : A → A → A) (one : A) (H1 : associative mul) (H2 : is_identity mul one) (H3 : inverse_ex mul one) : group -:= pair A (pair mul (pair one (pair H1 (pair H2 H3)))) - --- The following definitions can be generated automatically. -definition carrier (g : group) := proj1 g -definition G_mul {g : group} : carrier g → carrier g → carrier g -:= proj1 (proj2 g) -infixl 70 * : G_mul -definition one {g : group} : carrier g -:= proj1 (proj2 (proj2 g)) -theorem G_assoc {g : group} (x y z : carrier g) : (x * y) * z = x * (y * z) -:= (proj1 (proj2 (proj2 (proj2 g)))) x y z -theorem G_id {g : group} (x : carrier g) : x * one = x -:= (proj1 (proj2 (proj2 (proj2 (proj2 g))))) x -theorem G_inv {g : group} (x : carrier g) : ∃ y, x * y = one -:= (proj2 (proj2 (proj2 (proj2 (proj2 g))))) x - --- First example: the pairwise product of two groups is a group -definition product (g1 g2 : group) : group -:= let S := carrier g1 # carrier g2, - -- It would be nice to be able to define local notation, and write _*_ instead of f - f := λ x y, pair (proj1 x * proj1 y) (proj2 x * proj2 y), - o := pair one one -- this is actually (pair (@one g1) (@one g2)) - in have assoc : associative f, - -- The elaborator failed to infer the type of the pairs. - -- I had to annotate the pairs with their types. - from take x y z : S, -- We don't really need to provide S, but it will make the elaborator to work much harder - -- since * is an overloaded operator, we also have * as notation for Nat::mul in the context. - calc f (f x y) z = (pair ((proj1 x * proj1 y) * proj1 z) ((proj2 x * proj2 y) * proj2 z) : S) : refl (f (f x y) z) - ... = (pair (proj1 x * (proj1 y * proj1 z)) ((proj2 x * proj2 y) * proj2 z) : S) : { G_assoc (proj1 x) (proj1 y) (proj1 z) } - ... = (pair (proj1 x * (proj1 y * proj1 z)) (proj2 x * (proj2 y * proj2 z)) : S) : { G_assoc (proj2 x) (proj2 y) (proj2 z) } - ... = f x (f y z) : refl (f x (f y z)), - have id : is_identity f o, - from take x : S, - calc f x o = (pair (proj1 x * one) (proj2 x * one) : S) : refl (f x o) - ... = (pair (proj1 x) (proj2 x * one) : S) : { G_id (proj1 x) } - ... = (pair (proj1 x) (proj2 x) : S) : { G_id (proj2 x) } - ... = x : pair_proj_eq x, - have inv : inverse_ex f o, - from take x : S, - obtain (y1 : carrier g1) (Hy1 : proj1 x * y1 = one), from G_inv (proj1 x), - obtain (y2 : carrier g2) (Hy2 : proj2 x * y2 = one), from G_inv (proj2 x), - show ∃ y, f x y = o, - from exists_intro (pair y1 y2 : S) - (calc f x (pair y1 y2 : S) = (pair (proj1 x * y1) (proj2 x * y2) : S) : refl (f x (pair y1 y2 : S)) - ... = (pair one (proj2 x * y2) : S) : { Hy1 } - ... = (pair one one : S) : { Hy2 } - ... = o : refl o), - to_group S f o assoc id inv - --- It would be nice to be able to write x.first and x.second instead of (proj1 x) and (proj2 x) - --- Remark: * is overloaded since Lean loads Nat.lean by default. --- The type errors related to * are quite cryptic because of that - --- Use 'star' for creating products -infixr 50 ⋆ : product - --- It would be nice to be able to write (p1 p2 : g1 ⋆ g2 ⋆ g3) -check λ (g1 g2 g3 : group) (p1 p2 : carrier (g1 ⋆ g2 ⋆ g3)), p1 * p2 = p2 * p1 - -theorem group_inhab (g : group) : inhabited (carrier g) -:= inhabited_intro (@one g) - -definition inv {g : group} (a : carrier g) : carrier g -:= ε (group_inhab g) (λ x : carrier g, a * x = one) - -theorem G_idl {g : group} (x : carrier g) : x * one = x -:= G_id x - -theorem G_invl {g : group} (x : carrier g) : x * inv x = one -:= obtain (y : carrier g) (Hy : x * y = one), from G_inv x, - eps_ax (group_inhab g) y Hy - -theorem G_inv_aux {g : group} (x : carrier g) : inv x = (inv x * x) * inv x -:= symm (calc (inv x * x) * inv x = inv x * (x * inv x) : G_assoc (inv x) x (inv x) - ... = inv x * one : { G_invl x } - ... = inv x : G_idl (inv x)) - -theorem G_invr {g : group} (x : carrier g) : inv x * x = one -:= calc inv x * x = (inv x * x) * one : symm (G_idl (inv x * x)) - ... = (inv x * x) * (inv x * inv (inv x)) : { symm (G_invl (inv x)) } - ... = ((inv x * x) * inv x) * inv (inv x) : symm (G_assoc (inv x * x) (inv x) (inv (inv x))) - ... = (inv x * (x * inv x)) * inv (inv x) : { G_assoc (inv x) x (inv x) } - ... = (inv x * one) * inv (inv x) : { G_invl x } - ... = (inv x) * inv (inv x) : { G_idl (inv x) } - ... = one : G_invl (inv x) - -theorem G_idr {g : group} (x : carrier g) : one * x = x -:= calc one * x = (x * inv x) * x : { symm (G_invl x) } - ... = x * (inv x * x) : G_assoc x (inv x) x - ... = x * one : { G_invr x } - ... = x : G_idl x - -theorem G_inv_inv {g : group} (x : carrier g) : inv (inv x) = x -:= calc inv (inv x) = inv (inv x) * one : symm (G_idl (inv (inv x))) - ... = inv (inv x) * (inv x * x) : { symm (G_invr x) } - ... = (inv (inv x) * inv x) * x : symm (G_assoc (inv (inv x)) (inv x) x) - ... = one * x : { G_invr (inv x) } - ... = x : G_idr x - - diff --git a/examples/lean/opaque_pairs.lean b/examples/lean/opaque_pairs.lean deleted file mode 100644 index 485a82991..000000000 --- a/examples/lean/opaque_pairs.lean +++ /dev/null @@ -1,106 +0,0 @@ -import macros tactic -variable Sigma {A : (Type 1)} (B : A → (Type 1)) : (Type 1) -variable Pair {A : (Type 1)} {B : A → (Type 1)} (a : A) (b : B a) : Sigma B -variable Fst {A : (Type 1)} {B : A → (Type 1)} (p : Sigma B) : A -variable Snd {A : (Type 1)} {B : A → (Type 1)} (p : Sigma B) : B (Fst p) -axiom FstAx {A : (Type 1)} {B : A → (Type 1)} (a : A) (b : B a) : @Fst A B (Pair a b) = a -axiom SndAx {A : (Type 1)} {B : A → (Type 1)} (a : A) (b : B a) : @Snd A B (Pair a b) == b - -scope --- Remark: A1 a1 A2 a2 A3 a3 A3 a4 are parameters for the definitions and theorems in this scope. -variable A1 : (Type 1) -variable a1 : A1 -variable A2 : A1 → (Type 1) -variable a2 : A2 a1 -variable A3 : ∀ a1 : A1, A2 a1 → (Type 1) -variable a3 : A3 a1 a2 -variable A4 : ∀ (a1 : A1) (a2 : A2 a1), A3 a1 a2 → (Type 1) -variable a4 : A4 a1 a2 a3 --- Pair type parameterized by a1 and a2 -definition A1A2_tuple_ty (a1 : A1) (a2 : A2 a1) : (Type 1) -:= @Sigma (A3 a1 a2) (A4 a1 a2) --- Pair a3 a4 -definition tuple_34 : A1A2_tuple_ty a1 a2 -:= @Pair (A3 a1 a2) (A4 a1 a2) a3 a4 --- Triple type parameterized by a1 a2 a3 -definition A1_tuple_ty (a1 : A1) : (Type 1) -:= @Sigma (A2 a1) (A1A2_tuple_ty a1) --- Triple a2 a3 a4 -definition tuple_234 : A1_tuple_ty a1 -:= @Pair (A2 a1) (A1A2_tuple_ty a1) a2 tuple_34 --- Quadruple type -definition tuple_ty : (Type 1) -:= @Sigma A1 A1_tuple_ty --- Quadruple a1 a2 a3 a4 -definition tuple_1234 : tuple_ty -:= @Pair A1 A1_tuple_ty a1 tuple_234 --- First element of the quadruple -definition f_1234 : A1 -:= @Fst A1 A1_tuple_ty tuple_1234 --- Rest of the quadruple (i.e., a triple) -definition s_1234 : A1_tuple_ty f_1234 -:= @Snd A1 A1_tuple_ty tuple_1234 -theorem H_eq_a1 : f_1234 = a1 -:= @FstAx A1 A1_tuple_ty a1 tuple_234 -theorem H_eq_triple : s_1234 == tuple_234 -:= @SndAx A1 A1_tuple_ty a1 tuple_234 --- Second element of the quadruple -definition fs_1234 : A2 f_1234 -:= @Fst (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234 --- Rest of the triple (i.e., a pair) -definition ss_1234 : A1A2_tuple_ty f_1234 fs_1234 -:= @Snd (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234 -theorem H_eq_a2 : fs_1234 == a2 -:= have H1 : @Fst (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234 == @Fst (A2 a1) (A1A2_tuple_ty a1) tuple_234, - from hcongr (hcongr (hrefl (λ x, @Fst (A2 x) (A1A2_tuple_ty x))) (to_heq H_eq_a1)) H_eq_triple, - have H2 : @Fst (A2 a1) (A1A2_tuple_ty a1) tuple_234 = a2, - from FstAx _ _, - htrans H1 (to_heq H2) -theorem H_eq_pair : ss_1234 == tuple_34 -:= have H1 : @Snd (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234 == @Snd (A2 a1) (A1A2_tuple_ty a1) tuple_234, - from hcongr (hcongr (hrefl (λ x, @Snd (A2 x) (A1A2_tuple_ty x))) (to_heq H_eq_a1)) H_eq_triple, - have H2 : @Snd (A2 a1) (A1A2_tuple_ty a1) tuple_234 == tuple_34, - from SndAx _ _, - htrans H1 H2 --- Third element of the quadruple -definition fss_1234 : A3 f_1234 fs_1234 -:= @Fst (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234 --- Fourth element of the quadruple -definition sss_1234 : A4 f_1234 fs_1234 fss_1234 -:= @Snd (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234 -theorem H_eq_a3 : fss_1234 == a3 -:= have H1 : @Fst (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234 == @Fst (A3 a1 a2) (A4 a1 a2) tuple_34, - from hcongr (hcongr (hcongr (hrefl (λ x y z, @Fst (A3 x y) (A4 x y) z)) (to_heq H_eq_a1)) H_eq_a2) H_eq_pair, - have H2 : @Fst (A3 a1 a2) (A4 a1 a2) tuple_34 = a3, - from FstAx _ _, - htrans H1 (to_heq H2) -theorem H_eq_a4 : sss_1234 == a4 -:= have H1 : @Snd (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234 == @Snd (A3 a1 a2) (A4 a1 a2) tuple_34, - from hcongr (hcongr (hcongr (hrefl (λ x y z, @Snd (A3 x y) (A4 x y) z)) (to_heq H_eq_a1)) H_eq_a2) H_eq_pair, - have H2 : @Snd (A3 a1 a2) (A4 a1 a2) tuple_34 == a4, - from SndAx _ _, - htrans H1 H2 -eval tuple_1234 -eval f_1234 -eval fs_1234 -eval fss_1234 -eval sss_1234 -check H_eq_a1 -check H_eq_a2 -check H_eq_a3 -check H_eq_a4 -theorem f_quadruple : Fst (Pair a1 (Pair a2 (Pair a3 a4))) = a1 -:= H_eq_a1 -theorem fs_quadruple : Fst (Snd (Pair a1 (Pair a2 (Pair a3 a4)))) == a2 -:= H_eq_a2 -theorem fss_quadruple : Fst (Snd (Snd (Pair a1 (Pair a2 (Pair a3 a4))))) == a3 -:= H_eq_a3 -theorem sss_quadruple : Snd (Snd (Snd (Pair a1 (Pair a2 (Pair a3 a4))))) == a4 -:= H_eq_a4 -end --- Show the theorems with their parameters -check f_quadruple -check fs_quadruple -check fss_quadruple -check sss_quadruple -exit diff --git a/examples/lean/primes.lean b/examples/lean/primes.lean deleted file mode 100644 index 167800157..000000000 --- a/examples/lean/primes.lean +++ /dev/null @@ -1,542 +0,0 @@ ----------------------------------------------------------------------------------------------------- --- --- theory primes.lean --- author: Jeremy Avigad --- --- Experimenting with Lean. --- ----------------------------------------------------------------------------------------------------- - -import macros -import tactic -using Nat - --- --- fundamental properties of Nat --- - -theorem cases_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat), P (n + 1)) : P a -:= induction_on a H1 (take n : Nat, assume ih : P n, H2 n) - -theorem strong_induction_on {P : Nat → Bool} (a : Nat) (H : ∀ n, (∀ m, m < n → P m) → P n) : P a -:= @strong_induction P H a - --- in hindsight, now I know I don't need these -theorem one_ne_zero : 1 ≠ 0 := succ_nz 0 -theorem two_ne_zero : 2 ≠ 0 := succ_nz 1 - --- --- observation: the proof of lt_le_trans in Nat is not needed --- - -theorem lt_le_trans2 {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c -:= le_trans H1 H2 - --- --- also, contrapos and mt are the same theorem --- - -theorem contrapos2 {a b : Bool} (H : a → b) : ¬ b → ¬ a -:= mt H - --- --- properties of lt and le --- - -theorem succ_le_succ {a b : Nat} (H : a + 1 ≤ b + 1) : a ≤ b -:= - obtain (x : Nat) (Hx : a + 1 + x = b + 1), from lt_elim H, - have H2 : a + x + 1 = b + 1, from (calc - a + x + 1 = a + (x + 1) : add_assoc _ _ _ - ... = a + (1 + x) : { add_comm x 1 } - ... = a + 1 + x : symm (add_assoc _ _ _) - ... = b + 1 : Hx), - have H3 : a + x = b, from (succ_inj H2), - show a ≤ b, from (le_intro H3) - --- should we keep this duplication or < and <=? -theorem lt_succ {a b : Nat} (H : a < b + 1) : a ≤ b -:= succ_le_succ H - -theorem succ_le_succ_eq (a b : Nat) : a + 1 ≤ b + 1 ↔ a ≤ b -:= iff_intro succ_le_succ (assume H : a ≤ b, le_add H 1) - -theorem lt_succ_eq (a b : Nat) : a < b + 1 ↔ a ≤ b -:= succ_le_succ_eq a b - -theorem le_or_lt (a : Nat) : ∀ b : Nat, a ≤ b ∨ b < a -:= - induction_on a ( - show ∀b, 0 ≤ b ∨ b < 0, - from take b, or_introl (le_zero b) _ - ) ( - take a, - assume ih : ∀b, a ≤ b ∨ b < a, - show ∀b, a + 1 ≤ b ∨ b < a + 1, - from - take b, - cases_on b ( - show a + 1 ≤ 0 ∨ 0 < a + 1, - from or_intror _ (le_add (le_zero a) 1) - ) ( - take b, - have H : a ≤ b ∨ b < a, from ih b, - show a + 1 ≤ b + 1 ∨ b + 1 < a + 1, - from or_elim H ( - assume H1 : a ≤ b, - or_introl (le_add H1 1) (b + 1 < a + 1) - ) ( - assume H2 : b < a, - or_intror (a + 1 ≤ b + 1) (le_add H2 1) - ) - ) - ) - -theorem not_le_lt {a b : Nat} : ¬ a ≤ b → b < a -:= (or_imp _ _) ◂ le_or_lt a b - -theorem not_lt_le {a b : Nat} : ¬ a < b → b ≤ a -:= (or_imp _ _) ◂ (or_comm _ _ ◂ le_or_lt b a) - -theorem lt_not_le {a b : Nat} (H : a < b) : ¬ b ≤ a -:= not_intro (take H1 : b ≤ a, absurd (lt_le_trans H H1) (lt_nrefl a)) - -theorem le_not_lt {a b : Nat} (H : a ≤ b) : ¬ b < a -:= not_intro (take H1 : b < a, absurd H (lt_not_le H1)) - -theorem not_le_iff {a b : Nat} : ¬ a ≤ b ↔ b < a -:= iff_intro (@not_le_lt a b) (@lt_not_le b a) - -theorem not_lt_iff {a b : Nat} : ¬ a < b ↔ b ≤ a -:= iff_intro (@not_lt_le a b) (@le_not_lt b a) - -theorem le_iff {a b : Nat} : a ≤ b ↔ a < b ∨ a = b -:= - iff_intro ( - assume H : a ≤ b, - show a < b ∨ a = b, - from or_elim (em (a = b)) ( - take H1 : a = b, - show a < b ∨ a = b, from or_intror _ H1 - ) ( - take H2 : a ≠ b, - have H3 : ¬ b ≤ a, - from not_intro (take H4: b ≤ a, absurd (le_antisym H H4) H2), - have H4 : a < b, from resolve1 (le_or_lt b a) H3, - show a < b ∨ a = b, from or_introl H4 _ - ) - )( - assume H : a < b ∨ a = b, - show a ≤ b, - from or_elim H ( - take H1 : a < b, lt_le H1 - ) ( - take H1 : a = b, subst (le_refl a) H1 - ) - ) - -theorem ne_symm_iff {A : (Type U)} (a b : A) : a ≠ b ↔ b ≠ a -:= iff_intro ne_symm ne_symm - -theorem lt_iff (a b : Nat) : a < b ↔ a ≤ b ∧ a ≠ b -:= - calc - a < b = ¬ b ≤ a : symm (not_le_iff) - ... = ¬ (b < a ∨ b = a) : { le_iff } - ... = ¬ b < a ∧ b ≠ a : not_or _ _ - ... = a ≤ b ∧ b ≠ a : { not_lt_iff } - ... = a ≤ b ∧ a ≠ b : { ne_symm_iff _ _ } - -theorem ne_zero_ge_one {x : Nat} (H : x ≠ 0) : x ≥ 1 -:= resolve2 (le_iff ◂ (le_zero x)) (ne_symm H) - -theorem ne_zero_one_ge_two {x : Nat} (H0 : x ≠ 0) (H1 : x ≠ 1) : x ≥ 2 -:= resolve2 (le_iff ◂ (ne_zero_ge_one H0)) (ne_symm H1) - --- the forward direction can be replaced by ne_zero_ge_one, but --- note the comments below -theorem ne_zero_iff (n : Nat) : n ≠ 0 ↔ n > 0 -:= - iff_intro ( - assume H : n ≠ 0, - by_contradiction ( - assume H1 : ¬ n > 0, - -- curious: if you make the arguments implicit in the next line, - -- it fails (the evaluator is getting in the way, I think) - have H2 : n = 0, from le_antisym (@not_lt_le 0 n H1) (le_zero n), - absurd H2 H - ) - ) ( - -- here too - assume H : n > 0, ne_symm (@lt_ne 0 n H) - ) - --- Note: this differs from Leo's naming conventions -theorem mul_right_mono {x y : Nat} (H : x ≤ y) (z : Nat) : x * z ≤ y * z -:= - obtain (w : Nat) (Hw : x + w = y), - from le_elim H, - le_intro ( - show x * z + w * z = y * z, - from calc - x * z + w * z = (x + w) * z : symm (distributel x w z) - ... = y * z : { Hw } - ) - -theorem mul_left_mono (x : Nat) {y z : Nat} (H : y ≤ z) : x * y ≤ x * z -:= subst (subst (mul_right_mono H x) (mul_comm y x)) (mul_comm z x) - -theorem le_addr (a b : Nat) : a ≤ a + b -:= le_intro (refl (a + b)) - -theorem le_addl (a b : Nat) : a ≤ b + a -:= subst (le_addr a b) (add_comm a b) - -theorem add_left_mono {a b : Nat} (c : Nat) (H : a ≤ b) : c + a ≤ c + b -:= subst (subst (le_add H c) (add_comm a c)) (add_comm b c) - -theorem mul_right_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : x * z < y * z -:= - obtain (w : Nat) (Hw : x + 1 + w = y), - from le_elim H, - have H1 : y * z = x * z + w * z + z, - from calc - y * z = (x + 1 + w) * z : { symm Hw } - ... = (x + (1 + w)) * z : { add_assoc _ _ _ } - ... = (x + (w + 1)) * z : { add_comm _ _ } - ... = (x + w + 1) * z : { symm (add_assoc _ _ _) } - ... = (x + w) * z + 1 * z : distributel _ _ _ - ... = (x + w) * z + z : { mul_onel _ } - ... = x * z + w * z + z : { distributel _ _ _ }, - have H2 : x * z ≤ x * z + w * z, from le_addr _ _, - have H3 : x * z + w * z < x * z + w * z + z, from add_left_mono _ (ne_zero_ge_one znez), - show x * z < y * z, from subst (le_lt_trans H2 H3) (symm H1) - -theorem mul_left_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : z * x < z * y -:= subst (subst (mul_right_strict_mono H znez) (mul_comm x z)) (mul_comm y z) - -theorem mul_left_le_cancel {a b c : Nat} (H : a * b ≤ a * c) (anez : a ≠ 0) : b ≤ c -:= - by_contradiction ( - assume H1 : ¬ b ≤ c, - have H2 : a * c < a * b, from mul_left_strict_mono (not_le_lt H1) anez, - show false, from absurd H (lt_not_le H2) - ) - -theorem mul_right_le_cancel {a b c : Nat} (H : b * a ≤ c * a) (anez : a ≠ 0) : b ≤ c -:= mul_left_le_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez - -theorem mul_left_lt_cancel {a b c : Nat} (H : a * b < a * c) : b < c -:= - by_contradiction ( - assume H1 : ¬ b < c, - have H2 : a * c ≤ a * b, from mul_left_mono a (not_lt_le H1), - show false, from absurd H (le_not_lt H2) - ) - -theorem mul_right_lt_cancel {a b c : Nat} (H : b * a < c * a) : b < c -:= mul_left_lt_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) - -theorem add_right_comm (a b c : Nat) : a + b + c = a + c + b -:= - calc - a + b + c = a + (b + c) : add_assoc _ _ _ - ... = a + (c + b) : { add_comm b c } - ... = a + c + b : symm (add_assoc _ _ _) - -theorem add_left_le_cancel {a b c : Nat} (H : a + c ≤ b + c) : a ≤ b -:= - obtain (d : Nat) (Hd : a + c + d = b + c), from le_elim H, - le_intro (add_injl (subst Hd (add_right_comm a c d))) - -theorem add_right_le_cancel {a b c : Nat} (H : c + a ≤ c + b) : a ≤ b -:= add_left_le_cancel (subst (subst H (add_comm c a)) (add_comm c b)) - --- --- more properties of multiplication --- - -theorem mul_left_cancel {a b c : Nat} (H : a * b = a * c) (anez : a ≠ 0) : b = c -:= - have H1 : a * b ≤ a * c, from subst (le_refl _) H, - have H2 : a * c ≤ a * b, from subst (le_refl _) H, - le_antisym (mul_left_le_cancel H1 anez) (mul_left_le_cancel H2 anez) - -theorem mul_right_cancel {a b c : Nat} (H : b * a = c * a) (anez : a ≠ 0) : b = c -:= mul_left_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez - - --- --- divisibility --- - -definition dvd (a b : Nat) : Bool := ∃ c, a * c = b - -infix 50 | : dvd - -theorem dvd_intro {a b c : Nat} (H : a * c = b) : a | b -:= exists_intro c H - -theorem dvd_elim {a b : Nat} (H : a | b) : ∃ c, a * c = b -:= H - -theorem dvd_self (n : Nat) : n | n := dvd_intro (mul_oner n) - -theorem one_dvd (a : Nat) : 1 | a -:= dvd_intro (mul_onel a) - -theorem zero_dvd {a : Nat} (H: 0 | a) : a = 0 -:= - obtain (w : Nat) (H1 : 0 * w = a), from H, - subst (symm H1) (mul_zerol _) - -theorem dvd_zero (a : Nat) : a | 0 -:= exists_intro 0 (mul_zeror _) - -theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c -:= - obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1, - obtain (w2 : Nat) (Hw2 : b * w2 = c), from H2, - exists_intro (w1 * w2) - calc a * (w1 * w2) = a * w1 * w2 : symm (mul_assoc a w1 w2) - ... = b * w2 : { Hw1 } - ... = c : Hw2 - -theorem dvd_le {x y : Nat} (H : x | y) (ynez : y ≠ 0) : x ≤ y -:= - obtain (w : Nat) (Hw : x * w = y), from H, - have wnez : w ≠ 0, from - not_intro (take H1 : w = 0, absurd ( - calc y = x * w : symm Hw - ... = x * 0 : { H1 } - ... = 0 : mul_zeror x - ) ynez), - have H2 : x * 1 ≤ x * w, from mul_left_mono x (ne_zero_ge_one wnez), - show x ≤ y, from subst (subst H2 (mul_oner x)) Hw - -theorem dvd_mul_right {a b : Nat} (H : a | b) (c : Nat) : a | b * c -:= - obtain (d : Nat) (Hd : a * d = b), from dvd_elim H, - dvd_intro ( - calc - a * (d * c) = (a * d) * c : symm (mul_assoc _ _ _) - ... = b * c : { Hd } - ) - -theorem dvd_mul_left {a b : Nat} (H : a | b) (c : Nat) : a | c * b -:= subst (dvd_mul_right H c) (mul_comm b c) - -theorem dvd_add {a b c : Nat} (H1 : a | b) (H2 : a | c) : a | b + c -:= - obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1, - obtain (w2 : Nat) (Hw2 : a * w2 = c), from H2, - exists_intro (w1 + w2) - calc a * (w1 + w2) = a * w1 + a * w2 : distributer _ _ _ - ... = b + a * w2 : { Hw1 } - ... = b + c : { Hw2 } - -theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c -:= - or_elim (em (a = 0)) ( - assume az : a = 0, - have H3 : c = 0, from - calc c = 0 + c : symm (add_zerol _) - ... = b + c : { symm (zero_dvd (subst H2 az)) } - ... = 0 : zero_dvd (subst H1 az), - show a | c, from subst (dvd_zero a) (symm H3) - ) ( - assume anz : a ≠ 0, - obtain (w1 : Nat) (Hw1 : a * w1 = b + c), from H1, - obtain (w2 : Nat) (Hw2 : a * w2 = b), from H2, - have H3 : a * w1 = a * w2 + c, from subst Hw1 (symm Hw2), - have H4 : a * w2 ≤ a * w1, from le_intro (symm H3), - have H5 : w2 ≤ w1, from mul_left_le_cancel H4 anz, - obtain (w3 : Nat) (Hw3 : w2 + w3 = w1), from le_elim H5, - have H6 : b + a * w3 = b + c, from - calc - b + a * w3 = a * w2 + a * w3 : { symm Hw2 } - ... = a * (w2 + w3) : symm (distributer _ _ _) - ... = a * w1 : { Hw3 } - ... = b + c : Hw1, - have H7 : a * w3 = c, from add_injr H6, - show a | c, from dvd_intro H7 - ) - --- --- primes --- - -definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p - -theorem not_prime_has_divisor {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n -:= - have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n), - from not_and _ _ ◂ H2, - have H4 : ¬ ¬ n ≥ 2, - from (symm (not_not_eq _)) ◂ H1, - obtain (m : Nat) (H5 : ¬ (m | n → m = 1 ∨ m = n)), - from not_forall_elim (resolve1 H3 H4), - have H6 : m | n ∧ ¬ (m = 1 ∨ m = n), - from (not_implies _ _) ◂ H5, - have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n), - from not_or (m = 1) (m = n), - have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n, - from subst H6 H7, - show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n, - from exists_intro m H8 - -theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : - ∃ m, m | n ∧ m ≥ 2 ∧ m < n -:= - have n_ne_0 : n ≠ 0, from - not_intro (take n0 : n = 0, substp (fun n, n ≥ 2) H1 n0), - obtain (m : Nat) (Hm : m | n ∧ m ≠ 1 ∧ m ≠ n), - from not_prime_has_divisor H1 H2, - let m_dvd_n := and_eliml Hm in - let m_ne_1 := and_eliml (and_elimr Hm) in - let m_ne_n := and_elimr (and_elimr Hm) in - have m_ne_0 : m ≠ 0, from - not_intro ( - take m0 : m = 0, - have n0 : n = 0, from zero_dvd (subst m_dvd_n m0), - absurd n0 n_ne_0 - ), - exists_intro m ( - and_intro m_dvd_n ( - and_intro ( - show m ≥ 2, from ne_zero_one_ge_two m_ne_0 m_ne_1 - ) ( - have m_le_n : m ≤ n, from dvd_le m_dvd_n n_ne_0, - show m < n, from resolve2 (le_iff ◂ m_le_n) m_ne_n - ) - ) - ) - -theorem has_prime_divisor {n : Nat} : n ≥ 2 → ∃ p, prime p ∧ p | n -:= - strong_induction_on n ( - take n, - assume ih : ∀ m, m < n → m ≥ 2 → ∃ p, prime p ∧ p | m, - assume n_ge_2 : n ≥ 2, - show ∃ p, prime p ∧ p | n, from - or_elim (em (prime n)) ( - assume H : prime n, - exists_intro n (and_intro H (dvd_self n)) - ) ( - assume H : ¬ prime n, - obtain (m : Nat) (Hm : m | n ∧ m ≥ 2 ∧ m < n), - from not_prime_has_divisor2 n_ge_2 H, - obtain (p : Nat) (Hp : prime p ∧ p | m), - from ih m (and_elimr (and_elimr Hm)) (and_eliml (and_elimr Hm)), - have p_dvd_n : p | n, from dvd_trans (and_elimr Hp) (and_eliml Hm), - exists_intro p (and_intro (and_eliml Hp) p_dvd_n) - ) - ) - --- --- factorial --- - -variable fact : Nat → Nat - -axiom fact_0 : fact 0 = 1 - -axiom fact_succ : ∀ n, fact (n + 1) = (n + 1) * fact n - --- can the simplifier do this? -theorem fact_1 : fact 1 = 1 -:= - calc - fact 1 = fact (0 + 1) : { symm (add_zerol 1) } - ... = (0 + 1) * fact 0 : fact_succ _ - ... = 1 * fact 0 : { add_zerol 1 } - ... = 1 * 1 : { fact_0 } - ... = 1 : mul_oner _ - -theorem fact_ne_0 (n : Nat) : fact n ≠ 0 -:= - induction_on n ( - not_intro ( - assume H : fact 0 = 0, - have H1 : 1 = 0, from (subst H fact_0), - absurd H1 one_ne_zero - ) - ) ( - take n, - assume ih : fact n ≠ 0, - not_intro ( - assume H : fact (n + 1) = 0, - have H1 : n + 1 = 0, from - mul_right_cancel ( - calc - (n + 1) * fact n = fact (n + 1) : symm (fact_succ n) - ... = 0 : H - ... = 0 * fact n : symm (mul_zerol _) - ) ih, - absurd H1 (succ_nz _) - ) - ) - -theorem dvd_fact {m n : Nat} (m_gt_0 : m > 0) (m_le_n : m ≤ n) : m | fact n -:= - obtain (m' : Nat) (Hm' : 1 + m' = m), from le_elim m_gt_0, - obtain (n' : Nat) (Hn' : 1 + n' = n), from le_elim (le_trans m_gt_0 m_le_n), - have m'_le_n' : m' ≤ n', - from add_right_le_cancel (subst (subst m_le_n (symm Hm')) (symm Hn')), - have H : ∀ n' m', m' ≤ n' → m' + 1 | fact (n' + 1), from - induction ( - take m' , - assume m'_le_0 : m' ≤ 0, - have Hm' : m' + 1 = 1, - from calc - m' + 1 = 0 + 1 : { le_antisym m'_le_0 (le_zero m') } - ... = 1 : add_zerol _, - show m' + 1 | fact (0 + 1), from subst (one_dvd _) (symm Hm') - ) ( - take n', - assume ih : ∀m', m' ≤ n' → m' + 1 | fact (n' + 1), - take m', - assume Hm' : m' ≤ n' + 1, - have H1 : m' < n' + 1 ∨ m' = n' + 1, from le_iff ◂ Hm', - or_elim H1 ( - assume H2 : m' < n' + 1, - have H3 : m' ≤ n', from lt_succ H2, - have H4 : m' + 1 | fact (n' + 1), from ih _ H3, - have H5 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_left H4 _, - show m' + 1 | fact (n' + 1 + 1), from subst H5 (symm (fact_succ _)) - ) ( - assume H2 : m' = n' + 1, - have H3 : m' + 1 | n' + 1 + 1, from subst (dvd_self _) H2, - have H4 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_right H3 _, - show m' + 1 | fact (n' + 1 + 1), from subst H4 (symm (fact_succ _)) - ) - ), - have H1 : m' + 1 | fact (n' + 1), from H _ _ m'_le_n', - show m | fact n, - from (subst (subst (subst (subst H1 (add_comm m' 1)) Hm') (add_comm n' 1)) Hn') - -theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p -:= - let m := fact (n + 1) in - have Hn1 : n + 1 ≥ 1, from le_addl _ _, - have m_ge_1 : m ≥ 1, from ne_zero_ge_one (fact_ne_0 _), - have m1_ge_2 : m + 1 ≥ 2, from le_add m_ge_1 1, - obtain (p : Nat) (Hp : prime p ∧ p | m + 1), from has_prime_divisor m1_ge_2, - let prime_p := and_eliml Hp in - let p_dvd_m1 := and_elimr Hp in - have p_ge_2 : p ≥ 2, from and_eliml prime_p, - have two_gt_0 : 2 > 0, from (ne_zero_iff 2) ◂ (succ_nz 1), - -- fails if arguments are left implicit - have p_gt_0 : p > 0, from @lt_le_trans 0 2 p two_gt_0 p_ge_2, - have p_ge_n : p ≥ n, from - by_contradiction ( - assume H1 : ¬ p ≥ n, - have H2 : p < n, from not_le_lt H1, - have H3 : p ≤ n + 1, from lt_le (lt_le_trans H2 (le_addr n 1)), - have H4 : p | m, from dvd_fact p_gt_0 H3, - have H5 : p | 1, from dvd_add_cancel p_dvd_m1 H4, - have H6 : p ≤ 1, from dvd_le H5 (succ_nz 0), - have H7 : 2 ≤ 1, from le_trans p_ge_2 H6, - absurd H7 (lt_nrefl 1) - ), - exists_intro p (and_intro p_ge_n prime_p) diff --git a/examples/lean/set.lean b/examples/lean/set.lean deleted file mode 100644 index 7e2218d48..000000000 --- a/examples/lean/set.lean +++ /dev/null @@ -1,25 +0,0 @@ -import macros - -definition Set (A : Type) : Type := A → Bool - -definition element {A : Type} (x : A) (s : Set A) := s x -infix 60 ∈ : element - -definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 → x ∈ s2 -infix 50 ⊆ : subset - -theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 -:= take x : A, - assume Hin : x ∈ s1, - show x ∈ s3, from - let L1 : x ∈ s2 := H1 x Hin - in H2 x L1 - -theorem subset_ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2 -:= funext H - -theorem subset_antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2 -:= subset_ext (show (∀ x, x ∈ s1 = x ∈ s2), from - take x, show x ∈ s1 = x ∈ s2, from - boolext (show x ∈ s1 → x ∈ s2, from H1 x) - (show x ∈ s2 → x ∈ s1, from H2 x)) diff --git a/examples/lean/setoid.lean b/examples/lean/setoid.lean deleted file mode 100644 index 928a24b44..000000000 --- a/examples/lean/setoid.lean +++ /dev/null @@ -1,70 +0,0 @@ --- Setoid example/test -import macros - -definition reflexive {A : (Type U)} (r : A → A → Bool) := ∀ x, r x x -definition symmetric {A : (Type U)} (r : A → A → Bool) := ∀ x y, r x y → r y x -definition transitive {A : (Type U)} (r : A → A → Bool) := ∀ x y z, r x y → r y z → r x z - --- We need to create a universe smaller than U for defining setoids. --- If we use (Type U) in the definition of setoid, then we will not be --- able to write s1 = s2 given s1 s2 : setoid. --- Writing the universes explicitily is really annoying. We should try to hide them. -universe s ≥ 1 --- We currently don't have records. So, we use sigma types. -definition setoid := sig A : (Type s), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq) -definition to_setoid (S : (Type s)) (eq : S → S → Bool) (Hrefl : reflexive eq) (Hsymm : symmetric eq) (Htrans : transitive eq) : setoid -:= pair S (pair eq (pair Hrefl (pair Hsymm Htrans))) - --- The following definitions can be generated automatically. -definition carrier (s : setoid) := proj1 s -definition S_eq {s : setoid} : carrier s → carrier s → Bool -:= proj1 (proj2 s) -infix 50 ≈ : S_eq -definition S_refl {s : setoid} : ∀ x, x ≈ x -:= proj1 (proj2 (proj2 s)) -definition S_symm {s : setoid} {x y : carrier s} : x ≈ y → y ≈ x -:= proj1 (proj2 (proj2 (proj2 s))) x y -definition S_trans {s : setoid} {x y z : carrier s} : x ≈ y → y ≈ z → x ≈ z -:= proj2 (proj2 (proj2 (proj2 s))) x y z - --- First example: the cross-product of two setoids is a setoid -definition product (s1 s2 : setoid) : setoid -:= to_setoid - (carrier s1 # carrier s2) - (λ x y, proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y) - (take x, and_intro (S_refl (proj1 x)) (S_refl (proj2 x))) - (take x y, - assume H : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y, - and_intro (S_symm (and_eliml H)) (S_symm (and_elimr H))) - (take x y z, - assume H1 : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y, - assume H2 : proj1 y ≈ proj1 z ∧ proj2 y ≈ proj2 z, - and_intro (S_trans (and_eliml H1) (and_eliml H2)) - (S_trans (and_elimr H1) (and_elimr H2))) - -scope - -- We need to extend the elaborator to be able to write - -- p1 p2 : product s1 s2 - set_option pp::implicit true - check λ (s1 s2 : setoid) (p1 p2 : carrier (product s1 s2)), p1 ≈ p2 -end - -definition morphism (s1 s2 : setoid) := sig f : carrier s1 → carrier s2, ∀ x y, x ≈ y → f x ≈ f y -definition morphism_intro {s1 s2 : setoid} (f : carrier s1 → carrier s2) (H : ∀ x y, x ≈ y → f x ≈ f y) : morphism s1 s2 -:= pair f H -definition f {s1 s2 : setoid} (m : morphism s1 s2) : carrier s1 → carrier s2 -:= proj1 m --- It would be nice to support (m.f x) as syntax sugar for (f m x) -definition is_compat {s1 s2 : setoid} (m : morphism s1 s2) {x y : carrier s1} : x ≈ y → f m x ≈ f m y -:= proj2 m x y - --- Second example: the composition of two morphism is a morphism -definition compose {s1 s2 s3 : setoid} (m1 : morphism s1 s2) (m2 : morphism s2 s3) : morphism s1 s3 -:= morphism_intro - (λ x, f m2 (f m1 x)) - (take x y, assume Hxy : x ≈ y, - have Hfxy : f m1 x ≈ f m1 y, - from is_compat m1 Hxy, - show f m2 (f m1 x) ≈ f m2 (f m1 y), - from is_compat m2 Hfxy) - diff --git a/examples/lean/setoid2.lean b/examples/lean/setoid2.lean deleted file mode 100644 index 2f1b9abba..000000000 --- a/examples/lean/setoid2.lean +++ /dev/null @@ -1,113 +0,0 @@ --- Setoid example/test -import macros -import tactic - -variable first {A : (Type U)} {B : A → (Type U)} (p : sig x : A, B x) : A -variable second {A : (Type U)} {B : A → (Type U)} (p : sig x : A, B x) : B (first p) - -definition reflexive {A : (Type U)} (r : A → A → Bool) := ∀ x, r x x -definition symmetric {A : (Type U)} (r : A → A → Bool) := ∀ x y, r x y → r y x -definition transitive {A : (Type U)} (r : A → A → Bool) := ∀ x y z, r x y → r y z → r x z - --- We need to create a universe smaller than U for defining setoids. --- If we use (Type U) in the definition of setoid, then we will not be --- able to write s1 = s2 given s1 s2 : setoid. --- Writing the universes explicitily is really annoying. We should try to hide them. -universe M ≥ 1 --- We currently don't have records. So, we use sigma types. -definition setoid := sig A : (Type M), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq) -definition to_setoid (S : (Type M)) (eq : S → S → Bool) (Hrefl : reflexive eq) (Hsymm : symmetric eq) (Htrans : transitive eq) : setoid -:= pair S (pair eq (pair Hrefl (pair Hsymm Htrans))) - --- The following definitions can be generated automatically. -definition carrier (s : setoid) -:= @first - (Type M) - (λ A : (Type M), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)) - s - -definition setoid_unfold1 (s : setoid) : sig eq : carrier s → carrier s → Bool, (reflexive eq) # (symmetric eq) # (transitive eq) -:= (@second (Type M) - (λ A : (Type M), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)) - s) - -definition S_eq {s : setoid} : carrier s → carrier s → Bool -:= (@first (carrier s → carrier s → Bool) - (λ eq : carrier s → carrier s → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)) - (setoid_unfold1 s)) - -infix 50 ≈ : S_eq - -definition setoid_unfold2 (s : setoid) : (reflexive (@S_eq s)) # (symmetric (@S_eq s)) # (transitive (@S_eq s)) -:= (@second (carrier s → carrier s → Bool) - (λ eq : carrier s → carrier s → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)) - (setoid_unfold1 s)) - -definition S_refl {s : setoid} : ∀ x : carrier s, x ≈ x -:= (@first (reflexive (@S_eq s)) - (λ x : reflexive (@S_eq s), (symmetric (@S_eq s)) # (transitive (@S_eq s))) - (setoid_unfold2 s)) - -definition setoid_unfold3 (s : setoid) : (symmetric (@S_eq s)) # (transitive (@S_eq s)) -:= (@second (reflexive (@S_eq s)) - (λ x : reflexive (@S_eq s), (symmetric (@S_eq s)) # (transitive (@S_eq s))) - (setoid_unfold2 s)) - -definition S_symm {s : setoid} {x y : carrier s} : x ≈ y → y ≈ x -:= (@first (symmetric (@S_eq s)) - (λ x : symmetric (@S_eq s), (transitive (@S_eq s))) - (setoid_unfold3 s)) - x y - -definition S_trans {s : setoid} {x y z : carrier s} : x ≈ y → y ≈ z → x ≈ z -:= (@second (symmetric (@S_eq s)) - (λ x : symmetric (@S_eq s), (transitive (@S_eq s))) - (setoid_unfold3 s)) - x y z - -set_opaque carrier true -set_opaque S_eq true -set_opaque S_refl true -set_opaque S_symm true -set_opaque S_trans true - --- First example: the cross-product of two setoids is a setoid -definition product (s1 s2 : setoid) : setoid -:= to_setoid - (carrier s1 # carrier s2) - (λ x y, proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y) - (take x, and_intro (S_refl (proj1 x)) (S_refl (proj2 x))) - (take x y, - assume H : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y, - and_intro (S_symm (and_eliml H)) (S_symm (and_elimr H))) - (take x y z, - assume H1 : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y, - assume H2 : proj1 y ≈ proj1 z ∧ proj2 y ≈ proj2 z, - and_intro (S_trans (and_eliml H1) (and_eliml H2)) - (S_trans (and_elimr H1) (and_elimr H2))) - -scope - -- We need to extend the elaborator to be able to write - -- p1 p2 : product s1 s2 - set_option pp::implicit true - check λ (s1 s2 : setoid) (p1 p2 : carrier (product s1 s2)), p1 ≈ p2 -end - -definition morphism (s1 s2 : setoid) := sig f : carrier s1 → carrier s2, ∀ x y, x ≈ y → f x ≈ f y -definition morphism_intro {s1 s2 : setoid} (f : carrier s1 → carrier s2) (H : ∀ x y, x ≈ y → f x ≈ f y) : morphism s1 s2 -:= pair f H -definition f {s1 s2 : setoid} (m : morphism s1 s2) : carrier s1 → carrier s2 -:= proj1 m --- It would be nice to support (m.f x) as syntax sugar for (f m x) -definition is_compat {s1 s2 : setoid} (m : morphism s1 s2) {x y : carrier s1} : x ≈ y → f m x ≈ f m y -:= proj2 m x y - --- Second example: the composition of two morphism is a morphism -definition compose {s1 s2 s3 : setoid} (m1 : morphism s1 s2) (m2 : morphism s2 s3) : morphism s1 s3 -:= morphism_intro - (λ x, f m2 (f m1 x)) - (take x y, assume Hxy : x ≈ y, - have Hfxy : f m1 x ≈ f m1 y, - from is_compat m1 Hxy, - show f m2 (f m1 x) ≈ f m2 (f m1 y), - from is_compat m2 Hfxy) diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean deleted file mode 100644 index 4d1fa6b24..000000000 --- a/examples/lean/tactic1.lean +++ /dev/null @@ -1,57 +0,0 @@ --- This example demonstrates how to specify a proof skeleton that contains --- "holes" that must be filled using user-defined tactics. -import tactic - -(* --- Define a simple tactic using Lua -auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac())) - -conj_hyp = conj_hyp_tac() -conj = conj_tac() -*) - --- The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it. --- The "hint" is a tactic that should be used to fill the "hole". --- In the following example, we use the tactic "auto" defined by the Lua code above. --- --- The (show [expr], by [tactic]) expression is also creating a "hole" and associating a "hint" to it. --- The expression [expr] after the shows is fixing the type of the "hole" -theorem T1 (A B : Bool) : A /\ B -> B /\ A := - fun assumption : A /\ B, - let lemma1 : A := (by auto), - lemma2 : B := (by auto) - in (show B /\ A, by auto) - -print environment 1. -- print proof for the previous theorem - --- When hints are not provided, the user must fill the (remaining) holes using tactic command sequences. --- Each hole must be filled with a tactic command sequence that terminates with the command 'done' and --- successfully produces a proof term for filling the hole. Here is the same example without hints --- This style is more convenient for interactive proofs -theorem T2 (A B : Bool) : A /\ B -> B /\ A := - fun assumption : A /\ B, - let lemma1 : A := _, -- first hole - lemma2 : B := _ -- second hole - in _. -- third hole - auto. done. -- tactic command sequence for the first hole - auto. done. -- tactic command sequence for the second hole - auto. done. -- tactic command sequence for the third hole - --- In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics. -theorem T3 (A B : Bool) : A /\ B -> B /\ A := - fun assumption : A /\ B, - let lemma1 : A := _, -- first hole - lemma2 : B := _ -- second hole - in _. -- third hole - conj_hyp. exact. done. -- tactic command sequence for the first hole - conj_hyp. exact. done. -- tactic command sequence for the second hole - conj. exact. done. -- tactic command sequence for the third hole - --- We can also mix the two styles (hints and command sequences) -theorem T4 (A B : Bool) : A /\ B -> B /\ A := - fun assumption : A /\ B, - let lemma1 : A := _, -- first hole - lemma2 : B := _ -- second hole - in (show B /\ A, by auto). - auto. done. -- tactic command sequence for the first hole - auto. done. -- tactic command sequence for the second hole diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean deleted file mode 100644 index 2c758c878..000000000 --- a/examples/lean/tactic_in_lua.lean +++ /dev/null @@ -1,72 +0,0 @@ -(* - -- This example demonstrates how to create a new tactic using Lua. - -- The basic idea is to reimplement the tactic conj_tactic in Lua. - - -- Tactic for splitting goals of the form - -- n : Hs |- A /\ B - -- into - -- n::1 : Hs |- A - -- n::2 : Hs |- B - function conj_fn(env, ios, s) - local gs = s:goals() - -- We store the information needed by the proof_builder in the - -- array proof_info. - -- proof_info has the format {{name_1, expr_1}, ... {name_k, expr_k}} - -- where name_i is a goal splitted by this tactic, and expr_i - -- is the conclusion of the theorem, that is, an expression of the form - -- A /\ B - local proof_info = {} - -- We store the new goals into the Lua array new_gs. - -- new_gs has the format {{name_1, goal_1}, ..., {name_n, goal_n}} - local new_gs = {} - local found = false - for n, g in gs:pairs() do - yield() -- Give a chance to other tactics to run - local c = g:conclusion() - if c:is_and() then - -- Goal g is of the form Hs |- A /\ B - found = true -- The tactic managed to split at least one goal - local Hs = g:hypotheses() - local A = c:arg(1) - local B = c:arg(2) - proof_info[#proof_info + 1] = {n, c} -- Save information for implementing the proof builder - new_gs[#new_gs + 1] = {name(n, 1), goal(Hs, A)} -- Add goal n::1 : Hs |- A - new_gs[#new_gs + 1] = {name(n, 2), goal(Hs, B)} -- Add goal n::1 : Hs |- B - else - new_gs[#new_gs + 1] = {n, g} -- Keep the goal - end - end - if not found then - return nil -- Tactic is not applicable - end - local pb = s:proof_builder() - local new_pb = - function(m, a) - 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 - local c = p[2] -- c is the conclusion of the goal splitted by this tactic - assert(c:is_and()) -- c is of the form A /\ B - -- The proof for goal n is - -- Conj(A, B, H1, H2) - -- where H1 and H2 are the proofs for goals n::1 and n::2 - new_m:insert(n, Conj(c:arg(1), c:arg(2), m:find(name(n, 1)), m:find(name(n, 2)))) - -- We don't need the proofs for n::1 and n::2 anymore - new_m:erase(name(n, 1)) - new_m:erase(name(n, 2)) - end - return pb(new_m, a) -- Apply the proof builder for the original state - end - return proof_state(s, goals(new_gs), proof_builder(new_pb)) - end - conj_in_lua = tactic(conj_fn) -- Create a new tactic object using the Lua function conj_fn - -- Now, the tactic conj_in_lua can be used when proving theorems in Lean. -*) - -theorem T (a b : Bool) : a -> b -> a /\ b := _. - (* Then(conj_in_lua, assumption_tac()) *) - done - --- print proof created using our script -print environment 1. diff --git a/examples/lean/tc.lean b/examples/lean/tc.lean deleted file mode 100644 index f7e98136c..000000000 --- a/examples/lean/tc.lean +++ /dev/null @@ -1,38 +0,0 @@ -import macros - -definition reflexive {A : TypeU} (R : A → A → Bool) := ∀ x, R x x -definition transitive {A : TypeU} (R : A → A → Bool) := ∀ x y z, R x y → R y z → R x z -definition subrelation {A : TypeU} (R1 : A → A → Bool) (R2 : A → A → Bool) := ∀ x y, R1 x y → R2 x y -infix 50 ⊆ : subrelation - --- (tcls R) is the transitive closure of relation R --- We define it as the intersection of all transitive relations containing R -definition tcls {A : TypeU} (R : A → A → Bool) (a b : A) -:= ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → P a b -notation 65 _⁺ : tcls -- use superscript + as notation for transitive closure - -theorem tcls_trans {A : TypeU} {R : A → A → Bool} {a b c : A} (Hab : R⁺ a b) (Hbc : R⁺ b c) : R⁺ a c -:= take P, assume Hrefl Htrans Hsub, - let Pab : P a b := Hab P Hrefl Htrans Hsub, - Pbc : P b c := Hbc P Hrefl Htrans Hsub - in Htrans a b c Pab Pbc - -theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, R⁺ a a -:= take a P, assume Hrefl Htrans Hsub, - Hrefl a - -theorem tcls_sub {A : TypeU} (R : A → A → Bool) : R ⊆ R⁺ -:= take a b, - assume Hab : R a b, - show R⁺ a b, from - take P, assume Hrefl Htrans Hsub, - Hsub a b Hab - -theorem tcls_step {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : R a b) (H2 : R⁺ b c) : R⁺ a c -:= take P, assume Hrefl Htrans Hsub, - Htrans a b c (Hsub a b H1) (H2 P Hrefl Htrans Hsub) - -theorem tcls_smallest {A : TypeU} (R : A → A → Bool) : ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → (R⁺ ⊆ P) -:= take P, assume Hrefl Htrans Hsub, - take a b, assume H : R⁺ a b, - show P a b, from H P Hrefl Htrans Hsub diff --git a/examples/lean/test_algebra.lean b/examples/lean/test_algebra.lean deleted file mode 100644 index 6974930dc..000000000 --- a/examples/lean/test_algebra.lean +++ /dev/null @@ -1,108 +0,0 @@ -import macros - ---- ---- Classes of structures, and axiomatic classes of structures ---- - ---- A "structure" consists of a carrier, and some data (whose type depends on the carrier) - -definition StructClass : (Type 1) := Type → Type -- the type of the data - -definition structure (S : StructClass) : (Type 1) -:= sig T : Type, S T - -definition carrier {S : StructClass} (M : structure S) : Type -:= proj1 M - -definition data {S : StructClass} (M : structure S) : S (carrier M) -:= proj2 M - ---- An "axiomatic class" is a class of structures satisfying some predicate (the "axioms") - -definition AxClass : (Type 1) -:= sig S : StructClass, structure S → Bool - --- Coercion from AxClass to StructClass -definition struct_class (C : AxClass) : StructClass -:= proj1 C - -definition axioms {C : AxClass} (M : structure (struct_class C)) -:= proj2 C M - -definition instance (C : AxClass) : (Type 1) -:= sig M : structure (struct_class C), axioms M - -definition struct {C : AxClass} (M : instance C) -:= proj1 M - -definition hyps {C : AxClass} (M : instance C) : axioms (struct M) -:= proj2 M - ---- ---- Examples ---- - ---- multiplication (for overloading *) - -definition MulStruct : StructClass -:= λ T, T → T → T - -definition mul {M : structure MulStruct} (x y : carrier M) : carrier M -:= data M x y - -infixl 70 * : mul - -definition mul_is_assoc (M : structure MulStruct) : Bool -:= ∀ x y z : carrier M, (x * y) * z = x * (y * z) - -definition mul_is_comm (M : structure MulStruct) : Bool -:= ∀ x y z : carrier M, x * y = y * x - ---- semigroups - -definition Semigroup : AxClass -:= pair MulStruct mul_is_assoc - ---- to fill the hole above automatically -theorem semigroup_mul_is_assoc (M : instance Semigroup) : mul_is_assoc (struct M) -:= hyps M - -definition OneStruct : StructClass -:= λ T, T - -definition one {M : structure OneStruct} : carrier M -:= data M - --- structures with mult and one - -definition MonoidStruct : StructClass -:= λ T, OneStruct T # MulStruct T - -definition MonoidStruct_to_OneStruct (M : structure MonoidStruct) : (structure OneStruct) -:= pair (carrier M) (proj1 (data M)) - -definition MonoidStruct_to_MulStruct (M : structure MonoidStruct) : (structure MulStruct) -:= pair (carrier M) (proj2 (data M)) - -variable M : structure MonoidStruct -check carrier M = carrier (MonoidStruct_to_OneStruct M) - -theorem test1 (M : structure MonoidStruct) : carrier M = carrier (MonoidStruct_to_OneStruct M) -:= refl (carrier M) - -definition is_mul_right_id (M : structure MonoidStruct) : Bool -:= let m : carrier M → carrier M → carrier M := @mul (MonoidStruct_to_MulStruct M), - o : carrier M := @one (MonoidStruct_to_OneStruct M) - in ∀ x : carrier M, m x o = x - -definition is_monoid (M : structure MonoidStruct) : Bool -:= mul_is_assoc (MonoidStruct_to_MulStruct M) ∧ is_mul_right_id M - -definition Monoid : AxClass -:= pair MonoidStruct is_monoid - -theorem monoid_is_mul_right_id (M : instance Monoid) : is_mul_right_id (struct M) -:= and_elimr (proj2 M) - -theorem monoid_mul_is_assoc (M : instance Monoid) : mul_is_assoc (MonoidStruct_to_MulStruct (struct M)) -:= and_eliml (proj2 M) diff --git a/examples/lean/wf.lean b/examples/lean/wf.lean deleted file mode 100644 index e798f706c..000000000 --- a/examples/lean/wf.lean +++ /dev/null @@ -1,50 +0,0 @@ -import macros - --- Well-founded relation definition --- We are essentially saying that a relation R is well-founded --- if every non-empty "set" P, has a R-minimal element -definition wf {A : (Type U)} (R : A → A → Bool) : Bool -:= ∀ P, (∃ w, P w) → ∃ min, P min ∧ ∀ b, R b min → ¬ P b - --- Well-founded induction theorem -theorem wf_induction {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x) - : ∀ x, P x -:= by_contradiction (assume N : ¬ ∀ x, P x, - obtain (w : A) (Hw : ¬ P w), from not_forall_elim N, - -- The main "trick" is to define Q x as ¬ P x. - -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r) - let Q : A → Bool := λ x, ¬ P x in - have Qw : ∃ w, Q w, - from exists_intro w Hw, - have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b, - from Hwf Q Qw, - obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), - from Qwf, - -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction. - have s1 : ∀ b, R b r → P b, - from take b : A, assume H : R b r, - -- We are using Hr to derive ¬ ¬ P b - not_not_elim (and_elimr Hr b H), - have s2 : P r, - from iH r s1, - have s3 : ¬ P r, - from and_eliml Hr, - show false, - from absurd s2 s3) - --- More compact proof -theorem wf_induction2 {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x) - : ∀ x, P x -:= by_contradiction (assume N : ¬ ∀ x, P x, - obtain (w : A) (Hw : ¬ P w), from not_forall_elim N, - -- The main "trick" is to define Q x as ¬ P x. - -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r) - let Q : A → Bool := λ x, ¬ P x in - obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), - from Hwf Q (exists_intro w Hw), - -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction. - have s1 : ∀ b, R b r → P b, - from take b : A, assume H : R b r, - -- We are using Hr to derive ¬ ¬ P b - not_not_elim (and_elimr Hr b H), - absurd (iH r s1) (and_eliml Hr))