refactor(trunc): rename namespace is_trunc.trunc_index to trunc_index
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
e2b31a9b33
commit
1903601ba5
7 changed files with 239 additions and 228 deletions
|
|
@ -22,7 +22,7 @@ The rows indicate the chapters, the columns the sections.
|
|||
| Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | |
|
||||
| Ch 6 | . | + | + | + | + | ½ | ½ | + | ¾ | ¼ | ¾ | + | . | | |
|
||||
| Ch 7 | + | + | + | - | ¾ | - | - | | | | | | | | |
|
||||
| Ch 8 | ¾ | ¾ | - | - | ¼ | ¼ | - | - | - | - | | | | | |
|
||||
| Ch 8 | + | + | - | - | ¼ | ¼ | - | - | - | - | | | | | |
|
||||
| Ch 9 | ¾ | + | + | ½ | ¾ | ½ | - | - | - | | | | | | |
|
||||
| Ch 10 | - | - | - | - | - | | | | | | | | | | |
|
||||
| Ch 11 | - | - | - | - | - | - | | | | | | | | | |
|
||||
|
|
@ -141,7 +141,7 @@ Chapter 8: Homotopy theory
|
|||
|
||||
Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy.md)
|
||||
|
||||
- 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only one of the proofs)
|
||||
- 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only the encode-decode proof)
|
||||
- 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof)
|
||||
- 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): not formalized
|
||||
- 8.4 (Fiber sequences and the long exact sequence): not formalized
|
||||
|
|
|
|||
|
|
@ -275,7 +275,7 @@ namespace homotopy
|
|||
end
|
||||
|
||||
open trunc_index
|
||||
theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n.-1) (sphere n) :=
|
||||
theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (sphere n) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ apply is_trunc_trunc},
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ The Smash Product of Types
|
|||
|
||||
import hit.pushout .wedge .cofiber .susp .sphere
|
||||
|
||||
open eq pushout prod pointed pType is_trunc
|
||||
open eq pushout prod pointed is_trunc
|
||||
|
||||
definition product_of_wedge [constructor] (A B : Type*) : pwedge A B →* A ×* B :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -74,9 +74,10 @@ namespace sphere_index
|
|||
definition sub_one [reducible] (n : ℕ) : ℕ₋₁ :=
|
||||
nat.rec_on n -1 (λ n k, k.+1)
|
||||
|
||||
postfix `.-1`:(max+1) := sub_one
|
||||
postfix `..-1`:(max+1) := sub_one
|
||||
-- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂)
|
||||
|
||||
definition succ_sub_one (n : ℕ) : (nat.succ n).-1 = n :> ℕ₋₁ :=
|
||||
definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ :=
|
||||
idp
|
||||
|
||||
end sphere_index
|
||||
|
|
@ -85,15 +86,15 @@ open sphere_index
|
|||
namespace trunc_index
|
||||
definition sub_one [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
|
||||
sphere_index.rec_on n -2 (λ n k, k.+1)
|
||||
postfix `.-1`:(max+1) := sub_one
|
||||
postfix `..-1`:(max+1) := sub_one
|
||||
|
||||
definition of_sphere_index [coercion] [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
|
||||
n.-1.+1
|
||||
n..-1.+1
|
||||
|
||||
definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n.-1.-1 :=
|
||||
definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n..-1..-1 :=
|
||||
nat.rec_on n idp (λn p, ap trunc_index.succ p)
|
||||
|
||||
definition succ_sub_one (n : ℕ₋₁) : n.+1.-1 = n :> ℕ₋₂ :=
|
||||
definition succ_sub_one (n : ℕ₋₁) : n.+1..-1 = n :> ℕ₋₂ :=
|
||||
idp
|
||||
|
||||
definition of_sphere_index_of_nat (n : ℕ)
|
||||
|
|
@ -114,6 +115,8 @@ definition sphere : ℕ₋₁ → Type₀
|
|||
|
||||
namespace sphere
|
||||
|
||||
export [notation] [coercion] sphere_index
|
||||
|
||||
definition base {n : ℕ} : sphere n := north
|
||||
definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) :=
|
||||
pointed.mk base
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ The Wedge Sum of Two pType Types
|
|||
-/
|
||||
import hit.pointed_pushout .connectedness
|
||||
|
||||
open eq pushout pointed unit is_trunc.trunc_index pType
|
||||
open eq pushout pointed unit trunc_index
|
||||
|
||||
definition pwedge (A B : Type*) : Type* := ppushout (pconst punit A) (pconst punit B)
|
||||
|
||||
|
|
|
|||
|
|
@ -13,37 +13,40 @@ import .nat .logic .equiv .pathover
|
|||
open eq nat sigma unit sigma.ops
|
||||
--set_option class.force_new true
|
||||
|
||||
namespace is_trunc
|
||||
/- Truncation levels -/
|
||||
|
||||
/- Truncation levels -/
|
||||
inductive trunc_index : Type₀ :=
|
||||
| minus_two : trunc_index
|
||||
| succ : trunc_index → trunc_index
|
||||
|
||||
inductive trunc_index : Type₀ :=
|
||||
| minus_two : trunc_index
|
||||
| succ : trunc_index → trunc_index
|
||||
open trunc_index
|
||||
|
||||
open trunc_index
|
||||
/-
|
||||
notation for trunc_index is -2, -1, 0, 1, ...
|
||||
from 0 and up this comes from a coercion from num to trunc_index (via ℕ)
|
||||
-/
|
||||
|
||||
notation `ℕ₋₂` := trunc_index -- input using \N-2
|
||||
|
||||
definition has_zero_trunc_index [instance] [priority 2000] : has_zero ℕ₋₂ :=
|
||||
has_zero.mk (succ (succ minus_two))
|
||||
|
||||
definition has_one_trunc_index [instance] [priority 2000] : has_one ℕ₋₂ :=
|
||||
has_one.mk (succ (succ (succ minus_two)))
|
||||
|
||||
namespace trunc_index
|
||||
|
||||
/-
|
||||
notation for trunc_index is -2, -1, 0, 1, ...
|
||||
from 0 and up this comes from a coercion from num to trunc_index (via ℕ)
|
||||
-/
|
||||
notation `-1` := trunc_index.succ trunc_index.minus_two -- ISSUE: -1 gets printed as -2.+1?
|
||||
notation `-2` := trunc_index.minus_two
|
||||
postfix `.+1`:(max+1) := trunc_index.succ
|
||||
postfix `.+2`:(max+1) := λn, (n .+1 .+1)
|
||||
notation `ℕ₋₂` := trunc_index -- input using \N-2
|
||||
|
||||
definition has_zero_trunc_index [instance] [priority 2000] : has_zero ℕ₋₂ :=
|
||||
has_zero.mk (succ (succ minus_two))
|
||||
|
||||
definition has_one_trunc_index [instance] [priority 2000] : has_one ℕ₋₂ :=
|
||||
has_one.mk (succ (succ (succ minus_two)))
|
||||
|
||||
namespace trunc_index
|
||||
--addition, where we add two to the result
|
||||
definition add_plus_two [reducible] (n m : ℕ₋₂) : ℕ₋₂ :=
|
||||
trunc_index.rec_on m n (λ k l, l .+1)
|
||||
|
||||
infix ` +2+ `:65 := trunc_index.add_plus_two
|
||||
|
||||
-- addition of trunc_indices, where results smaller than -2 are changed to -2
|
||||
protected definition add (n m : ℕ₋₂) : ℕ₋₂ :=
|
||||
trunc_index.cases_on m
|
||||
|
|
@ -58,15 +61,17 @@ namespace is_trunc
|
|||
| tr_refl : le a a
|
||||
| step : Π {b}, le a b → le a (b.+1)
|
||||
|
||||
end trunc_index
|
||||
end trunc_index
|
||||
|
||||
definition has_le_trunc_index [instance] [priority 2000] : has_le ℕ₋₂ :=
|
||||
has_le.mk trunc_index.le
|
||||
definition has_le_trunc_index [instance] [priority 2000] : has_le ℕ₋₂ :=
|
||||
has_le.mk trunc_index.le
|
||||
|
||||
attribute trunc_index.add [reducible]
|
||||
infix ` +2+ `:65 := trunc_index.add_plus_two
|
||||
definition has_add_trunc_index [instance] [priority 2000] : has_add ℕ₋₂ :=
|
||||
has_add.mk trunc_index.add
|
||||
attribute trunc_index.add [reducible]
|
||||
|
||||
definition has_add_trunc_index [instance] [priority 2000] : has_add ℕ₋₂ :=
|
||||
has_add.mk trunc_index.add
|
||||
|
||||
namespace trunc_index
|
||||
|
||||
definition sub_two [reducible] (n : ℕ) : ℕ₋₂ :=
|
||||
nat.rec_on n -2 (λ n k, k.+1)
|
||||
|
|
@ -77,10 +82,9 @@ namespace is_trunc
|
|||
postfix `.-2`:(max+1) := sub_two
|
||||
postfix `.-1`:(max+1) := λn, (n .-2 .+1)
|
||||
|
||||
definition trunc_index.of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₂ :=
|
||||
definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₂ :=
|
||||
n.-2.+2
|
||||
|
||||
namespace trunc_index
|
||||
definition succ_le_succ {n m : ℕ₋₂} (H : n ≤ m) : n.+1 ≤ m.+1 :=
|
||||
by induction H with m H IH; apply le.tr_refl; exact le.step IH
|
||||
|
||||
|
|
@ -89,7 +93,11 @@ namespace is_trunc
|
|||
protected definition le_refl (n : ℕ₋₂) : n ≤ n :=
|
||||
le.tr_refl n
|
||||
|
||||
end trunc_index
|
||||
end trunc_index open trunc_index
|
||||
|
||||
namespace is_trunc
|
||||
|
||||
export [notation] [coercion] trunc_index
|
||||
|
||||
/- truncated types -/
|
||||
|
||||
|
|
@ -112,7 +120,7 @@ end is_trunc open is_trunc
|
|||
structure is_trunc [class] (n : ℕ₋₂) (A : Type) :=
|
||||
(to_internal : is_trunc_internal n A)
|
||||
|
||||
open nat num is_trunc.trunc_index
|
||||
open nat num trunc_index
|
||||
|
||||
namespace is_trunc
|
||||
|
||||
|
|
|
|||
|
|
@ -11,196 +11,196 @@ Properties of is_trunc and trunctype
|
|||
import .pointed2 ..function algebra.order types.nat.order
|
||||
|
||||
open eq sigma sigma.ops pi function equiv trunctype
|
||||
is_equiv prod is_trunc.trunc_index pointed nat is_trunc algebra
|
||||
is_equiv prod pointed nat is_trunc algebra
|
||||
|
||||
namespace trunc_index
|
||||
|
||||
definition minus_one_le_succ (n : trunc_index) : -1 ≤ n.+1 :=
|
||||
succ_le_succ (minus_two_le n)
|
||||
|
||||
definition zero_le_of_nat (n : ℕ) : 0 ≤ of_nat n :=
|
||||
succ_le_succ !minus_one_le_succ
|
||||
|
||||
open decidable
|
||||
protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₂), decidable (n = m)
|
||||
| has_decidable_eq -2 -2 := inl rfl
|
||||
| has_decidable_eq (n.+1) -2 := inr (by contradiction)
|
||||
| has_decidable_eq -2 (m.+1) := inr (by contradiction)
|
||||
| has_decidable_eq (n.+1) (m.+1) :=
|
||||
match has_decidable_eq n m with
|
||||
| inl xeqy := inl (by rewrite xeqy)
|
||||
| inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney)
|
||||
end
|
||||
|
||||
definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty :=
|
||||
by cases H
|
||||
|
||||
protected definition le_trans {n m k : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
|
||||
begin
|
||||
induction H2 with k H2 IH,
|
||||
{ exact H1},
|
||||
{ exact le.step IH}
|
||||
end
|
||||
|
||||
definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m :=
|
||||
begin
|
||||
cases H with m H',
|
||||
{ apply le.tr_refl},
|
||||
{ exact trunc_index.le_trans (le.step !le.tr_refl) H'}
|
||||
end
|
||||
|
||||
theorem not_succ_le_self {n : ℕ₋₂} : ¬n.+1 ≤ n :=
|
||||
begin
|
||||
induction n with n IH: intro H,
|
||||
{ exact not_succ_le_minus_two H},
|
||||
{ exact IH (le_of_succ_le_succ H)}
|
||||
end
|
||||
|
||||
protected definition le_antisymm {n m : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
|
||||
begin
|
||||
induction H2 with n H2 IH,
|
||||
{ reflexivity},
|
||||
{ exfalso, apply @not_succ_le_self n, exact trunc_index.le_trans H1 H2}
|
||||
end
|
||||
|
||||
protected definition le_succ {n m : ℕ₋₂} (H1 : n ≤ m): n ≤ m.+1 :=
|
||||
le.step H1
|
||||
|
||||
end trunc_index open trunc_index
|
||||
|
||||
definition weak_order_trunc_index [trans_instance] [reducible] : weak_order trunc_index :=
|
||||
weak_order.mk le trunc_index.le_refl @trunc_index.le_trans @trunc_index.le_antisymm
|
||||
|
||||
namespace trunc_index
|
||||
|
||||
/- more theorems about truncation indices -/
|
||||
|
||||
definition zero_add (n : ℕ₋₂) : (0 : ℕ₋₂) + n = n :=
|
||||
begin
|
||||
cases n with n, reflexivity,
|
||||
cases n with n, reflexivity,
|
||||
induction n with n IH, reflexivity, exact ap succ IH
|
||||
end
|
||||
|
||||
definition add_zero (n : ℕ₋₂) : n + (0 : ℕ₋₂) = n :=
|
||||
by reflexivity
|
||||
|
||||
definition succ_add_nat (n : ℕ₋₂) (m : ℕ) : n.+1 + m = (n + m).+1 :=
|
||||
by induction m with m IH; reflexivity; exact ap succ IH
|
||||
|
||||
definition nat_add_succ (n : ℕ) (m : ℕ₋₂) : n + m.+1 = (n + m).+1 :=
|
||||
begin
|
||||
cases m with m, reflexivity,
|
||||
cases m with m, reflexivity,
|
||||
induction m with m IH, reflexivity, exact ap succ IH
|
||||
end
|
||||
|
||||
definition add_nat_succ (n : ℕ₋₂) (m : ℕ) : n + (nat.succ m) = (n + m).+1 :=
|
||||
by reflexivity
|
||||
|
||||
definition nat_succ_add (n : ℕ) (m : ℕ₋₂) : (nat.succ n) + m = (n + m).+1 :=
|
||||
begin
|
||||
cases m with m, reflexivity,
|
||||
cases m with m, reflexivity,
|
||||
induction m with m IH, reflexivity, exact ap succ IH
|
||||
end
|
||||
|
||||
definition sub_two_add_two (n : ℕ₋₂) : sub_two (add_two n) = n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition add_two_sub_two (n : ℕ) : add_two (sub_two n) = n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap nat.succ IH}
|
||||
end
|
||||
|
||||
definition of_nat_add_plus_two_of_nat (n m : ℕ) : n +2+ m = of_nat (n + m + 2) :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition of_nat_add_of_nat (n m : ℕ) : of_nat n + of_nat m = of_nat (n + m) :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition succ_add_plus_two (n m : ℕ₋₂) : n.+1 +2+ m = (n +2+ m).+1 :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition add_plus_two_succ (n m : ℕ₋₂) : n +2+ m.+1 = (n +2+ m).+1 :=
|
||||
idp
|
||||
|
||||
definition add_succ_succ (n m : ℕ₋₂) : n + m.+2 = n +2+ m :=
|
||||
idp
|
||||
|
||||
definition succ_add_succ (n m : ℕ₋₂) : n.+1 + m.+1 = n +2+ m :=
|
||||
begin
|
||||
cases m with m IH,
|
||||
{ reflexivity},
|
||||
{ apply succ_add_plus_two}
|
||||
end
|
||||
|
||||
definition succ_succ_add (n m : ℕ₋₂) : n.+2 + m = n +2+ m :=
|
||||
begin
|
||||
cases m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact !succ_add_succ ⬝ !succ_add_plus_two}
|
||||
end
|
||||
|
||||
definition succ_sub_two (n : ℕ) : (nat.succ n).-2 = n.-2 .+1 := rfl
|
||||
definition sub_two_succ_succ (n : ℕ) : n.-2.+1.+1 = n := rfl
|
||||
definition succ_sub_two_succ (n : ℕ) : (nat.succ n).-2.+1 = n := rfl
|
||||
|
||||
definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
{ apply le.refl},
|
||||
{ exact trunc_index.le_succ IH}
|
||||
end
|
||||
|
||||
definition sub_two_le_sub_two {n m : ℕ} (H : n ≤ m) : n.-2 ≤ m.-2 :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
{ apply le.refl},
|
||||
{ exact trunc_index.le_succ IH}
|
||||
end
|
||||
|
||||
definition add_two_le_add_two {n m : ℕ₋₂} (H : n ≤ m) : add_two n ≤ add_two m :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
{ reflexivity},
|
||||
{ constructor, exact IH},
|
||||
end
|
||||
|
||||
definition le_of_sub_two_le_sub_two {n m : ℕ} (H : n.-2 ≤ m.-2) : n ≤ m :=
|
||||
begin
|
||||
rewrite [-add_two_sub_two n, -add_two_sub_two m],
|
||||
exact add_two_le_add_two H,
|
||||
end
|
||||
|
||||
definition le_of_of_nat_le_of_nat {n m : ℕ} (H : of_nat n ≤ of_nat m) : n ≤ m :=
|
||||
begin
|
||||
apply le_of_sub_two_le_sub_two,
|
||||
exact le_of_succ_le_succ (le_of_succ_le_succ H)
|
||||
end
|
||||
|
||||
end trunc_index open trunc_index
|
||||
|
||||
namespace is_trunc
|
||||
|
||||
namespace trunc_index
|
||||
|
||||
definition minus_one_le_succ (n : trunc_index) : -1 ≤ n.+1 :=
|
||||
succ_le_succ (minus_two_le n)
|
||||
|
||||
definition zero_le_of_nat (n : ℕ) : 0 ≤ of_nat n :=
|
||||
succ_le_succ !minus_one_le_succ
|
||||
|
||||
open decidable
|
||||
protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₂), decidable (n = m)
|
||||
| has_decidable_eq -2 -2 := inl rfl
|
||||
| has_decidable_eq (n.+1) -2 := inr (by contradiction)
|
||||
| has_decidable_eq -2 (m.+1) := inr (by contradiction)
|
||||
| has_decidable_eq (n.+1) (m.+1) :=
|
||||
match has_decidable_eq n m with
|
||||
| inl xeqy := inl (by rewrite xeqy)
|
||||
| inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney)
|
||||
end
|
||||
|
||||
definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty :=
|
||||
by cases H
|
||||
|
||||
protected definition le_trans {n m k : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
|
||||
begin
|
||||
induction H2 with k H2 IH,
|
||||
{ exact H1},
|
||||
{ exact le.step IH}
|
||||
end
|
||||
|
||||
definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m :=
|
||||
begin
|
||||
cases H with m H',
|
||||
{ apply le.tr_refl},
|
||||
{ exact trunc_index.le_trans (le.step !le.tr_refl) H'}
|
||||
end
|
||||
|
||||
theorem not_succ_le_self {n : ℕ₋₂} : ¬n.+1 ≤ n :=
|
||||
begin
|
||||
induction n with n IH: intro H,
|
||||
{ exact not_succ_le_minus_two H},
|
||||
{ exact IH (le_of_succ_le_succ H)}
|
||||
end
|
||||
|
||||
protected definition le_antisymm {n m : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
|
||||
begin
|
||||
induction H2 with n H2 IH,
|
||||
{ reflexivity},
|
||||
{ exfalso, apply @not_succ_le_self n, exact trunc_index.le_trans H1 H2}
|
||||
end
|
||||
|
||||
protected definition le_succ {n m : ℕ₋₂} (H1 : n ≤ m): n ≤ m.+1 :=
|
||||
le.step H1
|
||||
|
||||
end trunc_index open trunc_index
|
||||
|
||||
definition weak_order_trunc_index [trans_instance] [reducible] : weak_order trunc_index :=
|
||||
weak_order.mk le trunc_index.le_refl @trunc_index.le_trans @trunc_index.le_antisymm
|
||||
|
||||
namespace trunc_index
|
||||
|
||||
/- more theorems about truncation indices -/
|
||||
|
||||
definition zero_add (n : ℕ₋₂) : (0 : ℕ₋₂) + n = n :=
|
||||
begin
|
||||
cases n with n, reflexivity,
|
||||
cases n with n, reflexivity,
|
||||
induction n with n IH, reflexivity, exact ap succ IH
|
||||
end
|
||||
|
||||
definition add_zero (n : ℕ₋₂) : n + (0 : ℕ₋₂) = n :=
|
||||
by reflexivity
|
||||
|
||||
definition succ_add_nat (n : ℕ₋₂) (m : ℕ) : n.+1 + m = (n + m).+1 :=
|
||||
by induction m with m IH; reflexivity; exact ap succ IH
|
||||
|
||||
definition nat_add_succ (n : ℕ) (m : ℕ₋₂) : n + m.+1 = (n + m).+1 :=
|
||||
begin
|
||||
cases m with m, reflexivity,
|
||||
cases m with m, reflexivity,
|
||||
induction m with m IH, reflexivity, exact ap succ IH
|
||||
end
|
||||
|
||||
definition add_nat_succ (n : ℕ₋₂) (m : ℕ) : n + (nat.succ m) = (n + m).+1 :=
|
||||
by reflexivity
|
||||
|
||||
definition nat_succ_add (n : ℕ) (m : ℕ₋₂) : (nat.succ n) + m = (n + m).+1 :=
|
||||
begin
|
||||
cases m with m, reflexivity,
|
||||
cases m with m, reflexivity,
|
||||
induction m with m IH, reflexivity, exact ap succ IH
|
||||
end
|
||||
|
||||
definition sub_two_add_two (n : ℕ₋₂) : sub_two (add_two n) = n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition add_two_sub_two (n : ℕ) : add_two (sub_two n) = n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap nat.succ IH}
|
||||
end
|
||||
|
||||
definition of_nat_add_plus_two_of_nat (n m : ℕ) : n +2+ m = of_nat (n + m + 2) :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition of_nat_add_of_nat (n m : ℕ) : of_nat n + of_nat m = of_nat (n + m) :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition succ_add_plus_two (n m : ℕ₋₂) : n.+1 +2+ m = (n +2+ m).+1 :=
|
||||
begin
|
||||
induction m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact ap succ IH}
|
||||
end
|
||||
|
||||
definition add_plus_two_succ (n m : ℕ₋₂) : n +2+ m.+1 = (n +2+ m).+1 :=
|
||||
idp
|
||||
|
||||
definition add_succ_succ (n m : ℕ₋₂) : n + m.+2 = n +2+ m :=
|
||||
idp
|
||||
|
||||
definition succ_add_succ (n m : ℕ₋₂) : n.+1 + m.+1 = n +2+ m :=
|
||||
begin
|
||||
cases m with m IH,
|
||||
{ reflexivity},
|
||||
{ apply succ_add_plus_two}
|
||||
end
|
||||
|
||||
definition succ_succ_add (n m : ℕ₋₂) : n.+2 + m = n +2+ m :=
|
||||
begin
|
||||
cases m with m IH,
|
||||
{ reflexivity},
|
||||
{ exact !succ_add_succ ⬝ !succ_add_plus_two}
|
||||
end
|
||||
|
||||
definition succ_sub_two (n : ℕ) : (nat.succ n).-2 = n.-2 .+1 := rfl
|
||||
definition sub_two_succ_succ (n : ℕ) : n.-2.+1.+1 = n := rfl
|
||||
definition succ_sub_two_succ (n : ℕ) : (nat.succ n).-2.+1 = n := rfl
|
||||
|
||||
definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
{ apply le.refl},
|
||||
{ exact trunc_index.le_succ IH}
|
||||
end
|
||||
|
||||
definition sub_two_le_sub_two {n m : ℕ} (H : n ≤ m) : n.-2 ≤ m.-2 :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
{ apply le.refl},
|
||||
{ exact trunc_index.le_succ IH}
|
||||
end
|
||||
|
||||
definition add_two_le_add_two {n m : ℕ₋₂} (H : n ≤ m) : add_two n ≤ add_two m :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
{ reflexivity},
|
||||
{ constructor, exact IH},
|
||||
end
|
||||
|
||||
definition le_of_sub_two_le_sub_two {n m : ℕ} (H : n.-2 ≤ m.-2) : n ≤ m :=
|
||||
begin
|
||||
rewrite [-add_two_sub_two n, -add_two_sub_two m],
|
||||
exact add_two_le_add_two H,
|
||||
end
|
||||
|
||||
definition le_of_of_nat_le_of_nat {n m : ℕ} (H : of_nat n ≤ of_nat m) : n ≤ m :=
|
||||
begin
|
||||
apply le_of_sub_two_le_sub_two,
|
||||
exact le_of_succ_le_succ (le_of_succ_le_succ H)
|
||||
end
|
||||
|
||||
end trunc_index open trunc_index
|
||||
|
||||
variables {A B : Type} {n : ℕ₋₂}
|
||||
|
||||
/- theorems about trunctype -/
|
||||
|
|
@ -374,7 +374,7 @@ namespace is_trunc
|
|||
{ apply is_trunc_eq}
|
||||
end
|
||||
|
||||
end is_trunc open is_trunc is_trunc.trunc_index
|
||||
end is_trunc open is_trunc
|
||||
|
||||
namespace trunc
|
||||
variable {A : Type}
|
||||
|
|
|
|||
Loading…
Reference in a new issue