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

refactor(library/logic/heq): minor change

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-30 13:52:34 -08:00
parent c08f4672e4
commit f24eed50af
2 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/logic/cast.lean
View file

@ -29,9 +29,6 @@ namespace heq
theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b :=
drec_on H !cast_eq
theorem elim {D : Type} (H₁ : a == b) (H₂ : ∀ (Hab : A = B), cast Hab a = b → D) : D :=
H₂ (type_eq H₁) (to_cast_eq H₁)
end heq
section

16
library/logic/heq.lean
View file

@ -10,6 +10,15 @@ infixl `==`:50 := heq
namespace heq
universe variable u
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
definition to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
definition elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
eq.rec_on (to_eq H₁) H₂
theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
@ -17,7 +26,7 @@ namespace heq
rec_on H₁ H₂
theorem symm (H : a == b) : b == a :=
subst H (refl a)
rec_on H (refl a)
definition type_eq (H : a == b) : A = B :=
heq.rec_on H (eq.refl A)
@ -25,11 +34,6 @@ namespace heq
theorem from_eq (H : a = a') : a == a' :=
eq.subst H (refl a)
definition to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
subst H₂ H₁