refactor(library/data/int/basic): make the integers an instance of ring
This commit is contained in:
Jeremy Avigad
parent
43633085b9
commit
9d2587c79b
7 changed files with 427 additions and 499 deletions
|
|
@ -172,31 +172,31 @@ section group
|
|||
... = a⁻¹ * (a * b) : H
|
||||
... = b : inv_mul_cancel_left
|
||||
|
||||
theorem inv_one_eq : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (mul.left_id 1)
|
||||
theorem inv_one : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (mul.left_id 1)
|
||||
|
||||
theorem inv_inv_eq (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a)
|
||||
theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a)
|
||||
|
||||
theorem eq_of_inv_eq_inv {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
|
||||
theorem inv.inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
|
||||
calc
|
||||
a = (a⁻¹)⁻¹ : !inv_inv_eq⁻¹
|
||||
a = (a⁻¹)⁻¹ : !inv_inv⁻¹
|
||||
... = (b⁻¹)⁻¹ : H
|
||||
... = b : inv_inv_eq
|
||||
... = b : inv_inv
|
||||
|
||||
theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
|
||||
iff.intro (assume H, eq_of_inv_eq_inv H) (assume H, congr_arg _ H)
|
||||
iff.intro (assume H, inv.inj H) (assume H, congr_arg _ H)
|
||||
|
||||
theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
|
||||
inv_one_eq ▸ inv_eq_inv_iff_eq a 1
|
||||
inv_one ▸ inv_eq_inv_iff_eq a 1
|
||||
|
||||
theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
|
||||
H⁻¹ ▸ (inv_inv_eq b)⁻¹
|
||||
H⁻¹ ▸ (inv_inv b)⁻¹
|
||||
|
||||
theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
|
||||
iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv
|
||||
|
||||
theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
|
||||
calc
|
||||
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv_eq
|
||||
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv
|
||||
... = 1 : mul.left_inv
|
||||
|
||||
theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) = b :=
|
||||
|
|
@ -238,16 +238,16 @@ section group
|
|||
H⁻¹ ▸ !mul_inv_cancel_right
|
||||
|
||||
theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * b⁻¹ = c) : a = c * b :=
|
||||
!inv_inv_eq ▸ (eq_mul_inv_of_mul_eq H)
|
||||
!inv_inv ▸ (eq_mul_inv_of_mul_eq H)
|
||||
|
||||
theorem eq_mul_of_inv_mul_eq {a b c : A} (H : a⁻¹ * b = c) : b = a * c :=
|
||||
!inv_inv_eq ▸ (eq_inv_mul_of_mul_eq H)
|
||||
!inv_inv ▸ (eq_inv_mul_of_mul_eq H)
|
||||
|
||||
theorem mul_eq_of_eq_inv_mul {a b c : A} (H : a = b⁻¹ * c) : b * a = c :=
|
||||
!inv_inv_eq ▸ (inv_mul_eq_of_eq_mul H)
|
||||
!inv_inv ▸ (inv_mul_eq_of_eq_mul H)
|
||||
|
||||
theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
|
||||
!inv_inv_eq ▸ (mul_inv_eq_of_eq_mul H)
|
||||
!inv_inv ▸ (mul_inv_eq_of_eq_mul H)
|
||||
|
||||
theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
|
||||
iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
|
||||
|
|
@ -308,30 +308,30 @@ section add_group
|
|||
... = -a + (a + b) : H
|
||||
... = b : neg_add_cancel_left
|
||||
|
||||
theorem neg_zero_eq : -0 = 0 := neg_eq_of_add_eq_zero (add.left_id 0)
|
||||
theorem neg_zero : -0 = 0 := neg_eq_of_add_eq_zero (add.left_id 0)
|
||||
|
||||
theorem neg_neg_eq (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
|
||||
theorem neg_neg (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
|
||||
|
||||
theorem eq_of_neg_eq_neg {a b : A} (H : -a = -b) : a = b :=
|
||||
theorem neg.inj {a b : A} (H : -a = -b) : a = b :=
|
||||
calc
|
||||
a = -(-a) : neg_neg_eq
|
||||
a = -(-a) : neg_neg
|
||||
... = b : neg_eq_of_add_eq_zero (H⁻¹ ▸ (add.left_inv _))
|
||||
|
||||
theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
|
||||
iff.intro (assume H, eq_of_neg_eq_neg H) (assume H, congr_arg _ H)
|
||||
iff.intro (assume H, neg.inj H) (assume H, congr_arg _ H)
|
||||
|
||||
theorem neg_eq_zero_iff_eq_zero (a b : A) : -a = 0 ↔ a = 0 :=
|
||||
neg_zero_eq ▸ !neg_eq_neg_iff_eq
|
||||
theorem neg_eq_zero_iff_eq_zero (a : A) : -a = 0 ↔ a = 0 :=
|
||||
neg_zero ▸ !neg_eq_neg_iff_eq
|
||||
|
||||
theorem eq_neg_of_eq_neg {a b : A} (H : a = -b) : b = -a :=
|
||||
H⁻¹ ▸ (neg_neg_eq b)⁻¹
|
||||
H⁻¹ ▸ (neg_neg b)⁻¹
|
||||
|
||||
theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
|
||||
iff.intro !eq_neg_of_eq_neg !eq_neg_of_eq_neg
|
||||
|
||||
theorem add.right_inv (a : A) : a + -a = 0 :=
|
||||
calc
|
||||
a + -a = -(-a) + -a : neg_neg_eq
|
||||
a + -a = -(-a) + -a : neg_neg
|
||||
... = 0 : add.left_inv
|
||||
|
||||
theorem add_neg_cancel_left (a b : A) : a + (-a + b) = b :=
|
||||
|
|
@ -366,16 +366,16 @@ section add_group
|
|||
H⁻¹ ▸ !add_neg_cancel_right
|
||||
|
||||
theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -b = c) : a = c + b :=
|
||||
!neg_neg_eq ▸ (eq_add_neg_of_add_eq H)
|
||||
!neg_neg ▸ (eq_add_neg_of_add_eq H)
|
||||
|
||||
theorem eq_add_of_neg_add_eq {a b c : A} (H : -a + b = c) : b = a + c :=
|
||||
!neg_neg_eq ▸ (eq_neg_add_of_add_eq H)
|
||||
!neg_neg ▸ (eq_neg_add_of_add_eq H)
|
||||
|
||||
theorem add_eq_of_eq_neg_add {a b c : A} (H : a = -b + c) : b + a = c :=
|
||||
!neg_neg_eq ▸ (neg_add_eq_of_eq_add H)
|
||||
!neg_neg ▸ (neg_add_eq_of_eq_add H)
|
||||
|
||||
theorem add_eq_of_eq_add_neg {a b c : A} (H : a = b + -c) : a + c = b :=
|
||||
!neg_neg_eq ▸ (add_neg_eq_of_eq_add H)
|
||||
!neg_neg ▸ (add_neg_eq_of_eq_add H)
|
||||
|
||||
theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
|
||||
iff.intro eq_neg_add_of_add_eq add_eq_of_eq_neg_add
|
||||
|
|
@ -427,9 +427,9 @@ section add_group
|
|||
|
||||
theorem zero_sub_eq (a : A) : 0 - a = -a := !add.left_id
|
||||
|
||||
theorem sub_zero_eq (a : A) : a - 0 = a := subst (eq.symm neg_zero_eq) !add.right_id
|
||||
theorem sub_zero_eq (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add.right_id
|
||||
|
||||
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg_eq⁻¹ ▸ rfl
|
||||
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg⁻¹ ▸ rfl
|
||||
|
||||
theorem neg_sub_eq (a b : A) : -(a - b) = b - a :=
|
||||
neg_eq_of_add_eq_zero
|
||||
|
|
|
|||
|
|
@ -216,34 +216,34 @@ section
|
|||
-- !add.left_id ▸ !add_neg_cancel_right ▸ add_le_add_right H1 (-b) -- doesn't work?
|
||||
|
||||
theorem neg_le_neg_iff_le : -a ≤ -b ↔ b ≤ a :=
|
||||
iff.intro (take H, neg_neg_eq a ▸ neg_neg_eq b ▸ neg_le_neg_of_le H) neg_le_neg_of_le
|
||||
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_le_neg_of_le H) neg_le_neg_of_le
|
||||
|
||||
theorem neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a :=
|
||||
neg_zero_eq ▸ neg_le_neg_iff_le a 0
|
||||
neg_zero ▸ neg_le_neg_iff_le a 0
|
||||
|
||||
theorem neg_nonneg_iff_nonpos : 0 ≤ -a ↔ a ≤ 0 :=
|
||||
neg_zero_eq ▸ neg_le_neg_iff_le 0 a
|
||||
neg_zero ▸ neg_le_neg_iff_le 0 a
|
||||
|
||||
theorem neg_lt_neg_of_lt {a b : A} (H : a < b) : -b < -a :=
|
||||
have H1 : 0 < -a + b, from !add.left_inv ▸ !(add_lt_add_left H),
|
||||
!add_neg_cancel_right ▸ !add.left_id ▸ add_lt_add_right H1 (-b)
|
||||
|
||||
theorem neg_lt_neg_iff_lt : -a < -b ↔ b < a :=
|
||||
iff.intro (take H, neg_neg_eq a ▸ neg_neg_eq b ▸ neg_lt_neg_of_lt H) neg_lt_neg_of_lt
|
||||
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ neg_lt_neg_of_lt H) neg_lt_neg_of_lt
|
||||
|
||||
theorem neg_neg_iff_pos : -a < 0 ↔ 0 < a :=
|
||||
neg_zero_eq ▸ neg_lt_neg_iff_lt a 0
|
||||
neg_zero ▸ neg_lt_neg_iff_lt a 0
|
||||
|
||||
theorem neg_pos_iff_neg : 0 < -a ↔ a < 0 :=
|
||||
neg_zero_eq ▸ neg_lt_neg_iff_lt 0 a
|
||||
neg_zero ▸ neg_lt_neg_iff_lt 0 a
|
||||
|
||||
theorem le_neg_iff_le_neg : a ≤ -b ↔ b ≤ -a := !neg_neg_eq ▸ !neg_le_neg_iff_le
|
||||
theorem le_neg_iff_le_neg : a ≤ -b ↔ b ≤ -a := !neg_neg ▸ !neg_le_neg_iff_le
|
||||
|
||||
theorem neg_le_iff_neg_le : -a ≤ b ↔ -b ≤ a := !neg_neg_eq ▸ !neg_le_neg_iff_le
|
||||
theorem neg_le_iff_neg_le : -a ≤ b ↔ -b ≤ a := !neg_neg ▸ !neg_le_neg_iff_le
|
||||
|
||||
theorem lt_neg_iff_lt_neg : a < -b ↔ b < -a := !neg_neg_eq ▸ !neg_lt_neg_iff_lt
|
||||
theorem lt_neg_iff_lt_neg : a < -b ↔ b < -a := !neg_neg ▸ !neg_lt_neg_iff_lt
|
||||
|
||||
theorem neg_lt_iff_neg_lt : -a < b ↔ -b < a := !neg_neg_eq ▸ !neg_lt_neg_iff_lt
|
||||
theorem neg_lt_iff_neg_lt : -a < b ↔ -b < a := !neg_neg ▸ !neg_lt_neg_iff_lt
|
||||
|
||||
theorem sub_nonneg_iff_le : 0 ≤ a - b ↔ b ≤ a := !sub_self ▸ !add_le_add_right_iff
|
||||
|
||||
|
|
|
|||
|
|
@ -188,7 +188,7 @@ section
|
|||
calc
|
||||
-a * -b = -(a * -b) : !neg_mul_eq_neg_mul⁻¹
|
||||
... = - -(a * b) : neg_mul_eq_mul_neg
|
||||
... = a * b : neg_neg_eq
|
||||
... = a * b : neg_neg
|
||||
|
||||
theorem neg_mul_comm : -a * b = a * -b := !neg_mul_eq_neg_mul⁻¹ ⬝ !neg_mul_eq_mul_neg
|
||||
|
||||
|
|
@ -264,7 +264,7 @@ section
|
|||
(calc
|
||||
a * -c = -(a * c) : {!neg_mul_eq_mul_neg⁻¹}
|
||||
... = -(-b) : H'
|
||||
... = b : neg_neg_eq)))
|
||||
... = b : neg_neg)))
|
||||
(assume H : a | b,
|
||||
dvd.elim H
|
||||
(take c, assume H' : a * c = b,
|
||||
|
|
|
|||
|
|
@ -5,10 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Module: int.basic
|
||||
Authors: Floris van Doorn, Jeremy Avigad
|
||||
|
||||
The integers, with addition, multiplication, and subtraction.
|
||||
|
||||
The representation of the integers is chosen to compute efficiently; see the examples in the
|
||||
comments at the end of this file.
|
||||
The integers, with addition, multiplication, and subtraction. The representation of the integers is
|
||||
chosen to compute efficiently; see the examples in the comments at the end of this file.
|
||||
|
||||
To faciliate proving things about these operations, we show that the integers are a quotient of
|
||||
ℕ × ℕ with the usual equivalence relation ≡, and functions
|
||||
|
|
@ -27,31 +25,15 @@ following:
|
|||
|
||||
repr_add (a b : ℤ) : repr (a + b) = padd (repr a) (repr b)
|
||||
padd_congr (p p' q q' : ℕ × ℕ) (H1 : p ≡ p') (H2 : q ≡ q') : padd p q ≡ p' q'
|
||||
|
||||
-/
|
||||
|
||||
import data.nat.basic data.nat.order data.nat.sub data.prod algebra.relation
|
||||
import algebra.binary
|
||||
import data.nat.basic data.nat.order data.nat.sub data.prod
|
||||
import algebra.relation algebra.binary algebra.ordered_ring
|
||||
import tools.fake_simplifier
|
||||
|
||||
open prod relation
|
||||
open decidable binary fake_simplifier
|
||||
open eq.ops
|
||||
|
||||
-- TODO: move
|
||||
namespace nat
|
||||
|
||||
theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
|
||||
(or_resolve_right (zero_or_succ_pred n) (ne.symm (lt_imp_ne H))⁻¹)
|
||||
|
||||
theorem sub_pos_of_gt {m n : ℕ} (H : n > m) : n - m > 0 :=
|
||||
have H1 : n = n - m + m, from (add_sub_ge_left (lt_imp_le H))⁻¹,
|
||||
have H2 : 0 + m < n - m + m, from (add.zero_left m)⁻¹ ▸ H1 ▸ H,
|
||||
!add_lt_cancel_right H2
|
||||
|
||||
end nat
|
||||
|
||||
open nat
|
||||
open prod relation nat
|
||||
open decidable binary fake_simplifier
|
||||
|
||||
/- the type of integers -/
|
||||
|
||||
|
|
@ -65,8 +47,7 @@ definition int.of_num [coercion] (n : num) : ℤ := int.of_nat (nat.of_num n)
|
|||
|
||||
namespace int
|
||||
|
||||
|
||||
/- define key functions so that they compute well -/
|
||||
/- computational definitions of basic functions -/
|
||||
|
||||
definition neg_of_nat (m : ℕ) : ℤ :=
|
||||
nat.cases_on m 0 (take m', neg_succ_of_nat m')
|
||||
|
|
@ -87,11 +68,11 @@ definition add (a b : ℤ) : ℤ :=
|
|||
(take m, -- a = of_nat m
|
||||
cases_on b
|
||||
(take n, of_nat (m + n)) -- b = of_nat n
|
||||
(take n, sub_nat_nat m (succ n))) -- b = neg_succ_of_nat n
|
||||
(take n, sub_nat_nat m (succ n))) -- b = neg_succ_of_nat n
|
||||
(take m, -- a = neg_succ_of_nat m
|
||||
cases_on b
|
||||
(take n, sub_nat_nat n (succ m)) -- b = of_nat n
|
||||
(take n, neg_of_nat (succ m + succ n))) -- b = neg_succ_of_nat n
|
||||
(take n, sub_nat_nat n (succ m)) -- b = of_nat n
|
||||
(take n, neg_of_nat (succ m + succ n))) -- b = neg_succ_of_nat n
|
||||
|
||||
definition mul (a b : ℤ) : ℤ :=
|
||||
cases_on a
|
||||
|
|
@ -101,7 +82,7 @@ definition mul (a b : ℤ) : ℤ :=
|
|||
(take n, neg_of_nat (m * succ n))) -- b = neg_succ_of_nat n
|
||||
(take m, -- a = neg_succ_of_nat m
|
||||
cases_on b
|
||||
(take n, neg_of_nat (succ m * n)) -- b = of_nat n
|
||||
(take n, neg_of_nat (succ m * n)) -- b = of_nat n
|
||||
(take n, of_nat (succ m * succ n))) -- b = neg_succ_of_nat n
|
||||
|
||||
definition sub (a b : ℤ) : ℤ := add a (neg b)
|
||||
|
|
@ -112,7 +93,6 @@ definition le (a b : ℤ) : Prop := nonneg (sub b a)
|
|||
|
||||
definition lt (a b : ℤ) : Prop := le (add a 1) b
|
||||
|
||||
|
||||
/- notation -/
|
||||
|
||||
notation `-[` n `+1]` := int.neg_succ_of_nat n -- for pretty-printing output
|
||||
|
|
@ -124,7 +104,6 @@ infix <= := int.le
|
|||
infix ≤ := int.le
|
||||
infix < := int.lt
|
||||
|
||||
|
||||
/- some basic functions and properties -/
|
||||
|
||||
theorem of_nat_inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n :=
|
||||
|
|
@ -172,25 +151,30 @@ definition nat_abs (a : ℤ) : ℕ := cases_on a (take n, n) (take n', succ n')
|
|||
|
||||
theorem nat_abs_of_nat (n : ℕ) : nat_abs (of_nat n) = n := rfl
|
||||
|
||||
theorem nat_abs_eq_zero {a : ℤ} : nat_abs a = 0 → a = 0 :=
|
||||
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 _))
|
||||
|
||||
|
||||
/-
|
||||
Show int is a quotient of ordered pairs of natural numbers, with the usual
|
||||
equivalence relation.
|
||||
Show int is a quotient of ordered pairs of natural numbers, with the usual
|
||||
equivalence relation.
|
||||
-/
|
||||
|
||||
definition equiv (p q : ℕ × ℕ) : Prop := pr1 p + pr2 q = pr2 p + pr1 q
|
||||
|
||||
notation [local] p `≡` q := equiv p q
|
||||
|
||||
theorem equiv_refl {p : ℕ × ℕ} : p ≡ p := !add.comm
|
||||
theorem equiv.refl {p : ℕ × ℕ} : p ≡ p := !add.comm
|
||||
|
||||
theorem equiv_symm {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
|
||||
theorem equiv.symm {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
|
||||
calc
|
||||
pr1 q + pr2 p = pr2 p + pr1 q : !add.comm
|
||||
... = pr1 p + pr2 q : H⁻¹
|
||||
... = pr2 q + pr1 p : !add.comm
|
||||
|
||||
theorem equiv_trans {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
|
||||
theorem equiv.trans {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
|
||||
have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
|
||||
calc
|
||||
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by simp
|
||||
|
|
@ -201,7 +185,7 @@ have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
|
|||
show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3
|
||||
|
||||
theorem equiv_equiv : is_equivalence equiv :=
|
||||
is_equivalence.mk @equiv_refl @equiv_symm @equiv_trans
|
||||
is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
|
||||
|
||||
theorem equiv_cases {p q : ℕ × ℕ} (H : equiv p q) :
|
||||
(pr1 p ≥ pr2 p ∧ pr1 q ≥ pr2 q) ∨ (pr1 p < pr2 p ∧ pr1 q < pr2 q) :=
|
||||
|
|
@ -213,18 +197,17 @@ or.elim (@le_or_gt (pr2 p) (pr1 p))
|
|||
have H2 : pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_right H1 (pr2 q),
|
||||
or.inr (and.intro H1 (add_lt_cancel_left H2)))
|
||||
|
||||
theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv_refl
|
||||
theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl
|
||||
|
||||
theorem eq_equiv_trans {p q r : ℕ × ℕ} (H1 : p = q) (H2 : q ≡ r) : p ≡ r := H1⁻¹ ▸ H2
|
||||
theorem equiv_of_eq_of_equiv {p q r : ℕ × ℕ} (H1 : p = q) (H2 : q ≡ r) : p ≡ r := H1⁻¹ ▸ H2
|
||||
|
||||
theorem equiv_eq_trans {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q = r) : p ≡ r := H2 ▸ H1
|
||||
|
||||
calc_trans equiv_trans
|
||||
calc_refl equiv_refl
|
||||
calc_symm equiv_symm
|
||||
calc_trans eq_equiv_trans
|
||||
calc_trans equiv_eq_trans
|
||||
theorem equiv_of_equiv_of_eq {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q = r) : p ≡ r := H2 ▸ H1
|
||||
|
||||
calc_trans equiv.trans
|
||||
calc_refl equiv.refl
|
||||
calc_symm equiv.symm
|
||||
calc_trans equiv_of_eq_of_equiv
|
||||
calc_trans equiv_of_equiv_of_eq
|
||||
|
||||
/- the representation and abstraction functions -/
|
||||
|
||||
|
|
@ -295,10 +278,10 @@ or.elim (equiv_cases Hequiv)
|
|||
theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ ((p ≡ p) ∧ (q ≡ q) ∧ (abstr p = abstr q)) :=
|
||||
iff.intro
|
||||
(assume H : equiv p q,
|
||||
and.intro !equiv_refl (and.intro !equiv_refl (abstr_eq H)))
|
||||
and.intro !equiv.refl (and.intro !equiv.refl (abstr_eq H)))
|
||||
(assume H : equiv p p ∧ equiv q q ∧ abstr p = abstr q,
|
||||
have H1 : abstr p = abstr q, from and.elim_right (and.elim_right H),
|
||||
equiv_trans (H1 ▸ equiv_symm (repr_abstr p)) (repr_abstr q))
|
||||
equiv.trans (H1 ▸ equiv.symm (repr_abstr p)) (repr_abstr q))
|
||||
|
||||
theorem eq_abstr_of_equiv_repr {a : ℤ} {p : ℕ × ℕ} (Hequiv : repr a ≡ p) : a = abstr p :=
|
||||
calc
|
||||
|
|
@ -325,100 +308,20 @@ or.elim (@le_or_gt n m)
|
|||
... = n - m : succ_pred_of_pos (sub_pos_of_gt H)
|
||||
... = dist m n : dist_le (lt_imp_le H))
|
||||
|
||||
theorem nat_abs_eq_zero {a : ℤ} : nat_abs a = 0 → a = 0 :=
|
||||
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 _))
|
||||
|
||||
|
||||
/-
|
||||
Properties of the basic operations.
|
||||
-/
|
||||
|
||||
/- negation -/
|
||||
|
||||
definition pneg (p : ℕ × ℕ) : ℕ × ℕ := (pr2 p, pr1 p)
|
||||
|
||||
-- note: this is =, not just ≡
|
||||
theorem repr_neg (a : ℤ) : repr (- a) = pneg (repr a) :=
|
||||
cases_on a
|
||||
(take m,
|
||||
nat.cases_on m rfl (take m', rfl))
|
||||
(take m', rfl)
|
||||
|
||||
theorem pneg_congr {p p' : ℕ × ℕ} (H : p ≡ p') : pneg p ≡ pneg p' := eq.symm H
|
||||
|
||||
theorem pneg_pneg (p : ℕ × ℕ) : pneg (pneg p) = p := !prod.eta
|
||||
|
||||
theorem neg_zero : -0 = 0 := rfl
|
||||
|
||||
theorem neg_neg (a : ℤ) : -(-a) = a :=
|
||||
have H : repr (-(-a)) = repr a, from
|
||||
(calc
|
||||
repr (-(-a)) = pneg (repr (-a)) : repr_neg
|
||||
... = pneg (pneg (repr a)) : repr_neg
|
||||
... = repr a : pneg_pneg),
|
||||
eq_of_repr_equiv_repr (H ▸ equiv_refl)
|
||||
|
||||
theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b :=
|
||||
calc
|
||||
a = -(-a) : neg_neg
|
||||
... = -(-b) : H
|
||||
... = b : neg_neg
|
||||
|
||||
theorem neg_move {a b : ℤ} (H : -a = b) : -b = a :=
|
||||
H ▸ neg_neg a
|
||||
|
||||
theorem nat_abs_neg (a : ℤ) : nat_abs (-a) = nat_abs a :=
|
||||
calc
|
||||
nat_abs (-a) = nat_abs (abstr (repr (-a))) : abstr_repr
|
||||
... = nat_abs (abstr (pneg (repr a))) : repr_neg
|
||||
... = dist (pr1 (pneg (repr a))) (pr2 (pneg (repr a))) : nat_abs_abstr
|
||||
... = dist (pr2 (pneg (repr a))) (pr1 (pneg (repr a))) : dist_comm
|
||||
... = nat_abs (abstr (repr a)) : nat_abs_abstr
|
||||
... = nat_abs a : abstr_repr
|
||||
|
||||
theorem pos_eq_neg {n m : ℕ} : n = -m → n = 0 ∧ m = 0 :=
|
||||
nat.cases_on m
|
||||
(take H, and.intro (of_nat_inj H) rfl)
|
||||
(take m' H, no_confusion H)
|
||||
|
||||
theorem cases (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - n) :=
|
||||
theorem cases (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) :=
|
||||
cases_on a
|
||||
(take n, or.inl (exists.intro n rfl))
|
||||
(take n', or.inr (exists.intro (succ n') rfl))
|
||||
|
||||
theorem by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) :
|
||||
theorem by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (- of_nat n)) :
|
||||
P a :=
|
||||
or.elim (cases a)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = n), from H, H3⁻¹ ▸ H1 n)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = -n), from H, H3⁻¹ ▸ H2 n)
|
||||
|
||||
---reverse equalities, rename
|
||||
theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) :=
|
||||
or.elim (cases a)
|
||||
(assume H : (∃n : ℕ, a = of_nat n), or.inl H)
|
||||
(assume H,
|
||||
obtain (n : ℕ) (H2 : a = -(of_nat n)), from H,
|
||||
discriminate
|
||||
(assume H3 : n = 0,
|
||||
have H4 : a = of_nat 0, from
|
||||
calc
|
||||
a = -(of_nat n) : H2
|
||||
... = -(of_nat 0) : {H3}
|
||||
... = of_nat 0 : neg_zero,
|
||||
or.inl (exists.intro 0 H4))
|
||||
(take k : ℕ,
|
||||
assume H3 : n = succ k,
|
||||
have H4 : a = -(of_nat (succ k)), from H3 ▸ H2,
|
||||
or.inr (exists.intro k H4)))
|
||||
|
||||
theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ)
|
||||
(H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-(of_nat (succ n)))) : P a :=
|
||||
or.elim (cases_succ a)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = of_nat n), from H, H3⁻¹ ▸ H1 n)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = -(of_nat (succ n))), from H, H3⁻¹ ▸ H2 n)
|
||||
|
||||
/-
|
||||
Show int is a ring.
|
||||
-/
|
||||
|
||||
/- addition -/
|
||||
|
||||
|
|
@ -428,7 +331,7 @@ theorem repr_add (a b : ℤ) : repr (add a b) ≡ padd (repr a) (repr b) :=
|
|||
cases_on a
|
||||
(take m,
|
||||
cases_on b
|
||||
(take n, !equiv_refl)
|
||||
(take n, !equiv.refl)
|
||||
(take n',
|
||||
have H1 : equiv (repr (add (of_nat m) (neg_succ_of_nat n'))) (m, succ n'),
|
||||
from !repr_sub_nat_nat,
|
||||
|
|
@ -466,223 +369,72 @@ calc
|
|||
... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : add.assoc
|
||||
... = padd p (padd q r) : rfl
|
||||
|
||||
theorem add_comm (a b : ℤ) : a + b = b + a :=
|
||||
theorem add.comm (a b : ℤ) : a + b = b + a :=
|
||||
begin
|
||||
apply eq_of_repr_equiv_repr,
|
||||
apply equiv_trans,
|
||||
apply equiv.trans,
|
||||
apply repr_add,
|
||||
apply equiv_symm,
|
||||
apply equiv.symm,
|
||||
apply (eq.subst (padd_comm (repr b) (repr a))),
|
||||
apply repr_add
|
||||
end
|
||||
|
||||
theorem add_assoc (a b c : ℤ) : a + b + c = a + (b + c) :=
|
||||
theorem add.assoc (a b c : ℤ) : a + b + c = a + (b + c) :=
|
||||
have H1 [visible]: repr (a + b + c) ≡ padd (padd (repr a) (repr b)) (repr c), from
|
||||
equiv_trans (repr_add (a + b) c) (padd_congr !repr_add !equiv_refl),
|
||||
equiv.trans (repr_add (a + b) c) (padd_congr !repr_add !equiv.refl),
|
||||
have H2 [visible]: repr (a + (b + c)) ≡ padd (repr a) (padd (repr b) (repr c)), from
|
||||
equiv_trans (repr_add a (b + c)) (padd_congr !equiv_refl !repr_add),
|
||||
equiv.trans (repr_add a (b + c)) (padd_congr !equiv.refl !repr_add),
|
||||
begin
|
||||
apply eq_of_repr_equiv_repr,
|
||||
apply equiv_trans,
|
||||
apply equiv.trans,
|
||||
apply H1,
|
||||
apply (eq.subst ((padd_assoc _ _ _)⁻¹)),
|
||||
apply equiv_symm,
|
||||
apply equiv.symm,
|
||||
apply H2
|
||||
end
|
||||
|
||||
theorem add_zero_right (a : ℤ) : a + 0 = a := cases_on a (take m, rfl) (take m', rfl)
|
||||
theorem add.right_id (a : ℤ) : a + 0 = a := cases_on a (take m, rfl) (take m', rfl)
|
||||
|
||||
theorem add_left_comm (a b c : ℤ) : a + (b + c) = b + (a + c) :=
|
||||
left_comm add_comm add_assoc a b c
|
||||
theorem add.left_id (a : ℤ) : 0 + a = a := add.comm a 0 ▸ add.right_id a
|
||||
|
||||
theorem add_right_comm (a b c : ℤ) : a + b + c = a + c + b :=
|
||||
right_comm add_comm add_assoc a b c
|
||||
/- negation -/
|
||||
|
||||
theorem add_zero_left (a : ℤ) : 0 + a = a :=
|
||||
add_comm a 0 ▸ add_zero_right a
|
||||
definition pneg (p : ℕ × ℕ) : ℕ × ℕ := (pr2 p, pr1 p)
|
||||
|
||||
-- note: this is =, not just ≡
|
||||
theorem repr_neg (a : ℤ) : repr (- a) = pneg (repr a) :=
|
||||
cases_on a
|
||||
(take m,
|
||||
nat.cases_on m rfl (take m', rfl))
|
||||
(take m', rfl)
|
||||
|
||||
theorem pneg_congr {p p' : ℕ × ℕ} (H : p ≡ p') : pneg p ≡ pneg p' := eq.symm H
|
||||
|
||||
theorem pneg_pneg (p : ℕ × ℕ) : pneg (pneg p) = p := !prod.eta
|
||||
|
||||
theorem nat_abs_neg (a : ℤ) : nat_abs (-a) = nat_abs a :=
|
||||
calc
|
||||
nat_abs (-a) = nat_abs (abstr (repr (-a))) : abstr_repr
|
||||
... = nat_abs (abstr (pneg (repr a))) : repr_neg
|
||||
... = dist (pr1 (pneg (repr a))) (pr2 (pneg (repr a))) : nat_abs_abstr
|
||||
... = dist (pr2 (pneg (repr a))) (pr1 (pneg (repr a))) : dist_comm
|
||||
... = nat_abs (abstr (repr a)) : nat_abs_abstr
|
||||
... = nat_abs a : abstr_repr
|
||||
|
||||
theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) :=
|
||||
show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !add.comm ▸ rfl
|
||||
show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add.comm ▸ rfl
|
||||
|
||||
theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
|
||||
show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, by simp
|
||||
|
||||
theorem add_inverse_right (a : ℤ) : a + -a = 0 :=
|
||||
have H : repr (a + -a) ≡ repr 0, from
|
||||
theorem add.left_inv (a : ℤ) : -a + a = 0 :=
|
||||
have H : repr (-a + a) ≡ repr 0, from
|
||||
calc
|
||||
repr (a + -a) ≡ padd (repr a) (repr (neg a)) : repr_add
|
||||
... = padd (repr a) (pneg (repr a)) : repr_neg
|
||||
repr (-a + a) ≡ padd (repr (neg a)) (repr a) : repr_add
|
||||
... = padd (pneg (repr a)) (repr a) : repr_neg
|
||||
... ≡ repr 0 : padd_pneg,
|
||||
eq_of_repr_equiv_repr H
|
||||
|
||||
theorem add_inverse_left (a : ℤ) : -a + a = 0 :=
|
||||
add_comm a (-a) ▸ add_inverse_right a
|
||||
|
||||
theorem pneg_padd_distr (p q : ℕ × ℕ) : pneg (padd p q) = padd (pneg p) (pneg q) := rfl
|
||||
|
||||
theorem neg_add_distr (a b : ℤ) : -(a + b) = -a + -b :=
|
||||
eq_of_repr_equiv_repr
|
||||
(calc
|
||||
repr (-(a + b)) = pneg (repr (a + b)) : repr_neg
|
||||
... ≡ pneg (padd (repr a) (repr b)) : pneg_congr (!repr_add)
|
||||
... = padd (pneg (repr a)) (pneg (repr b)) : pneg_padd_distr
|
||||
... = padd (repr (-a)) (pneg (repr b)) : repr_neg
|
||||
... = padd (repr (-a)) (repr (-b)) : repr_neg
|
||||
... ≡ repr (-a + -b) : equiv_symm (!repr_add))
|
||||
-- TODO: should calc reorient this for us?
|
||||
|
||||
definition pabs (p : ℕ × ℕ) : ℕ := dist (pr1 p) (pr2 p)
|
||||
|
||||
theorem pabs_congr {p q : ℕ × ℕ} (H : p ≡ q) : pabs p = pabs q :=
|
||||
calc
|
||||
pabs p = nat_abs (abstr p) : nat_abs_abstr
|
||||
... = nat_abs (abstr q) : abstr_eq H
|
||||
... = pabs q : nat_abs_abstr
|
||||
|
||||
theorem nat_abs_eq_pabs_repr (a : ℤ) : nat_abs a = pabs (repr a) :=
|
||||
calc
|
||||
nat_abs a = nat_abs (abstr (repr a)) : abstr_repr
|
||||
... = pabs (repr a) : nat_abs_abstr
|
||||
|
||||
theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
|
||||
have H : nat_abs (a + b) = pabs (padd (repr a) (repr b)), from
|
||||
calc
|
||||
nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr
|
||||
... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add,
|
||||
have H1 : nat_abs a = pabs (repr a), from !nat_abs_eq_pabs_repr,
|
||||
have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr,
|
||||
have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b), from !dist_add_le_add_dist,
|
||||
H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
|
||||
|
||||
theorem add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := rfl
|
||||
|
||||
theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl
|
||||
|
||||
/- subtraction -/
|
||||
|
||||
theorem sub_def (a b : ℤ) : a - b = a + -b :=
|
||||
rfl
|
||||
|
||||
theorem add_neg_right (a b : ℤ) : a + -b = a - b :=
|
||||
rfl
|
||||
|
||||
theorem add_neg_left (a b : ℤ) : -a + b = b - a :=
|
||||
add_comm (-a) b
|
||||
|
||||
theorem sub_neg_right (a b : ℤ) : a - (-b) = a + b :=
|
||||
neg_neg b ▸ eq.refl (a - (-b))
|
||||
|
||||
theorem sub_neg_neg (a b : ℤ) : -a - (-b) = b - a :=
|
||||
neg_neg b ▸ add_comm (-a) (-(-b))
|
||||
|
||||
theorem sub_self (a : ℤ) : a - a = 0 :=
|
||||
add_inverse_right a
|
||||
|
||||
theorem sub_zero_right (a : ℤ) : a - 0 = a :=
|
||||
neg_zero⁻¹ ▸ add_zero_right a
|
||||
|
||||
theorem sub_zero_left (a : ℤ) : 0 - a = -a :=
|
||||
add_zero_left (-a)
|
||||
|
||||
theorem neg_sub (a b : ℤ) : -(a - b) = -a + b :=
|
||||
calc
|
||||
-(a - b) = -a + -(-b) : neg_add_distr a (-b)
|
||||
... = -a + b : {neg_neg b}
|
||||
|
||||
theorem neg_sub_flip (a b : ℤ) : -(a - b) = b - a :=
|
||||
calc
|
||||
-(a - b) = -a + b : neg_sub a b
|
||||
... = b - a : add_comm (-a) b
|
||||
|
||||
theorem sub_sub_assoc (a b c : ℤ) : a - b - c = a - (b + c) :=
|
||||
calc
|
||||
a - b - c = a + (-b + -c) : add_assoc a (-b) (-c)
|
||||
... = a + -(b + c) : {(neg_add_distr b c)⁻¹}
|
||||
|
||||
theorem sub_add_assoc (a b c : ℤ) : a - b + c = a - (b - c) :=
|
||||
calc
|
||||
a - b + c = a + (-b + c) : add_assoc a (-b) c
|
||||
... = a + -(b - c) : {(neg_sub b c)⁻¹}
|
||||
|
||||
theorem add_sub_assoc (a b c : ℤ) : a + b - c = a + (b - c) :=
|
||||
add_assoc a b (-c)
|
||||
|
||||
theorem add_sub_inverse (a b : ℤ) : a + b - b = a :=
|
||||
calc
|
||||
a + b - b = a + (b - b) : add_assoc a b (-b)
|
||||
... = a + 0 : {sub_self b}
|
||||
... = a : add_zero_right a
|
||||
|
||||
theorem add_sub_inverse2 (a b : ℤ) : a + b - a = b :=
|
||||
add_comm b a ▸ add_sub_inverse b a
|
||||
|
||||
theorem sub_add_inverse (a b : ℤ) : a - b + b = a :=
|
||||
add_right_comm a b (-b) ▸ add_sub_inverse a b
|
||||
|
||||
-- add_rewrite add_zero_left add_zero_right
|
||||
-- add_rewrite add_comm add_assoc add_left_comm
|
||||
-- add_rewrite sub_def add_inverse_right add_inverse_left
|
||||
-- add_rewrite neg_add_distr
|
||||
---- add_rewrite sub_sub_assoc sub_add_assoc add_sub_assoc
|
||||
---- add_rewrite add_neg_right add_neg_left
|
||||
---- add_rewrite sub_self
|
||||
|
||||
-- ### inversion theorems for add and sub
|
||||
|
||||
-- a + a = 0 -> a = 0
|
||||
-- a = -a -> a = 0
|
||||
|
||||
theorem add_cancel_right {a b c : ℤ} (H : a + c = b + c) : a = b :=
|
||||
calc
|
||||
a = a + c - c : (add_sub_inverse a c)⁻¹
|
||||
... = b + c - c : {H}
|
||||
... = b : add_sub_inverse b c
|
||||
|
||||
theorem add_cancel_left {a b c : ℤ} (H : a + b = a + c) : b = c :=
|
||||
add_cancel_right ((H ▸ (add_comm a b)) ▸ add_comm a c)
|
||||
|
||||
theorem add_eq_zero_right {a b : ℤ} (H : a + b = 0) : -a = b :=
|
||||
have H2 : a + -a = a + b, from (add_inverse_right a)⁻¹ ▸ H⁻¹,
|
||||
show -a = b, from add_cancel_left H2
|
||||
|
||||
theorem add_eq_zero_left {a b : ℤ} (H : a + b = 0) : -b = a :=
|
||||
neg_move (add_eq_zero_right H)
|
||||
|
||||
theorem add_eq_self {a b : ℤ} (H : a + b = a) : b = 0 :=
|
||||
add_cancel_left (H ⬝ (add_zero_right a)⁻¹)
|
||||
|
||||
theorem sub_inj_left {a b c : ℤ} (H : a - b = a - c) : b = c :=
|
||||
neg_inj (add_cancel_left H)
|
||||
|
||||
theorem sub_inj_right {a b c : ℤ} (H : a - b = c - b) : a = c :=
|
||||
add_cancel_right H
|
||||
|
||||
theorem sub_eq_zero {a b : ℤ} (H : a - b = 0) : a = b :=
|
||||
neg_inj (add_eq_zero_right H)
|
||||
|
||||
theorem add_imp_sub_right {a b c : ℤ} (H : a + b = c) : c - b = a :=
|
||||
have H2 : c - b + b = a + b, from (sub_add_inverse c b) ⬝ H⁻¹,
|
||||
add_cancel_right H2
|
||||
|
||||
theorem add_imp_sub_left {a b c : ℤ} (H : a + b = c) : c - a = b :=
|
||||
add_imp_sub_right (add_comm a b ▸ H)
|
||||
|
||||
theorem sub_imp_add {a b c : ℤ} (H : a - b = c) : c + b = a :=
|
||||
neg_neg b ▸ add_imp_sub_right H
|
||||
|
||||
theorem sub_imp_sub {a b c : ℤ} (H : a - b = c) : a - c = b :=
|
||||
have H2 : c + b = a, from sub_imp_add H, add_imp_sub_left H2
|
||||
|
||||
theorem sub_add_add_right (a b c : ℤ) : a + c - (b + c) = a - b :=
|
||||
calc
|
||||
a + c - (b + c) = a + (c - (b + c)) : add_sub_assoc a c (b + c)
|
||||
... = a + (c - b - c) : {(sub_sub_assoc c b c)⁻¹}
|
||||
... = a + -b : {add_sub_inverse2 c (-b)}
|
||||
|
||||
theorem sub_add_add_left (a b c : ℤ) : c + a - (c + b) = a - b :=
|
||||
add_comm b c ▸ add_comm a c ▸ sub_add_add_right a b c
|
||||
|
||||
|
||||
/- multiplication -/
|
||||
|
||||
definition pmul (p q : ℕ × ℕ) : ℕ × ℕ :=
|
||||
|
|
@ -750,97 +502,228 @@ calc
|
|||
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 p * pr2 q + pr2 p * pr1 q) : mul.comm
|
||||
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr2 q * pr1 p + pr2 p * pr1 q) : mul.comm
|
||||
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr2 q * pr1 p + pr1 q * pr2 p) : mul.comm
|
||||
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 q * pr2 p + pr2 q * pr1 p) : add.comm
|
||||
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 q * pr2 p + pr2 q * pr1 p) : nat.add.comm
|
||||
|
||||
theorem mul_comm (a b : ℤ) : a * b = b * a :=
|
||||
theorem mul.comm (a b : ℤ) : a * b = b * a :=
|
||||
eq_of_repr_equiv_repr
|
||||
((calc
|
||||
repr (a * b) = pmul (repr a) (repr b) : repr_mul
|
||||
... = pmul (repr b) (repr a) : pmul_comm
|
||||
... = repr (b * a) : repr_mul) ▸ !equiv_refl)
|
||||
... = repr (b * a) : repr_mul) ▸ !equiv.refl)
|
||||
|
||||
theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) :=
|
||||
by simp
|
||||
|
||||
theorem mul_assoc (a b c : ℤ) : (a * b) * c = a * (b * c) :=
|
||||
theorem mul.assoc (a b c : ℤ) : (a * b) * c = a * (b * c) :=
|
||||
eq_of_repr_equiv_repr
|
||||
((calc
|
||||
repr (a * b * c) = pmul (repr (a * b)) (repr c) : repr_mul
|
||||
... = pmul (pmul (repr a) (repr b)) (repr c) : repr_mul
|
||||
... = pmul (repr a) (pmul (repr b) (repr c)) : pmul_assoc
|
||||
... = pmul (repr a) (repr (b * c)) : repr_mul
|
||||
... = repr (a * (b * c)) : repr_mul) ▸ !equiv_refl)
|
||||
... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl)
|
||||
|
||||
theorem mul_left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) :=
|
||||
left_comm mul_comm mul_assoc
|
||||
|
||||
theorem mul_right_comm : ∀a b c : ℤ, a * b * c = a * c * b :=
|
||||
right_comm mul_comm mul_assoc
|
||||
|
||||
theorem mul_zero_right (a : ℤ) : a * 0 = 0 :=
|
||||
eq_of_repr_equiv_repr (equiv_of_eq
|
||||
((calc
|
||||
repr (a * 0) = pmul (repr a) (repr 0) : repr_mul
|
||||
... = (0, 0) : by simp)))
|
||||
|
||||
theorem mul_zero_left (a : ℤ) : 0 * a = 0 :=
|
||||
mul_comm a 0 ▸ mul_zero_right a
|
||||
|
||||
theorem mul_one_right (a : ℤ) : a * 1 = a :=
|
||||
theorem mul.right_id (a : ℤ) : a * 1 = a :=
|
||||
eq_of_repr_equiv_repr (equiv_of_eq
|
||||
((calc
|
||||
repr (a * 1) = pmul (repr a) (repr 1) : repr_mul
|
||||
... = (pr1 (repr a), pr2 (repr a)) : by simp
|
||||
... = repr a : prod.eta)))
|
||||
|
||||
theorem mul_one_left (a : ℤ) : 1 * a = a :=
|
||||
mul_comm a 1 ▸ mul_one_right a
|
||||
theorem mul.left_id (a : ℤ) : 1 * a = a :=
|
||||
mul.comm a 1 ▸ mul.right_id a
|
||||
|
||||
theorem mul_neg_right (a b : ℤ) : a * -b = -(a * b) :=
|
||||
let a1 := pr1 (repr a), a2 := pr2 (repr a), b1 := pr1 (repr b), b2 := pr2 (repr b) in
|
||||
eq_of_repr_equiv_repr (equiv_of_eq
|
||||
((calc
|
||||
repr (a * -b) = pmul (repr a) (repr (-b)) : repr_mul
|
||||
... = pmul (repr a) (pneg (repr b)) : repr_neg
|
||||
... = (a1 * b2 + a2 * b1, a1 * b1 + a2 * b2) : rfl
|
||||
... = pneg (pmul (repr a) (repr b)) : rfl
|
||||
... = pneg (repr (a * b)) : repr_mul
|
||||
... = repr (-(a * b)) : repr_neg)))
|
||||
|
||||
theorem mul_neg_left (a b : ℤ) : -a * b = -(a * b) :=
|
||||
mul_comm b a ▸ mul_comm b (-a) ▸ mul_neg_right b a
|
||||
|
||||
-- add_rewrite mul_neg_right mul_neg_left
|
||||
|
||||
theorem mul_neg_neg (a b : ℤ) : -a * -b = a * b :=
|
||||
by simp
|
||||
|
||||
theorem mul_right_distr (a b c : ℤ) : (a + b) * c = a * c + b * c :=
|
||||
theorem mul.right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c :=
|
||||
eq_of_repr_equiv_repr
|
||||
(calc
|
||||
repr ((a + b) * c) = pmul (repr (a + b)) (repr c) : repr_mul
|
||||
... ≡ pmul (padd (repr a) (repr b)) (repr c) : pmul_congr !repr_add equiv_refl
|
||||
... ≡ pmul (padd (repr a) (repr b)) (repr c) : pmul_congr !repr_add equiv.refl
|
||||
... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : by simp
|
||||
... = padd (repr (a * c)) (pmul (repr b) (repr c)) : {(repr_mul a c)⁻¹}
|
||||
... = padd (repr (a * c)) (repr (b * c)) : repr_mul
|
||||
... ≡ repr (a * c + b * c) : equiv_symm !repr_add)
|
||||
... ≡ repr (a * c + b * c) : equiv.symm !repr_add)
|
||||
|
||||
theorem mul_left_distr (a b c : ℤ) : a * (b + c) = a * b + a * c :=
|
||||
theorem mul.left_distrib (a b c : ℤ) : a * (b + c) = a * b + a * c :=
|
||||
calc
|
||||
a * (b + c) = (b + c) * a : mul_comm a (b + c)
|
||||
... = b * a + c * a : mul_right_distr b c a
|
||||
... = a * b + c * a : {mul_comm b a}
|
||||
... = a * b + a * c : {mul_comm c a}
|
||||
a * (b + c) = (b + c) * a : mul.comm a (b + c)
|
||||
... = b * a + c * a : mul.right_distrib b c a
|
||||
... = a * b + c * a : {mul.comm b a}
|
||||
... = a * b + a * c : {mul.comm c a}
|
||||
|
||||
theorem mul_sub_right_distr (a b c : ℤ) : (a - b) * c = a * c - b * c :=
|
||||
calc
|
||||
(a + -b) * c = a * c + -b * c : mul_right_distr a (-b) c
|
||||
... = a * c + - (b * c) : {mul_neg_left b c}
|
||||
theorem zero_ne_one : (typeof 0 : int) ≠ 1 :=
|
||||
assume H : 0 = 1,
|
||||
show false, from succ_ne_zero 0 ((of_nat_inj H)⁻¹)
|
||||
|
||||
theorem mul_sub_left_distr (a b c : ℤ) : a * (b - c) = a * b - a * c :=
|
||||
definition comm_ring : algebra.comm_ring int :=
|
||||
algebra.comm_ring.mk add add.assoc zero add.left_id add.right_id neg add.left_inv
|
||||
add.comm mul mul.assoc (of_num 1) mul.left_id mul.right_id mul.left_distrib mul.right_distrib
|
||||
zero_ne_one mul.comm
|
||||
|
||||
/-
|
||||
Instantiate ring theorems to int
|
||||
-/
|
||||
|
||||
section port_algebra
|
||||
open algebra -- TODO: can we "open" algebra only for the duration of this section?
|
||||
instance comm_ring
|
||||
|
||||
theorem mul.left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
|
||||
theorem mul.right_comm : ∀a b c : ℤ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
|
||||
theorem add.left_comm : ∀a b c : ℤ, a + (b + c) = b + (a + c) := algebra.add.left_comm
|
||||
theorem add.right_comm : ∀a b c : ℤ, (a + b) + c = (a + c) + b := algebra.add.right_comm
|
||||
theorem add.left_cancel : ∀{a b c : ℤ}, a + b = a + c → b = c := @algebra.add.left_cancel _ _
|
||||
theorem add.right_cancel : ∀{a b c : ℤ}, a + b = c + b → a = c := @algebra.add.right_cancel _ _
|
||||
theorem neg_add_cancel_left : ∀a b : ℤ, -a + (a + b) = b := algebra.neg_add_cancel_left
|
||||
theorem neg_add_cancel_right : ∀a b : ℤ, a + -b + b = a := algebra.neg_add_cancel_right
|
||||
theorem neg_eq_of_add_eq_zero : ∀{a b : ℤ}, a + b = 0 → -a = b :=
|
||||
@algebra.neg_eq_of_add_eq_zero _ _
|
||||
theorem neg_zero : -0 = 0 := algebra.neg_zero
|
||||
theorem neg_neg : ∀a : ℤ, -(-a) = a := algebra.neg_neg
|
||||
theorem neg.inj : ∀{a b : ℤ}, -a = -b → a = b := @algebra.neg.inj _ _
|
||||
theorem neg_eq_neg_iff_eq : ∀a b : ℤ, -a = -b ↔ a = b := algebra.neg_eq_neg_iff_eq
|
||||
theorem neg_eq_zero_iff_eq_zero : ∀a : ℤ, -a = 0 ↔ a = 0 := algebra.neg_eq_zero_iff_eq_zero
|
||||
theorem eq_neg_of_eq_neg : ∀{a b : ℤ}, a = -b → b = -a := @algebra.eq_neg_of_eq_neg _ _
|
||||
theorem eq_neg_iff_eq_neg : ∀{a b : ℤ}, a = -b ↔ b = -a := @algebra.eq_neg_iff_eq_neg _ _
|
||||
theorem add.right_inv : ∀a : ℤ, a + -a = 0 := algebra.add.right_inv
|
||||
theorem add_neg_cancel_left : ∀a b : ℤ, a + (-a + b) = b := algebra.add_neg_cancel_left
|
||||
theorem add_neg_cancel_right : ∀a b : ℤ, a + b + -b = a := algebra.add_neg_cancel_right
|
||||
theorem neg_add_eq : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add_eq
|
||||
theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + b = c → a = c + -b :=
|
||||
@algebra.eq_add_neg_of_add_eq _ _
|
||||
theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, a + b = c → b = -a + c :=
|
||||
@algebra.eq_neg_add_of_add_eq _ _
|
||||
theorem neg_add_eq_of_eq_add : ∀{a b c : ℤ}, a = b + c → -b + a = c :=
|
||||
@algebra.neg_add_eq_of_eq_add _ _
|
||||
theorem add_neg_eq_of_eq_add : ∀{a b c : ℤ}, a = b + c → a + -c = b :=
|
||||
@algebra.add_neg_eq_of_eq_add _ _
|
||||
theorem eq_add_of_add_neg_eq : ∀{a b c : ℤ}, a + -b = c → a = c + b :=
|
||||
@algebra.eq_add_of_add_neg_eq _ _
|
||||
theorem eq_add_of_neg_add_eq : ∀{a b c : ℤ}, -a + b = c → b = a + c :=
|
||||
@algebra.eq_add_of_neg_add_eq _ _
|
||||
theorem add_eq_of_eq_neg_add : ∀{a b c : ℤ}, a = -b + c → b + a = c :=
|
||||
@algebra.add_eq_of_eq_neg_add _ _
|
||||
theorem add_eq_of_eq_add_neg : ∀{a b c : ℤ}, a = b + -c → a + c = b :=
|
||||
@algebra.add_eq_of_eq_add_neg _ _
|
||||
theorem add_eq_iff_eq_neg_add : ∀a b c : ℤ, a + b = c ↔ b = -a + c :=
|
||||
@algebra.add_eq_iff_eq_neg_add _ _
|
||||
theorem add_eq_iff_eq_add_neg : ∀a b c : ℤ, a + b = c ↔ a = c + -b :=
|
||||
@algebra.add_eq_iff_eq_add_neg _ _
|
||||
theorem sub_self : ∀a : ℤ, a - a = 0 := algebra.sub_self
|
||||
theorem sub_add_cancel : ∀a b : ℤ, a - b + b = a := algebra.sub_add_cancel
|
||||
theorem add_sub_cancel : ∀a b : ℤ, a + b - b = a := algebra.add_sub_cancel
|
||||
theorem eq_of_sub_eq_zero : ∀{a b : ℤ}, a - b = 0 → a = b := @algebra.eq_of_sub_eq_zero _ _
|
||||
theorem eq_iff_sub_eq_zero : ∀a b : ℤ, a = b ↔ a - b = 0 := algebra.eq_iff_sub_eq_zero
|
||||
-- TODO: is there a bug here? see below
|
||||
-- theorem zero_sub_eq : ∀a : ℤ, 0 - a = -a := algebra.zero_sub_eq
|
||||
theorem sub_zero_eq : ∀a : ℤ, a - 0 = a := algebra.sub_zero_eq
|
||||
theorem sub_neg_eq_add : ∀a b : ℤ, a - (-b) = a + b := algebra.sub_neg_eq_add
|
||||
theorem neg_sub_eq : ∀a b : ℤ, -(a - b) = b - a := algebra.neg_sub_eq
|
||||
theorem add_sub_eq : ∀a b c : ℤ, a + (b - c) = a + b - c := algebra.add_sub_eq
|
||||
theorem sub_add_eq_sub_sub_swap : ∀a b c : ℤ, a - (b + c) = a - c - b :=
|
||||
algebra.sub_add_eq_sub_sub_swap
|
||||
theorem sub_eq_iff_eq_add : ∀a b c : ℤ, a - b = c ↔ a = c + b := algebra.sub_eq_iff_eq_add
|
||||
theorem eq_sub_iff_add_eq : ∀a b c : ℤ, a = b - c ↔ a + c = b := algebra.eq_sub_iff_add_eq
|
||||
theorem eq_iff_eq_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a = b ↔ c = d :=
|
||||
@algebra.eq_iff_eq_of_sub_eq_sub _ _
|
||||
theorem sub_add_eq_sub_sub : ∀a b c : ℤ, a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub
|
||||
theorem neg_add_eq_sub : ∀a b : ℤ, -a + b = b - a := algebra.neg_add_eq_sub
|
||||
theorem neg_add_distrib : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add_distrib
|
||||
theorem sub_add_eq_add_sub : ∀a b c : ℤ, a - b + c = a + c - b := algebra.sub_add_eq_add_sub
|
||||
theorem sub_sub_eq : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub_eq
|
||||
theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b :=
|
||||
algebra.add_sub_add_left_eq_sub
|
||||
theorem zero_mul_eq : ∀a : ℤ, 0 * a = 0 := algebra.zero_mul_eq
|
||||
theorem mul_zero_eq : ∀a : ℤ, a * 0 = 0 := algebra.mul_zero_eq
|
||||
theorem neg_mul_eq_neg_mul : ∀a b : ℤ, -(a * b) = -a * b := algebra.neg_mul_eq_neg_mul
|
||||
theorem neg_mul_eq_mul_neg : ∀a b : ℤ, -(a * b) = a * -b := algebra.neg_mul_eq_mul_neg
|
||||
theorem neg_mul_neg_eq : ∀a b : ℤ, -a * -b = a * b := algebra.neg_mul_neg_eq
|
||||
theorem neg_mul_comm : ∀a b : ℤ, -a * b = a * -b := algebra.neg_mul_comm
|
||||
theorem mul_sub_left_distrib : ∀a b c : ℤ, a * (b - c) = a * b - a * c :=
|
||||
algebra.mul_sub_left_distrib
|
||||
theorem mul_sub_right_distrib : ∀a b c : ℤ, (a - b) * c = a * c - b * c :=
|
||||
algebra.mul_sub_right_distrib
|
||||
theorem mul_add_eq_mul_add_iff_sub_mul_add_eq :
|
||||
∀a b c d e : ℤ, a * e + c = b * e + d ↔ (a - b) * e + c = d :=
|
||||
algebra.mul_add_eq_mul_add_iff_sub_mul_add_eq
|
||||
theorem mul_self_sub_mul_self_eq : ∀a b : ℤ, a * a - b * b = (a + b) * (a - b) :=
|
||||
algebra.mul_self_sub_mul_self_eq
|
||||
theorem mul_self_sub_one_eq : ∀a : ℤ, a * a - 1 = (a + 1) * (a - 1) :=
|
||||
algebra.mul_self_sub_one_eq
|
||||
|
||||
/-
|
||||
-- TODO: Something strange is going on this this theorem.
|
||||
|
||||
set_option pp.implicit true
|
||||
set_option pp.coercions true
|
||||
set_option pp.notation false
|
||||
|
||||
theorem zero_sub_eq : ∀a : ℤ, 0 - a = -a := algebra.zero_sub_eq
|
||||
|
||||
-- Lean reports a type mismatch, but evaluating both sides gives exactly the same result.
|
||||
|
||||
eval
|
||||
∀ (a : int),
|
||||
@eq int
|
||||
(@algebra.sub int
|
||||
(@add_comm_group.to_add_group int
|
||||
(@ring.to_add_comm_group int (@comm_ring.to_ring int comm_ring)))
|
||||
(@has_zero.zero int
|
||||
(@add_monoid.to_has_zero int
|
||||
(@add_group.to_add_monoid int
|
||||
(@add_comm_group.to_add_group int
|
||||
(@ring.to_add_comm_group int (@comm_ring.to_ring int comm_ring))))))
|
||||
a)
|
||||
(@has_neg.neg int
|
||||
(@add_group.to_has_neg int
|
||||
(@add_comm_group.to_add_group int
|
||||
(@ring.to_add_comm_group int (@comm_ring.to_ring int comm_ring))))
|
||||
a)
|
||||
|
||||
eval
|
||||
∀ (a : int),
|
||||
@eq int
|
||||
(sub
|
||||
(@has_zero.zero int
|
||||
(@zero_ne_one_class.to_has_zero int
|
||||
(@ring.to_zero_ne_one_class int (@comm_ring.to_ring int comm_ring))))
|
||||
a)
|
||||
(neg a)
|
||||
-/
|
||||
|
||||
end port_algebra
|
||||
|
||||
|
||||
/-
|
||||
Other stuff.
|
||||
TODO: pare down and clean up.
|
||||
-/
|
||||
|
||||
definition pabs (p : ℕ × ℕ) : ℕ := dist (pr1 p) (pr2 p)
|
||||
|
||||
theorem pabs_congr {p q : ℕ × ℕ} (H : p ≡ q) : pabs p = pabs q :=
|
||||
calc
|
||||
a * (b + -c) = a * b + a * -c : mul_left_distr a b (-c)
|
||||
... = a * b + - (a * c) : {mul_neg_right a c}
|
||||
pabs p = nat_abs (abstr p) : nat_abs_abstr
|
||||
... = nat_abs (abstr q) : abstr_eq H
|
||||
... = pabs q : nat_abs_abstr
|
||||
|
||||
theorem nat_abs_eq_pabs_repr (a : ℤ) : nat_abs a = pabs (repr a) :=
|
||||
calc
|
||||
nat_abs a = nat_abs (abstr (repr a)) : abstr_repr
|
||||
... = pabs (repr a) : nat_abs_abstr
|
||||
|
||||
theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
|
||||
have H : nat_abs (a + b) = pabs (padd (repr a) (repr b)), from
|
||||
calc
|
||||
nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr
|
||||
... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add,
|
||||
have H1 : nat_abs a = pabs (repr a), from !nat_abs_eq_pabs_repr,
|
||||
have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr,
|
||||
have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b), from !dist_add_le_add_dist,
|
||||
H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
|
||||
|
||||
theorem add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := rfl
|
||||
|
||||
theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl
|
||||
|
||||
theorem mul_of_nat (n m : ℕ) : of_nat n * of_nat m = n * m := rfl
|
||||
|
||||
|
|
@ -855,31 +738,76 @@ cases_on a
|
|||
(take n, !nat_abs_neg ▸ rfl)
|
||||
(take n', rfl))
|
||||
|
||||
-- add_rewrite mul_zero_left mul_zero_right mul_one_right mul_one_left
|
||||
-- add_rewrite mul_comm mul_assoc mul_left_comm
|
||||
-- add_rewrite mul_distr_right mul_distr_left mul_of_nat mul_sub_distr_left mul_sub_distr_right
|
||||
---reverse equalities, rename
|
||||
theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) :=
|
||||
or.elim (cases a)
|
||||
(assume H : (∃n : ℕ, a = of_nat n), or.inl H)
|
||||
(assume H,
|
||||
obtain (n : ℕ) (H2 : a = -(of_nat n)), from H,
|
||||
discriminate
|
||||
(assume H3 : n = nat.zero,
|
||||
have H4 : a = of_nat nat.zero, from
|
||||
calc
|
||||
a = -(of_nat n) : H2
|
||||
... = -(of_nat nat.zero) : {H3}
|
||||
... = of_nat nat.zero : neg_zero,
|
||||
or.inl (exists.intro nat.zero H4))
|
||||
(take k : ℕ,
|
||||
assume H3 : n = succ k,
|
||||
have H4 : a = -(of_nat (succ k)), from H3 ▸ H2,
|
||||
or.inr (exists.intro k H4)))
|
||||
|
||||
theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ)
|
||||
(H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-(of_nat (succ n)))) : P a :=
|
||||
or.elim (cases_succ a)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = of_nat n), from H, H3⁻¹ ▸ H1 n)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = -(of_nat (succ n))), from H, H3⁻¹ ▸ H2 n)
|
||||
|
||||
theorem neg_sub' (a b : ℤ) : -(a - b) = -a + b :=
|
||||
calc
|
||||
-(a - b) = -a + -(-b) : neg_add_distrib a (-b)
|
||||
... = -a + b : {neg_neg b}
|
||||
|
||||
theorem sub_add_assoc (a b c : ℤ) : a - b + c = a - (b - c) :=
|
||||
calc
|
||||
a - b + c = a + (-b + c) : add.assoc a (-b) c
|
||||
... = a + -(b - c) : {(neg_sub' b c)⁻¹}
|
||||
|
||||
theorem add_sub_assoc (a b c : ℤ) : a + b - c = a + (b - c) :=
|
||||
add.assoc a b (-c)
|
||||
|
||||
theorem add_sub_inverse2 (a b : ℤ) : a + b - a = b :=
|
||||
add.comm b a ▸ !add_sub_cancel
|
||||
|
||||
-- add_rewrite add_left_id add_right_id
|
||||
-- add_rewrite add_comm add.assoc add_left_comm
|
||||
-- add_rewrite sub_def add_inverse_right add_inverse_left
|
||||
-- add_rewrite neg_add_distr
|
||||
---- add_rewrite sub_sub_assoc sub_add_assoc add_sub_assoc
|
||||
---- add_rewrite add_neg_right add_neg_left
|
||||
---- add_rewrite sub_self
|
||||
|
||||
theorem mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 :=
|
||||
have H2 : (nat_abs a) * (nat_abs b) = 0, from
|
||||
have H2 : (nat_abs a) * (nat_abs b) = nat.zero, from
|
||||
calc
|
||||
(nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (mul_nat_abs a b)⁻¹
|
||||
... = (nat_abs 0) : {H}
|
||||
... = 0 : nat_abs_of_nat 0,
|
||||
have H3 : (nat_abs a) = 0 ∨ (nat_abs b) = 0, from mul.eq_zero H2,
|
||||
... = nat.zero : nat_abs_of_nat nat.zero,
|
||||
have H3 : (nat_abs a) = nat.zero ∨ (nat_abs b) = nat.zero, from mul.eq_zero H2,
|
||||
or_of_or_of_imp_of_imp H3
|
||||
(assume H : (nat_abs a) = 0, nat_abs_eq_zero H)
|
||||
(assume H : (nat_abs b) = 0, nat_abs_eq_zero H)
|
||||
(assume H : (nat_abs a) = nat.zero, nat_abs_eq_zero H)
|
||||
(assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H)
|
||||
|
||||
theorem mul_cancel_left_or {a b c : ℤ} (H : a * b = a * c) : a = 0 ∨ b = c :=
|
||||
have H2 : a * (b - c) = 0, by simp,
|
||||
have H3 : a = 0 ∨ b - c = 0, from mul_eq_zero H2,
|
||||
or_of_or_of_imp_right H3 (assume H4 : b - c = 0, sub_eq_zero H4)
|
||||
or_of_or_of_imp_right H3 eq_of_sub_eq_zero
|
||||
|
||||
theorem mul_cancel_left {a b c : ℤ} (H1 : a ≠ 0) (H2 : a * b = a * c) : b = c :=
|
||||
or_resolve_right (mul_cancel_left_or H2) H1
|
||||
|
||||
theorem mul_cancel_right_or {a b c : ℤ} (H : b * a = c * a) : a = 0 ∨ b = c :=
|
||||
mul_cancel_left_or ((H ▸ (mul_comm b a)) ▸ mul_comm c a)
|
||||
mul_cancel_left_or ((H ▸ (mul.comm b a)) ▸ mul.comm c a)
|
||||
|
||||
theorem mul_cancel_right {a b c : ℤ} (H1 : c ≠ 0) (H2 : a * c = b * c) : a = b :=
|
||||
or_resolve_right (mul_cancel_right_or H2) H1
|
||||
|
|
@ -896,7 +824,13 @@ theorem mul_ne_zero_left {a b : ℤ} (H : a * b ≠ 0) : a ≠ 0 :=
|
|||
absurd H3 H)
|
||||
|
||||
theorem mul_ne_zero_right {a b : ℤ} (H : a * b ≠ 0) : b ≠ 0 :=
|
||||
mul_ne_zero_left (mul_comm a b ▸ H)
|
||||
mul_ne_zero_left (mul.comm a b ▸ H)
|
||||
|
||||
theorem sub_inj_left {a b c : ℤ} (H : a - b = a - c) : b = c :=
|
||||
neg.inj (add.left_cancel H)
|
||||
|
||||
theorem sub_inj_right {a b c : ℤ} (H : a - b = c - b) : a = c :=
|
||||
add.right_cancel H
|
||||
|
||||
end int
|
||||
|
||||
|
|
|
|||
|
|
@ -21,18 +21,18 @@ theorem nonneg_elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n :=
|
|||
cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H)
|
||||
|
||||
theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
|
||||
have H1 : b - a = n, from add_imp_sub_right (!add_comm ▸ H),
|
||||
have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
|
||||
have H2 : nonneg n, from true.intro,
|
||||
show nonneg (b - a), from H1⁻¹ ▸ H2
|
||||
|
||||
theorem le_elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
|
||||
obtain (n : ℕ) (H1 : b - a = n), from nonneg_elim H,
|
||||
exists.intro n (!add_comm ▸ sub_imp_add H1)
|
||||
exists.intro n (!add.comm ▸ iff.mp' !add_eq_iff_eq_add_neg (H1⁻¹))
|
||||
|
||||
-- ### partial order
|
||||
|
||||
theorem le_refl (a : ℤ) : a ≤ a :=
|
||||
le_intro (add_zero_right a)
|
||||
le_intro (add.right_id a)
|
||||
|
||||
theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) :=
|
||||
iff.intro
|
||||
|
|
@ -51,7 +51,7 @@ obtain (m : ℕ) (Hm : b + m = c), from le_elim H2,
|
|||
have H3 : a + of_nat (n + m) = c, from
|
||||
calc
|
||||
a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹}
|
||||
... = a + n + m : (add_assoc a n m)⁻¹
|
||||
... = a + n + m : (add.assoc a n m)⁻¹
|
||||
... = b + m : {Hn}
|
||||
... = c : Hm,
|
||||
le_intro H3
|
||||
|
|
@ -62,16 +62,16 @@ obtain (m : ℕ) (Hm : b + m = a), from le_elim H2,
|
|||
have H3 : a + of_nat (n + m) = a + 0, from
|
||||
calc
|
||||
a + of_nat (n + m) = a + (of_nat n + m) : {(add_of_nat n m)⁻¹}
|
||||
... = a + n + m : (add_assoc a n m)⁻¹
|
||||
... = a + n + m : (add.assoc a n m)⁻¹
|
||||
... = b + m : {Hn}
|
||||
... = a : Hm
|
||||
... = a + 0 : (add_zero_right a)⁻¹,
|
||||
have H4 : of_nat (n + m) = of_nat 0, from add_cancel_left H3,
|
||||
... = a + 0 : (add.right_id a)⁻¹,
|
||||
have H4 : of_nat (n + m) = of_nat 0, from add.left_cancel H3,
|
||||
have H5 : n + m = 0, from of_nat_inj H4,
|
||||
have H6 : n = 0, from nat.add.eq_zero_left H5,
|
||||
show a = b, from
|
||||
calc
|
||||
a = a + of_nat 0 : (add_zero_right a)⁻¹
|
||||
a = a + of_nat 0 : (add.right_id a)⁻¹
|
||||
... = a + n : {H6⁻¹}
|
||||
... = b : Hn
|
||||
|
||||
|
|
@ -81,33 +81,32 @@ theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n :=
|
|||
le_intro (eq.refl (a + n))
|
||||
|
||||
theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a :=
|
||||
le_intro (add_comm a n)
|
||||
le_intro (add.comm a n)
|
||||
|
||||
theorem add_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
|
||||
obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
|
||||
have H2 : c + a + n = c + b, from
|
||||
calc
|
||||
c + a + n = c + (a + n) : add_assoc c a n
|
||||
c + a + n = c + (a + n) : add.assoc c a n
|
||||
... = c + b : {Hn},
|
||||
le_intro H2
|
||||
|
||||
theorem add_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a + c ≤ b + c :=
|
||||
add_comm c b ▸ add_comm c a ▸ add_le_left H c
|
||||
add.comm c b ▸ add.comm c a ▸ add_le_left H c
|
||||
|
||||
theorem add_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : c ≤ d) : a + c ≤ b + d :=
|
||||
le_trans (add_le_right H1 c) (add_le_left H2 b)
|
||||
|
||||
theorem add_le_cancel_right {a b c : ℤ} (H : a + c ≤ b + c) : a ≤ b :=
|
||||
have H1 : a + c + -c ≤ b + c + -c, from add_le_right H (-c),
|
||||
have H2 : a + c - c ≤ b + c - c, from !add_neg_right ▸ !add_neg_right ▸ H1,
|
||||
add_sub_inverse b c ▸ add_sub_inverse a c ▸ H2
|
||||
!add_neg_cancel_right ▸ !add_neg_cancel_right ▸ H1
|
||||
|
||||
theorem add_le_cancel_left {a b c : ℤ} (H : c + a ≤ c + b) : a ≤ b :=
|
||||
add_le_cancel_right (add_comm c b ▸ add_comm c a ▸ H)
|
||||
add_le_cancel_right (add.comm c b ▸ add.comm c a ▸ H)
|
||||
|
||||
theorem add_le_inv {a b c d : ℤ} (H1 : a + b ≤ c + d) (H2 : c ≤ a) : b ≤ d :=
|
||||
obtain (n : ℕ) (Hn : c + n = a), from le_elim H2,
|
||||
have H3 : c + (n + b) ≤ c + d, from add_assoc c n b ▸ Hn⁻¹ ▸ H1,
|
||||
have H3 : c + (n + b) ≤ c + d, from add.assoc c n b ▸ Hn⁻¹ ▸ H1,
|
||||
have H4 : n + b ≤ d, from add_le_cancel_left H3,
|
||||
show b ≤ d, from le_trans (le_add_of_nat_left b n) H4
|
||||
|
||||
|
|
@ -120,7 +119,7 @@ discriminate
|
|||
(assume H2 : n = 0,
|
||||
have H3 : a = b, from
|
||||
calc
|
||||
a = a + 0 : (add_zero_right a)⁻¹
|
||||
a = a + 0 : (add.right_id a)⁻¹
|
||||
... = a + n : {H2⁻¹}
|
||||
... = b : Hn,
|
||||
or.inr H3)
|
||||
|
|
@ -137,12 +136,11 @@ discriminate
|
|||
|
||||
theorem le_neg {a b : ℤ} (H : a ≤ b) : -b ≤ -a :=
|
||||
obtain (n : ℕ) (Hn : a + n = b), from le_elim H,
|
||||
have H2 : b - n = a, from add_imp_sub_right Hn,
|
||||
have H2 : b - n = a, from (iff.mp !add_eq_iff_eq_add_neg Hn)⁻¹,
|
||||
have H3 : -b + n = -a, from
|
||||
calc
|
||||
-b + n = -b + -(-n) : {(neg_neg n)⁻¹}
|
||||
... = -(b + -n) : (neg_add_distr b (-n))⁻¹
|
||||
... = -(b - n) : {!add_neg_right}
|
||||
... = -(b + -n) : (neg_add_distrib b (-n))⁻¹
|
||||
... = -a : {H2},
|
||||
le_intro H3
|
||||
|
||||
|
|
@ -156,32 +154,30 @@ theorem le_neg_inv {a b : ℤ} (H : -a ≤ -b) : b ≤ a :=
|
|||
neg_neg b ▸ neg_neg a ▸ le_neg H
|
||||
|
||||
theorem le_sub_of_nat (a : ℤ) (n : ℕ) : a - n ≤ a :=
|
||||
le_intro (sub_add_inverse a n)
|
||||
le_intro (neg_add_cancel_right a n)
|
||||
|
||||
theorem sub_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a - c ≤ b - c :=
|
||||
!add_neg_right ▸ !add_neg_right ▸ add_le_right H _
|
||||
add_le_right H _
|
||||
|
||||
theorem sub_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c - b ≤ c - a :=
|
||||
!add_neg_right ▸ !add_neg_right ▸ add_le_left (le_neg H) _
|
||||
add_le_left (le_neg H) _
|
||||
|
||||
theorem sub_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : d ≤ c) : a - c ≤ b - d :=
|
||||
!add_neg_right ▸ !add_neg_right ▸ add_le H1 (le_neg H2)
|
||||
add_le H1 (le_neg H2)
|
||||
|
||||
theorem sub_le_right_inv {a b c : ℤ} (H : a - c ≤ b - c) : a ≤ b :=
|
||||
add_le_cancel_right (!add_neg_right⁻¹ ▸ !add_neg_right⁻¹ ▸ H)
|
||||
add_le_cancel_right H
|
||||
|
||||
theorem sub_le_left_inv {a b c : ℤ} (H : c - a ≤ c - b) : b ≤ a :=
|
||||
le_neg_inv (add_le_cancel_left (!add_neg_right⁻¹ ▸ !add_neg_right⁻¹ ▸ H))
|
||||
le_neg_inv (add_le_cancel_left H)
|
||||
|
||||
theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a :=
|
||||
iff.intro
|
||||
(assume H, !sub_self ▸ sub_le_right H a)
|
||||
(assume H,
|
||||
have H1 : a ≤ b - a + a, from add_zero_left a ▸ add_le_right H a,
|
||||
!sub_add_inverse ▸ H1)
|
||||
have H1 : a ≤ b - a + a, from add.left_id a ▸ add_le_right H a,
|
||||
!neg_add_cancel_right ▸ H1)
|
||||
|
||||
-- TODO: this no longer works:
|
||||
--!sub_add_inverse ▸ add_zero_left a ▸ add_le_right H a)
|
||||
|
||||
-- Less than, Greater than, Greater than or equal
|
||||
-- ----------------------------------------------
|
||||
|
|
@ -227,7 +223,7 @@ theorem lt_irrefl (a : ℤ) : ¬ a < a :=
|
|||
calc
|
||||
a + succ n = a : Hn
|
||||
... = a + 0 : by simp,
|
||||
have H3 : succ n = 0, from add_cancel_left H2,
|
||||
have H3 : succ n = 0, from add.left_cancel H2,
|
||||
have H4 : succ n = 0, from of_nat_inj H3,
|
||||
absurd H4 !succ_ne_zero)
|
||||
|
||||
|
|
@ -295,10 +291,10 @@ le_imp_not_gt (lt_imp_le H)
|
|||
|
||||
-- TODO: note: no longer works without the "show"
|
||||
theorem add_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b :=
|
||||
show (c + a) + 1 ≤ c + b, from (add_assoc c a 1)⁻¹ ▸ add_le_left H c
|
||||
show (c + a) + 1 ≤ c + b, from (add.assoc c a 1)⁻¹ ▸ add_le_left H c
|
||||
|
||||
theorem add_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a + c < b + c :=
|
||||
add_comm c b ▸ add_comm c a ▸ add_lt_left H c
|
||||
add.comm c b ▸ add.comm c a ▸ add_lt_left H c
|
||||
|
||||
theorem add_le_lt {a b c d : ℤ} (H1 : a ≤ c) (H2 : b < d) : a + b < c + d :=
|
||||
le_lt_trans (add_le_right H1 b) (add_lt_left H2 c)
|
||||
|
|
@ -310,10 +306,10 @@ theorem add_lt {a b c d : ℤ} (H1 : a < c) (H2 : b < d) : a + b < c + d :=
|
|||
add_lt_le H1 (lt_imp_le H2)
|
||||
|
||||
theorem add_lt_cancel_left {a b c : ℤ} (H : c + a < c + b) : a < b :=
|
||||
show a + 1 ≤ b, from add_le_cancel_left (add_assoc c a 1 ▸ H)
|
||||
show a + 1 ≤ b, from add_le_cancel_left (add.assoc c a 1 ▸ H)
|
||||
|
||||
theorem add_lt_cancel_right {a b c : ℤ} (H : a + c < b + c) : a < b :=
|
||||
add_lt_cancel_left (add_comm b c ▸ add_comm a c ▸ H)
|
||||
add_lt_cancel_left (add.comm b c ▸ add.comm a c ▸ H)
|
||||
|
||||
-- ### interaction with neg and sub
|
||||
|
||||
|
|
@ -333,22 +329,22 @@ theorem lt_neg_inv {a b : ℤ} (H : -a < -b) : b < a :=
|
|||
neg_neg b ▸ neg_neg a ▸ lt_neg H
|
||||
|
||||
theorem lt_sub_of_nat_succ (a : ℤ) (n : ℕ) : a - succ n < a :=
|
||||
lt_intro (sub_add_inverse a (succ n))
|
||||
lt_intro (neg_add_cancel_right a (succ n))
|
||||
|
||||
theorem sub_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a - c < b - c :=
|
||||
!add_neg_right ▸ !add_neg_right ▸ add_lt_right H _
|
||||
add_lt_right H _
|
||||
|
||||
theorem sub_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c - b < c - a :=
|
||||
!add_neg_right ▸ !add_neg_right ▸ add_lt_left (lt_neg H) _
|
||||
add_lt_left (lt_neg H) _
|
||||
|
||||
theorem sub_lt {a b c d : ℤ} (H1 : a < b) (H2 : d < c) : a - c < b - d :=
|
||||
!add_neg_right ▸ !add_neg_right ▸ add_lt H1 (lt_neg H2)
|
||||
add_lt H1 (lt_neg H2)
|
||||
|
||||
theorem sub_lt_right_inv {a b c : ℤ} (H : a - c < b - c) : a < b :=
|
||||
add_lt_cancel_right (!add_neg_right⁻¹ ▸ !add_neg_right⁻¹ ▸ H)
|
||||
add_lt_cancel_right H
|
||||
|
||||
theorem sub_lt_left_inv {a b c : ℤ} (H : c - a < c - b) : b < a :=
|
||||
lt_neg_inv (add_lt_cancel_left (!add_neg_right⁻¹ ▸ !add_neg_right⁻¹ ▸ H))
|
||||
lt_neg_inv (add_lt_cancel_left H)
|
||||
|
||||
-- ### totality of lt and le
|
||||
|
||||
|
|
@ -409,12 +405,12 @@ or_resolve_right (le_or_gt a b) H
|
|||
|
||||
theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n :=
|
||||
obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H,
|
||||
exists.intro n (Hn⁻¹ ⬝ add_zero_left n)
|
||||
exists.intro n (Hn⁻¹ ⬝ add.left_id n)
|
||||
|
||||
theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
|
||||
have H2 : -a ≥ 0, from zero_le_neg H,
|
||||
obtain (n : ℕ) (Hn : -a = n), from pos_imp_exists_nat H2,
|
||||
have H3 : a = -n, from (neg_move Hn)⁻¹,
|
||||
have H3 : a = -n, from (eq_neg_of_eq_neg (Hn⁻¹)),
|
||||
exists.intro n H3
|
||||
|
||||
theorem nat_abs_nonneg_eq {a : ℤ} (H : a ≥ 0) : (nat_abs a) = a :=
|
||||
|
|
@ -424,16 +420,6 @@ Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n)
|
|||
theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
|
||||
iff.mp (iff.symm !le_of_nat) !zero_le
|
||||
|
||||
definition le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
|
||||
have aux : Πx, decidable (0 ≤ x), from
|
||||
take x,
|
||||
have H : 0 ≤ x ↔ of_nat (nat_abs x) = x, from
|
||||
iff.intro
|
||||
(assume H1, nat_abs_nonneg_eq H1)
|
||||
(assume H1, H1 ▸ of_nat_nonneg (nat_abs x)),
|
||||
decidable_of_decidable_of_iff _ (iff.symm H),
|
||||
decidable_of_decidable_of_iff !aux (iff.symm (le_iff_sub_nonneg a b))
|
||||
|
||||
definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _
|
||||
definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _
|
||||
definition gt_decidable [instance] {a b : ℤ} : decidable (a > b) := _
|
||||
|
|
@ -445,12 +431,12 @@ calc
|
|||
(nat_abs a) = (nat_abs (-n)) : {Hn}
|
||||
... = (nat_abs n) : nat_abs_neg
|
||||
... = n : {nat_abs_of_nat n}
|
||||
... = -a : (neg_move (Hn⁻¹))⁻¹
|
||||
... = -a : (eq_neg_of_eq_neg Hn)⁻¹
|
||||
|
||||
theorem nat_abs_cases (a : ℤ) : a = (nat_abs a) ∨ a = - (nat_abs a) :=
|
||||
or_of_or_of_imp_of_imp (le_total 0 a)
|
||||
(assume H : a ≥ 0, (nat_abs_nonneg_eq H)⁻¹)
|
||||
(assume H : a ≤ 0, (neg_move ((nat_abs_negative H)⁻¹))⁻¹)
|
||||
(assume H : a ≤ 0, (eq_neg_of_eq_neg (nat_abs_negative H)))
|
||||
|
||||
-- ### interaction of mul with le and lt
|
||||
|
||||
|
|
@ -465,15 +451,15 @@ have H2 : a * b + of_nat ((nat_abs a) * n) = a * c, from
|
|||
le_intro H2
|
||||
|
||||
theorem mul_le_right_nonneg {a b c : ℤ} (Hb : b ≥ 0) (H : a ≤ c) : a * b ≤ c * b :=
|
||||
!mul_comm ▸ !mul_comm ▸ mul_le_left_nonneg Hb H
|
||||
!mul.comm ▸ !mul.comm ▸ mul_le_left_nonneg Hb H
|
||||
|
||||
theorem mul_le_left_nonpos {a b c : ℤ} (Ha : a ≤ 0) (H : b ≤ c) : a * c ≤ a * b :=
|
||||
have H2 : -a * b ≤ -a * c, from mul_le_left_nonneg (zero_le_neg Ha) H,
|
||||
have H3 : -(a * b) ≤ -(a * c), from !mul_neg_left ▸ !mul_neg_left ▸ H2,
|
||||
have H3 : -(a * b) ≤ -(a * c), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H2,
|
||||
le_neg_inv H3
|
||||
|
||||
theorem mul_le_right_nonpos {a b c : ℤ} (Hb : b ≤ 0) (H : c ≤ a) : a * b ≤ c * b :=
|
||||
!mul_comm ▸ !mul_comm ▸ mul_le_left_nonpos Hb H
|
||||
!mul.comm ▸ !mul.comm ▸ mul_le_left_nonpos Hb H
|
||||
|
||||
---this theorem can be made more general by replacing either Ha with 0 ≤ a or Hb with 0 ≤ d...
|
||||
theorem mul_le_nonneg {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b ≤ d)
|
||||
|
|
@ -485,20 +471,20 @@ theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb : b ≤ 0) (Hc : c ≤
|
|||
le_trans (mul_le_right_nonpos Hb Hc) (mul_le_left_nonpos (le_trans Hc Ha) Hd)
|
||||
|
||||
theorem mul_lt_left_pos {a b c : ℤ} (Ha : a > 0) (H : b < c) : a * b < a * c :=
|
||||
have H2 : a * b < a * b + a, from add_zero_right (a * b) ▸ add_lt_left Ha (a * b),
|
||||
have H2 : a * b < a * b + a, from add.right_id (a * b) ▸ add_lt_left Ha (a * b),
|
||||
have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (lt_imp_le Ha) H,
|
||||
lt_le_trans H2 H3
|
||||
|
||||
theorem mul_lt_right_pos {a b c : ℤ} (Hb : b > 0) (H : a < c) : a * b < c * b :=
|
||||
mul_comm b c ▸ mul_comm b a ▸ mul_lt_left_pos Hb H
|
||||
mul.comm b c ▸ mul.comm b a ▸ mul_lt_left_pos Hb H
|
||||
|
||||
theorem mul_lt_left_neg {a b c : ℤ} (Ha : a < 0) (H : b < c) : a * c < a * b :=
|
||||
have H2 : -a * b < -a * c, from mul_lt_left_pos (zero_lt_neg Ha) H,
|
||||
have H3 : -(a * b) < -(a * c), from mul_neg_left a c ▸ mul_neg_left a b ▸ H2,
|
||||
have H3 : -(a * b) < -(a * c), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H2,
|
||||
lt_neg_inv H3
|
||||
|
||||
theorem mul_lt_right_neg {a b c : ℤ} (Hb : b < 0) (H : c < a) : a * b < c * b :=
|
||||
!mul_comm ▸ !mul_comm ▸ mul_lt_left_neg Hb H
|
||||
!mul.comm ▸ !mul.comm ▸ mul_lt_left_neg Hb H
|
||||
|
||||
theorem mul_le_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b < d)
|
||||
: a * b < c * d :=
|
||||
|
|
@ -526,16 +512,16 @@ or.elim (le_or_gt b a)
|
|||
(assume H2 : a < b, H2)
|
||||
|
||||
theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b :=
|
||||
mul_lt_cancel_left_nonneg Hc (mul_comm b c ▸ mul_comm a c ▸ H)
|
||||
mul_lt_cancel_left_nonneg Hc (mul.comm b c ▸ mul.comm a c ▸ H)
|
||||
|
||||
theorem mul_lt_cancel_left_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : c * b < c * a) : a < b :=
|
||||
have H2 : -(c * a) < -(c * b), from lt_neg H,
|
||||
have H3 : -c * a < -c * b, from !mul_neg_left⁻¹ ▸ !mul_neg_left⁻¹ ▸ H2,
|
||||
have H3 : -c * a < -c * b, from !neg_mul_eq_neg_mul ▸ !neg_mul_eq_neg_mul ▸ H2,
|
||||
have H4 : -c ≥ 0, from zero_le_neg Hc,
|
||||
mul_lt_cancel_left_nonneg H4 H3
|
||||
|
||||
theorem mul_lt_cancel_right_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : b * c < a * c) : a < b :=
|
||||
mul_lt_cancel_left_nonpos Hc (!mul_comm ▸ !mul_comm ▸ H)
|
||||
mul_lt_cancel_left_nonpos Hc (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_le_cancel_left_pos {a b c : ℤ} (Hc : c > 0) (H : c * a ≤ c * b) : a ≤ b :=
|
||||
or.elim (le_or_gt a b)
|
||||
|
|
@ -545,17 +531,17 @@ or.elim (le_or_gt a b)
|
|||
absurd H3 (le_imp_not_gt H))
|
||||
|
||||
theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b :=
|
||||
mul_le_cancel_left_pos Hc (!mul_comm ▸ !mul_comm ▸ H)
|
||||
mul_le_cancel_left_pos Hc (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_le_cancel_left_neg {a b c : ℤ} (Hc : c < 0) (H : c * b ≤ c * a) : a ≤ b :=
|
||||
have H2 : -(c * a) ≤ -(c * b), from le_neg H,
|
||||
have H3 : -c * a ≤ -c * b,
|
||||
from (mul_neg_left c b)⁻¹ ▸ (mul_neg_left c a)⁻¹ ▸ H2,
|
||||
from neg_mul_eq_neg_mul c b ▸ neg_mul_eq_neg_mul c a ▸ H2,
|
||||
have H4 : -c > 0, from zero_lt_neg Hc,
|
||||
mul_le_cancel_left_pos H4 H3
|
||||
|
||||
theorem mul_le_cancel_right_neg {a b c : ℤ} (Hc : c < 0) (H : b * c ≤ a * c) : a ≤ b :=
|
||||
mul_le_cancel_left_neg Hc (!mul_comm ▸ !mul_comm ▸ H)
|
||||
mul_le_cancel_left_neg Hc (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_eq_one_left {a b : ℤ} (H : a * b = 1) : a = 1 ∨ a = - 1 :=
|
||||
have H2 : (nat_abs a) * (nat_abs b) = 1, from
|
||||
|
|
@ -569,7 +555,7 @@ or_of_or_of_imp_of_imp (nat_abs_cases a)
|
|||
(assume H4 : a = - (nat_abs a), H3 ▸ H4)
|
||||
|
||||
theorem mul_eq_one_right {a b : ℤ} (H : a * b = 1) : b = 1 ∨ b = - 1 :=
|
||||
mul_eq_one_left (!mul_comm ▸ H)
|
||||
mul_eq_one_left (!mul.comm ▸ H)
|
||||
|
||||
|
||||
-- sign function
|
||||
|
|
|
|||
|
|
@ -258,6 +258,9 @@ iff.intro
|
|||
theorem succ_pos (n : ℕ) : 0 < succ n :=
|
||||
!zero_lt_succ
|
||||
|
||||
theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
|
||||
(or_resolve_right (zero_or_succ_pred n) (ne.symm (lt_imp_ne H))⁻¹)
|
||||
|
||||
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
|
||||
discriminate
|
||||
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
|
||||
|
|
|
|||
|
|
@ -306,6 +306,11 @@ sub_split
|
|||
... = k - n + n : (add_sub_ge_left H3)⁻¹,
|
||||
le_intro (add.cancel_right H4))
|
||||
|
||||
theorem sub_pos_of_gt {m n : ℕ} (H : n > m) : n - m > 0 :=
|
||||
have H1 : n = n - m + m, from (add_sub_ge_left (lt_imp_le H))⁻¹,
|
||||
have H2 : 0 + m < n - m + m, from (add.zero_left m)⁻¹ ▸ H1 ▸ H,
|
||||
!add_lt_cancel_right H2
|
||||
|
||||
-- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
|
||||
-- :=
|
||||
-- _
|
||||
|
|
|
|||
Loading…
Reference in a new issue