From ac03bf7a4a9315ede17831ed28d1491618a73b69 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 4 Jun 2015 22:30:09 -0400 Subject: [PATCH] feat(hott/nat): prove computation rule for cases by inequality --- hott/init/nat.hlean | 121 +++++++++++++++++++------------------- hott/types/nat/hott.hlean | 61 ++++++++++++++----- 2 files changed, 106 insertions(+), 76 deletions(-) diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index bfa3a244c..2657dfdd3 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura prelude import init.wf init.tactic init.hedberg init.util init.types -open eq decidable sum lift +open eq decidable sum lift is_trunc namespace nat notation `ℕ` := nat @@ -58,20 +58,20 @@ namespace nat /- properties of inequality -/ - theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n + definition le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n - theorem le_succ (n : ℕ) : n ≤ succ n := by repeat constructor + definition le_succ (n : ℕ) : n ≤ succ n := by repeat constructor - theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) + definition pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) - theorem le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := + 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 - theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ + definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ - theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H + definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H - theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le 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 @@ -85,28 +85,28 @@ namespace nat 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 - theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n := + 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 - theorem zero_le (n : ℕ) : 0 ≤ n := + definition zero_le (n : ℕ) : 0 ≤ n := by induction n with n IH;apply le.refl;exact le.step IH - theorem lt.step {n m : ℕ} (H : n < m) : n < succ m := + definition lt.step {n m : ℕ} (H : n < m) : n < succ m := le.step H - theorem zero_lt_succ (n : ℕ) : 0 < succ n := + definition zero_lt_succ (n : ℕ) : 0 < succ n := by induction n with n IH;apply le.refl;exact le.step IH - theorem lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := + definition lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := le.trans (le.step H1) H2 - theorem lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k := + 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 - theorem lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k := + 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 := + definition le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := begin cases H1 with m' H1', { reflexivity}, @@ -115,47 +115,48 @@ namespace nat { exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}}, end - theorem not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero := + definition not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero := by intro H; cases H - theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self + definition 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 + definition self_lt_succ (n : ℕ) : n < succ n := !le.refl + definition lt.base (n : ℕ) : n < succ n := !le.refl - theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : empty := + definition 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 := + definition 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 := + definition lt.asymm {n m : ℕ} (H1 : n < m) (H2 : m < n) : empty := le_lt_antisymm (le_of_lt H1) H2 - definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := + definition lt.trichotomy (a b : ℕ) : a < b ⊎ a = b ⊎ b < a := 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)}} + revert b, induction a with a IH, + { intro b, cases b, + exact inr (inl idp), + exact inl !zero_lt_succ}, + { intro b, cases b with b, + exact inr (inr !zero_lt_succ), + { cases IH b with H H, + exact inl (succ_le_succ H), + cases H with H H, + exact inr (inl (ap succ H)), + exact inr (inr (succ_le_succ H))}} end - theorem lt.trichotomy (a b : ℕ) : a < b ⊎ a = b ⊎ b < a := - lt.by_cases inl (λH, inr (inl H)) (λH, inr (inr H)) + definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := + by induction (lt.trichotomy a b) with H H; exact H1 H; cases H with H H; exact H2 H;exact H3 H definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := lt.by_cases H1 (λH, H2 (le_of_eq H⁻¹)) (λH, H2 (le_of_lt H)) - theorem lt_or_ge (a b : ℕ) : (a < b) ⊎ (a ≥ b) := + definition lt_or_ge (a b : ℕ) : (a < b) ⊎ (a ≥ b) := lt_ge_by_cases inl inr - theorem not_lt_zero (a : ℕ) : ¬ a < zero := + definition not_lt_zero (a : ℕ) : ¬ a < zero := by intro H; cases H -- less-than is well-founded @@ -177,13 +178,13 @@ namespace nat definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := inv_image.wf f lt.wf - theorem succ_lt_succ {a b : ℕ} (H : a < b) : succ a < succ b := + definition succ_lt_succ {a b : ℕ} (H : a < b) : succ a < succ b := succ_le_succ H - theorem lt_of_succ_lt {a b : ℕ} (H : succ a < b) : a < b := + definition lt_of_succ_lt {a b : ℕ} (H : succ a < b) : a < b := le_of_succ_le H - theorem lt_of_succ_lt_succ {a b : ℕ} (H : succ a < succ b) : a < b := + definition 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 := @@ -202,49 +203,49 @@ namespace nat definition decidable_gt [instance] : decidable_rel gt := _ definition decidable_ge [instance] : decidable_rel ge := _ - theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ⊎ a < b := + 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) - theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ⊎ a < b) : a ≤ b := + 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 - theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ⊎ b < a := + 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) - theorem lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b := + definition lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b := succ_le_succ h - theorem lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h + definition lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h - theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h + definition succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h definition max (a b : ℕ) : ℕ := if a < b then b else a definition min (a b : ℕ) : ℕ := if a < b then a else b - theorem max_self (a : ℕ) : max a a = a := + definition max_self (a : ℕ) : max a a = a := eq.rec_on !if_t_t rfl - theorem max_eq_right {a b : ℕ} (H : a < b) : max a b = b := + definition max_eq_right {a b : ℕ} (H : a < b) : max a b = b := if_pos H - theorem max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a := + definition max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a := if_neg H - theorem eq_max_right {a b : ℕ} (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 - theorem eq_max_left {a b : ℕ} (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 - theorem le_max_left (a b : ℕ) : 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) - theorem le_max_right (a b : ℕ) : 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) @@ -253,21 +254,21 @@ namespace nat have aux : a = max a b, from eq_max_left (lt.asymm h), eq.rec_on aux (le_of_lt h))) - theorem succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := + 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 - theorem sub_eq_succ_sub_succ (a b : ℕ) : 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 - theorem zero_sub_eq_zero (a : ℕ) : 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) - theorem zero_eq_zero_sub (a : ℕ) : zero = zero - a := + definition zero_eq_zero_sub (a : ℕ) : zero = zero - a := eq.rec_on (zero_sub_eq_zero a) rfl - theorem sub_lt {a b : ℕ} : 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₁, le.rec_on h₁ (λb h₂, le.cases_on h₂ @@ -282,7 +283,7 @@ namespace nat (lt.trans (@ih b₁ bpos) (lt.base a₁)))), λ h₁ h₂, aux h₁ h₂ - theorem sub_le (a b : ℕ) : 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) diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index cedfaf40a..30e8657bc 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -11,7 +11,6 @@ import .basic open is_trunc unit empty eq equiv namespace nat - definition is_hprop_le [instance] (n m : ℕ) : is_hprop (n ≤ m) := begin assert lem : Π{n m : ℕ} (p : n ≤ m) (q : n = m), p = q ▸ le.refl n, @@ -25,27 +24,57 @@ namespace nat { 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 + 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', + { 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 - -- 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 + 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', + { 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 - -- definition is_hprop_le (n m : ℕ) : is_hprop (n ≤ m) := !is_hprop_lt + 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', + { 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 + + theorem lt_ge_by_cases_lt {n m : ℕ} {P : Type} (H1 : n < m → P) (H2 : n ≥ m → P) + (H : n < m) : lt_ge_by_cases H1 H2 = H1 H := + by apply lt_by_cases_lt + + 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', + { 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 + + theorem lt_ge_by_cases_le {n m : ℕ} {P : Type} {H1 : n ≤ m → P} {H2 : n ≥ m → P} + (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', + { esimp, apply ap H1 !is_hprop.elim}, + { cases H' with H' H', + esimp, exact !Heq⁻¹ ⬝ ap H1 !is_hprop.elim, + exfalso, apply lt.irrefl, apply lt_of_le_of_lt H H'} + end end nat