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

fix(types/nat/hott): workaround failed inductions

Browse source
This commit is contained in:
Floris van Doorn 2015-06-25 23:13:47 -04:00
parent 9ef1ae0848
commit 69f91bfd86
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
hott/types/nat/hott.hlean
View file

@ -33,7 +33,7 @@ namespace nat
theorem lt_by_cases_lt {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
(H3 : a > b → P) (H : a < b) : lt.by_cases H1 H2 H3 = H1 H :=
begin
unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
{ esimp, exact ap H1 !is_hprop.elim},
{ exfalso, cases H' with H' H', apply lt.irrefl, exact H' ▸ H, exact lt.asymm H H'}
end
@ -41,7 +41,7 @@ namespace nat
theorem lt_by_cases_eq {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
(H3 : a > b → P) (H : a = b) : lt.by_cases H1 H2 H3 = H2 H :=
begin
unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
{ exfalso, apply lt.irrefl, exact H ▸ H'},
{ cases H' with H' H', esimp, exact ap H2 !is_hprop.elim, exfalso, apply lt.irrefl, exact H ▸ H'}
end
@ -49,7 +49,7 @@ namespace nat
theorem lt_by_cases_ge {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
(H3 : a > b → P) (H : a > b) : lt.by_cases H1 H2 H3 = H3 H :=
begin
unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
{ exfalso, exact lt.asymm H H'},
{ cases H' with H' H', exfalso, apply lt.irrefl, exact H' ▸ H, esimp, exact ap H3 !is_hprop.elim}
end
@ -61,7 +61,8 @@ namespace nat
theorem lt_ge_by_cases_ge {n m : ℕ} {P : Type} (H1 : n < m → P) (H2 : n ≥ m → P)
(H : n ≥ m) : lt_ge_by_cases H1 H2 = H2 H :=
begin
unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H',
unfold [lt_ge_by_cases,lt.by_cases], generalize (lt.trichotomy n m),
intro X, induction X with H' H',
{ exfalso, apply lt.irrefl, exact lt_of_le_of_lt H H'},
{ cases H' with H' H'; all_goals (esimp; apply ap H2 !is_hprop.elim)}
end
@ -70,7 +71,8 @@ namespace nat
(H : n ≤ m) (Heq : Π(p : n = m), H1 (le_of_eq p) = H2 (le_of_eq p⁻¹))
: lt_ge_by_cases (λH', H1 (le_of_lt H')) H2 = H1 H :=
begin
unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H',
unfold [lt_ge_by_cases,lt.by_cases], generalize (lt.trichotomy n m),
intro X, induction X with H' H',
{ esimp, apply ap H1 !is_hprop.elim},
{ cases H' with H' H',
esimp, exact !Heq⁻¹ ⬝ ap H1 !is_hprop.elim,