From 7eaade4ceb0e0e57dce7b3ee7bcd584b34d9a96b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Dec 2013 16:00:42 -0800
Subject: [PATCH] chore(examples/lean): rename examples

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/lean/macros.lean | 20 --------------------
 examples/lean/set.lean    | 34 ++++++++++++----------------------
 2 files changed, 12 insertions(+), 42 deletions(-)
 delete mode 100644 examples/lean/macros.lean

diff --git a/examples/lean/macros.lean b/examples/lean/macros.lean
deleted file mode 100644
index 6725034b6..000000000
--- a/examples/lean/macros.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-(**
--- import macros for, assume, mp, ...
-import("macros.lua")
-**)
-
-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 SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 :=
-   for s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3),
-      show s1 ⊆ s3,
-        for x, assume Hin : x ∈ s1,
-           show x ∈ s3,
-             let L1 : x ∈ s2 := mp (instantiate H1 x) Hin
-             in mp (instantiate H2 x) L1
diff --git a/examples/lean/set.lean b/examples/lean/set.lean
index ccaf4259a..6725034b6 100644
--- a/examples/lean/set.lean
+++ b/examples/lean/set.lean
@@ -1,3 +1,8 @@
+(**
+-- import macros for, assume, mp, ...
+import("macros.lua")
+**)
+
 Definition Set (A : Type) : Type := A → Bool
 
 Definition element {A : Type} (x : A) (s : Set A) := s x
@@ -6,25 +11,10 @@ Infix 60 ∈ : element
 Definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 ⇒ x ∈ s2
 Infix 50 ⊆ : subset
 
-Theorem SubsetProp {A : Type} {s1 s2 : Set A} {x : A} (H1 : s1 ⊆ s2) (H2 : x ∈ s1) : x ∈ s2 :=
-   MP (ForallElim H1 x) H2
-
-Theorem SubsetTrans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 :=
-   ForallIntro (λ x,
-       Discharge (λ Hin : x ∈ s1,
-          let L1 : x ∈ s2 := SubsetProp H1 Hin,
-              L2 : x ∈ s3 := SubsetProp H2 L1
-          in  L2)).
-
-Definition transitive {A : Type} (R : A → A → Bool) := ∀ x y z, R x y ⇒ R y z ⇒ R x z
-
-Theorem SubsetTrans2 {A : Type} : transitive (@subset A) :=
-   ForallIntro (λ s1, ForallIntro (λ s2, ForallIntro (λ s3,
-      Discharge (λ H1, (Discharge (λ H2,
-         SubsetTrans H1 H2)))))).
-
-Theorem SubsetRefl {A : Type} (s : Set A) : s ⊆ s :=
-   ForallIntro (λ x, Discharge (λ H : x ∈ s, H))
-
-Definition union {A : Type} (s1 : Set A) (s2 : Set A) := λ x, x ∈ s1 ∨ x ∈ s2
-Infix 55 ∪ : union
+Theorem SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 :=
+   for s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3),
+      show s1 ⊆ s3,
+        for x, assume Hin : x ∈ s1,
+           show x ∈ s3,
+             let L1 : x ∈ s2 := mp (instantiate H1 x) Hin
+             in mp (instantiate H2 x) L1