385 lines
15 KiB
Text
385 lines
15 KiB
Text
/-
|
||
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Jeremy Avigad
|
||
|
||
The integers, with addition, multiplication, and subtraction.
|
||
-/
|
||
prelude
|
||
import init.data.nat.lemmas init.meta.transfer
|
||
open nat
|
||
|
||
/- the type, coercions, and notation -/
|
||
|
||
inductive int : Type
|
||
| of_nat : nat → int
|
||
| neg_succ_of_nat : nat → int
|
||
|
||
notation `ℤ` := int
|
||
|
||
instance : has_coe nat int := ⟨int.of_nat⟩
|
||
|
||
notation `-[1+ ` n `]` := int.neg_succ_of_nat n
|
||
|
||
instance : decidable_eq int :=
|
||
by tactic.mk_dec_eq_instance
|
||
|
||
protected def int.to_string : int → string
|
||
| (int.of_nat n) := to_string n
|
||
| (int.neg_succ_of_nat n) := "-" ++ to_string (succ n)
|
||
|
||
instance : has_to_string int :=
|
||
⟨int.to_string⟩
|
||
|
||
namespace int
|
||
|
||
protected lemma coe_nat_eq (n : ℕ) : ↑n = int.of_nat n := rfl
|
||
|
||
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
|
||
|
||
/- definitions of basic functions -/
|
||
|
||
def neg_of_nat : ℕ → ℤ
|
||
| 0 := 0
|
||
| (succ m) := -[1+ m]
|
||
|
||
def sub_nat_nat (m n : ℕ) : ℤ :=
|
||
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 : ℤ → ℤ
|
||
| (of_nat n) := neg_of_nat n
|
||
| -[1+ n] := succ n
|
||
|
||
protected def add : ℤ → ℤ → ℤ
|
||
| (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 : ℤ → ℤ → ℤ
|
||
| (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⟩
|
||
|
||
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
|
||
|
||
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
|
||
|
||
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, take 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
|
||
assert 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,
|
||
assert 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 } },
|
||
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)
|
||
(take i n, have n + i + k = (n + k) + i, by simp,
|
||
begin rw [this], exact sub_nat_nat_add_left end)
|
||
(take 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 -/
|
||
|
||
def nat_abs (a : ℤ) : ℕ := int.cases_on a id succ
|
||
|
||
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_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
|
||
|
||
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⟩
|
||
|
||
/-- 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))
|
||
(take i n, rel_int_nat_nat.pos) (take 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, repeat {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, repeat {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]
|
||
|
||
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
|
||
|
||
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 : ℤ → ℕ
|
||
| (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)
|
||
|
||
end int
|