doc(examples/lean): new examples

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/lean/principia.lean

@@ -0,0 +1,57 @@
+import macros
+
+-- Some theorems from Pricipia Mathematica
+theorem p1 {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 p2 {A : TypeU} (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)   : p1 p φ
+                  ...  = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
+
+theorem p3 {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 p4 {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 p5 {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)) : p4 p φ
+                 ...   = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x)
+
+theorem p6 {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)))