From 7142c0fed3b20e05a7e2c6fe621aad2d76a27dfc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 May 2014 10:43:30 -0700 Subject: [PATCH] doc(demo): remove Lean 0.1 demo files Signed-off-by: Leonardo de Moura --- doc/demo/Nat.lean | 360 ----------------------- doc/demo/add_assoc.lean | 21 -- doc/demo/congr.lean | 25 -- doc/demo/even.lean | 84 ------ doc/demo/goals.txt | 49 ---- doc/demo/kernel.lean | 628 ---------------------------------------- doc/demo/monitor.lean | 36 --- doc/demo/mul_succl.lean | 59 ---- doc/demo/nnf.lean | 17 -- doc/demo/reflif.lean | 20 -- doc/demo/set.lean | 33 --- doc/demo/subst.lean | 9 - doc/demo/tc.lean | 38 --- 13 files changed, 1379 deletions(-) delete mode 100644 doc/demo/Nat.lean delete mode 100644 doc/demo/add_assoc.lean delete mode 100644 doc/demo/congr.lean delete mode 100644 doc/demo/even.lean delete mode 100644 doc/demo/goals.txt delete mode 100644 doc/demo/kernel.lean delete mode 100644 doc/demo/monitor.lean delete mode 100644 doc/demo/mul_succl.lean delete mode 100644 doc/demo/nnf.lean delete mode 100644 doc/demo/reflif.lean delete mode 100644 doc/demo/set.lean delete mode 100644 doc/demo/subst.lean delete mode 100644 doc/demo/tc.lean diff --git a/doc/demo/Nat.lean b/doc/demo/Nat.lean deleted file mode 100644 index 92c94d039..000000000 --- a/doc/demo/Nat.lean +++ /dev/null @@ -1,360 +0,0 @@ -import kernel -import macros - -variable Nat : Type -alias ℕ : Nat - -namespace Nat -builtin numeral - -builtin add : Nat → Nat → Nat -infixl 65 + : add - -builtin mul : Nat → Nat → Nat -infixl 70 * : mul - -builtin le : Nat → Nat → Bool -infix 50 <= : le -infix 50 ≤ : le - -definition ge (a b : Nat) := b ≤ a -infix 50 >= : ge -infix 50 ≥ : ge - -definition lt (a b : Nat) := a + 1 ≤ b -infix 50 < : lt - -definition gt (a b : Nat) := b < a -infix 50 > : gt - -definition id (a : Nat) := a -notation 55 | _ | : id - -axiom succ_nz (a : Nat) : a + 1 ≠ 0 -axiom succ_inj {a b : Nat} (H : a + 1 = b + 1) : a = b -axiom add_zeror (a : Nat) : a + 0 = a -axiom add_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} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a - -theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a -:= induction H1 H2 a - -theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a -:= induction_on a - (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H) - (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (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 (iH Hne0), - exists_intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))) - -theorem discriminate {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 (pred_nz Hne0), - H2 w (symm Hw)) - -theorem add_zerol (a : Nat) : 0 + a = a -:= induction_on a - (have 0 + 0 = 0 : trivial) - (λ (n : Nat) (iH : 0 + n = n), - calc 0 + (n + 1) = (0 + n) + 1 : add_succr 0 n - ... = n + 1 : { iH }) - -theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1 -:= induction_on b - (calc (a + 1) + 0 = a + 1 : add_zeror (a + 1) - ... = (a + 0) + 1 : { symm (add_zeror a) }) - (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), - calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add_succr (a + 1) n - ... = ((a + n) + 1) + 1 : { iH } - ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add_succr a n) }) - -theorem add_comm (a b : Nat) : a + b = b + a -:= induction_on b - (calc a + 0 = a : add_zeror a - ... = 0 + a : symm (add_zerol a)) - (λ (n : Nat) (iH : a + n = n + a), - calc a + (n + 1) = (a + n) + 1 : add_succr a n - ... = (n + a) + 1 : { iH } - ... = (n + 1) + a : symm (add_succl n a)) - -theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) -:= symm (induction_on a - (calc 0 + (b + c) = b + c : add_zerol (b + c) - ... = (0 + b) + c : { symm (add_zerol b) }) - (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), - calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add_succl n (b + c) - ... = ((n + b) + c) + 1 : { iH } - ... = ((n + b) + 1) + c : symm (add_succl (n + b) c) - ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add_succl n b) })) - -theorem mul_zerol (a : Nat) : 0 * a = 0 -:= induction_on a - (have 0 * 0 = 0 : trivial) - (λ (n : Nat) (iH : 0 * n = 0), - calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n - ... = 0 + 0 : { iH } - ... = 0 : trivial) - -theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b -:= induction_on b - (calc (a + 1) * 0 = 0 : mul_zeror (a + 1) - ... = a * 0 : symm (mul_zeror a) - ... = a * 0 + 0 : symm (add_zeror (a * 0))) - (λ (n : Nat) (iH : (a + 1) * n = a * n + 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 : symm (add_assoc (a * n + n) a 1) - ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : add_assoc (a * n) n a } - ... = a * n + (a + n) + 1 : { add_comm n a } - ... = a * n + a + n + 1 : { symm (add_assoc (a * n) a n) } - ... = a * (n + 1) + n + 1 : { symm (mul_succr a n) } - ... = a * (n + 1) + (n + 1) : add_assoc (a * (n + 1)) n 1) - -theorem mul_onel (a : Nat) : 1 * a = a -:= induction_on a - (have 1 * 0 = 0 : trivial) - (λ (n : Nat) (iH : 1 * n = n), - calc 1 * (n + 1) = 1 * n + 1 : mul_succr 1 n - ... = n + 1 : { iH }) - -theorem mul_oner (a : Nat) : a * 1 = a -:= induction_on a - (have 0 * 1 = 0 : trivial) - (λ (n : Nat) (iH : n * 1 = n), - calc (n + 1) * 1 = n * 1 + 1 : mul_succl n 1 - ... = n + 1 : { iH }) - -theorem mul_comm (a b : Nat) : a * b = b * a -:= induction_on 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 : mul_succr a n - ... = n * a + a : { iH } - ... = (n + 1) * a : symm (mul_succl n a)) - -theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c -:= induction_on 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) : mul_succl n (b + c) - ... = n * b + n * c + (b + c) : { iH } - ... = n * b + n * c + b + c : symm (add_assoc (n * b + n * c) b c) - ... = n * b + (n * c + b) + c : { add_assoc (n * b) (n * c) b } - ... = n * b + (b + n * c) + c : { add_comm (n * c) b } - ... = n * b + b + n * c + c : { symm (add_assoc (n * b) b (n * c)) } - ... = (n + 1) * b + n * c + c : { symm (mul_succl n b) } - ... = (n + 1) * b + (n * c + c) : add_assoc ((n + 1) * b) (n * c) c - ... = (n + 1) * b + (n + 1) * c : { symm (mul_succl n c) }) - -theorem distributel (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 : distributer c a b - ... = a * c + c * b : { mul_comm c a } - ... = a * c + b * c : { mul_comm c b } - -theorem mul_assoc (a b c : Nat) : (a * b) * c = a * (b * c) -:= symm (induction_on 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) : mul_succl n (b * c) - ... = n * b * c + (b * c) : { iH } - ... = (n * b + b) * c : symm (distributel (n * b) b c) - ... = (n + 1) * b * c : { symm (mul_succl n b) })) - -theorem add_left_comm (a b c : Nat) : a + (b + c) = b + (a + c) -:= left_comm add_comm add_assoc a b c - -theorem mul_left_comm (a b c : Nat) : a * (b * c) = b * (a * c) -:= left_comm mul_comm mul_assoc a b c - -theorem add_injr {a b c : Nat} : a + b = a + c → b = c -:= induction_on a - (λ H : 0 + b = 0 + c, - calc b = 0 + b : symm (add_zerol b) - ... = 0 + c : H - ... = c : add_zerol c) - (λ (n : Nat) (iH : n + b = n + c → b = c) (H : n + 1 + b = n + 1 + c), - let L1 : n + b + 1 = n + c + 1 - := (calc n + b + 1 = n + (b + 1) : add_assoc n b 1 - ... = n + (1 + b) : { add_comm b 1 } - ... = n + 1 + b : symm (add_assoc n 1 b) - ... = n + 1 + c : H - ... = n + (1 + c) : add_assoc n 1 c - ... = n + (c + 1) : { add_comm 1 c } - ... = n + c + 1 : symm (add_assoc n c 1)), - L2 : n + b = n + c := succ_inj L1 - in iH L2) - -theorem add_injl {a b c : Nat} (H : a + b = c + b) : a = c -:= add_injr (calc b + a = a + b : add_comm _ _ - ... = c + b : H - ... = b + c : add_comm _ _) - -theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0 -:= discriminate - (λ H1 : a = 0, H1) - (λ (n : Nat) (H1 : a = n + 1), - absurd_elim (a = 0) - H (calc a + b = n + 1 + b : { H1 } - ... = n + (1 + b) : add_assoc n 1 b - ... = n + (b + 1) : { add_comm 1 b } - ... = n + b + 1 : symm (add_assoc n b 1) - ... ≠ 0 : succ_nz (n + b))) - -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 le_elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b -:= (le_def a b) ◂ H - -theorem le_refl (a : Nat) : a ≤ a := le_intro (add_zeror a) - -theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a) - - -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 : symm (add_assoc a w1 w2) - ... = b + w2 : { Hw1 } - ... = c : Hw2) - -theorem le_add {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) : add_assoc a c w - ... = a + (w + c) : { add_comm c w } - ... = a + w + c : symm (add_assoc a w c) - ... = b + c : { Hw }) - -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 - := add_injr (calc a + (w1 + w2) = a + w1 + w2 : { symm (add_assoc a w1 w2) } - ... = b + w2 : { Hw1 } - ... = a : Hw2 - ... = a + 0 : symm (add_zeror a)), - L2 : w1 = 0 := add_eqz L1 - in calc a = a + 0 : symm (add_zeror a) - ... = a + w1 : { symm L2 } - ... = b : Hw1 - -theorem not_lt_0 (a : Nat) : ¬ a < 0 -:= not_intro (λ H : a + 1 ≤ 0, - obtain (w : Nat) (Hw1 : a + 1 + w = 0), from (le_elim H), - absurd - (calc a + w + 1 = a + (w + 1) : add_assoc _ _ _ - ... = a + (1 + w) : { add_comm _ _ } - ... = a + 1 + w : symm (add_assoc _ _ _) - ... = 0 : Hw1) - (succ_nz (a + w))) - -theorem lt_intro {a b c : Nat} (H : a + 1 + c = b) : a < b -:= le_intro H - -theorem lt_elim {a b : Nat} (H : a < b) : ∃ x, a + 1 + x = b -:= le_elim H - -theorem lt_le {a b : Nat} (H : a < b) : a ≤ b -:= obtain (w : Nat) (Hw : a + 1 + w = b), from (le_elim H), - le_intro (calc a + (1 + w) = a + 1 + w : symm (add_assoc _ _ _) - ... = b : Hw) - -theorem lt_ne {a b : Nat} (H : a < b) : a ≠ b -:= not_intro (λ H1 : a = b, - obtain (w : Nat) (Hw : a + 1 + w = b), from (lt_elim H), - absurd (calc w + 1 = 1 + w : add_comm _ _ - ... = 0 : - add_injr (calc b + (1 + w) = b + 1 + w : symm (add_assoc b 1 w) - ... = a + 1 + w : { symm H1 } - ... = b : Hw - ... = b + 0 : symm (add_zeror b))) - (succ_nz w)) - -theorem lt_nrefl (a : Nat) : ¬ a < a -:= not_intro (λ H : a < a, - absurd (refl a) (lt_ne H)) - -theorem lt_trans {a b c : Nat} (H1 : a < b) (H2 : b < c) : a < c -:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1), - obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2), - lt_intro (calc a + 1 + (w1 + 1 + w2) = a + 1 + (w1 + (1 + w2)) : { add_assoc w1 1 w2 } - ... = (a + 1 + w1) + (1 + w2) : symm (add_assoc _ _ _) - ... = b + (1 + w2) : { Hw1 } - ... = b + 1 + w2 : symm (add_assoc _ _ _) - ... = c : Hw2) - -theorem lt_le_trans {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c -:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1), - obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2), - lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : symm (add_assoc _ _ _) - ... = b + w2 : { Hw1 } - ... = c : Hw2) - -theorem le_lt_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 + 1 + w2 = c), from (lt_elim H2), - lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2 : symm (add_assoc _ _ _) - ... = a + (1 + w1) + w2 : { add_assoc a 1 w1 } - ... = a + (w1 + 1) + w2 : { add_comm 1 w1 } - ... = a + w1 + 1 + w2 : { symm (add_assoc a w1 1) } - ... = b + 1 + w2 : { Hw1 } - ... = c : Hw2) - -theorem ne_lt_succ {a b : Nat} (H1 : a ≠ b) (H2 : a < b + 1) : a < b -:= obtain (w : Nat) (Hw : a + 1 + w = b + 1), from (lt_elim H2), - let L : a + w = b := add_injl (calc a + w + 1 = a + (w + 1) : add_assoc _ _ _ - ... = a + (1 + w) : { add_comm _ _ } - ... = a + 1 + w : symm (add_assoc _ _ _) - ... = b + 1 : Hw) - in discriminate (λ Hz : w = 0, absurd_elim (a < b) (calc a = a + 0 : symm (add_zeror _) - ... = a + w : { symm Hz } - ... = b : L) - H1) - (λ (p : Nat) (Hp : w = p + 1), lt_intro (calc a + 1 + p = a + (1 + p) : add_assoc _ _ _ - ... = a + (p + 1) : { add_comm _ _ } - ... = a + w : { symm Hp } - ... = b : L)) - -theorem strong_induction {P : Nat → Bool} (H : ∀ n, (∀ m, m < n → P m) → P n) : ∀ a, P a -:= take a, - let stronger : P a ∧ ∀ m, m < a → P m := - -- we prove a stronger result by regular induction on a - induction_on a - (have P 0 ∧ ∀ m, m < 0 → P m : - let c2 : ∀ m, m < 0 → P m := λ (m : Nat) (Hlt : m < 0), absurd_elim (P m) Hlt (not_lt_0 m), - c1 : P 0 := H 0 c2 - in and_intro c1 c2) - (λ (n : Nat) (iH : P n ∧ ∀ m, m < n → P m), - have P (n + 1) ∧ ∀ m, m < n + 1 → P m : - let iH1 : P n := and_eliml iH, - iH2 : ∀ m, m < n → P m := and_elimr iH, - c2 : ∀ m, m < n + 1 → P m := λ (m : Nat) (Hlt : m < n + 1), - or_elim (em (m = n)) - (λ Heq : m = n, subst iH1 (symm Heq)) - (λ Hne : m ≠ n, iH2 m (ne_lt_succ Hne Hlt)), - c1 : P (n + 1) := H (n + 1) c2 - in and_intro c1 c2) - in and_eliml stronger - -set_opaque add true -set_opaque mul true -set_opaque le true -set_opaque id true -set_opaque ge true -set_opaque lt true -set_opaque gt true -set_opaque id true -end \ No newline at end of file diff --git a/doc/demo/add_assoc.lean b/doc/demo/add_assoc.lean deleted file mode 100644 index 736e70c25..000000000 --- a/doc/demo/add_assoc.lean +++ /dev/null @@ -1,21 +0,0 @@ -import tactic -using Nat - -rewrite_set basic -add_rewrite add_zerol add_succl eq_id : basic - -theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c -:= induction_on a - (have 0 + (b + c) = (0 + b) + c : - by simp basic) - (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), - have (n + 1) + (b + c) = ((n + 1) + b) + c : - by simp basic) - -exit - -check add_zerol -check add_succl -check @eq_id - -print environment 1 \ No newline at end of file diff --git a/doc/demo/congr.lean b/doc/demo/congr.lean deleted file mode 100644 index a0d5d980f..000000000 --- a/doc/demo/congr.lean +++ /dev/null @@ -1,25 +0,0 @@ -rewrite_set simple -add_rewrite and_truer and_truel and_falser and_falsel or_falsel : simple -(* - add_congr_theorem("simple", "and_congr") - add_congr_theorem("simple", "or_congr") -*) - -variables a b c : Nat - -(* -local t = parse_lean([[a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)]]) -local s, pr = simplify(t, "simple") -print(s) -print(pr) -print(get_environment():type_check(pr)) -*) - -exit - -check @and_congr -check @or_congr -check @and_congrr -check @and_congrl -import if_then_else -check @if_congr diff --git a/doc/demo/even.lean b/doc/demo/even.lean deleted file mode 100644 index badf9c228..000000000 --- a/doc/demo/even.lean +++ /dev/null @@ -1,84 +0,0 @@ -import macros -import tactic -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)) - -exit - -rewrite_set basic -add_rewrite distributer eq_id : basic - -theorem EvenPlusEven2 {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 + w2) : by simp basic) - --- 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/doc/demo/goals.txt b/doc/demo/goals.txt deleted file mode 100644 index 5665106fc..000000000 --- a/doc/demo/goals.txt +++ /dev/null @@ -1,49 +0,0 @@ -1- Coq expressivity + Z3 automation -2- "Real" proof objects -3- "Freedom to trust", semantic attachments - (speed) vs (trusted code base size) - Example: (by simp using t1 ... tn) -4- Extensible system (without compromising soundness) -5- Better support for "interactive proofs" - "Proofs with holes" - "Glue" different components - Script language - Extensibility - Proof maintenance - Unreliable automation produces "recipes" for reliable playback -6- Every component is exposed in the script language API -7- Lean is also a platform for implementing your own custom logic - -Status - * Elaboration engine - - Type inference, - - Fill holes by solving typing constraints - - Higher-order unification - - Non-chronological backtracking - - ... - - * Generic bottom-up simplifier - - Extend by providing theorems/axioms - - Support for dependent types - - Predictable/Reliable - - * Tactic framework - - "Glue" different engines - - Standard combinators + - timeout + parallel solving - -Next steps - * Generic tableaux like prover - - Extend by providing set of theorems that should be used as - alpha/beta/delta/gamma rules - - Non-chronological backtracking - - Callbacks: simplifier and decision procedures - - * MCSat - - Model constructing satisfiability calculus. - New SMT engine - - * Independent type/proof checker - - F-star - - * Interface with existing tools: MiniSAT and Z3 diff --git a/doc/demo/kernel.lean b/doc/demo/kernel.lean deleted file mode 100644 index 35111d0b1..000000000 --- a/doc/demo/kernel.lean +++ /dev/null @@ -1,628 +0,0 @@ -import macros - -universe U ≥ 1 -definition TypeU := (Type U) - -variable Bool : Type --- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions -builtin true : Bool -builtin false : Bool - -definition not (a : Bool) := a → false -notation 40 ¬ _ : not - -definition or (a b : Bool) := ¬ a → b -infixr 30 || : or -infixr 30 \/ : or -infixr 30 ∨ : or - -definition and (a b : Bool) := ¬ (a → ¬ b) -infixr 35 && : and -infixr 35 /\ : and -infixr 35 ∧ : and - -definition implies (a b : Bool) := a → b - -builtin eq {A : (Type U)} (a b : A) : Bool -infix 50 = : eq - -definition neq {A : TypeU} (a b : A) := ¬ (a = b) -infix 50 ≠ : neq - -definition iff (a b : Bool) := a = b -infixr 25 <-> : iff -infixr 25 ↔ : iff - --- The Lean parser has special treatment for the constant exists. --- It allows us to write --- exists x y : A, P x y and ∃ x y : A, P x y --- as syntax sugar for --- exists A (fun x : A, exists A (fun y : A, P x y)) --- That is, it treats the exists as an extra binder such as fun and forall. --- It also provides an alias (Exists) that should be used when we --- want to treat exists as a constant. -definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x, ¬ (P x)) - -definition nonempty (A : TypeU) := ∃ x : A, true - --- If we have an element of type A, then A is nonempty -theorem nonempty_intro {A : TypeU} (a : A) : nonempty A -:= assume H : (∀ x, ¬ true), (H a) - -theorem em (a : Bool) : a ∨ ¬ a -:= assume Hna : ¬ a, Hna - -axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a - -axiom refl {A : TypeU} (a : A) : a = a - -axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b - --- Function extensionality -axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g - --- Forall extensionality -axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x) - --- Epsilon (Hilbert's operator) -variable eps {A : TypeU} (H : nonempty A) (P : A → Bool) : A -alias ε : eps -axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P (ε H P) - --- Proof irrelevance -axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 - -theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (nonempty_intro a) P) -:= assume H : P a, @eps_ax A (nonempty_intro a) P a H - --- Alias for subst where we can provide P explicitly, but keep A,a,b implicit -theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b -:= subst H1 H2 - --- We will mark not as opaque later -theorem not_intro {a : Bool} (H : a → false) : ¬ a -:= H - -theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f -:= funext (λ x : A, refl (f x)) - --- create default rewrite rule set -(* mk_rewrite_rule_set() *) - -theorem trivial : true -:= refl true - -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 - -infixl 100 <| : eqmp -infixl 100 ◂ : eqmp - -theorem boolcomplete (a : Bool) : a = true ∨ a = false -:= case (λ x, x = true ∨ x = false) trivial trivial a - -theorem false_elim (a : Bool) (H : false) : a -:= case (λ x, x) trivial H a - -theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c -:= assume Ha, H2 (H1 Ha) - -theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c -:= assume Ha, H2 ◂ (H1 Ha) - -theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c -:= assume Ha, H2 (H1 ◂ Ha) - -theorem not_not_eq (a : Bool) : ¬ ¬ a ↔ a -:= case (λ x, ¬ ¬ x ↔ x) trivial trivial a - -theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a -:= (not_not_eq a) ◂ H - -theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a -:= assume Ha : a, absurd (H1 Ha) H2 - -theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a -:= assume Hnb : ¬ b, mt H Hnb - -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} (Hnab : ¬ (a → b)) : a -:= not_not_elim - (have ¬ ¬ a : - assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna) - Hnab) - -theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b -:= assume Hb : b, absurd (assume Ha : a, Hb) - H - -theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b -:= H1 H2 - --- Recall that and is defined as ¬ (a → ¬ b) -theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b -:= assume H : a → ¬ b, absurd H2 (H H1) - -theorem and_eliml {a b : Bool} (H : a ∧ b) : a -:= not_imp_eliml H - -theorem and_elimr {a b : Bool} (H : a ∧ b) : b -:= not_not_elim (not_imp_elimr H) - --- Recall that or is defined as ¬ a → b -theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b -:= assume H1 : ¬ a, absurd_elim b H H1 - -theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b -:= assume H1 : ¬ a, 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 -:= 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 eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a -:= (symm H1) ◂ H2 - -theorem trans {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 eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c -:= subst H2 (symm H1) - -theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c -:= subst H1 H2 - -theorem eqt_elim {a : Bool} (H : a = true) : a -:= (symm H) ◂ trivial - -theorem eqf_elim {a : Bool} (H : a = false) : ¬ a -:= not_intro (λ Ha : a, H ◂ Ha) - -theorem congr1 {A B : TypeU} {f g : A → B} (a : A) (H : f = g) : f a = g a -:= substp (fun h : A → B, f a = h a) (refl (f a)) H - -theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b -:= substp (fun x : A, f a = f x) (refl (f a)) H - -theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b -:= subst (congr2 f H2) (congr1 b H1) - --- Recall that exists is defined as ¬ ∀ x : A, ¬ P x -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 (take a : A, mt (assume H : P a, H2 a H) R) - H1) - -theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P -:= assume H1 : (∀ x : A, ¬ P x), - absurd H (H1 a) - -theorem nonempty_elim {A : TypeU} (H1 : nonempty A) {B : Bool} (H2 : A → B) : B -:= obtain (w : A) (Hw : true), from H1, - H2 w - -theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A -:= obtain (w : A) (Hw : P w), from H, - exists_intro w trivial - -theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P) -:= obtain (w : A) (Hw : P w), from H, - eps_ax (nonempty_ex_intro H) w Hw - -theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) -:= exists_intro - (λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y)) -- witness for f - (λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x) - -theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b -:= or_elim (boolcomplete a) - (λ Hat : a = true, or_elim (boolcomplete b) - (λ Hbt : b = true, trans Hat (symm Hbt)) - (λ Hbf : b = false, false_elim (a = b) (subst (Hab (eqt_elim Hat)) Hbf))) - (λ Haf : a = false, or_elim (boolcomplete b) - (λ Hbt : b = true, false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf)) - (λ Hbf : b = false, trans Haf (symm Hbf))) - -theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b -:= boolext Hab Hba - -theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b -:= (λ Ha : a, eqmp H Ha) - -theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a -:= (λ Hb : b, eqmpr H Hb) - -theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} : - (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) -:= iff_intro - (λ H : (∀ x, ∃ y, P x y), axiom_of_choice H) - (λ H : (∃ f, (∀ x, P x (f x))), - take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H, - exists_intro (fw x) (Hw x)) - -theorem eqt_intro {a : Bool} (H : a) : a = true -:= boolext (assume H1 : a, trivial) - (assume H2 : true, H) - -theorem eqf_intro {a : Bool} (H : ¬ a) : a = false -:= boolext (assume H1 : a, absurd H1 H) - (assume H2 : false, false_elim a H2) - -theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false -:= eqf_intro H - -theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true -:= eqt_intro (refl a) - -theorem iff_id (a : Bool) : (a ↔ a) ↔ true -:= eqt_intro (refl a) - -theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a) -:= boolext (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) -:= boolext (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 or_id (a : Bool) : a ∨ a ↔ a -:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2)) - (assume H, or_introl H a) - -theorem or_falsel (a : Bool) : a ∨ false ↔ a -:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2)) - (assume H, or_introl H false) - -theorem or_falser (a : Bool) : false ∨ a ↔ a -:= trans (or_comm false a) (or_falsel a) - -theorem or_truel (a : Bool) : true ∨ a ↔ true -:= eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a) - -theorem or_truer (a : Bool) : a ∨ true ↔ true -:= trans (or_comm a true) (or_truel a) - -theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true -:= eqt_intro (em a) - -theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a -:= boolext (assume H, and_intro (and_elimr H) (and_eliml H)) - (assume H, and_intro (and_elimr H) (and_eliml H)) - -theorem and_id (a : Bool) : a ∧ a ↔ a -:= boolext (assume H, and_eliml H) - (assume H, and_intro H H) - -theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) -:= boolext (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 and_truer (a : Bool) : a ∧ true ↔ a -:= boolext (assume H : a ∧ true, and_eliml H) - (assume H : a, and_intro H trivial) - -theorem and_truel (a : Bool) : true ∧ a ↔ a -:= trans (and_comm true a) (and_truer a) - -theorem and_falsel (a : Bool) : a ∧ false ↔ false -:= boolext (assume H, and_elimr H) - (assume H, false_elim (a ∧ false) H) - -theorem and_falser (a : Bool) : false ∧ a ↔ false -:= trans (and_comm false a) (and_falsel a) - -theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false -:= boolext (assume H, absurd (and_eliml H) (and_elimr H)) - (assume H, false_elim (a ∧ ¬ a) H) - -theorem imp_truer (a : Bool) : (a → true) ↔ true -:= case (λ x, (x → true) ↔ true) trivial trivial a - -theorem imp_truel (a : Bool) : (true → a) ↔ a -:= case (λ x, (true → x) ↔ x) trivial trivial a - -theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a -:= refl _ - -theorem imp_falsel (a : Bool) : (false → a) ↔ true -:= case (λ x, (false → x) ↔ true) trivial trivial a - -theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b -:= iff_intro - (assume H : a → b, - (or_elim (em a) - (λ Ha : a, or_intror (¬ a) (H Ha)) - (λ Hna : ¬ a, or_introl Hna b))) - (assume H : ¬ a ∨ b, - assume Ha : a, - resolve1 H ((symm (not_not_eq a)) ◂ Ha)) - -theorem not_true : ¬ true ↔ false -:= trivial - -theorem not_false : ¬ false ↔ true -:= trivial - -theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b -:= not_not_eq (a = b) - -theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b -:= (not_neq a b) ◂ H - -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 not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b -:= (not_and a b) ◂ H - -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 not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b -:= (not_or a b) ◂ H - -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 not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b -:= (not_iff a b) ◂ H - -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 not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b -:= (not_implies a b) ◂ H - -theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b -:= congr2 not H - -theorem exists_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∃ x : A, p) ↔ p -:= iff_intro - (assume Hl : (∃ x : A, p), - obtain (w : A) (Hw : p), from Hl, - Hw) - (assume Hr : p, - nonempty_elim H (λ w, exists_intro w Hr)) - -theorem forall_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∀ x : A, p) ↔ p -:= iff_intro - (assume Hl : (∀ x : A, p), - nonempty_elim H (λ w, Hl w)) - (assume Hr : p, - take x, Hr) - -theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x) -:= congr2 (Exists A) (funext H) - -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 (allext (λ x : A, symm (not_not_eq (P x)))) - ... = ∃ x : A, ¬ P x : refl (∃ x : A, ¬ P x) - -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 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 not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x -:= (not_exists A P) ◂ 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), - 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 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), - exists_elim H2 - (λ (w : A) (Hw : w ≠ a ∧ P w), - exists_intro w (and_elimr Hw))) - -theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ↔ (P a ∨ (∃ x : A, x ≠ a ∧ P x)) -:= boolext (assume H : (∃ x : A, P x), exists_unfold1 a H) - (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H) - - --- Remark: ordered rewriting + assoc + comm + left_comm sorts a term lexicographically -theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) : - ∀ x y z, R x (R y z) = R y (R x z) -:= take x y z, calc R x (R y z) = R (R x y) z : symm (assoc x y z) - ... = R (R y x) z : { comm x y } - ... = R y (R x z) : assoc y x z - -theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) -:= left_comm and_comm and_assoc a b c - -theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) -:= left_comm or_comm or_assoc a b c - --- Congruence theorems for contextual simplification - --- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then --- b to d using the fact that c is true -theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d) -:= or_elim (em b) - (λ H_b : b, - or_elim (em c) - (λ H_c : c, - calc (a → b) = (a → true) : { eqt_intro H_b } - ... = true : imp_truer a - ... = (c → true) : symm (imp_truer c) - ... = (c → b) : { symm (eqt_intro H_b) } - ... = (c → d) : { H_bd H_c }) - (λ H_nc : ¬ c, - calc (a → b) = (a → true) : { eqt_intro H_b } - ... = true : imp_truer a - ... = (false → d) : symm (imp_falsel d) - ... = (c → d) : { symm (eqf_intro H_nc) })) - (λ H_nb : ¬ b, - or_elim (em c) - (λ H_c : c, - calc (a → b) = (c → b) : { H_ac H_nb } - ... = (c → d) : { H_bd H_c }) - (λ H_nc : ¬ c, - calc (a → b) = (c → b) : { H_ac H_nb } - ... = (false → b) : { eqf_intro H_nc } - ... = true : imp_falsel b - ... = (false → d) : symm (imp_falsel d) - ... = (c → d) : { symm (eqf_intro H_nc) })) - - --- Simplify a → b, by first simplifying b to d using the fact that a is true, and then --- b to d using the fact that ¬ d is true. --- This kind of congruence seems to be useful in very rare cases. -theorem imp_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : (a → b) = (c → d) -:= or_elim (em a) - (λ H_a : a, - or_elim (em d) - (λ H_d : d, - calc (a → b) = (a → d) : { H_bd H_a } - ... = (a → true) : { eqt_intro H_d } - ... = true : imp_truer a - ... = (c → true) : symm (imp_truer c) - ... = (c → d) : { symm (eqt_intro H_d) }) - (λ H_nd : ¬ d, - calc (a → b) = (c → b) : { H_ac H_nd } - ... = (c → d) : { H_bd H_a })) - (λ H_na : ¬ a, - or_elim (em d) - (λ H_d : d, - calc (a → b) = (false → b) : { eqf_intro H_na } - ... = true : imp_falsel b - ... = (c → true) : symm (imp_truer c) - ... = (c → d) : { symm (eqt_intro H_d) }) - (λ H_nd : ¬ d, - calc (a → b) = (false → b) : { eqf_intro H_na } - ... = true : imp_falsel b - ... = (false → d) : symm (imp_falsel d) - ... = (a → d) : { symm (eqf_intro H_na) } - ... = (c → d) : { H_ac H_nd })) - --- (Common case) simplify a to c, and then b to d using the fact that c is true -theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d) -:= imp_congrr (λ H, H_ac) H_bd - --- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b -theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d -:= imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd -theorem or_congrl {a b c d : Bool} (H_bd : ∀ (H_na : ¬ a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : a ∨ b ↔ c ∨ d -:= imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) --- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true -theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d -:= or_congrr (λ H, H_ac) H_bd - --- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b) -theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d -:= congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))) -theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_d : d), a = c) : a ∧ b ↔ c ∧ d -:= congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd))) --- (Common case) simplify a to c, and then b to d using the fact that c is true -theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d -:= and_congrr (λ H, H_ac) H_bd - -theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) -:= boolext - (assume H : (∀ x, p ∨ φ x), - or_elim (em p) - (λ Hp : p, or_introl Hp (∀ x, φ x)) - (λ Hnp : ¬ p, or_intror p (take x, - resolve1 (H x) Hnp))) - (assume H : (p ∨ ∀ x, φ x), - take x, - or_elim H - (λ H1 : p, or_introl H1 (φ x)) - (λ H2 : (∀ x, φ x), or_intror p (H2 x))) - -theorem forall_or_distributel {A : Type} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p) -:= calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p) - ... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ - ... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x) - -theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) -:= boolext - (assume H : (∀ x, φ x ∧ ψ x), - and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x))) - (assume H : (∀ x, φ x) ∧ (∀ x, ψ x), - take x, and_intro (and_eliml H x) (and_elimr H x)) - -theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ↔ p ∧ ∃ x, φ x -:= boolext - (assume H : (∃ x, p ∧ φ x), - obtain (w : A) (Hw : p ∧ φ w), from H, - and_intro (and_eliml Hw) (exists_intro w (and_elimr Hw))) - (assume H : (p ∧ ∃ x, φ x), - obtain (w : A) (Hw : φ w), from (and_elimr H), - exists_intro w (and_intro (and_eliml H) Hw)) - -theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p -:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p) - ... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ - ... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x) - -theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x) -:= boolext - (assume H : (∃ x, φ x ∨ ψ x), - obtain (w : A) (Hw : φ w ∨ ψ w), from H, - or_elim Hw - (λ Hw1 : φ w, or_introl (exists_intro w Hw1) (∃ x, ψ x)) - (λ Hw2 : ψ w, or_intror (∃ x, φ x) (exists_intro w Hw2))) - (assume H : (∃ x, φ x) ∨ (∃ x, ψ x), - or_elim H - (λ H1 : (∃ x, φ x), - obtain (w : A) (Hw : φ w), from H1, - exists_intro w (or_introl Hw (ψ w))) - (λ H2 : (∃ x, ψ x), - obtain (w : A) (Hw : ψ w), from H2, - exists_intro w (or_intror (φ w) Hw))) - - -theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x)) -:= calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x) : eq_exists_intro (λ x, imp_or (φ x) (ψ x)) - ... = (∃ x, ¬ φ x) ∨ (∃ x, ψ x) : exists_or_distribute _ _ - ... = ¬ (∀ x, φ x) ∨ (∃ x, ψ x) : { symm (not_forall A φ) } - ... = (∀ x, φ x) → (∃ x, ψ x) : symm (imp_or _ _) - -set_opaque exists true -set_opaque not true -set_opaque or true -set_opaque and true -set_opaque implies true \ No newline at end of file diff --git a/doc/demo/monitor.lean b/doc/demo/monitor.lean deleted file mode 100644 index f4ff64c69..000000000 --- a/doc/demo/monitor.lean +++ /dev/null @@ -1,36 +0,0 @@ -rewrite_set simple -add_rewrite Nat::add_comm Nat::add_left_comm Nat::add_assoc Nat::add_zeror : simple -variables a b c : Nat - -(* - function indent(s) - for i = 1, s:depth()-1 do - io.write(" ") - end - end - local m = simplifier_monitor(function(s, e) - indent(s) - print("Visit, depth: " .. s:depth() .. ", " .. tostring(e)) - end, - function(s, e, new_e, pr) - indent(s) - print("Step: " .. tostring(e) .. " ===> " .. tostring(new_e)) - end, - function(s, e, new_e, ceq, ceq_id) - -- if ceq_id == name("Nat", "add_assoc") then - indent(s) - print("Rewrite using: " .. tostring(ceq_id)) - indent(s) - print(" " .. tostring(e) .. " ===> " .. tostring(new_e)) - -- end - end - ) - local s = simplifier("simple", options(), m) - local t = parse_lean('a + (b + 0) + a') - print(t) - print("=====>") - local t2, pr = s(t) - print(t2) - print(pr) - get_environment():type_check(pr) -*) diff --git a/doc/demo/mul_succl.lean b/doc/demo/mul_succl.lean deleted file mode 100644 index e35857e94..000000000 --- a/doc/demo/mul_succl.lean +++ /dev/null @@ -1,59 +0,0 @@ -import tactic -using Nat - -rewrite_set basic -add_rewrite add_zerol add_succl eq_id : basic - -theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) -:= induction_on a - (have (0 + b) + c = 0 + (b + c) : - by simp basic) - (λ (n : Nat) (iH : (n + b) + c = n + (b + c)), - have ((n + 1) + b) + c = (n + 1) + (b + c) : - by simp basic) - -check add_zerol -check add_succl -check @eq_id - --- print environment 1 - -add_rewrite add_assoc add_comm mul_zeror mul_zerol mul_succr : basic - -theorem mul_succl_1 (a b : Nat) : (a + 1) * b = a * b + b -:= induction_on b - (have (a + 1) * 0 = a * 0 + 0 : - by simp basic) - (λ (n : Nat) (iH : (a + 1) * n = a * n + n), - have (a + 1) * (n + 1) = a * (n + 1) + (n + 1) : - by simp basic) - -exit - -rewrite_set first_pass -add_rewrite mul_succr eq_id : first_pass - -rewrite_set sort_add -add_rewrite add_assoc add_comm add_left_comm eq_id : sort_add - -theorem mul_succl_2 (a b : Nat) : (a + 1) * b = a * b + b -:= induction_on b - (have (a + 1) * 0 = a * 0 + 0 : - by simp basic) - (λ (n : Nat) (iH : (a + 1) * n = a * n + n), - have (a + 1) * (n + 1) = a * (n + 1) + (n + 1) : - by Then (simp first_pass) (simp sort_add)) - - - -exit - - -theorem mul_succl_3 (a b : Nat) : (a + 1) * b = a * b + b -:= induction_on b - (have (a + 1) * 0 = a * 0 + 0 : - by simp basic) - (λ (n : Nat) (iH : (a + 1) * n = a * n + n), - calc (a + 1) * (n + 1) = (a * n + n) + (a + 1) : by simp first_pass - ... = (a * n + a) + (n + 1) : by simp sort_add - ... = a * (n + 1) + (n + 1) : by simp first_pass) \ No newline at end of file diff --git a/doc/demo/nnf.lean b/doc/demo/nnf.lean deleted file mode 100644 index 518b40f50..000000000 --- a/doc/demo/nnf.lean +++ /dev/null @@ -1,17 +0,0 @@ -rewrite_set NNF -add_rewrite not_not_eq not_true not_false not_neq not_and not_or not_iff not_implies not_forall - not_exists forall_and_distribute exists_and_distributer exists_and_distributel : NNF - -variable p : Nat → Nat → Bool -variable f : Nat → Nat -variable g : Nat → Nat → Nat - -(* -local t1 = parse_lean('¬ ∀ x, (∃ y, p x y ∨ p (f x) (f y)) ∨ f 0 = 1') -local t2, pr = simplify(t1, "NNF") -print(t1) -print("====>") -print(t2) --- print(pr) -get_environment():type_check(pr) -*) diff --git a/doc/demo/reflif.lean b/doc/demo/reflif.lean deleted file mode 100644 index e4f27c129..000000000 --- a/doc/demo/reflif.lean +++ /dev/null @@ -1,20 +0,0 @@ -import macros - -scope - 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 - - theorem ReflIf (Linked : ∀ x, ∃ y, R x y) : ∀ x, R x x := - take x, obtain (w : A) (Hw : R x w), from Linked x, - let lemma1 : R w x := Symm Hw - in Trans Hw lemma1 - - theorem ReflIf2 (Linked : ∀ x, ∃ y, R x y) : ∀ x, R x x := - λ x, exists_elim (Linked x) - (λ w Hw, - Trans Hw (Symm Hw)) -end - -print environment 1 diff --git a/doc/demo/set.lean b/doc/demo/set.lean deleted file mode 100644 index 17d310a3f..000000000 --- a/doc/demo/set.lean +++ /dev/null @@ -1,33 +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, - have x ∈ s3 : - 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 (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)) - -exit - -theorem subset_trans2 {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 -:= λ x Hin, H2 x (H1 x Hin) - -theorem subset_antisym2 {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2 -:= funext (λ x, iff_intro (H1 x) (H2 x)) diff --git a/doc/demo/subst.lean b/doc/demo/subst.lean deleted file mode 100644 index a13a42f69..000000000 --- a/doc/demo/subst.lean +++ /dev/null @@ -1,9 +0,0 @@ -variable q : Nat → Bool -variable f : Nat → Nat → Nat - -theorem T1 (a b : Nat) (H1 : a = b) (H2 : q (f (f a a) (f a a))) : q (f (f a b) (f a a)) -:= subst H2 H1 - -check @subst -set_option pp::implicit true -print environment 1 diff --git a/doc/demo/tc.lean b/doc/demo/tc.lean deleted file mode 100644 index e360d91ef..000000000 --- a/doc/demo/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, - have R⁺ a b : - 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, - have P a b : H P Hrefl Htrans Hsub