From 0c7e16e0172701424c08e831dbc55a8e2cf5e9d8 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 14 May 2015 20:18:29 -0400 Subject: [PATCH] feat(library.data.int.basic): move theorems about successor and predecessor from HoTT to standard library --- library/data/int/basic.lean | 37 +++++++++++++++++++++++++++---------- library/data/int/order.lean | 34 +++++++++++++++++----------------- 2 files changed, 44 insertions(+), 27 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 074223d99..1ff98569b 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -147,16 +147,6 @@ int.cases_on a (take m, assume H : nat_abs (of_nat m) = 0, congr_arg of_nat H) (take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _)) -definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) - (Hpred : Π⦃n : ℕ⦄, P (- n) → P (-succ n)) : P z := -int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H)) - ---the only computation rule of rec_nat_on which is not definitional -definition rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P 0) - (Hsucc : Π⦃n : nat⦄, P n → P (succ n)) (Hpred : Π⦃n : nat⦄, P (- n) → P (-succ n)) - : rec_nat_on (-succ n) H0 Hsucc Hpred = Hpred (rec_nat_on (-n) H0 Hsucc Hpred) := -nat.rec_on n rfl (λn H, rfl) - /- int is a quotient of ordered pairs of natural numbers -/ protected definition equiv (p q : ℕ × ℕ) : Prop := pr1 p + pr2 q = pr2 p + pr1 q @@ -651,4 +641,31 @@ have H2 : m = (#nat m - n) + n, from congr_arg of_nat H1, theorem neg_succ_of_nat_eq' (m : ℕ) : -[m +1] = -m - 1 := by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add] +definition succ (a : ℤ) := a + (nat.succ zero) +definition pred (a : ℤ) := a - (nat.succ zero) +theorem pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel +theorem succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel +theorem neg_succ (a : ℤ) : -succ a = pred (-a) := +by rewrite [↑succ,neg_add] +theorem succ_neg_succ (a : ℤ) : succ (-succ a) = -a := +by rewrite [neg_succ,succ_pred] +theorem neg_pred (a : ℤ) : -pred a = succ (-a) := +by rewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm] +theorem pred_neg_pred (a : ℤ) : pred (-pred a) = -a := +by rewrite [neg_pred,pred_succ] + +theorem pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n +theorem neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ +theorem succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ + +definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) + (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := +int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H)) + +--the only computation rule of rec_nat_on which is not definitional +theorem rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P zero) + (Hsucc : Π⦃n : nat⦄, P n → P (succ n)) (Hpred : Π⦃n : nat⦄, P (-n) → P (-nat.succ n)) + : rec_nat_on (-nat.succ n) H0 Hsucc Hpred = Hpred (rec_nat_on (-n) H0 Hsucc Hpred) := +nat.rec_on n rfl (λn H, rfl) + end int diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 5be61940c..4f5d3b135 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -84,8 +84,8 @@ exists.intro n H2 theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m := calc of_nat n < of_nat m ↔ of_nat n + 1 ≤ of_nat m : iff.refl - ... ↔ of_nat (succ n) ≤ of_nat m : of_nat_succ n ▸ !iff.refl - ... ↔ succ n ≤ m : of_nat_le_of_nat + ... ↔ of_nat (nat.succ n) ≤ of_nat m : of_nat_succ n ▸ !iff.refl + ... ↔ nat.succ n ≤ m : of_nat_le_of_nat ... ↔ n < m : iff.symm (lt_iff_succ_le _ _) theorem lt_of_of_nat_lt_of_nat {m n : ℕ} (H : of_nat m < of_nat n) : #nat m < n := @@ -137,8 +137,8 @@ theorem lt.irrefl (a : ℤ) : ¬ a < a := calc a + succ n = a : Hn ... = a + 0 : by simp, - have H3 : succ n = 0, from add.left_cancel H2, - have H4 : succ n = 0, from of_nat.inj H3, + have H3 : nat.succ n = 0, from add.left_cancel H2, + have H4 : nat.succ n = 0, from of_nat.inj H3, absurd H4 !succ_ne_zero) theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b := @@ -160,7 +160,7 @@ iff.intro have H2 : a ≠ b, from and.elim_right H, obtain (n : ℕ) (Hn : a + n = b), from le.elim H1, have H3 : n ≠ 0, from (assume H' : n = 0, H2 (!add_zero ▸ H' ▸ Hn)), - obtain (k : ℕ) (Hk : n = succ k), from nat.exists_eq_succ_of_ne_zero H3, + obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero H3, lt.intro (Hk ▸ Hn)) theorem le_iff_lt_or_eq (a b : ℤ) : a ≤ b ↔ (a < b ∨ a = b) := @@ -171,7 +171,7 @@ iff.intro (assume H1 : a ≠ b, obtain (n : ℕ) (Hn : a + n = b), from le.elim H, have H2 : n ≠ 0, from (assume H' : n = 0, H1 (!add_zero ▸ H' ▸ Hn)), - obtain (k : ℕ) (Hk : n = succ k), from nat.exists_eq_succ_of_ne_zero H2, + obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero H2, or.inl (lt.intro (Hk ▸ Hn)))) (assume H, or.elim H @@ -202,19 +202,19 @@ le.intro ... = 0 + n * m : zero_add)) theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b := -obtain (n : ℕ) (Hn : 0 + succ n = a), from lt.elim Ha, -obtain (m : ℕ) (Hm : 0 + succ m = b), from lt.elim Hb, +obtain (n : ℕ) (Hn : 0 + nat.succ n = a), from lt.elim Ha, +obtain (m : ℕ) (Hm : 0 + nat.succ m = b), from lt.elim Hb, lt.intro (eq.symm (calc - a * b = (0 + succ n) * b : Hn - ... = succ n * b : nat.zero_add - ... = succ n * (0 + succ m) : {Hm⁻¹} - ... = succ n * succ m : nat.zero_add - ... = of_nat (succ n * succ m) : of_nat_mul - ... = of_nat (succ n * m + succ n) : nat.mul_succ - ... = of_nat (succ (succ n * m + n)) : nat.add_succ - ... = 0 + succ (succ n * m + n) : zero_add)) + a * b = (0 + nat.succ n) * b : Hn + ... = nat.succ n * b : nat.zero_add + ... = nat.succ n * (0 + nat.succ m) : {Hm⁻¹} + ... = nat.succ n * nat.succ m : nat.zero_add + ... = of_nat (nat.succ n * nat.succ m) : of_nat_mul + ... = of_nat (nat.succ n * m + nat.succ n) : nat.mul_succ + ... = of_nat (nat.succ (nat.succ n * m + n)) : nat.add_succ + ... = 0 + nat.succ (nat.succ n * m + n) : zero_add)) section migrate_algebra open [classes] algebra @@ -324,7 +324,7 @@ le_of_lt_add_one (!sub_add_cancel⁻¹ ▸ H) theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := !sub_add_cancel ▸ (lt_add_one_of_le H) -theorem sign_of_succ (n : nat) : sign (succ n) = 1 := +theorem sign_of_succ (n : nat) : sign (nat.succ n) = 1 := sign_of_pos (of_nat_pos !nat.succ_pos) theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[m +1] :=