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

feat(library/standard/cast): add dcongr2 theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-22 05:58:58 -07:00
parent a9f7d87aae
commit b7838f5db7
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/standard/cast.lean
View file

@ -82,6 +82,15 @@ theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc
... == a : cast_heq Hab a ... == a : cast_heq Hab a
... == cast (trans Hab Hbc) a : hsymm (cast_heq (trans Hab Hbc) a)) ... == cast (trans Hab Hbc) a : hsymm (cast_heq (trans Hab Hbc) a))
theorem dcongr2 {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b
:= have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from
assume H, cast_eq H (f a),
have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from
subst H e1,
have e3 : cast (congr2 B H) (f a) = f b, from
e2 (congr2 B H),
cast_eq_to_heq e3
theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x)
:= subst H (refl (Π x, B x)) := subst H (refl (Π x, B x))