michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(examples/lean): rename examples

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-26 16:00:42 -08:00
parent f1b97b18b4
commit 7eaade4ceb
2 changed files with 12 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
examples/lean/macros.lean
View file

@ -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

34
examples/lean/set.lean
View file

@ -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