chore(library/init/data/int): keep only definitions
This commit is contained in:
Leonardo de Moura
parent
a023128738
commit
c03d351744
4 changed files with 50 additions and 786 deletions
|
|
@ -6,7 +6,7 @@ Authors: Jeremy Avigad
|
|||
The integers, with addition, multiplication, and subtraction.
|
||||
-/
|
||||
prelude
|
||||
import init.data.nat.lemmas init.data.nat.gcd init.meta.transfer init.data.list
|
||||
import init.data.nat.gcd init.meta.transfer init.data.list
|
||||
open nat
|
||||
|
||||
/- the type, coercions, and notation -/
|
||||
|
|
@ -34,204 +34,71 @@ instance : has_to_string int :=
|
|||
|
||||
namespace int
|
||||
|
||||
protected lemma coe_nat_eq (n : ℕ) : ↑n = int.of_nat n := rfl
|
||||
protected def zero : int := of_nat 0
|
||||
protected def one : int := of_nat 1
|
||||
|
||||
protected def zero : ℤ := of_nat 0
|
||||
protected def one : ℤ := of_nat 1
|
||||
|
||||
instance : has_zero ℤ := ⟨int.zero⟩
|
||||
instance : has_one ℤ := ⟨int.one⟩
|
||||
|
||||
lemma of_nat_zero : of_nat (0 : nat) = (0 : int) := rfl
|
||||
|
||||
lemma of_nat_one : of_nat (1 : nat) = (1 : int) := rfl
|
||||
instance : has_zero int := ⟨int.zero⟩
|
||||
instance : has_one int := ⟨int.one⟩
|
||||
|
||||
/- definitions of basic functions -/
|
||||
|
||||
def neg_of_nat : ℕ → ℤ
|
||||
def neg_of_nat : ℕ → int
|
||||
| 0 := 0
|
||||
| (succ m) := -[1+ m]
|
||||
|
||||
def sub_nat_nat (m n : ℕ) : ℤ :=
|
||||
def sub_nat_nat (m n : ℕ) : int :=
|
||||
match (n - m : nat) with
|
||||
| 0 := of_nat (m - n) -- m ≥ n
|
||||
| (succ k) := -[1+ k] -- m < n, and n - m = succ k
|
||||
end
|
||||
|
||||
protected def neg : ℤ → ℤ
|
||||
protected def neg : int → int
|
||||
| (of_nat n) := neg_of_nat n
|
||||
| -[1+ n] := succ n
|
||||
|
||||
protected def add : ℤ → ℤ → ℤ
|
||||
protected def add : int → int → int
|
||||
| (of_nat m) (of_nat n) := of_nat (m + n)
|
||||
| (of_nat m) -[1+ n] := sub_nat_nat m (succ n)
|
||||
| -[1+ m] (of_nat n) := sub_nat_nat n (succ m)
|
||||
| -[1+ m] -[1+ n] := -[1+ succ (m + n)]
|
||||
|
||||
protected def mul : ℤ → ℤ → ℤ
|
||||
protected def mul : int → int → int
|
||||
| (of_nat m) (of_nat n) := of_nat (m * n)
|
||||
| (of_nat m) -[1+ n] := neg_of_nat (m * succ n)
|
||||
| -[1+ m] (of_nat n) := neg_of_nat (succ m * n)
|
||||
| -[1+ m] -[1+ n] := of_nat (succ m * succ n)
|
||||
|
||||
instance : has_neg ℤ := ⟨int.neg⟩
|
||||
instance : has_add ℤ := ⟨int.add⟩
|
||||
instance : has_mul ℤ := ⟨int.mul⟩
|
||||
instance : has_neg int := ⟨int.neg⟩
|
||||
instance : has_add int := ⟨int.add⟩
|
||||
instance : has_mul int := ⟨int.mul⟩
|
||||
|
||||
lemma of_nat_add (n m : ℕ) : of_nat (n + m) = of_nat n + of_nat m := rfl
|
||||
lemma of_nat_mul (n m : ℕ) : of_nat (n * m) = of_nat n * of_nat m := rfl
|
||||
lemma of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl
|
||||
protected def sub (m n : int) : int :=
|
||||
m + -n
|
||||
|
||||
lemma neg_of_nat_zero : -(of_nat 0) = 0 := rfl
|
||||
lemma neg_of_nat_of_succ (n : ℕ) : -(of_nat (succ n)) = -[1+ n] := rfl
|
||||
lemma neg_neg_of_nat_succ (n : ℕ) : -(-[1+ n]) = of_nat (succ n) := rfl
|
||||
instance : has_sub int := ⟨int.sub⟩
|
||||
|
||||
lemma of_nat_eq_coe (n : ℕ) : of_nat n = ↑n := rfl
|
||||
lemma neg_succ_of_nat_coe (n : ℕ) : -[1+ n] = -↑(n + 1) := rfl
|
||||
|
||||
protected lemma coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n := rfl
|
||||
protected lemma coe_nat_mul (m n : ℕ) : (↑(m * n) : ℤ) = ↑m * ↑n := rfl
|
||||
protected lemma coe_nat_zero : ↑(0 : ℕ) = (0 : ℤ) := rfl
|
||||
protected lemma coe_nat_one : ↑(1 : ℕ) = (1 : ℤ) := rfl
|
||||
protected lemma coe_nat_succ (n : ℕ) : (↑(succ n) : ℤ) = ↑n + 1 := rfl
|
||||
|
||||
protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl
|
||||
protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl
|
||||
protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl
|
||||
|
||||
/- injectivity of the constructor functions -/
|
||||
|
||||
protected lemma of_nat_inj {m n : ℕ} (h : of_nat m = of_nat n) : m = n :=
|
||||
int.no_confusion h id
|
||||
|
||||
protected lemma coe_nat_inj {m n : ℕ} (h : (↑m : ℤ) = ↑n) : m = n :=
|
||||
int.of_nat_inj h
|
||||
|
||||
lemma of_nat_eq_of_nat_iff (m n : ℕ) : of_nat m = of_nat n ↔ m = n :=
|
||||
iff.intro int.of_nat_inj (congr_arg _)
|
||||
|
||||
protected lemma coe_nat_eq_coe_nat_iff (m n : ℕ) : (↑m : ℤ) = ↑n ↔ m = n :=
|
||||
of_nat_eq_of_nat_iff m n
|
||||
|
||||
lemma neg_succ_of_nat_inj {m n : ℕ} (h : neg_succ_of_nat m = neg_succ_of_nat n) : m = n :=
|
||||
int.no_confusion h id
|
||||
|
||||
lemma neg_succ_of_nat_inj_iff {m n : ℕ} : neg_succ_of_nat m = neg_succ_of_nat n ↔ m = n :=
|
||||
⟨neg_succ_of_nat_inj, assume H, by simp [H]⟩
|
||||
|
||||
lemma neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl
|
||||
|
||||
/- basic properties of sub_nat_nat -/
|
||||
|
||||
lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop)
|
||||
(hp : ∀i n, P (n + i) n (of_nat i))
|
||||
(hn : ∀i m, P m (m + i + 1) (-[1+ i])) :
|
||||
P m n (sub_nat_nat m n) :=
|
||||
begin
|
||||
have H : ∀k, n - m = k → P m n (nat.cases_on k (of_nat (m - n)) (λa, -[1+ a])),
|
||||
{ intro k, cases k,
|
||||
{ intro e,
|
||||
cases (nat.le.dest (nat.le_of_sub_eq_zero e)) with k h,
|
||||
rw [h.symm, nat.add_sub_cancel_left],
|
||||
apply hp },
|
||||
{ intro heq,
|
||||
have h : m ≤ n,
|
||||
{ exact nat.le_of_lt (nat.lt_of_sub_eq_succ heq) },
|
||||
rw [nat.sub_eq_iff_eq_add h] at heq,
|
||||
rw [heq, add_comm],
|
||||
apply hn } },
|
||||
delta sub_nat_nat,
|
||||
exact H _ rfl
|
||||
end
|
||||
|
||||
private lemma sub_nat_nat_add_left {m n : ℕ} :
|
||||
sub_nat_nat (m + n) m = of_nat n :=
|
||||
begin
|
||||
dunfold sub_nat_nat,
|
||||
rw [nat.sub_eq_zero_of_le],
|
||||
dunfold sub_nat_nat._match_1,
|
||||
rw [nat.add_sub_cancel_left],
|
||||
apply nat.le_add_right
|
||||
end
|
||||
|
||||
private lemma sub_nat_nat_add_right {m n : ℕ} :
|
||||
sub_nat_nat m (m + n + 1) = neg_succ_of_nat n :=
|
||||
calc sub_nat_nat._match_1 m (m + n + 1) (m + n + 1 - m) =
|
||||
sub_nat_nat._match_1 m (m + n + 1) (m + (n + 1) - m) : by simp
|
||||
... = sub_nat_nat._match_1 m (m + n + 1) (n + 1) : by rw [nat.add_sub_cancel_left]
|
||||
... = neg_succ_of_nat n : rfl
|
||||
|
||||
private lemma sub_nat_nat_add_add (m n k : ℕ) : sub_nat_nat (m + k) (n + k) = sub_nat_nat m n :=
|
||||
sub_nat_nat_elim m n (λm n i, sub_nat_nat (m + k) (n + k) = i)
|
||||
(assume i n, have n + i + k = (n + k) + i, by simp,
|
||||
begin rw [this], exact sub_nat_nat_add_left end)
|
||||
(assume i m, have m + i + 1 + k = (m + k) + i + 1, by simp,
|
||||
begin rw [this], exact sub_nat_nat_add_right end)
|
||||
|
||||
/- nat_abs -/
|
||||
|
||||
@[simp] def nat_abs : ℤ → ℕ
|
||||
@[simp] def nat_abs : int → ℕ
|
||||
| (of_nat m) := m
|
||||
| -[1+ m] := succ m
|
||||
|
||||
lemma nat_abs_of_nat (n : ℕ) : nat_abs ↑n = n := rfl
|
||||
|
||||
lemma eq_zero_of_nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0
|
||||
| (of_nat m) H := congr_arg of_nat H
|
||||
| -[1+ m'] H := absurd H (succ_ne_zero _)
|
||||
|
||||
lemma nat_abs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) : nat_abs a > 0 :=
|
||||
(eq_zero_or_pos _).resolve_left $ mt eq_zero_of_nat_abs_eq_zero h
|
||||
|
||||
lemma nat_abs_zero : nat_abs (0 : int) = (0 : nat) := rfl
|
||||
|
||||
lemma nat_abs_one : nat_abs (1 : int) = (1 : nat) := rfl
|
||||
|
||||
lemma nat_abs_mul_self : Π {a : ℤ}, ↑(nat_abs a * nat_abs a) = a * a
|
||||
| (of_nat m) := rfl
|
||||
| -[1+ m'] := rfl
|
||||
|
||||
@[simp] lemma nat_abs_neg (a : ℤ) : nat_abs (-a) = nat_abs a :=
|
||||
by {cases a with n n, cases n; refl, refl}
|
||||
|
||||
lemma nat_abs_eq : Π (a : ℤ), a = nat_abs a ∨ a = -(nat_abs a)
|
||||
| (of_nat m) := or.inl rfl
|
||||
| -[1+ m'] := or.inr rfl
|
||||
|
||||
lemma eq_coe_or_neg (a : ℤ) : ∃n : ℕ, a = n ∨ a = -n := ⟨_, nat_abs_eq a⟩
|
||||
|
||||
/- sign -/
|
||||
|
||||
def sign : ℤ → ℤ
|
||||
def sign : int → int
|
||||
| (n+1:ℕ) := 1
|
||||
| 0 := 0
|
||||
| -[1+ n] := -1
|
||||
|
||||
@[simp] theorem sign_zero : sign 0 = 0 := rfl
|
||||
@[simp] theorem sign_one : sign 1 = 1 := rfl
|
||||
@[simp] theorem sign_neg_one : sign (-1) = -1 := rfl
|
||||
|
||||
/- Quotient and remainder -/
|
||||
|
||||
-- There are three main conventions for integer division,
|
||||
-- referred here as the E, F, T rounding conventions.
|
||||
-- All three pairs satisfy the identity x % y + (x / y) * y = x
|
||||
-- unconditionally.
|
||||
|
||||
-- E-rounding: This pair satisfies 0 ≤ mod x y < nat_abs y for y ≠ 0
|
||||
protected def div : ℤ → ℤ → ℤ
|
||||
protected def div : int → int → int
|
||||
| (m : ℕ) (n : ℕ) := of_nat (m / n)
|
||||
| (m : ℕ) -[1+ n] := -of_nat (m / succ n)
|
||||
| -[1+ m] 0 := 0
|
||||
| -[1+ m] (n+1:ℕ) := -[1+ m / succ n]
|
||||
| -[1+ m] -[1+ n] := of_nat (succ (m / succ n))
|
||||
|
||||
protected def mod : ℤ → ℤ → ℤ
|
||||
protected def mod : int → int → int
|
||||
| (m : ℕ) n := (m % nat_abs n : ℕ)
|
||||
| -[1+ m] n := sub_nat_nat (nat_abs n) (succ (m % nat_abs n))
|
||||
|
||||
-- F-rounding: This pair satisfies fdiv x y = floor (x / y)
|
||||
def fdiv : ℤ → ℤ → ℤ
|
||||
def fdiv : int → int → int
|
||||
| 0 _ := 0
|
||||
| (m : ℕ) (n : ℕ) := of_nat (m / n)
|
||||
| (m+1:ℕ) -[1+ n] := -[1+ m / succ n]
|
||||
|
|
@ -239,7 +106,7 @@ def fdiv : ℤ → ℤ → ℤ
|
|||
| -[1+ m] (n+1:ℕ) := -[1+ m / succ n]
|
||||
| -[1+ m] -[1+ n] := of_nat (succ m / succ n)
|
||||
|
||||
def fmod : ℤ → ℤ → ℤ
|
||||
def fmod : int → int → int
|
||||
| 0 _ := 0
|
||||
| (m : ℕ) (n : ℕ) := of_nat (m % n)
|
||||
| (m+1:ℕ) -[1+ n] := sub_nat_nat (m % succ n) n
|
||||
|
|
@ -247,225 +114,49 @@ def fmod : ℤ → ℤ → ℤ
|
|||
| -[1+ m] -[1+ n] := -of_nat (succ m % succ n)
|
||||
|
||||
-- T-rounding: This pair satisfies quot x y = round_to_zero (x / y)
|
||||
def quot : ℤ → ℤ → ℤ
|
||||
def quot : int → int → int
|
||||
| (of_nat m) (of_nat n) := of_nat (m / n)
|
||||
| (of_nat m) -[1+ n] := -of_nat (m / succ n)
|
||||
| -[1+ m] (of_nat n) := -of_nat (succ m / n)
|
||||
| -[1+ m] -[1+ n] := of_nat (succ m / succ n)
|
||||
|
||||
def rem : ℤ → ℤ → ℤ
|
||||
def rem : int → int → int
|
||||
| (of_nat m) (of_nat n) := of_nat (m % n)
|
||||
| (of_nat m) -[1+ n] := of_nat (m % succ n)
|
||||
| -[1+ m] (of_nat n) := -of_nat (succ m % n)
|
||||
| -[1+ m] -[1+ n] := -of_nat (succ m % succ n)
|
||||
|
||||
instance : has_div ℤ := ⟨int.div⟩
|
||||
instance : has_mod ℤ := ⟨int.mod⟩
|
||||
instance : has_div int := ⟨int.div⟩
|
||||
instance : has_mod int := ⟨int.mod⟩
|
||||
|
||||
/- gcd -/
|
||||
def gcd (m n : int) : ℕ := gcd (nat_abs m) (nat_abs n)
|
||||
|
||||
def gcd (m n : ℤ) : ℕ := gcd (nat_abs m) (nat_abs n)
|
||||
|
||||
/-- Relator between integers and pairs of natural numbers -/
|
||||
|
||||
inductive rel_int_nat_nat : ℤ → ℕ × ℕ → Prop
|
||||
| pos : ∀{m p}, rel_int_nat_nat (of_nat p) (m + p, m)
|
||||
| neg : ∀{m n}, rel_int_nat_nat (neg_succ_of_nat n) (m, m + n + 1)
|
||||
|
||||
protected lemma rel_sub_nat_nat {a b : ℕ} : rel_int_nat_nat (sub_nat_nat a b) (a, b) :=
|
||||
sub_nat_nat_elim a b (λa b i, rel_int_nat_nat i (a, b))
|
||||
(assume i n, rel_int_nat_nat.pos) (assume i n, rel_int_nat_nat.neg)
|
||||
|
||||
instance right_total_rel_int_nat_nat : relator.right_total rel_int_nat_nat
|
||||
| (n, m) := ⟨_, int.rel_sub_nat_nat⟩
|
||||
|
||||
instance left_total_rel_int_nat_nat : relator.left_total rel_int_nat_nat
|
||||
| (of_nat n) := ⟨(0 + n, 0), rel_int_nat_nat.pos⟩
|
||||
| (neg_succ_of_nat n) := ⟨(0, 0 + n + 1), rel_int_nat_nat.neg⟩
|
||||
|
||||
instance bi_total_rel_int_nat_nat : relator.bi_total rel_int_nat_nat :=
|
||||
⟨int.left_total_rel_int_nat_nat, int.right_total_rel_int_nat_nat⟩
|
||||
|
||||
protected lemma rel_neg_of_nat {m} : ∀{n}, rel_int_nat_nat (neg_of_nat n) (m, m + n)
|
||||
| 0 := rel_int_nat_nat.pos
|
||||
| (nat.succ n) := rel_int_nat_nat.neg
|
||||
|
||||
protected lemma rel_eq : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ iff))
|
||||
eq (λa b, a.1 + b.2 = b.1 + a.2)
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') :=
|
||||
calc of_nat p = of_nat p'
|
||||
↔ (m + m') + p = (m + m') + p' : by rw [of_nat_eq_of_nat_iff, add_left_cancel_iff]
|
||||
... ↔ (m + p) + m' = (m' + p') + m : by simp
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') :=
|
||||
calc of_nat p = -[1+ n'] ↔ (m' + m) + (n' + p + 1) = (m' + m) + 0 :
|
||||
begin rw [add_left_cancel_iff], apply iff.intro; intro; contradiction end
|
||||
... ↔ (m + p) + (m' + n' + 1) = m' + m : by simp
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') :=
|
||||
calc -[1+ n] = of_nat p' ↔ (m + m') + 0 = (m + m') + (n + p' + 1) :
|
||||
begin rw [add_left_cancel_iff], apply iff.intro; intro; contradiction end
|
||||
... ↔ m + m' = m' + p' + (m + n + 1) : by simp
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') :=
|
||||
calc -[1+ n] = -[1+ n'] ↔ (m + m' + 1) + n' = (m + m' + 1) + n :
|
||||
by rw [neg_succ_of_nat_inj_iff, add_left_cancel_iff, eq_comm]
|
||||
... ↔ m + (m' + n' + 1) = m' + (m + n + 1) : by simp
|
||||
|
||||
/- should this be more general, i.e. ∀{n}, rel_int_nat_nat 0 (n, n) ? -/
|
||||
protected lemma rel_zero : rel_int_nat_nat 0 (0, 0) :=
|
||||
rel_int_nat_nat.pos
|
||||
|
||||
protected lemma rel_one : rel_int_nat_nat 1 (1, 0) :=
|
||||
rel_int_nat_nat.pos
|
||||
|
||||
protected lemma rel_neg : (rel_int_nat_nat ⇒ rel_int_nat_nat) has_neg.neg (λa, (a.2, a.1))
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) := int.rel_neg_of_nat
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) := rel_int_nat_nat.pos
|
||||
|
||||
protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat))
|
||||
has_add.add (λa b, (a.1 + b.1, a.2 + b.2))
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') :=
|
||||
have eq : m + p + (m' + p') = m + m' + (p + p'),
|
||||
by simp,
|
||||
show rel_int_nat_nat (of_nat (p + p')) (m + p + (m' + p'), m + m'),
|
||||
begin rw [eq], apply rel_int_nat_nat.pos end
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') :=
|
||||
have eq1 : m + p + m' = p + (m + m'),
|
||||
by simp,
|
||||
have eq2 : m + (m' + n' + 1) = (n' + 1) + (m + m'),
|
||||
by simp,
|
||||
show rel_int_nat_nat (sub_nat_nat p (n' + 1)) (m + p + m', m + (m' + n' + 1)),
|
||||
begin
|
||||
rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm],
|
||||
apply int.rel_sub_nat_nat
|
||||
end
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') :=
|
||||
have eq1 : m + (m' + p') = p' + (m + m'),
|
||||
by simp,
|
||||
have eq2 : (m + n + 1) + m' = (n + 1) + (m + m'),
|
||||
by simp,
|
||||
show rel_int_nat_nat (sub_nat_nat p' (n + 1)) (m + (m' + p'), (m + n + 1) + m'),
|
||||
begin
|
||||
rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm],
|
||||
apply int.rel_sub_nat_nat
|
||||
end
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') :=
|
||||
have eq : (m + n + 1) + (m' + n' + 1) = (m + m') + (n + n' + 1) + 1,
|
||||
by simp,
|
||||
show rel_int_nat_nat -[1+ (n + n' + 1)] (m + m', (m + n + 1) + (m' + n' + 1)),
|
||||
begin rw [eq], apply rel_int_nat_nat.neg end
|
||||
|
||||
protected lemma rel_mul : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat))
|
||||
has_mul.mul (λa b, (a.1 * b.1 + a.2 * b.2, a.1 * b.2 + a.2 * b.1))
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') :=
|
||||
have e : (m + p) * (m' + p') + m * m' = (m + p) * m' + m * (m' + p') + p * p',
|
||||
by simp [mul_add, add_mul],
|
||||
show rel_int_nat_nat (of_nat (p * p'))
|
||||
((m + p) * (m' + p') + m * m', (m + p) * m' + m * (m' + p')),
|
||||
begin rw [e], exact rel_int_nat_nat.pos end
|
||||
| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') :=
|
||||
have e : (m + p) * (m' + n' + 1) + m * m' = (m + p) * m' + m * (m' + n' + 1) + (p * (n' + 1)),
|
||||
by simp [mul_add, add_mul],
|
||||
show rel_int_nat_nat (of_nat p * -[1+ n'])
|
||||
((m + p) * m' + m * (m' + n' + 1), (m + p) * (m' + n' + 1) + m * m'),
|
||||
begin rw [e], exact int.rel_neg_of_nat end
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') :=
|
||||
have e : m * m' + (m + n + 1) * (m' + p') = m * (m' + p') + (m + n + 1) * m' + ((n + 1) * p'),
|
||||
by simp [mul_add, add_mul],
|
||||
show rel_int_nat_nat (-[1+ n] * of_nat p')
|
||||
(m * (m' + p') + (m + n + 1) * m', m * m' + (m + n + 1) * (m' + p')),
|
||||
begin rw [e], exact int.rel_neg_of_nat end
|
||||
| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') :=
|
||||
have e : m * m' + (m + n + 1) * (m' + n' + 1) =
|
||||
m * (m' + n' + 1) + (m + n + 1) * m' + ((n + 1) * (n' + 1)),
|
||||
by simp [mul_add, add_mul],
|
||||
show rel_int_nat_nat (-[1+ n] * -[1+ n'])
|
||||
(m * m' + (m + n + 1) * (m' + n' + 1), m * (m' + n' + 1) + (m + n + 1) * m'),
|
||||
begin rw [e], exact rel_int_nat_nat.pos end
|
||||
|
||||
/-
|
||||
int is a ring
|
||||
-/
|
||||
|
||||
protected meta def transfer_core : tactic unit := do
|
||||
transfer.transfer [`relator.rel_forall_of_total, `relator.rel_not,
|
||||
`int.rel_eq, `int.rel_zero, `int.rel_one,
|
||||
`int.rel_add, `int.rel_neg, `int.rel_mul]
|
||||
|
||||
protected meta def transfer (distrib := tt) : tactic unit :=
|
||||
if distrib then `[int.transfer_core, simp [add_mul, mul_add]]
|
||||
else `[int.transfer_core, simp]
|
||||
|
||||
local attribute [simp] mul_assoc mul_comm mul_left_comm
|
||||
|
||||
instance : comm_ring int :=
|
||||
{ add := int.add,
|
||||
add_assoc := by int.transfer,
|
||||
zero := int.zero,
|
||||
zero_add := by int.transfer,
|
||||
add_zero := by int.transfer,
|
||||
neg := int.neg,
|
||||
add_left_neg := by int.transfer,
|
||||
add_comm := by int.transfer,
|
||||
mul := int.mul,
|
||||
mul_assoc := by int.transfer tt,
|
||||
one := int.one,
|
||||
one_mul := by int.transfer,
|
||||
mul_one := by int.transfer,
|
||||
left_distrib := by int.transfer tt,
|
||||
right_distrib := by int.transfer tt,
|
||||
mul_comm := by int.transfer}
|
||||
|
||||
/- Extra instances to short-circuit type class resolution -/
|
||||
instance : has_sub int := by apply_instance
|
||||
instance : add_comm_monoid int := by apply_instance
|
||||
instance : add_monoid int := by apply_instance
|
||||
instance : monoid int := by apply_instance
|
||||
instance : comm_monoid int := by apply_instance
|
||||
instance : comm_semigroup int := by apply_instance
|
||||
instance : semigroup int := by apply_instance
|
||||
instance : add_comm_semigroup int := by apply_instance
|
||||
instance : add_semigroup int := by apply_instance
|
||||
instance : comm_semiring int := by apply_instance
|
||||
instance : semiring int := by apply_instance
|
||||
instance : ring int := by apply_instance
|
||||
instance : distrib int := by apply_instance
|
||||
|
||||
instance : zero_ne_one_class ℤ :=
|
||||
{ zero := 0, one := 1, zero_ne_one := by int.transfer }
|
||||
|
||||
lemma of_nat_sub {n m : ℕ} (h : m ≤ n) : of_nat (n - m) = of_nat n - of_nat m :=
|
||||
show of_nat (n - m) = of_nat n + neg_of_nat m, from match m, h with
|
||||
| 0, h := rfl
|
||||
| succ m, h := show of_nat (n - succ m) = sub_nat_nat n (succ m),
|
||||
by delta sub_nat_nat; rw sub_eq_zero_of_le h; refl
|
||||
end
|
||||
|
||||
lemma neg_succ_of_nat_coe' (n : ℕ) : -[1+ n] = -↑n - 1 :=
|
||||
by rw [sub_eq_add_neg, ← neg_add]; refl
|
||||
|
||||
protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := of_nat_sub
|
||||
|
||||
protected lemma sub_nat_nat_eq_coe {m n : ℕ} : sub_nat_nat m n = ↑m - ↑n :=
|
||||
sub_nat_nat_elim m n (λm n i, i = ↑m - ↑n)
|
||||
(λi n, by simp [int.coe_nat_add]; refl)
|
||||
(λi n, by simp [int.coe_nat_add, int.coe_nat_one, int.neg_succ_of_nat_eq];
|
||||
apply congr_arg; rw[add_left_comm]; simp)
|
||||
|
||||
def to_nat : ℤ → ℕ
|
||||
def to_nat : int → ℕ
|
||||
| (n : ℕ) := n
|
||||
| -[1+ n] := 0
|
||||
|
||||
theorem to_nat_sub (m n : ℕ) : to_nat (m - n) = m - n :=
|
||||
by rw [← int.sub_nat_nat_eq_coe]; exact sub_nat_nat_elim m n
|
||||
(λm n i, to_nat i = m - n)
|
||||
(λi n, by rw [nat.add_sub_cancel_left]; refl)
|
||||
(λi n, by rw [add_assoc, nat.sub_eq_zero_of_le (nat.le_add_right _ _)]; refl)
|
||||
def nat_mod (m n : int) : ℕ := (m % n).to_nat
|
||||
|
||||
-- Since mod x y is always nonnegative when y ≠ 0, we can make a nat version of it
|
||||
def nat_mod (m n : ℤ) : ℕ := (m % n).to_nat
|
||||
private def nonneg : int → Prop
|
||||
| (of_nat _) := true
|
||||
| -[1+ _] := false
|
||||
|
||||
theorem sign_mul_nat_abs : ∀ (a : ℤ), sign a * nat_abs a = a
|
||||
| (n+1:ℕ) := one_mul _
|
||||
| 0 := rfl
|
||||
| -[1+ n] := (neg_eq_neg_one_mul _).symm
|
||||
protected def le (a b : int) : Prop := nonneg (b - a)
|
||||
|
||||
instance : has_le int := ⟨int.le⟩
|
||||
|
||||
protected def lt (a b : int) : Prop := (a + 1) ≤ b
|
||||
|
||||
instance : has_lt int := ⟨int.lt⟩
|
||||
|
||||
private def decidable_nonneg : Π (a : int), decidable (nonneg a)
|
||||
| (of_nat m) := decidable.true
|
||||
| -[1+ m] := decidable.false
|
||||
|
||||
instance decidable_le (a b : int) : decidable (a ≤ b) :=
|
||||
decidable_nonneg _
|
||||
|
||||
instance decidable_lt (a b : int) : decidable (a < b) :=
|
||||
decidable_nonneg _
|
||||
|
||||
end int
|
||||
|
|
|
|||
|
|
@ -1,120 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
|
||||
Auxiliary lemmas used to compare int numerals.
|
||||
-/
|
||||
prelude
|
||||
import init.data.int.order
|
||||
|
||||
namespace int
|
||||
/- Auxiliary lemmas for proving that to int numerals are different -/
|
||||
|
||||
/- 1. Lemmas for reducing the problem to the case where the numerals are positive -/
|
||||
|
||||
protected lemma ne_neg_of_ne {a b : ℤ} : a ≠ b → -a ≠ -b :=
|
||||
λ h₁ h₂, absurd (neg_inj h₂) h₁
|
||||
|
||||
protected lemma neg_ne_zero_of_ne {a : ℤ} : a ≠ 0 → -a ≠ 0 :=
|
||||
λ h₁ h₂,
|
||||
have -a = -0, by rwa neg_zero,
|
||||
have a = 0, from neg_inj this,
|
||||
by contradiction
|
||||
|
||||
protected lemma zero_ne_neg_of_ne {a : ℤ} (h : 0 ≠ a) : 0 ≠ -a :=
|
||||
ne.symm (int.neg_ne_zero_of_ne (ne.symm h))
|
||||
|
||||
protected lemma neg_ne_of_pos {a b : ℤ} : a > 0 → b > 0 → -a ≠ b :=
|
||||
λ h₁ h₂ h,
|
||||
begin
|
||||
rw [← h] at h₂,
|
||||
exact absurd (le_of_lt h₁) (not_le_of_gt (neg_of_neg_pos h₂))
|
||||
end
|
||||
|
||||
protected lemma ne_neg_of_pos {a b : ℤ} : a > 0 → b > 0 → a ≠ -b :=
|
||||
λ h₁ h₂, ne.symm (int.neg_ne_of_pos h₂ h₁)
|
||||
|
||||
/- 2. Lemmas for proving that positive int numerals are nonneg and positive -/
|
||||
|
||||
protected lemma one_pos : (1:int) > 0 :=
|
||||
zero_lt_one
|
||||
|
||||
protected lemma bit0_pos {a : ℤ} : a > 0 → bit0 a > 0 :=
|
||||
λ h, add_pos h h
|
||||
|
||||
protected lemma bit1_pos {a : ℤ} : a ≥ 0 → bit1 a > 0 :=
|
||||
λ h, lt_add_of_le_of_pos (add_nonneg h h) zero_lt_one
|
||||
|
||||
protected lemma zero_nonneg : (0:int) ≥ 0 :=
|
||||
le_refl 0
|
||||
|
||||
protected lemma one_nonneg : (1:int) ≥ 0 :=
|
||||
le_of_lt (zero_lt_one)
|
||||
|
||||
protected lemma bit0_nonneg {a : ℤ} : a ≥ 0 → bit0 a ≥ 0 :=
|
||||
λ h, add_nonneg h h
|
||||
|
||||
protected lemma bit1_nonneg {a : ℤ} : a ≥ 0 → bit1 a ≥ 0 :=
|
||||
λ h, le_of_lt (int.bit1_pos h)
|
||||
|
||||
protected lemma nonneg_of_pos {a : ℤ} : a > 0 → a ≥ 0 :=
|
||||
le_of_lt
|
||||
|
||||
/- 3. nat_abs auxiliary lemmas -/
|
||||
|
||||
lemma neg_succ_of_nat_lt_zero (n : ℕ) : neg_succ_of_nat n < 0 :=
|
||||
@lt.intro _ _ n (by simp [neg_succ_of_nat_coe, int.coe_nat_succ, int.coe_nat_add, int.coe_nat_one])
|
||||
|
||||
lemma of_nat_ge_zero (n : ℕ) : of_nat n ≥ 0 :=
|
||||
@le.intro _ _ n (by rw [zero_add, int.coe_nat_eq])
|
||||
|
||||
lemma of_nat_nat_abs_eq_of_nonneg : ∀ {a : ℤ}, a ≥ 0 → of_nat (nat_abs a) = a
|
||||
| (of_nat n) h := rfl
|
||||
| (neg_succ_of_nat n) h := absurd (neg_succ_of_nat_lt_zero n) (not_lt_of_ge h)
|
||||
|
||||
lemma ne_of_nat_abs_ne_nat_abs_of_nonneg {a b : ℤ} (ha : a ≥ 0) (hb : b ≥ 0) (h : nat_abs a ≠ nat_abs b) : a ≠ b :=
|
||||
assume h,
|
||||
have of_nat (nat_abs a) = of_nat (nat_abs b), by rwa [of_nat_nat_abs_eq_of_nonneg ha, of_nat_nat_abs_eq_of_nonneg hb],
|
||||
begin injection this, contradiction end
|
||||
|
||||
protected lemma ne_of_nat_ne_nonneg_case {a b : ℤ} {n m : nat} (ha : a ≥ 0) (hb : b ≥ 0) (e1 : nat_abs a = n) (e2 : nat_abs b = m) (h : n ≠ m) : a ≠ b :=
|
||||
have nat_abs a ≠ nat_abs b, by rwa [e1, e2],
|
||||
ne_of_nat_abs_ne_nat_abs_of_nonneg ha hb this
|
||||
|
||||
/- 4. Aux lemmas for pushing nat_abs inside numerals
|
||||
nat_abs_zero and nat_abs_one are defined at init/data/int/basic.lean -/
|
||||
|
||||
lemma nat_abs_of_nat_core (n : ℕ) : nat_abs (of_nat n) = n :=
|
||||
rfl
|
||||
|
||||
lemma nat_abs_of_neg_succ_of_nat (n : ℕ) : nat_abs (neg_succ_of_nat n) = nat.succ n :=
|
||||
rfl
|
||||
|
||||
protected lemma nat_abs_add_nonneg : ∀ {a b : int}, a ≥ 0 → b ≥ 0 → nat_abs (a + b) = nat_abs a + nat_abs b
|
||||
| (of_nat n) (of_nat m) h₁ h₂ :=
|
||||
have of_nat n + of_nat m = of_nat (n + m), from rfl,
|
||||
by simp [nat_abs_of_nat_core, this]
|
||||
| _ (neg_succ_of_nat m) h₁ h₂ := absurd (neg_succ_of_nat_lt_zero m) (not_lt_of_ge h₂)
|
||||
| (neg_succ_of_nat n) _ h₁ h₂ := absurd (neg_succ_of_nat_lt_zero n) (not_lt_of_ge h₁)
|
||||
|
||||
protected lemma nat_abs_add_neg : ∀ {a b : int}, a < 0 → b < 0 → nat_abs (a + b) = nat_abs a + nat_abs b
|
||||
| (neg_succ_of_nat n) (neg_succ_of_nat m) h₁ h₂ :=
|
||||
have -[1+ n] + -[1+ m] = -[1+ nat.succ (n + m)], from rfl,
|
||||
begin simp [nat_abs_of_neg_succ_of_nat, this, nat.succ_add, nat.add_succ] end
|
||||
|
||||
protected lemma nat_abs_bit0 : ∀ (a : int), nat_abs (bit0 a) = bit0 (nat_abs a)
|
||||
| (of_nat n) := int.nat_abs_add_nonneg (of_nat_ge_zero n) (of_nat_ge_zero n)
|
||||
| (neg_succ_of_nat n) := int.nat_abs_add_neg (neg_succ_of_nat_lt_zero n) (neg_succ_of_nat_lt_zero n)
|
||||
|
||||
protected lemma nat_abs_bit0_step {a : int} {n : nat} (h : nat_abs a = n) : nat_abs (bit0 a) = bit0 n :=
|
||||
begin rw [← h], apply int.nat_abs_bit0 end
|
||||
|
||||
protected lemma nat_abs_bit1_nonneg {a : int} (h : a ≥ 0) : nat_abs (bit1 a) = bit1 (nat_abs a) :=
|
||||
show nat_abs (bit0 a + 1) = bit0 (nat_abs a) + nat_abs 1, from
|
||||
by rw [int.nat_abs_add_nonneg (int.bit0_nonneg h) (le_of_lt (zero_lt_one)), int.nat_abs_bit0]
|
||||
|
||||
protected lemma nat_abs_bit1_nonneg_step {a : int} {n : nat} (h₁ : a ≥ 0) (h₂ : nat_abs a = n) : nat_abs (bit1 a) = bit1 n :=
|
||||
begin rw [← h₂], apply int.nat_abs_bit1_nonneg h₁ end
|
||||
|
||||
end int
|
||||
|
|
@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.data.int.basic init.data.int.order init.data.int.comp_lemmas
|
||||
import init.data.int.basic
|
||||
|
|
|
|||
|
|
@ -1,307 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Jeremy Avigad
|
||||
|
||||
The order relation on the integers.
|
||||
-/
|
||||
prelude
|
||||
import init.data.int.basic init.data.ordering.basic
|
||||
|
||||
namespace int
|
||||
|
||||
private def nonneg (a : ℤ) : Prop := int.cases_on a (assume n, true) (assume n, false)
|
||||
|
||||
protected def le (a b : ℤ) : Prop := nonneg (b - a)
|
||||
|
||||
instance : has_le int := ⟨int.le⟩
|
||||
|
||||
protected def lt (a b : ℤ) : Prop := (a + 1) ≤ b
|
||||
|
||||
instance : has_lt int := ⟨int.lt⟩
|
||||
|
||||
private def decidable_nonneg (a : ℤ) : decidable (nonneg a) :=
|
||||
int.cases_on a (assume a, decidable.true) (assume a, decidable.false)
|
||||
|
||||
instance decidable_le (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _
|
||||
|
||||
instance decidable_lt (a b : ℤ) : decidable (a < b) := decidable_nonneg _
|
||||
|
||||
lemma lt_iff_add_one_le (a b : ℤ) : a < b ↔ a + 1 ≤ b := iff.refl _
|
||||
|
||||
private lemma nonneg.elim {a : ℤ} : nonneg a → ∃ n : ℕ, a = n :=
|
||||
int.cases_on a (assume n H, exists.intro n rfl) (assume n', false.elim)
|
||||
|
||||
private lemma nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
|
||||
int.cases_on a (assume n, or.inl trivial) (assume n, or.inr trivial)
|
||||
|
||||
lemma le.intro_sub {a b : ℤ} {n : ℕ} (h : b - a = n) : a ≤ b :=
|
||||
show nonneg (b - a), by rw h; trivial
|
||||
|
||||
lemma le.intro {a b : ℤ} {n : ℕ} (h : a + n = b) : a ≤ b :=
|
||||
le.intro_sub (by rw [← h]; simp)
|
||||
|
||||
lemma le.dest_sub {a b : ℤ} (h : a ≤ b) : ∃ n : ℕ, b - a = n := nonneg.elim h
|
||||
|
||||
lemma le.dest {a b : ℤ} (h : a ≤ b) : ∃ n : ℕ, a + n = b :=
|
||||
match (le.dest_sub h) with
|
||||
| ⟨n, h₁⟩ := exists.intro n begin rw [← h₁, add_comm], simp end
|
||||
end
|
||||
|
||||
lemma le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P :=
|
||||
exists.elim (le.dest h) h'
|
||||
|
||||
protected lemma le_total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
|
||||
or.imp_right
|
||||
(assume H : nonneg (-(b - a)),
|
||||
have -(b - a) = a - b, by simp,
|
||||
show nonneg (a - b), from this ▸ H)
|
||||
(nonneg_or_nonneg_neg (b - a))
|
||||
|
||||
lemma coe_nat_le_coe_nat_of_le {m n : ℕ} (h : m ≤ n) : (↑m : ℤ) ≤ ↑n :=
|
||||
match nat.le.dest h with
|
||||
| ⟨k, (hk : m + k = n)⟩ := le.intro (begin rw [← hk], reflexivity end)
|
||||
end
|
||||
|
||||
lemma le_of_coe_nat_le_coe_nat {m n : ℕ} (h : (↑m : ℤ) ≤ ↑n) : m ≤ n :=
|
||||
le.elim h (assume k, assume hk : ↑m + ↑k = ↑n,
|
||||
have m + k = n, from int.coe_nat_inj ((int.coe_nat_add m k).trans hk),
|
||||
nat.le.intro this)
|
||||
|
||||
lemma coe_nat_le_coe_nat_iff (m n : ℕ) : (↑m : ℤ) ≤ ↑n ↔ m ≤ n :=
|
||||
iff.intro le_of_coe_nat_le_coe_nat coe_nat_le_coe_nat_of_le
|
||||
|
||||
lemma coe_zero_le (n : ℕ) : 0 ≤ (↑n : ℤ) :=
|
||||
coe_nat_le_coe_nat_of_le n.zero_le
|
||||
|
||||
lemma eq_coe_of_zero_le {a : ℤ} (h : 0 ≤ a) : ∃ n : ℕ, a = n :=
|
||||
by have t := le.dest_sub h; simp at t; exact t
|
||||
|
||||
lemma eq_succ_of_zero_lt {a : ℤ} (h : 0 < a) : ∃ n : ℕ, a = n.succ :=
|
||||
let ⟨n, (h : ↑(1+n) = a)⟩ := le.dest h in
|
||||
⟨n, by rw add_comm at h; exact h.symm⟩
|
||||
|
||||
lemma lt_add_succ (a : ℤ) (n : ℕ) : a < a + ↑(nat.succ n) :=
|
||||
le.intro (show a + 1 + n = a + nat.succ n, begin simp [int.coe_nat_eq], reflexivity end)
|
||||
|
||||
lemma lt.intro {a b : ℤ} {n : ℕ} (h : a + nat.succ n = b) : a < b :=
|
||||
h ▸ lt_add_succ a n
|
||||
|
||||
lemma lt.dest {a b : ℤ} (h : a < b) : ∃ n : ℕ, a + ↑(nat.succ n) = b :=
|
||||
le.elim h (assume n, assume hn : a + 1 + n = b,
|
||||
exists.intro n begin rw [← hn, add_assoc, add_comm (1 : int)], reflexivity end)
|
||||
|
||||
lemma lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(nat.succ n) = b → P) : P :=
|
||||
exists.elim (lt.dest h) h'
|
||||
|
||||
lemma coe_nat_lt_coe_nat_iff (n m : ℕ) : (↑n : ℤ) < ↑m ↔ n < m :=
|
||||
begin rw [lt_iff_add_one_le, ← int.coe_nat_succ, coe_nat_le_coe_nat_iff], reflexivity end
|
||||
|
||||
lemma lt_of_coe_nat_lt_coe_nat {m n : ℕ} (h : (↑m : ℤ) < ↑n) : m < n :=
|
||||
(coe_nat_lt_coe_nat_iff _ _).mp h
|
||||
|
||||
lemma coe_nat_lt_coe_nat_of_lt {m n : ℕ} (h : m < n) : (↑m : ℤ) < ↑n :=
|
||||
(coe_nat_lt_coe_nat_iff _ _).mpr h
|
||||
|
||||
/- show that the integers form an ordered additive group -/
|
||||
|
||||
protected lemma le_refl (a : ℤ) : a ≤ a :=
|
||||
le.intro (add_zero a)
|
||||
|
||||
protected lemma le_trans {a b c : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
|
||||
le.elim h₁ (assume n, assume hn : a + n = b,
|
||||
le.elim h₂ (assume m, assume hm : b + m = c,
|
||||
begin apply le.intro, rw [← hm, ← hn, add_assoc], reflexivity end))
|
||||
|
||||
protected lemma le_antisymm {a b : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b :=
|
||||
le.elim h₁ (assume n, assume hn : a + n = b,
|
||||
le.elim h₂ (assume m, assume hm : b + m = a,
|
||||
have a + ↑(n + m) = a + 0, by rw [int.coe_nat_add, ← add_assoc, hn, hm, add_zero a],
|
||||
have (↑(n + m) : ℤ) = 0, from add_left_cancel this,
|
||||
have n + m = 0, from int.coe_nat_inj this,
|
||||
have n = 0, from nat.eq_zero_of_add_eq_zero_right this,
|
||||
show a = b, begin rw [← hn, this, int.coe_nat_zero, add_zero a] end))
|
||||
|
||||
protected lemma lt_irrefl (a : ℤ) : ¬ a < a :=
|
||||
assume : a < a,
|
||||
lt.elim this (assume n, assume hn : a + nat.succ n = a,
|
||||
have a + nat.succ n = a + 0, by rw [hn, add_zero],
|
||||
have nat.succ n = 0, from int.coe_nat_inj (add_left_cancel this),
|
||||
show false, from nat.succ_ne_zero _ this)
|
||||
|
||||
protected lemma ne_of_lt {a b : ℤ} (h : a < b) : a ≠ b :=
|
||||
(assume : a = b, absurd (begin rewrite this at h, exact h end) (int.lt_irrefl b))
|
||||
|
||||
lemma le_of_lt {a b : ℤ} (h : a < b) : a ≤ b :=
|
||||
lt.elim h (assume n, assume hn : a + nat.succ n = b, le.intro hn)
|
||||
|
||||
protected lemma lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) :=
|
||||
iff.intro
|
||||
(assume h, ⟨le_of_lt h, int.ne_of_lt h⟩)
|
||||
(assume ⟨aleb, aneb⟩,
|
||||
le.elim aleb (assume n, assume hn : a + n = b,
|
||||
have n ≠ 0,
|
||||
from (assume : n = 0, aneb begin rw [← hn, this, int.coe_nat_zero, add_zero] end),
|
||||
have n = nat.succ (nat.pred n),
|
||||
from eq.symm (nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero this)),
|
||||
lt.intro (begin rewrite this at hn, exact hn end)))
|
||||
|
||||
lemma lt_succ (a : ℤ) : a < a + 1 :=
|
||||
int.le_refl (a + 1)
|
||||
|
||||
protected lemma add_le_add_left {a b : ℤ} (h : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
|
||||
le.elim h (assume n, assume hn : a + n = b,
|
||||
le.intro (show c + a + n = c + b, begin rw [add_assoc, hn] end))
|
||||
|
||||
protected lemma add_lt_add_left {a b : ℤ} (h : a < b) (c : ℤ) : c + a < c + b :=
|
||||
iff.mpr (int.lt_iff_le_and_ne _ _)
|
||||
(and.intro
|
||||
(int.add_le_add_left (le_of_lt h) _)
|
||||
(assume heq, int.lt_irrefl b begin rw add_left_cancel heq at h, exact h end))
|
||||
|
||||
protected lemma mul_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b :=
|
||||
le.elim ha (assume n, assume hn,
|
||||
le.elim hb (assume m, assume hm,
|
||||
le.intro (show 0 + ↑n * ↑m = a * b, begin rw [← hn, ← hm], simp [zero_add] end)))
|
||||
|
||||
protected lemma mul_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
|
||||
lt.elim ha (assume n, assume hn,
|
||||
lt.elim hb (assume m, assume hm,
|
||||
lt.intro (show 0 + ↑(nat.succ (nat.succ n * m + n)) = a * b,
|
||||
begin rw [← hn, ← hm], simp [int.coe_nat_zero],
|
||||
rw [← int.coe_nat_mul], simp [nat.mul_succ, nat.succ_add] end)))
|
||||
|
||||
protected lemma zero_lt_one : (0 : ℤ) < 1 := trivial
|
||||
|
||||
protected lemma lt_iff_le_not_le {a b : ℤ} : a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
|
||||
begin
|
||||
simp [int.lt_iff_le_and_ne], split; intro h,
|
||||
{ cases h with hab hn, split,
|
||||
{ assumption },
|
||||
{ intro hba, simp [int.le_antisymm hab hba] at *, contradiction } },
|
||||
{ cases h with hab hn, split,
|
||||
{ assumption },
|
||||
{ intro h, simp [*] at * } }
|
||||
end
|
||||
|
||||
instance : decidable_linear_ordered_comm_ring int :=
|
||||
{ le := int.le,
|
||||
le_refl := int.le_refl,
|
||||
le_trans := @int.le_trans,
|
||||
le_antisymm := @int.le_antisymm,
|
||||
lt := int.lt,
|
||||
lt_iff_le_not_le := @int.lt_iff_le_not_le,
|
||||
add_le_add_left := @int.add_le_add_left,
|
||||
add_lt_add_left := @int.add_lt_add_left,
|
||||
zero_ne_one := zero_ne_one,
|
||||
mul_nonneg := @int.mul_nonneg,
|
||||
mul_pos := @int.mul_pos,
|
||||
le_total := int.le_total,
|
||||
zero_lt_one := int.zero_lt_one,
|
||||
decidable_eq := int.decidable_eq,
|
||||
decidable_le := int.decidable_le,
|
||||
decidable_lt := int.decidable_lt,
|
||||
..int.comm_ring }
|
||||
|
||||
instance : decidable_linear_ordered_comm_group int :=
|
||||
by apply_instance
|
||||
|
||||
lemma eq_nat_abs_of_zero_le {a : ℤ} (h : 0 ≤ a) : a = nat_abs a :=
|
||||
let ⟨n, e⟩ := eq_coe_of_zero_le h in by rw e; refl
|
||||
|
||||
lemma le_nat_abs {a : ℤ} : a ≤ nat_abs a :=
|
||||
or.elim (le_total 0 a)
|
||||
(λh, by rw eq_nat_abs_of_zero_le h; refl)
|
||||
(λh, le_trans h (coe_zero_le _))
|
||||
|
||||
lemma neg_succ_lt_zero (n : ℕ) : -[1+ n] < 0 :=
|
||||
lt_of_not_ge $ λ h, let ⟨m, h⟩ := eq_coe_of_zero_le h in by contradiction
|
||||
|
||||
lemma eq_neg_succ_of_lt_zero : ∀ {a : ℤ}, a < 0 → ∃ n : ℕ, a = -[1+ n]
|
||||
| (n : ℕ) h := absurd h (not_lt_of_ge (coe_zero_le _))
|
||||
| -[1+ n] h := ⟨n, rfl⟩
|
||||
|
||||
/- more facts specific to int -/
|
||||
|
||||
theorem of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial
|
||||
|
||||
theorem coe_succ_pos (n : nat) : (nat.succ n : ℤ) > 0 :=
|
||||
coe_nat_lt_coe_nat_of_lt (nat.succ_pos _)
|
||||
|
||||
theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
|
||||
let ⟨n, h⟩ := eq_coe_of_zero_le (neg_nonneg_of_nonpos H) in
|
||||
⟨n, eq_neg_of_eq_neg h.symm⟩
|
||||
|
||||
theorem nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : (nat_abs a : ℤ) = a :=
|
||||
match a, eq_coe_of_zero_le H with ._, ⟨n, rfl⟩ := rfl end
|
||||
|
||||
theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : (nat_abs a : ℤ) = -a :=
|
||||
by rw [← nat_abs_neg, nat_abs_of_nonneg (neg_nonneg_of_nonpos H)]
|
||||
|
||||
theorem abs_eq_nat_abs : ∀ a : ℤ, abs a = nat_abs a
|
||||
| (n : ℕ) := abs_of_nonneg $ coe_zero_le _
|
||||
| -[1+ n] := abs_of_nonpos $ le_of_lt $ neg_succ_lt_zero _
|
||||
|
||||
theorem nat_abs_abs (a : ℤ) : nat_abs (abs a) = nat_abs a :=
|
||||
by rw [abs_eq_nat_abs]; refl
|
||||
|
||||
theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b := H
|
||||
|
||||
theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := H
|
||||
|
||||
theorem lt_add_one_of_le {a b : ℤ} (H : a ≤ b) : a < b + 1 :=
|
||||
add_le_add_right H 1
|
||||
|
||||
theorem le_of_lt_add_one {a b : ℤ} (H : a < b + 1) : a ≤ b :=
|
||||
le_of_add_le_add_right H
|
||||
|
||||
theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b :=
|
||||
sub_right_lt_of_lt_add $ lt_add_one_of_le H
|
||||
|
||||
theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b :=
|
||||
le_of_lt_add_one $ lt_add_of_sub_right_lt H
|
||||
|
||||
theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 :=
|
||||
le_sub_right_of_add_le H
|
||||
|
||||
theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b :=
|
||||
add_le_of_le_sub_right H
|
||||
|
||||
theorem sign_of_succ (n : nat) : sign (nat.succ n) = 1 := rfl
|
||||
|
||||
theorem sign_eq_one_of_pos {a : ℤ} (h : 0 < a) : sign a = 1 :=
|
||||
match a, eq_succ_of_zero_lt h with ._, ⟨n, rfl⟩ := rfl end
|
||||
|
||||
theorem sign_eq_neg_one_of_neg {a : ℤ} (h : a < 0) : sign a = -1 :=
|
||||
match a, eq_neg_succ_of_lt_zero h with ._, ⟨n, rfl⟩ := rfl end
|
||||
|
||||
lemma eq_zero_of_sign_eq_zero : Π {a : ℤ}, sign a = 0 → a = 0
|
||||
| 0 _ := rfl
|
||||
|
||||
theorem pos_of_sign_eq_one : ∀ {a : ℤ}, sign a = 1 → 0 < a
|
||||
| (n+1:ℕ) _ := coe_nat_lt_coe_nat_of_lt (nat.succ_pos _)
|
||||
|
||||
theorem neg_of_sign_eq_neg_one : ∀ {a : ℤ}, sign a = -1 → a < 0
|
||||
| (n+1:ℕ) h := match h with end
|
||||
| 0 h := match h with end
|
||||
| -[1+ n] _ := neg_succ_lt_zero _
|
||||
|
||||
theorem sign_eq_one_iff_pos (a : ℤ) : sign a = 1 ↔ 0 < a :=
|
||||
⟨pos_of_sign_eq_one, sign_eq_one_of_pos⟩
|
||||
|
||||
theorem sign_eq_neg_one_iff_neg (a : ℤ) : sign a = -1 ↔ a < 0 :=
|
||||
⟨neg_of_sign_eq_neg_one, sign_eq_neg_one_of_neg⟩
|
||||
|
||||
theorem sign_eq_zero_iff_zero (a : ℤ) : sign a = 0 ↔ a = 0 :=
|
||||
⟨eq_zero_of_sign_eq_zero, λ h, by rw [h, sign_zero]⟩
|
||||
|
||||
theorem sign_mul_abs (a : ℤ) : sign a * abs a = a :=
|
||||
by rw [abs_eq_nat_abs, sign_mul_nat_abs]
|
||||
|
||||
theorem eq_one_of_mul_eq_self_left {a b : ℤ} (Hpos : a ≠ 0) (H : b * a = a) : b = 1 :=
|
||||
eq_of_mul_eq_mul_right Hpos (by rw [one_mul, H])
|
||||
|
||||
theorem eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
|
||||
eq_of_mul_eq_mul_left Hpos (by rw [mul_one, H])
|
||||
|
||||
end int
|
||||
Loading…
Add table
Reference in a new issue