feat(hott): redefine nat.le and nat.lt
also some minor modifications in other files
This commit is contained in:
Floris van Doorn
parent
d4a991ef84
commit
4117455e97
8 changed files with 287 additions and 319 deletions
|
|
@ -10,7 +10,7 @@ Type quotients (quotient without truncation)
|
|||
The hit type_quotient is primitive, declared in init.hit.
|
||||
The constructors are
|
||||
class_of : A → A / R (A implicit, R explicit)
|
||||
eq_of_rel : R a a' → a = a' (R explicit)
|
||||
eq_of_rel : Π{a a' : A}, R a a' → a = a' (R explicit)
|
||||
-/
|
||||
|
||||
open eq equiv sigma.ops
|
||||
|
|
|
|||
|
|
@ -246,7 +246,6 @@ equiv.mk apd10 _
|
|||
definition eq_of_homotopy [reducible] : f ∼ g → f = g :=
|
||||
(@apd10 A P f g)⁻¹
|
||||
|
||||
--TODO: rename to eq_of_homotopy_idp
|
||||
definition eq_of_homotopy_idp (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f :=
|
||||
is_equiv.left_inv apd10 idp
|
||||
|
||||
|
|
|
|||
|
|
@ -11,19 +11,37 @@ open eq decidable sum lift
|
|||
namespace nat
|
||||
notation `ℕ` := nat
|
||||
|
||||
inductive lt (a : nat) : nat → Type₀ :=
|
||||
| base : lt a (succ a)
|
||||
| step : Π {b}, lt a b → lt a (succ b)
|
||||
/- basic definitions on natural numbers -/
|
||||
inductive le (a : ℕ) : ℕ → Type₀ :=
|
||||
| refl : le a a
|
||||
| step : Π {b}, le a b → le a (succ b)
|
||||
|
||||
notation a < b := lt a b
|
||||
infix `≤` := le
|
||||
attribute le.refl [refl]
|
||||
|
||||
definition le [reducible] (a b : nat) : Type₀ := a < succ b
|
||||
definition lt [reducible] (n m : ℕ) := succ n ≤ m
|
||||
definition ge [reducible] (n m : ℕ) := m ≤ n
|
||||
definition gt [reducible] (n m : ℕ) := succ m ≤ n
|
||||
infix `<` := lt
|
||||
infix `≥` := ge
|
||||
infix `>` := gt
|
||||
|
||||
notation a ≤ b := le a b
|
||||
|
||||
definition pred (a : nat) : nat :=
|
||||
definition pred [unfold-c 1] (a : nat) : nat :=
|
||||
nat.cases_on a zero (λ a₁, a₁)
|
||||
|
||||
-- add is defined in init.num
|
||||
definition sub (a b : nat) : nat :=
|
||||
nat.rec_on b a (λ b₁ r, pred r)
|
||||
|
||||
definition mul (a b : nat) : nat :=
|
||||
nat.rec_on b zero (λ b₁ r, r + a)
|
||||
|
||||
notation a - b := sub a b
|
||||
notation a * b := mul a b
|
||||
|
||||
|
||||
/- properties of ℕ -/
|
||||
|
||||
protected definition is_inhabited [instance] : inhabited nat :=
|
||||
inhabited.mk zero
|
||||
|
||||
|
|
@ -37,200 +55,192 @@ namespace nat
|
|||
| inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney)
|
||||
end
|
||||
|
||||
/- properties of inequality -/
|
||||
|
||||
definition le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n
|
||||
|
||||
definition le_succ (n : ℕ) : n ≤ succ n := by repeat constructor
|
||||
|
||||
definition pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor)
|
||||
|
||||
definition le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
|
||||
by induction H2 with n H2 IH;exact H1;exact le.step IH
|
||||
|
||||
definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ
|
||||
|
||||
definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H
|
||||
|
||||
definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
|
||||
|
||||
definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
|
||||
by induction H;reflexivity;exact le.step v_0
|
||||
|
||||
definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
|
||||
by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
|
||||
|
||||
definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
|
||||
pred_le_pred H
|
||||
|
||||
definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m :=
|
||||
by cases n;exact le.step H;exact succ_le_succ H
|
||||
|
||||
definition not_succ_le_self {n : ℕ} : ¬succ n ≤ n :=
|
||||
by induction n with n IH;all_goals intros;cases a;apply IH;exact le_of_succ_le_succ a
|
||||
|
||||
definition zero_le (n : ℕ) : 0 ≤ n :=
|
||||
by induction n with n IH;apply le.refl;exact le.step IH
|
||||
|
||||
definition zero_lt_succ (n : ℕ) : 0 < succ n :=
|
||||
by induction n with n IH;apply le.refl;exact le.step IH
|
||||
|
||||
definition lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
|
||||
le.trans (le.step H1) H2
|
||||
|
||||
definition lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k :=
|
||||
le.trans (succ_le_succ H1) H2
|
||||
|
||||
definition lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k :=
|
||||
le.trans H1 H2
|
||||
|
||||
theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
|
||||
begin
|
||||
cases H1 with m' H1',
|
||||
{ reflexivity},
|
||||
{ cases H2 with n' H2',
|
||||
{ reflexivity},
|
||||
{ exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}},
|
||||
end
|
||||
|
||||
definition not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero :=
|
||||
by intro H; cases H
|
||||
|
||||
theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self
|
||||
|
||||
theorem self_lt_succ (n : ℕ) : n < succ n := !le.refl
|
||||
theorem lt.base (n : ℕ) : n < succ n := !le.refl
|
||||
|
||||
theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : empty :=
|
||||
!lt.irrefl (lt_of_le_of_lt H1 H2)
|
||||
|
||||
theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : empty :=
|
||||
le_lt_antisymm H2 H1
|
||||
|
||||
theorem lt.asymm {n m : ℕ} (H1 : n < m) (H2 : m < n) : empty :=
|
||||
le_lt_antisymm (le_of_lt H1) H2
|
||||
|
||||
theorem lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
|
||||
begin
|
||||
revert b H1 H2 H3, induction a with a IH,
|
||||
{ intros, cases b,
|
||||
exact H2 idp,
|
||||
exact H1 !zero_lt_succ},
|
||||
{ intros, cases b with b,
|
||||
exact H3 !zero_lt_succ,
|
||||
{ apply IH,
|
||||
intro H, exact H1 (succ_le_succ H),
|
||||
intro H, exact H2 (ap succ H),
|
||||
intro H, exact H3 (succ_le_succ H)}}
|
||||
end
|
||||
|
||||
definition lt.trichotomy (a b : ℕ) : a < b ⊎ a = b ⊎ b < a :=
|
||||
lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H))
|
||||
|
||||
theorem lt_or_ge (a b : ℕ) : (a < b) ⊎ (a ≥ b) :=
|
||||
lt.by_cases inl (λH, inr (eq.rec_on H !le.refl)) (λH, inr (le_of_lt H))
|
||||
|
||||
definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P :=
|
||||
sum.rec_on (lt_or_ge a b) H1 H2
|
||||
|
||||
definition not_lt_zero (a : ℕ) : ¬ a < zero :=
|
||||
by intro H; cases H
|
||||
|
||||
-- less-than is well-founded
|
||||
definition lt.wf [instance] : well_founded lt :=
|
||||
well_founded.intro (λn, nat.rec_on n
|
||||
(acc.intro zero (λ (y : nat) (hlt : y < zero),
|
||||
have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from
|
||||
λ n₁ hlt, nat.lt.cases_on hlt
|
||||
(by contradiction)
|
||||
(by contradiction),
|
||||
aux hlt rfl))
|
||||
(λ (n : nat) (ih : acc lt n),
|
||||
acc.intro (succ n) (λ (m : nat) (hlt : m < succ n),
|
||||
have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from
|
||||
λ n₁ hlt, nat.lt.cases_on hlt
|
||||
(λ (sn_eq_sm : succ n = succ m),
|
||||
by injection sn_eq_sm with neqm; rewrite neqm at ih; exact ih)
|
||||
(λ b (hlt : m < b) (sn_eq_sb : succ n = succ b),
|
||||
by injection sn_eq_sb with neqb; rewrite neqb at ih; exact acc.inv ih hlt),
|
||||
aux hlt rfl)))
|
||||
begin
|
||||
constructor, intro n, induction n with n IH,
|
||||
{ constructor, intros n H, exfalso, exact !not_lt_zero H},
|
||||
{ constructor, intros m H,
|
||||
assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m,
|
||||
{ intros n₁ hlt, induction hlt,
|
||||
{ intro p, injection p with q, exact q ▸ IH},
|
||||
{ intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}},
|
||||
apply aux H idp},
|
||||
end
|
||||
|
||||
definition measure {A : Type} (f : A → nat) : A → A → Type₀ :=
|
||||
definition measure {A : Type} (f : A → ℕ) : A → A → Type₀ :=
|
||||
inv_image lt f
|
||||
|
||||
definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
|
||||
definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) :=
|
||||
inv_image.wf f lt.wf
|
||||
|
||||
definition not_lt_zero (a : nat) : ¬ a < zero :=
|
||||
have aux : Π {b}, a < b → b = zero → empty, from
|
||||
λ b H, lt.cases_on H
|
||||
(by contradiction)
|
||||
(by contradiction),
|
||||
λ H, aux H rfl
|
||||
theorem succ_lt_succ {a b : ℕ} (H : a < b) : succ a < succ b :=
|
||||
succ_le_succ H
|
||||
|
||||
definition zero_lt_succ (a : nat) : zero < succ a :=
|
||||
nat.rec_on a
|
||||
(lt.base zero)
|
||||
(λ a (hlt : zero < succ a), lt.step hlt)
|
||||
theorem lt_of_succ_lt {a b : ℕ} (H : succ a < b) : a < b :=
|
||||
le_of_succ_le H
|
||||
|
||||
definition lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
|
||||
have aux : a < b → a < c, from
|
||||
lt.rec_on H₂
|
||||
(λ h₁, lt.step h₁)
|
||||
(λ b₁ bb₁ ih h₁, lt.step (ih h₁)),
|
||||
aux H₁
|
||||
|
||||
definition succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
|
||||
lt.rec_on H
|
||||
(lt.base (succ a))
|
||||
(λ b hlt ih, lt.trans ih (lt.base (succ b)))
|
||||
|
||||
definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
|
||||
lt.rec_on H
|
||||
(lt.step (lt.base a))
|
||||
(λ b h ih, lt.step ih)
|
||||
|
||||
definition lt_of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
|
||||
have aux : pred (succ a) < pred (succ b), from
|
||||
lt.rec_on H
|
||||
(lt.base a)
|
||||
(λ (b : nat) (hlt : succ a < b) ih,
|
||||
show pred (succ a) < pred (succ b), from
|
||||
lt_of_succ_lt hlt),
|
||||
aux
|
||||
|
||||
definition decidable_lt [instance] : decidable_rel lt :=
|
||||
λ a b, nat.rec_on b
|
||||
(λ (a : nat), inr (not_lt_zero a))
|
||||
(λ (b₁ : nat) (ih : Π a, decidable (a < b₁)) (a : nat), nat.cases_on a
|
||||
(inl !zero_lt_succ)
|
||||
(λ a, decidable.rec_on (ih a)
|
||||
(λ h_pos : a < b₁, inl (succ_lt_succ h_pos))
|
||||
(λ h_neg : ¬ a < b₁,
|
||||
have aux : ¬ succ a < succ b₁, from
|
||||
λ h : succ a < succ b₁, h_neg (lt_of_succ_lt_succ h),
|
||||
inr aux)))
|
||||
a
|
||||
|
||||
definition le.refl (a : nat) : a ≤ a :=
|
||||
lt.base a
|
||||
|
||||
definition le_of_lt {a b : nat} (H : a < b) : a ≤ b :=
|
||||
lt.step H
|
||||
|
||||
definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ⊎ a < b :=
|
||||
begin
|
||||
cases H with b hlt,
|
||||
apply sum.inl rfl,
|
||||
apply sum.inr hlt
|
||||
end
|
||||
|
||||
definition le_of_eq_or_lt {a b : nat} (H : a = b ⊎ a < b) : a ≤ b :=
|
||||
sum.rec_on H
|
||||
(λ hl, eq.rec_on hl !le.refl)
|
||||
(λ hr, le_of_lt hr)
|
||||
theorem lt_of_succ_lt_succ {a b : ℕ} (H : succ a < succ b) : a < b :=
|
||||
le_of_succ_le_succ H
|
||||
|
||||
definition decidable_le [instance] : decidable_rel le :=
|
||||
λ a b, decidable_iff_equiv _ (iff.intro le_of_eq_or_lt eq_or_lt_of_le)
|
||||
|
||||
definition le.rec_on {a : nat} {P : nat → Type} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : Π b, a < b → P b) : P b :=
|
||||
begin
|
||||
cases H with b hlt,
|
||||
apply H₁,
|
||||
apply H₂ b hlt
|
||||
intros n, induction n with n IH,
|
||||
{ intro m, left, apply zero_le},
|
||||
{ intro m, cases m with m,
|
||||
{ right, apply not_succ_le_zero},
|
||||
{ let H := IH m, clear IH,
|
||||
cases H with H H,
|
||||
left, exact succ_le_succ H,
|
||||
right, intro H2, exact H (le_of_succ_le_succ H2)}}
|
||||
end
|
||||
|
||||
definition lt.irrefl (a : nat) : ¬ a < a :=
|
||||
nat.rec_on a
|
||||
!not_lt_zero
|
||||
(λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
|
||||
ih (lt_of_succ_lt_succ h))
|
||||
definition decidable_lt [instance] : decidable_rel lt := _
|
||||
definition decidable_gt [instance] : decidable_rel gt := _
|
||||
definition decidable_ge [instance] : decidable_rel ge := _
|
||||
|
||||
definition lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
|
||||
lt.rec_on H
|
||||
(λ h : succ a < a, !lt.irrefl (lt_of_succ_lt h))
|
||||
(λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt_of_succ_lt h))
|
||||
definition eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ⊎ a < b :=
|
||||
by cases H with b' H; exact sum.inl rfl; exact sum.inr (succ_le_succ H)
|
||||
|
||||
definition lt.trichotomy (a b : nat) : a < b ⊎ a = b ⊎ b < a :=
|
||||
nat.rec_on b
|
||||
(λa, nat.cases_on a
|
||||
(sum.inr (sum.inl rfl))
|
||||
(λ a₁, sum.inr (sum.inr !zero_lt_succ)))
|
||||
(λ b₁ (ih : Πa, a < b₁ ⊎ a = b₁ ⊎ b₁ < a) (a : nat), nat.cases_on a
|
||||
(sum.inl !zero_lt_succ)
|
||||
(λ a, sum.rec_on (ih a)
|
||||
(λ h : a < b₁, sum.inl (succ_lt_succ h))
|
||||
(λ h, sum.rec_on h
|
||||
(λ h : a = b₁, sum.inr (sum.inl (eq.rec_on h rfl)))
|
||||
(λ h : b₁ < a, sum.inr (sum.inr (succ_lt_succ h))))))
|
||||
a
|
||||
|
||||
definition eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ⊎ b < a :=
|
||||
definition le_of_eq_or_lt {a b : ℕ} (H : a = b ⊎ a < b) : a ≤ b :=
|
||||
by cases H with H H; exact le_of_eq H; exact le_of_lt H
|
||||
|
||||
definition eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ⊎ b < a :=
|
||||
sum.rec_on (lt.trichotomy a b)
|
||||
(λ hlt, absurd hlt hnlt)
|
||||
(λ h, h)
|
||||
|
||||
definition lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
|
||||
h
|
||||
definition lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b :=
|
||||
succ_le_succ h
|
||||
|
||||
definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
|
||||
lt_of_succ_lt_succ h
|
||||
definition lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h
|
||||
|
||||
definition le_succ_of_le {a b : nat} (h : a ≤ b) : a ≤ succ b :=
|
||||
lt.step h
|
||||
definition succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h
|
||||
|
||||
definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
|
||||
succ_lt_succ h
|
||||
definition max (a b : ℕ) : ℕ := if a < b then b else a
|
||||
definition min (a b : ℕ) : ℕ := if a < b then a else b
|
||||
|
||||
definition le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
|
||||
begin
|
||||
cases h₁ with b' hlt,
|
||||
apply h₂,
|
||||
apply lt.trans hlt h₂
|
||||
end
|
||||
|
||||
definition lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
|
||||
begin
|
||||
cases h₁ with b' hlt,
|
||||
apply h₂,
|
||||
apply lt.trans hlt h₂
|
||||
end
|
||||
|
||||
definition lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
|
||||
begin
|
||||
cases h₁ with b' hlt,
|
||||
apply lt_of_succ_lt_succ h₂,
|
||||
apply lt.trans hlt (lt_of_succ_lt_succ h₂)
|
||||
end
|
||||
|
||||
definition max (a b : nat) : nat :=
|
||||
if a < b then b else a
|
||||
|
||||
definition min (a b : nat) : nat :=
|
||||
if a < b then a else b
|
||||
|
||||
definition max_self (a : nat) : max a a = a :=
|
||||
definition max_self (a : ℕ) : max a a = a :=
|
||||
eq.rec_on !if_t_t rfl
|
||||
|
||||
definition max_eq_right {a b : nat} (H : a < b) : max a b = b :=
|
||||
definition max_eq_right {a b : ℕ} (H : a < b) : max a b = b :=
|
||||
if_pos H
|
||||
|
||||
definition max_eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
|
||||
definition max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a :=
|
||||
if_neg H
|
||||
|
||||
definition eq_max_right {a b : nat} (H : a < b) : b = max a b :=
|
||||
definition eq_max_right {a b : ℕ} (H : a < b) : b = max a b :=
|
||||
eq.rec_on (max_eq_right H) rfl
|
||||
|
||||
definition eq_max_left {a b : nat} (H : ¬ a < b) : a = max a b :=
|
||||
definition eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b :=
|
||||
eq.rec_on (max_eq_left H) rfl
|
||||
|
||||
definition le_max_left (a b : nat) : a ≤ max a b :=
|
||||
definition le_max_left (a b : ℕ) : a ≤ max a b :=
|
||||
by_cases
|
||||
(λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h))
|
||||
(λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
|
||||
|
||||
definition le_max_right (a b : nat) : b ≤ max a b :=
|
||||
definition le_max_right (a b : ℕ) : b ≤ max a b :=
|
||||
by_cases
|
||||
(λ h : a < b, eq.rec_on (eq_max_right h) !le.refl)
|
||||
(λ h : ¬ a < b, sum.rec_on (eq_or_lt_of_not_lt h)
|
||||
|
|
@ -239,71 +249,36 @@ namespace nat
|
|||
have aux : a = max a b, from eq_max_left (lt.asymm h),
|
||||
eq.rec_on aux (le_of_lt h)))
|
||||
|
||||
definition gt [reducible] a b := lt b a
|
||||
definition decidable_gt [instance] : decidable_rel gt :=
|
||||
_
|
||||
definition succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b :=
|
||||
by induction b with b IH; reflexivity; apply ap pred IH
|
||||
|
||||
notation a > b := gt a b
|
||||
|
||||
definition ge [reducible] a b := le b a
|
||||
definition decidable_ge [instance] : decidable_rel ge :=
|
||||
_
|
||||
|
||||
notation a ≥ b := ge a b
|
||||
|
||||
-- add is defined in init.num
|
||||
|
||||
definition sub (a b : nat) : nat :=
|
||||
nat.rec_on b a (λ b₁ r, pred r)
|
||||
|
||||
notation a - b := sub a b
|
||||
|
||||
definition mul (a b : nat) : nat :=
|
||||
nat.rec_on b zero (λ b₁ r, r + a)
|
||||
|
||||
notation a * b := mul a b
|
||||
|
||||
section
|
||||
local attribute sub [reducible]
|
||||
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
|
||||
nat.rec_on b
|
||||
rfl
|
||||
(λ b₁ (ih : succ a - succ b₁ = a - b₁),
|
||||
eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
|
||||
end
|
||||
|
||||
definition sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
|
||||
definition sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b :=
|
||||
eq.rec_on (succ_sub_succ_eq_sub a b) rfl
|
||||
|
||||
definition zero_sub_eq_zero (a : nat) : zero - a = zero :=
|
||||
definition zero_sub_eq_zero (a : ℕ) : zero - a = zero :=
|
||||
nat.rec_on a
|
||||
rfl
|
||||
(λ a₁ (ih : zero - a₁ = zero), ap pred ih)
|
||||
|
||||
definition zero_eq_zero_sub (a : nat) : zero = zero - a :=
|
||||
definition zero_eq_zero_sub (a : ℕ) : zero = zero - a :=
|
||||
eq.rec_on (zero_sub_eq_zero a) rfl
|
||||
|
||||
definition sub_lt {a b : nat} : zero < a → zero < b → a - b < a :=
|
||||
definition sub_lt {a b : ℕ} : zero < a → zero < b → a - b < a :=
|
||||
have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
|
||||
λa h₁, lt.rec_on h₁
|
||||
(λb h₂, lt.cases_on h₂
|
||||
λa h₁, le.rec_on h₁
|
||||
(λb h₂, le.cases_on h₂
|
||||
(lt.base zero)
|
||||
(λ b₁ bpos,
|
||||
eq.rec_on (sub_eq_succ_sub_succ zero b₁)
|
||||
(eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero))))
|
||||
(λa₁ apos ih b h₂, lt.cases_on h₂
|
||||
(λa₁ apos ih b h₂, le.cases_on h₂
|
||||
(lt.base a₁)
|
||||
(λ b₁ bpos,
|
||||
eq.rec_on (sub_eq_succ_sub_succ a₁ b₁)
|
||||
(lt.trans (@ih b₁ bpos) (lt.base a₁)))),
|
||||
λ h₁ h₂, aux h₁ h₂
|
||||
|
||||
definition pred_le (a : nat) : pred a ≤ a :=
|
||||
nat.cases_on a
|
||||
(le.refl zero)
|
||||
(λ a₁, le_of_lt (lt.base a₁))
|
||||
|
||||
definition sub_le (a b : nat) : a - b ≤ a :=
|
||||
definition sub_le (a b : ℕ) : a - b ≤ a :=
|
||||
nat.rec_on b
|
||||
(le.refl a)
|
||||
(λ b₁ ih, le.trans !pred_le ih)
|
||||
|
|
|
|||
|
|
@ -141,38 +141,48 @@ namespace eq
|
|||
q ⬝ p = r → q = r ⬝ p⁻¹ :=
|
||||
eq.rec_on p (take r h, !con_idp⁻¹ ⬝ h ⬝ !con_idp⁻¹) r
|
||||
|
||||
definition eq_of_con_inv_eq_idp {p q : x = y} :
|
||||
p ⬝ q⁻¹ = idp → p = q :=
|
||||
definition eq_of_con_inv_eq_idp {p q : x = y} : p ⬝ q⁻¹ = idp → p = q :=
|
||||
eq.rec_on q (take p h, !con_idp⁻¹ ⬝ h) p
|
||||
|
||||
definition eq_of_inv_con_eq_idp {p q : x = y} :
|
||||
q⁻¹ ⬝ p = idp → p = q :=
|
||||
definition eq_of_inv_con_eq_idp {p q : x = y} : q⁻¹ ⬝ p = idp → p = q :=
|
||||
eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p
|
||||
|
||||
definition eq_inv_of_con_eq_idp' {p : x = y} {q : y = x} :
|
||||
p ⬝ q = idp → p = q⁻¹ :=
|
||||
definition eq_inv_of_con_eq_idp' {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ :=
|
||||
eq.rec_on q (take p h, !con_idp⁻¹ ⬝ h) p
|
||||
|
||||
definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} :
|
||||
q ⬝ p = idp → p = q⁻¹ :=
|
||||
definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} : q ⬝ p = idp → p = q⁻¹ :=
|
||||
eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p
|
||||
|
||||
definition eq_of_idp_eq_inv_con {p q : x = y} :
|
||||
idp = p⁻¹ ⬝ q → p = q :=
|
||||
definition eq_of_idp_eq_inv_con {p q : x = y} : idp = p⁻¹ ⬝ q → p = q :=
|
||||
eq.rec_on p (take q h, h ⬝ !idp_con) q
|
||||
|
||||
definition eq_of_idp_eq_con_inv {p q : x = y} :
|
||||
idp = q ⬝ p⁻¹ → p = q :=
|
||||
definition eq_of_idp_eq_con_inv {p q : x = y} : idp = q ⬝ p⁻¹ → p = q :=
|
||||
eq.rec_on p (take q h, h ⬝ !con_idp) q
|
||||
|
||||
definition inv_eq_of_idp_eq_con {p : x = y} {q : y = x} :
|
||||
idp = q ⬝ p → p⁻¹ = q :=
|
||||
definition inv_eq_of_idp_eq_con {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q :=
|
||||
eq.rec_on p (take q h, h ⬝ !con_idp) q
|
||||
|
||||
definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} :
|
||||
idp = p ⬝ q → p⁻¹ = q :=
|
||||
definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q :=
|
||||
eq.rec_on p (take q h, h ⬝ !idp_con) q
|
||||
|
||||
definition con_inv_eq_idp {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp :=
|
||||
by cases r;apply con.right_inv
|
||||
|
||||
definition inv_con_eq_idp {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp :=
|
||||
by cases r;apply con.left_inv
|
||||
|
||||
definition con_eq_idp {p : x = y} {q : y = x} (r : p = q⁻¹) : p ⬝ q = idp :=
|
||||
by cases q;exact r
|
||||
|
||||
definition idp_eq_inv_con {p q : x = y} (r : p = q) : idp = p⁻¹ ⬝ q :=
|
||||
by cases r;exact !con.left_inv⁻¹
|
||||
|
||||
definition idp_eq_con_inv {p q : x = y} (r : p = q) : idp = q ⬝ p⁻¹ :=
|
||||
by cases r;exact !con.right_inv⁻¹
|
||||
|
||||
definition idp_eq_con {p : x = y} {q : y = x} (r : p⁻¹ = q) : idp = q ⬝ p :=
|
||||
by cases p;exact r
|
||||
|
||||
/- Transport -/
|
||||
|
||||
definition transport [subst] [reducible] [unfold-c 5] (P : A → Type) {x y : A} (p : x = y)
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ namespace is_trunc
|
|||
|
||||
definition is_trunc_eq [instance] [priority 1200]
|
||||
(n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) :=
|
||||
is_trunc.mk (@is_trunc.to_internal (n .+1) A H x y)
|
||||
is_trunc.mk (is_trunc.to_internal (n.+1) A x y)
|
||||
|
||||
/- contractibility -/
|
||||
|
||||
|
|
@ -95,10 +95,10 @@ namespace is_trunc
|
|||
is_trunc.mk (contr_internal.mk center center_eq)
|
||||
|
||||
definition center (A : Type) [H : is_contr A] : A :=
|
||||
@contr_internal.center A (@is_trunc.to_internal -2 A H)
|
||||
contr_internal.center (is_trunc.to_internal -2 A)
|
||||
|
||||
definition center_eq [H : is_contr A] (a : A) : !center = a :=
|
||||
@contr_internal.center_eq A !is_trunc.to_internal a
|
||||
contr_internal.center_eq !is_trunc.to_internal a
|
||||
|
||||
definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y :=
|
||||
(center_eq x)⁻¹ ⬝ (center_eq y)
|
||||
|
|
@ -107,14 +107,14 @@ namespace is_trunc
|
|||
have K : ∀ (r : x = y), eq_of_is_contr x y = r, from (λ r, eq.rec_on r !con.left_inv),
|
||||
(K p)⁻¹ ⬝ K q
|
||||
|
||||
definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
|
||||
theorem is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
|
||||
is_contr.mk !eq_of_is_contr (λ p, !hprop_eq_of_is_contr)
|
||||
local attribute is_contr_eq [instance]
|
||||
|
||||
/- truncation is upward close -/
|
||||
|
||||
-- n-types are also (n+1)-types
|
||||
definition is_trunc_succ [instance] [priority 900] (A : Type) (n : trunc_index)
|
||||
theorem is_trunc_succ [instance] [priority 900] (A : Type) (n : trunc_index)
|
||||
[H : is_trunc n A] : is_trunc (n.+1) A :=
|
||||
trunc_index.rec_on n
|
||||
(λ A (H : is_contr A), !is_trunc_succ_intro)
|
||||
|
|
@ -122,7 +122,7 @@ namespace is_trunc
|
|||
A H
|
||||
--in the proof the type of H is given explicitly to make it available for class inference
|
||||
|
||||
definition is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m)
|
||||
theorem is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m)
|
||||
[Hn : is_trunc n A] : is_trunc m A :=
|
||||
have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
|
||||
λ k A, trunc_index.cases_on k
|
||||
|
|
@ -139,16 +139,16 @@ namespace is_trunc
|
|||
trunc_index.rec_on m base step n A Hnm Hn
|
||||
|
||||
-- the following cannot be instances in their current form, because they are looping
|
||||
definition is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
|
||||
theorem is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
|
||||
trunc_index.rec_on n H _
|
||||
|
||||
definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
|
||||
theorem is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
|
||||
: is_trunc (n.+1) A :=
|
||||
@is_trunc_of_leq A (-2.+1) _ star _
|
||||
is_trunc_of_leq A (star : -1 ≤ n.+1)
|
||||
|
||||
definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
|
||||
theorem is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
|
||||
: is_trunc (n.+2) A :=
|
||||
@is_trunc_of_leq A (-2.+1.+1) _ star _
|
||||
is_trunc_of_leq A (star : 0 ≤ n.+2)
|
||||
|
||||
/- hprops -/
|
||||
|
||||
|
|
@ -158,19 +158,21 @@ namespace is_trunc
|
|||
definition is_contr_of_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A :=
|
||||
is_contr.mk x (λy, !is_hprop.elim)
|
||||
|
||||
--Coq has the following as instance, but doesn't look too useful
|
||||
definition is_hprop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_hprop A :=
|
||||
theorem is_hprop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_hprop A :=
|
||||
@is_trunc_succ_intro A -2
|
||||
(λx y,
|
||||
have H2 [visible] : is_contr A, from H x,
|
||||
!is_contr_eq)
|
||||
|
||||
definition is_hprop.mk {A : Type} (H : ∀x y : A, x = y) : is_hprop A :=
|
||||
theorem is_hprop.mk {A : Type} (H : ∀x y : A, x = y) : is_hprop A :=
|
||||
is_hprop_of_imp_is_contr (λ x, is_contr.mk x (H x))
|
||||
|
||||
theorem is_hprop_elim_self {A : Type} {H : is_hprop A} (x : A) : is_hprop.elim x x = idp :=
|
||||
!is_hprop.elim
|
||||
|
||||
/- hsets -/
|
||||
|
||||
definition is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_hset A :=
|
||||
theorem is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_hset A :=
|
||||
@is_trunc_succ_intro _ _ (λ x y, is_hprop.mk (H x y))
|
||||
|
||||
definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x = y) : p = q :=
|
||||
|
|
@ -218,15 +220,15 @@ namespace is_trunc
|
|||
: (is_contr B) :=
|
||||
is_contr.mk (f (center A)) (λp, eq_of_eq_inv !center_eq)
|
||||
|
||||
theorem is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
|
||||
@is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _
|
||||
definition is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
|
||||
is_contr_is_equiv_closed (to_fun H)
|
||||
|
||||
definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
|
||||
equiv.mk
|
||||
(λa, center B)
|
||||
(is_equiv.adjointify (λa, center B) (λb, center A) center_eq center_eq)
|
||||
|
||||
definition is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f]
|
||||
theorem is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f]
|
||||
[HA : is_trunc n A] : is_trunc n B :=
|
||||
trunc_index.rec_on n
|
||||
(λA (HA : is_contr A) B f (H : is_equiv f), is_contr_is_equiv_closed f)
|
||||
|
|
@ -246,15 +248,15 @@ namespace is_trunc
|
|||
: is_trunc n A :=
|
||||
is_trunc_is_equiv_closed n (to_inv f)
|
||||
|
||||
definition is_equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
|
||||
: is_equiv f :=
|
||||
definition is_equiv_of_is_hprop [constructor] [HA : is_hprop A] [HB : is_hprop B]
|
||||
(f : A → B) (g : B → A) : is_equiv f :=
|
||||
is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim)
|
||||
|
||||
definition equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
|
||||
: A ≃ B :=
|
||||
definition equiv_of_is_hprop [constructor] [HA : is_hprop A] [HB : is_hprop B]
|
||||
(f : A → B) (g : B → A) : A ≃ B :=
|
||||
equiv.mk f (is_equiv_of_is_hprop f g)
|
||||
|
||||
definition equiv_of_iff_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B :=
|
||||
definition equiv_of_iff_of_is_hprop [unfold-c 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B :=
|
||||
equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -8,25 +8,44 @@ Theorems about the natural numbers specific to HoTT
|
|||
|
||||
import .basic
|
||||
|
||||
open is_trunc unit empty eq
|
||||
open is_trunc unit empty eq equiv
|
||||
|
||||
namespace nat
|
||||
|
||||
definition is_hprop_lt [instance] (n m : ℕ) : is_hprop (n < m) :=
|
||||
definition is_hprop_le [instance] (n m : ℕ) : is_hprop (n ≤ m) :=
|
||||
begin
|
||||
assert H : Π{n m : ℕ} (p : n < m) (q : succ n = m), p = q ▸ lt.base n,
|
||||
assert lem : Π{n m : ℕ} (p : n ≤ m) (q : n = m), p = q ▸ le.refl n,
|
||||
{ intros, cases p,
|
||||
{ assert H' : q = idp, apply is_hset.elim,
|
||||
cases H', reflexivity},
|
||||
{ cases q, exfalso, exact lt.irrefl b a}},
|
||||
apply is_hprop.mk, intros p q,
|
||||
induction q,
|
||||
{ apply H},
|
||||
{ cases p,
|
||||
exfalso, exact lt.irrefl b a,
|
||||
exact ap lt.step !v_0}
|
||||
{ cases q, exfalso, apply not_succ_le_self a}},
|
||||
apply is_hprop.mk, intro H1 H2, induction H2,
|
||||
{ apply lem},
|
||||
{ cases H1,
|
||||
{ exfalso, apply not_succ_le_self a},
|
||||
{ exact ap le.step !v_0}},
|
||||
end
|
||||
definition le_equiv_succ_le_succ (n m : ℕ) : (n ≤ m) ≃ (succ n ≤ succ m) :=
|
||||
equiv_of_is_hprop succ_le_succ le_of_succ_le_succ
|
||||
definition le_succ_equiv_pred_le (n m : ℕ) : (n ≤ succ m) ≃ (pred n ≤ m) :=
|
||||
equiv_of_is_hprop pred_le_pred le_succ_of_pred_le
|
||||
|
||||
definition is_hprop_le (n m : ℕ) : is_hprop (n ≤ m) := !is_hprop_lt
|
||||
|
||||
-- definition is_hprop_lt [instance] (n m : ℕ) : is_hprop (n < m) :=
|
||||
-- begin
|
||||
-- assert H : Π{n m : ℕ} (p : n < m) (q : succ n = m), p = q ▸ lt.base n,
|
||||
-- { intros, cases p,
|
||||
-- { assert H' : q = idp, apply is_hset.elim,
|
||||
-- cases H', reflexivity},
|
||||
-- { cases q, exfalso, exact lt.irrefl b a}},
|
||||
-- apply is_hprop.mk, intros p q,
|
||||
-- induction q,
|
||||
-- { apply H},
|
||||
-- { cases p,
|
||||
-- exfalso, exact lt.irrefl b a,
|
||||
-- exact ap lt.step !v_0}
|
||||
-- end
|
||||
|
||||
-- definition is_hprop_le (n m : ℕ) : is_hprop (n ≤ m) := !is_hprop_lt
|
||||
|
||||
end nat
|
||||
|
|
|
|||
|
|
@ -5,11 +5,11 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
|
|||
|
||||
The order relation on the natural numbers.
|
||||
|
||||
Ported from standard library
|
||||
Note: this file has significant differences than the standard library version
|
||||
-/
|
||||
|
||||
import .basic algebra.ordered_ring
|
||||
open prod decidable sum eq
|
||||
open prod decidable sum eq sigma sigma.ops
|
||||
|
||||
namespace nat
|
||||
|
||||
|
|
@ -18,12 +18,6 @@ namespace nat
|
|||
theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ⊎ m = n) : m ≤ n :=
|
||||
sum.rec_on H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
|
||||
|
||||
theorem lt.by_cases {a b : ℕ} {P : Type}
|
||||
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
|
||||
sum.rec_on !lt.trichotomy
|
||||
(assume H, H1 H)
|
||||
(assume H, sum.rec_on H (assume H', H2 H') (assume H', H3 H'))
|
||||
|
||||
theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ⊎ m = n :=
|
||||
lt.by_cases
|
||||
(assume H1 : m < n, sum.inl H1)
|
||||
|
|
@ -58,15 +52,7 @@ theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
|
|||
h ▸ le_add_right n k
|
||||
|
||||
theorem le.elim {n m : ℕ} (h : n ≤ m) : Σk, n + k = m :=
|
||||
le.rec_on h
|
||||
(sigma.mk 0 rfl)
|
||||
(λ m (h : n < m), lt.rec_on h
|
||||
(sigma.mk 1 rfl)
|
||||
(λ b hlt (ih : Σ (k : ℕ), n + k = b),
|
||||
sigma.rec_on ih (λ(k : ℕ) (h : n + k = b),
|
||||
sigma.mk (succ k) (calc
|
||||
n + succ k = succ (n + k) : add_succ
|
||||
... = succ b : h))))
|
||||
by induction h with m h ih;exact ⟨0, idp⟩;exact ⟨succ ih.1, ap succ ih.2⟩
|
||||
|
||||
theorem le.total {m n : ℕ} : m ≤ n ⊎ n ≤ m :=
|
||||
lt.by_cases
|
||||
|
|
@ -123,25 +109,6 @@ lt_of_lt_of_le H2 H3
|
|||
theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
|
||||
|
||||
theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
|
||||
sigma.rec_on (le.elim H1) (λ(k : ℕ) (Hk : n + k = m),
|
||||
sigma.rec_on (le.elim H2) (λ(l : ℕ) (Hl : m + l = n),
|
||||
have L1 : k + l = 0, from
|
||||
add.cancel_left
|
||||
(calc
|
||||
n + (k + l) = n + k + l : (!add.assoc)⁻¹
|
||||
... = m + l : {Hk}
|
||||
... = n : Hl
|
||||
... = n + 0 : (!add_zero)⁻¹),
|
||||
have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
|
||||
calc
|
||||
n = n + 0 : (!add_zero)⁻¹
|
||||
... = n + k : {L2⁻¹}
|
||||
... = m : Hk))
|
||||
|
||||
theorem zero_le (n : ℕ) : 0 ≤ n :=
|
||||
le.intro !zero_add
|
||||
|
||||
/- nat is an instance of a linearly ordered semiring -/
|
||||
|
||||
section
|
||||
|
|
@ -224,17 +191,6 @@ eq_zero_of_add_eq_zero_right Hk
|
|||
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
|
||||
iff.intro succ_le_of_lt lt_of_succ_le
|
||||
|
||||
theorem not_succ_le_zero (n : ℕ) : ¬ succ n ≤ 0 :=
|
||||
(assume H : succ n ≤ 0,
|
||||
have H2 : succ n = 0, from eq_zero_of_le_zero H,
|
||||
absurd H2 !succ_ne_zero)
|
||||
|
||||
theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
|
||||
!add_one ▸ !add_one ▸ add_le_add_right H 1
|
||||
|
||||
theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
|
||||
le_of_add_le_add_right ((!add_one)⁻¹ ▸ (!add_one)⁻¹ ▸ H)
|
||||
|
||||
theorem self_le_succ (n : ℕ) : n ≤ succ n :=
|
||||
le.intro !add_one
|
||||
|
||||
|
|
@ -243,14 +199,6 @@ sum.rec_on (lt_or_eq_of_le H)
|
|||
(assume H1 : n < m, sum.inl (succ_le_of_lt H1))
|
||||
(assume H1 : n = m, sum.inr H1)
|
||||
|
||||
theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
|
||||
nat.cases_on n
|
||||
(assume H : pred 0 ≤ m, !zero_le)
|
||||
(take n',
|
||||
assume H : pred (succ n') ≤ m,
|
||||
have H1 : n' ≤ m, from pred_succ n' ▸ H,
|
||||
succ_le_succ H1)
|
||||
|
||||
theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m :=
|
||||
nat.cases_on n
|
||||
(assume H, !pred_zero⁻¹ ▸ zero_le m)
|
||||
|
|
|
|||
|
|
@ -91,6 +91,10 @@ namespace eq
|
|||
{ intro s, cases s, apply idp},
|
||||
end
|
||||
|
||||
definition naturality [unfold-c 8] {f g : A → B} (p : f ∼ g) (q : a = a') :
|
||||
square (p a) (p a') (ap f q) (ap g q) :=
|
||||
eq.rec_on q vrfl
|
||||
|
||||
definition rec_on_b [recursor] {a₀₀ : A}
|
||||
{P : Π{a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}, square t idp l r → Type}
|
||||
{a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}
|
||||
|
|
@ -141,10 +145,21 @@ namespace eq
|
|||
from eq.rec_on (eq_of_square s : idp ⬝ r = l) (by cases r; exact H),
|
||||
left_inv (to_fun !square_equiv_eq) s ▸ H2
|
||||
|
||||
definition naturality [unfold-c 8] {f g : A → B} (p : f ∼ g) (q : a = a') :
|
||||
square (p a) (p a') (ap f q) (ap g q) :=
|
||||
eq.rec_on q vrfl
|
||||
definition rec_on_lr [recursor] {a : A}
|
||||
{P : Π{a' : A} {t : a = a'} {b : a = a'}, square t b idp idp → Type}
|
||||
{a' : A} {t : a = a'} {b : a = a'}
|
||||
(s : square t b idp idp) (H : P ids) : P s :=
|
||||
let p : idp ⬝ b = t := (eq_of_square s)⁻¹ in
|
||||
assert H2 : P (square_of_eq (eq_of_square s)⁻¹⁻¹),
|
||||
from @eq.rec_on _ _ (λx q, P (square_of_eq q⁻¹)) _ p (by cases b; exact H),
|
||||
to_left_inv (!square_equiv_eq) s ▸ !inv_inv ▸ H2
|
||||
|
||||
--we can also do the other recursors (lr, tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed
|
||||
definition eq_of_hdeg_square {p q : a = a'} (s : square idp idp p q) : p = q :=
|
||||
rec_on_tb s idp
|
||||
|
||||
definition eq_of_vdeg_square {p q : a = a'} (s : square p q idp idp) : p = q :=
|
||||
rec_on_lr s idp
|
||||
|
||||
--we can also do the other recursors (tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed
|
||||
|
||||
end eq
|
||||
|
|
|
|||
Loading…
Reference in a new issue