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

doc(examples/lean): update notation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-16 04:52:45 -08:00
parent 2ce245d68e
commit fd8a1266d0
1 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
examples/lean/tc.lean
View file

@ -9,26 +9,27 @@ infix 50 ⊆ : subrelation
-- We define it as the intersection of all transitive relations containing R -- We define it as the intersection of all transitive relations containing R
definition tcls {A : TypeU} (R : A → A → Bool) (a b : A) definition tcls {A : TypeU} (R : A → A → Bool) (a b : A)
:= ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → P a b := ∀ 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} (H1 : tcls R a b) (H2 : tcls R b c) : tcls R a c 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, := take P, assume Hrefl Htrans Hsub,
let Pab : P a b := H1 P Hrefl Htrans Hsub, let Pab : P a b := Hab P Hrefl Htrans Hsub,
Pbc : P b c := H2 P Hrefl Htrans Hsub Pbc : P b c := Hbc P Hrefl Htrans Hsub
in Htrans a b c Pab Pbc in Htrans a b c Pab Pbc
theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, tcls R a a theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, R⁺ a a
:= take a P, assume Hrefl Htrans Hsub, := take a P, assume Hrefl Htrans Hsub,
Hrefl a Hrefl a
theorem tcls_sub {A : TypeU} {R : A → A → Bool} {a b : A} (H : R a b) : tcls R a b theorem tcls_sub {A : TypeU} {R : A → A → Bool} {a b : A} (H : R a b) : R⁺ a b
:= take P, assume Hrefl Htrans Hsub, := take P, assume Hrefl Htrans Hsub,
Hsub a b H Hsub a b H
theorem tcls_step {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : R a b) (H2 : tcls R b c) : tcls R a c 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, := take P, assume Hrefl Htrans Hsub,
Htrans a b c (Hsub a b H1) (H2 P 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) → (tcls R ⊆ P) 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 P, assume Hrefl Htrans Hsub,
take a b, assume H : tcls R a b, take a b, assume H : R⁺ a b,
have P a b : H P Hrefl Htrans Hsub have P a b : H P Hrefl Htrans Hsub