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

chore(hott) fix sum proof by adding manual coercions

Browse source
This commit is contained in:
Jakob von Raumer 2016-03-30 11:43:41 +01:00 committed by Leonardo de Moura
parent a6319118e3
commit 7a9e1c7f4f
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
hott/types/sum.hlean
View file

@ -231,15 +231,15 @@ namespace sum
esimp[unit_sum_equiv_cancel_map], apply sum.rec,
{ intro x, cases x with u Hu, esimp, apply sum.rec,
{ intro x, exfalso, cases x with u' Hu', apply empty_of_inl_eq_inr,
calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
... = H⁻¹ (inl u') : ap H⁻¹ Hu'
... = H⁻¹ (inl u) : {!is_prop.elim}
... = H⁻¹ (H (inr _)) : {Hu⁻¹}
calc inl ⋆ = (to_fun H)⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
... = (to_fun H)⁻¹ (inl u') : ap (to_fun H)⁻¹ Hu'
... = (to_fun H)⁻¹ (inl u) : {!is_prop.elim}
... = (to_fun H)⁻¹ (H (inr _)) : {Hu⁻¹}
... = inr _ : to_left_inv H },
{ intro x, cases x with b' Hb', esimp, cases sum.mem_cases (H⁻¹ (inr b)) with x x,
{ intro x, cases x with b' Hb', esimp, cases sum.mem_cases ((to_fun H)⁻¹ (inr b)) with x x,
{ cases x with u' Hu', cases u', apply eq_of_inr_eq_inr,
calc inr b' = H (inl ⋆) : Hb'⁻¹
... = H (H⁻¹ (inr b)) : (ap (to_fun H) Hu')⁻¹
... = H ((to_fun H)⁻¹ (inr b)) : (ap (to_fun H) Hu')⁻¹
... = inr b : to_right_inv H (inr b)},
{ exfalso, cases x with a Ha, apply empty_of_inl_eq_inr,
cases u, apply concat, apply Hu⁻¹, apply concat, rotate 1, apply !(to_right_inv H),
@ -249,13 +249,13 @@ namespace sum
apply concat, exact x.2⁻¹, apply Ha,
intro x, cases x with a' Ha', esimp, apply eq_of_inr_eq_inr, apply Ha'⁻¹ ⬝ Ha } } },
{ intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ ⬝ _,
cases sum.mem_cases (to_fun H⁻¹ᵉ (inr b)) with x x,
{ cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ᵉ (inl ⋆)) with x x,
cases sum.mem_cases ((to_fun H)⁻¹ (inr b)) with x x,
{ cases x with u Hu, esimp, cases sum.mem_cases ((to_fun H)⁻¹ (inl ⋆)) with x x,
{ cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr,
calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹
calc inl ⋆ = H ((to_fun H)⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹
... = H (inl u') : ap H Hu'
... = H (inl u) : by rewrite [is_prop.elim u' u]
... = H (H⁻¹ᵉ (inr b)) : ap H Hu⁻¹
... = H ((to_fun H)⁻¹ (inr b)) : ap H Hu⁻¹
... = inr b : to_right_inv H (inr b) },
{ cases x with a Ha, exfalso, apply empty_of_inl_eq_inr,
apply concat, rotate 1, exact Hb',
@ -267,8 +267,8 @@ namespace sum
apply !(to_left_inv H)⁻¹ ⬝ Ha'',
intro x, exfalso, cases x with a'' Ha'', apply empty_of_inl_eq_inr,
apply Hu⁻¹ ⬝ Ha'', } },
{ cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H,
exact sorry /-apply Ha'⁻¹-/ } }
{ cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H,
apply Ha'⁻¹ } }
end
definition unit_sum_equiv_cancel : A ≃ B :=