refactor(library): use type classes for encoding all arithmetic operations
Before this commit we were using overloading for concrete structures and type classes for abstract ones. This is the first of series of commits that implement this modification
This commit is contained in:
Leonardo de Moura
parent
06e35b4863
commit
a618bd7d6c
30 changed files with 447 additions and 479 deletions
|
|
@ -68,10 +68,10 @@ lemma le_inf {a b c : A} : c ≤ a → c ≤ b → c ≤ a ⊓ b :=
|
|||
assume h₁ h₂,
|
||||
le_Inf (take x, suppose x ∈ '{a, b},
|
||||
or.elim (eq_or_mem_of_mem_insert this)
|
||||
(suppose x = a, by subst x; assumption)
|
||||
(suppose x = a, begin subst x, exact h₁ end)
|
||||
(suppose x ∈ '{b},
|
||||
assert x = b, from !eq_of_mem_singleton this,
|
||||
by subst x; assumption))
|
||||
begin subst x, exact h₂ end))
|
||||
|
||||
lemma le_sup_left (a b : A) : a ≤ a ⊔ b :=
|
||||
le_Sup !mem_insert
|
||||
|
|
|
|||
|
|
@ -24,11 +24,13 @@ section division_ring
|
|||
variables [s : division_ring A] {a b c : A}
|
||||
include s
|
||||
|
||||
definition divide (a b : A) : A := a * b⁻¹
|
||||
infix [priority algebra.prio] / := divide
|
||||
protected definition division (a b : A) : A := a * b⁻¹
|
||||
|
||||
-- only in this file
|
||||
local attribute divide [reducible]
|
||||
definition division_ring_has_division [reducible] [instance] : has_division A :=
|
||||
has_division.mk algebra.division
|
||||
|
||||
lemma division.def (a b : A) : a / b = a * b⁻¹ :=
|
||||
rfl
|
||||
|
||||
theorem mul_inv_cancel (H : a ≠ 0) : a * a⁻¹ = 1 :=
|
||||
division_ring.mul_inv_cancel H
|
||||
|
|
@ -39,7 +41,7 @@ section division_ring
|
|||
theorem inv_eq_one_div (a : A) : a⁻¹ = 1 / a := !one_mul⁻¹
|
||||
|
||||
theorem div_eq_mul_one_div (a b : A) : a / b = a * (1 / b) :=
|
||||
by rewrite [↑divide, one_mul]
|
||||
by rewrite [*division.def, one_mul]
|
||||
|
||||
theorem mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 :=
|
||||
by rewrite [-inv_eq_one_div, (mul_inv_cancel H)]
|
||||
|
|
@ -62,7 +64,7 @@ section division_ring
|
|||
by rewrite [-mul_one, inv_mul_cancel (ne.symm (@zero_ne_one A _))]
|
||||
|
||||
theorem div_one (a : A) : a / 1 = a :=
|
||||
by rewrite [↑divide, one_inv_eq, mul_one]
|
||||
by rewrite [*division.def, one_inv_eq, mul_one]
|
||||
|
||||
theorem zero_div (a : A) : 0 / a = 0 := !zero_mul
|
||||
|
||||
|
|
@ -129,7 +131,7 @@ section division_ring
|
|||
|
||||
theorem div_neg_eq_neg_div (b : A) (Ha : a ≠ 0) : b / (- a) = - (b / a) :=
|
||||
calc
|
||||
b / (- a) = b * (1 / (- a)) : inv_eq_one_div
|
||||
b / (- a) = b * (1 / (- a)) : by rewrite -inv_eq_one_div
|
||||
... = b * -(1 / a) : division_ring.one_div_neg_eq_neg_one_div Ha
|
||||
... = -(b * (1 / a)) : neg_mul_eq_mul_neg
|
||||
... = - (b * a⁻¹) : inv_eq_one_div
|
||||
|
|
@ -155,10 +157,10 @@ section division_ring
|
|||
... = (b * a)⁻¹ : inv_eq_one_div)
|
||||
|
||||
theorem mul_div_cancel (a : A) {b : A} (Hb : b ≠ 0) : a * b / b = a :=
|
||||
by rewrite [↑divide, mul.assoc, (mul_inv_cancel Hb), mul_one]
|
||||
by rewrite [*division.def, mul.assoc, (mul_inv_cancel Hb), mul_one]
|
||||
|
||||
theorem div_mul_cancel (a : A) {b : A} (Hb : b ≠ 0) : a / b * b = a :=
|
||||
by rewrite [↑divide, mul.assoc, (inv_mul_cancel Hb), mul_one]
|
||||
by rewrite [*division.def, mul.assoc, (inv_mul_cancel Hb), mul_one]
|
||||
|
||||
theorem div_add_div_same (a b c : A) : a / c + b / c = (a + b) / c := !right_distrib⁻¹
|
||||
|
||||
|
|
@ -173,7 +175,7 @@ section division_ring
|
|||
theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) :
|
||||
(1 / a) * (b - a) * (1 / b) = 1 / a - 1 / b :=
|
||||
by rewrite [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel Ha), mul_sub_right_distrib,
|
||||
one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one, one_mul]
|
||||
one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one]
|
||||
|
||||
theorem div_eq_one_iff_eq (a : A) {b : A} (Hb : b ≠ 0) : a / b = 1 ↔ a = b :=
|
||||
iff.intro
|
||||
|
|
@ -218,7 +220,6 @@ structure field [class] (A : Type) extends division_ring A, comm_ring A
|
|||
section field
|
||||
variables [s : field A] {a b c d: A}
|
||||
include s
|
||||
local attribute divide [reducible]
|
||||
|
||||
theorem field.one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (a * b) :=
|
||||
by rewrite [(division_ring.one_div_mul_one_div Ha Hb), mul.comm b]
|
||||
|
|
@ -246,12 +247,12 @@ section field
|
|||
|
||||
theorem one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
|
||||
assert a * b ≠ 0, from (division_ring.mul_ne_zero Ha Hb),
|
||||
by rewrite [add.comm, -(field.div_mul_left Ha this), -(field.div_mul_right Hb this), ↑divide,
|
||||
by rewrite [add.comm, -(field.div_mul_left Ha this), -(field.div_mul_right Hb this), *division.def,
|
||||
-right_distrib]
|
||||
|
||||
theorem field.div_mul_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0) (Hd : d ≠ 0) :
|
||||
(a / b) * (c / d) = (a * c) / (b * d) :=
|
||||
by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)]
|
||||
by rewrite [*division.def, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)]
|
||||
|
||||
theorem mul_div_mul_left (a : A) {b c : A} (Hb : b ≠ 0) (Hc : c ≠ 0) :
|
||||
(c * a) / (c * b) = a / b :=
|
||||
|
|
@ -262,7 +263,7 @@ section field
|
|||
by rewrite [(mul.comm a), (mul.comm b), (!mul_div_mul_left Hb Hc)]
|
||||
|
||||
theorem div_mul_eq_mul_div (a b c : A) : (b / c) * a = (b * a) / c :=
|
||||
by rewrite [↑divide, mul.assoc, (mul.comm c⁻¹), -mul.assoc]
|
||||
by rewrite [*division.def, mul.assoc, (mul.comm c⁻¹), -mul.assoc]
|
||||
|
||||
theorem field.div_mul_eq_mul_div_comm (a b : A) {c : A} (Hc : c ≠ 0) :
|
||||
(b / c) * a = b * (a / c) :=
|
||||
|
|
@ -275,7 +276,7 @@ section field
|
|||
|
||||
theorem div_sub_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0) (Hd : d ≠ 0) :
|
||||
(a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) :=
|
||||
by rewrite [↑sub, neg_eq_neg_one_mul, -mul_div_assoc, (!div_add_div Hb Hd),
|
||||
by rewrite [*sub_eq_add_neg, neg_eq_neg_one_mul, -mul_div_assoc, (!div_add_div Hb Hd),
|
||||
-mul.assoc, (mul.comm b), mul.assoc, -neg_eq_neg_one_mul]
|
||||
|
||||
theorem mul_eq_mul_of_div_eq_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0)
|
||||
|
|
@ -339,7 +340,7 @@ section discrete_field
|
|||
theorem one_div_zero : 1 / 0 = (0:A) :=
|
||||
calc
|
||||
1 / 0 = 1 * 0⁻¹ : refl
|
||||
... = 1 * 0 : discrete_field.inv_zero A
|
||||
... = 1 * 0 : inv_zero
|
||||
... = 0 : mul_zero
|
||||
|
||||
theorem div_zero (a : A) : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
|
||||
|
|
|
|||
|
|
@ -16,30 +16,12 @@ namespace algebra
|
|||
|
||||
variable {A : Type}
|
||||
|
||||
/- overloaded symbols -/
|
||||
|
||||
structure has_mul [class] (A : Type) :=
|
||||
(mul : A → A → A)
|
||||
|
||||
structure has_add [class] (A : Type) :=
|
||||
(add : A → A → A)
|
||||
|
||||
structure has_one [class] (A : Type) :=
|
||||
(one : A)
|
||||
|
||||
structure has_zero [class] (A : Type) :=
|
||||
(zero : A)
|
||||
|
||||
structure has_inv [class] (A : Type) :=
|
||||
(inv : A → A)
|
||||
|
||||
structure has_neg [class] (A : Type) :=
|
||||
(neg : A → A)
|
||||
|
||||
infixl [priority algebra.prio] ` * ` := has_mul.mul
|
||||
infixl [priority algebra.prio] ` + ` := has_add.add
|
||||
postfix [priority algebra.prio] `⁻¹` := has_inv.inv
|
||||
prefix [priority algebra.prio] `-` := has_neg.neg
|
||||
notation 1 := !has_one.one
|
||||
notation 0 := !has_zero.zero
|
||||
|
||||
|
|
@ -478,7 +460,8 @@ section add_group
|
|||
-- TODO: derive corresponding facts for div in a field
|
||||
definition sub [reducible] (a b : A) : A := a + -b
|
||||
|
||||
infix [priority algebra.prio] - := sub
|
||||
definition add_group_has_sub [reducible] [instance] : has_sub A :=
|
||||
has_sub.mk algebra.sub
|
||||
|
||||
theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
|
||||
|
||||
|
|
@ -499,7 +482,8 @@ section add_group
|
|||
|
||||
theorem zero_sub (a : A) : 0 - a = -a := !zero_add
|
||||
|
||||
theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
|
||||
theorem sub_zero (a : A) : a - 0 = a :=
|
||||
by rewrite [sub_eq_add_neg, neg_zero, add_zero]
|
||||
|
||||
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b :=
|
||||
by change a + -(-b) = a + b; rewrite neg_neg
|
||||
|
|
@ -515,7 +499,7 @@ section add_group
|
|||
|
||||
theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b :=
|
||||
calc
|
||||
a - (b + c) = a + (-c - b) : neg_add_rev
|
||||
a - (b + c) = a + (-c - b) : by rewrite [sub_eq_add_neg, neg_add_rev]
|
||||
... = a - c - b : by krewrite -add.assoc
|
||||
|
||||
theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
|
||||
|
|
|
|||
|
|
@ -107,23 +107,24 @@ theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
|
|||
|
||||
end nat
|
||||
|
||||
open int
|
||||
open nat int
|
||||
|
||||
definition gpow (a : A) : ℤ → A
|
||||
| (of_nat n) := a^n
|
||||
| -[1+n] := (a^(nat.succ n))⁻¹
|
||||
|
||||
/-
|
||||
private lemma gpow_add_aux (a : A) (m n : nat) :
|
||||
gpow a ((of_nat m) + -[1+n]) = gpow a (of_nat m) * gpow a (-[1+n]) :=
|
||||
or.elim (nat.lt_or_ge m (nat.succ n))
|
||||
(assume H : (#nat m < nat.succ n),
|
||||
assert H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
|
||||
(assume H : (m < nat.succ n),
|
||||
assert H1 : (nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
|
||||
calc
|
||||
gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n)) : rfl
|
||||
... = gpow a (-[1+ nat.pred (nat.sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H}
|
||||
... = (pow a (nat.succ (nat.pred (nat.sub (nat.succ n) m))))⁻¹ : rfl
|
||||
... = gpow a (-[1+ nat.pred (sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H}
|
||||
... = (pow a (nat.succ (nat.pred (sub (nat.succ n) m))))⁻¹ : rfl
|
||||
... = (pow a (nat.succ n) * (pow a m)⁻¹)⁻¹ :
|
||||
by rewrite [nat.succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)]
|
||||
by rewrite [succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)]
|
||||
... = pow a m * (pow a (nat.succ n))⁻¹ :
|
||||
by rewrite [mul_inv, inv_inv]
|
||||
... = gpow a (of_nat m) * gpow a (-[1+n]) : rfl)
|
||||
|
|
@ -146,8 +147,9 @@ theorem gpow_add (a : A) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j
|
|||
|
||||
theorem gpow_comm (a : A) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i :=
|
||||
by rewrite [-*gpow_add, int.add.comm]
|
||||
-/
|
||||
end group
|
||||
|
||||
/-
|
||||
section ordered_ring
|
||||
open nat
|
||||
variable [s : linear_ordered_ring A]
|
||||
|
|
@ -248,5 +250,6 @@ theorem add_imul (i j : ℤ) (a : A) : imul (i + j) a = imul i a + imul j a :=
|
|||
theorem imul_comm (i j : ℤ) (a : A) : imul i a + imul j a = imul j a + imul i a := gpow_comm a i j
|
||||
|
||||
end add_group
|
||||
-/
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -12,25 +12,6 @@ namespace algebra
|
|||
|
||||
variable {A : Type}
|
||||
|
||||
/- overloaded symbols -/
|
||||
|
||||
structure has_le [class] (A : Type) :=
|
||||
(le : A → A → Prop)
|
||||
|
||||
structure has_lt [class] (A : Type) :=
|
||||
(lt : A → A → Prop)
|
||||
|
||||
infixl [priority algebra.prio] <= := has_le.le
|
||||
infixl [priority algebra.prio] ≤ := has_le.le
|
||||
infixl [priority algebra.prio] < := has_lt.lt
|
||||
|
||||
definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a
|
||||
notation [priority algebra.prio] a ≥ b := has_le.ge a b
|
||||
notation [priority algebra.prio] a >= b := has_le.ge a b
|
||||
|
||||
definition has_lt.gt [reducible] {A : Type} [s : has_lt A] (a b : A) := b < a
|
||||
notation [priority algebra.prio] a > b := has_lt.gt a b
|
||||
|
||||
/- weak orders -/
|
||||
|
||||
structure weak_order [class] (A : Type) extends has_le A :=
|
||||
|
|
@ -443,18 +424,3 @@ section
|
|||
end
|
||||
|
||||
end algebra
|
||||
|
||||
/-
|
||||
For reference, these are all the transitivity rules defined in this file:
|
||||
calc_trans le.trans
|
||||
calc_trans lt.trans
|
||||
|
||||
calc_trans lt_of_lt_of_le
|
||||
calc_trans lt_of_le_of_lt
|
||||
|
||||
calc_trans ge.trans
|
||||
calc_trans gt.trans
|
||||
|
||||
calc_trans gt_of_gt_of_ge
|
||||
calc_trans gt_of_ge_of_gt
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -169,14 +169,14 @@ section linear_ordered_field
|
|||
assert H1 : (a * d - c * b) / (c * d) < 0, by rewrite [mul.comm c b]; exact H,
|
||||
assert H2 : a / c - b / d < 0, by rewrite [!div_sub_div Hc Hd]; exact H1,
|
||||
assert H3 : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _,
|
||||
begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end
|
||||
begin rewrite [zero_add at H3, sub_eq_add_neg at H3, neg_add_cancel_right at H3], exact H3 end
|
||||
|
||||
theorem div_le_div_of_mul_sub_mul_div_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0)
|
||||
(H : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d :=
|
||||
assert H1 : (a * d - c * b) / (c * d) ≤ 0, by rewrite [mul.comm c b]; exact H,
|
||||
assert H2 : a / c - b / d ≤ 0, by rewrite [!div_sub_div Hc Hd]; exact H1,
|
||||
assert H3 : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _,
|
||||
begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end
|
||||
begin rewrite [zero_add at H3, sub_eq_add_neg at H3, neg_add_cancel_right at H3], exact H3 end
|
||||
|
||||
theorem div_pos_of_pos_of_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a / b :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -137,7 +137,7 @@ section
|
|||
have Hb' : b ≤ 0, from
|
||||
calc
|
||||
b = 0 + b : by rewrite zero_add
|
||||
... ≤ a + b : add_le_add_right Ha
|
||||
... ≤ a + b : by exact add_le_add_right Ha _
|
||||
... = 0 : Hab,
|
||||
have Hbz : b = 0, from le.antisymm Hb' Hb,
|
||||
and.intro Haz Hbz)
|
||||
|
|
@ -368,7 +368,7 @@ section
|
|||
|
||||
theorem le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b :=
|
||||
assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
|
||||
by rewrite add_neg_cancel_right at H; exact H
|
||||
by rewrite [sub_eq_add_neg (b+c) c at H, add_neg_cancel_right at H]; exact H
|
||||
|
||||
theorem le_add_of_sub_right_le {a b c : A} : a - c ≤ b → a ≤ b + c :=
|
||||
iff.mpr !le_add_iff_sub_right_le
|
||||
|
|
@ -448,7 +448,7 @@ section
|
|||
|
||||
theorem add_lt_iff_lt_sub_right : a + b < c ↔ a < c - b :=
|
||||
assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
|
||||
by rewrite add_neg_cancel_right at H; exact H
|
||||
by rewrite [sub_eq_add_neg at H, add_neg_cancel_right at H]; exact H
|
||||
|
||||
theorem add_lt_of_lt_sub_right {a b c : A} : a < c - b → a + b < c :=
|
||||
iff.mpr !add_lt_iff_lt_sub_right
|
||||
|
|
@ -793,8 +793,7 @@ section
|
|||
|
||||
theorem abs_sub_le (a b c : A) : abs (a - c) ≤ abs (a - b) + abs (b - c) :=
|
||||
calc
|
||||
abs (a - c) = abs (a - b + (b - c)) :
|
||||
by rewrite [sub_eq_add_neg, add.assoc, neg_add_cancel_left]
|
||||
abs (a - c) = abs (a - b + (b - c)) : by rewrite [*sub_eq_add_neg, add.assoc, neg_add_cancel_left]
|
||||
... ≤ abs (a - b) + abs (b - c) : abs_add_le_abs_add_abs
|
||||
|
||||
theorem abs_add_three (a b c : A) : abs (a + b + c) ≤ abs a + abs b + abs c :=
|
||||
|
|
|
|||
|
|
@ -686,9 +686,13 @@ section
|
|||
sub_lt_of_abs_sub_lt_left (!abs_sub ▸ H)
|
||||
|
||||
theorem abs_sub_square (a b : A) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
|
||||
by rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
|
||||
sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul,
|
||||
*add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
|
||||
begin
|
||||
rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib,
|
||||
sub_eq_add_neg (a*b), sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul,
|
||||
*add.assoc, {_ + b * b}add.comm, *sub_eq_add_neg],
|
||||
rewrite [{a*a + b*b}add.comm],
|
||||
rewrite [mul.comm b a, *add.assoc]
|
||||
end
|
||||
|
||||
theorem abs_abs_sub_abs_le_abs_sub (a b : A) : abs (abs a - abs b) ≤ abs (a - b) :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -72,8 +72,10 @@ section comm_semiring
|
|||
variables [s : comm_semiring A] (a b c : A)
|
||||
include s
|
||||
|
||||
definition dvd (a b : A) : Prop := ∃c, b = a * c
|
||||
notation [priority algebra.prio] a ∣ b := dvd a b
|
||||
protected definition dvd (a b : A) : Prop := ∃c, b = a * c
|
||||
|
||||
definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A :=
|
||||
has_dvd.mk algebra.dvd
|
||||
|
||||
theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b :=
|
||||
exists.intro _ H⁻¹
|
||||
|
|
|
|||
|
|
@ -116,7 +116,7 @@ begin
|
|||
induction i with [i, ih],
|
||||
{exfalso, exact !nat.lt.irrefl ipos},
|
||||
have xige1 : x^i ≥ 1, from pow_ge_one _ (le_of_lt xgt1),
|
||||
rewrite [pow_succ, -mul_one 1, ↑has_lt.gt],
|
||||
rewrite [pow_succ, -mul_one 1],
|
||||
apply mul_lt_mul xgt1 xige1 zero_lt_one,
|
||||
apply le_of_lt xpos
|
||||
end
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@ import algebra.relation algebra.binary algebra.ordered_ring
|
|||
open eq.ops
|
||||
open prod relation nat
|
||||
open decidable binary
|
||||
open - [notations] algebra
|
||||
|
||||
/- the type of integers -/
|
||||
|
||||
|
|
@ -54,21 +55,21 @@ definition neg_of_nat : ℕ → ℤ
|
|||
| (succ m) := -[1+ m]
|
||||
|
||||
definition sub_nat_nat (m n : ℕ) : ℤ :=
|
||||
match n - m with
|
||||
| 0 := m - n -- m ≥ n
|
||||
| (succ k) := -[1+ k] -- m < n, and n - m = succ k
|
||||
match (n - m : nat) with
|
||||
| 0 := (m - n : nat) -- m ≥ n
|
||||
| (succ k) := -[1+ k] -- m < n, and n - m = succ k
|
||||
end
|
||||
|
||||
definition neg (a : ℤ) : ℤ :=
|
||||
protected definition neg (a : ℤ) : ℤ :=
|
||||
int.cases_on a neg_of_nat succ
|
||||
|
||||
definition add : ℤ → ℤ → ℤ
|
||||
protected definition add : ℤ → ℤ → ℤ
|
||||
| (of_nat m) (of_nat n) := 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] := neg_of_nat (succ m + succ n)
|
||||
|
||||
definition mul : ℤ → ℤ → ℤ
|
||||
protected definition mul : ℤ → ℤ → ℤ
|
||||
| (of_nat m) (of_nat n) := m * n
|
||||
| (of_nat m) -[1+ n] := neg_of_nat (m * succ n)
|
||||
| -[1+ m] (of_nat n) := neg_of_nat (succ m * n)
|
||||
|
|
@ -76,11 +77,11 @@ definition mul : ℤ → ℤ → ℤ
|
|||
|
||||
/- notation -/
|
||||
|
||||
protected definition prio : num := num.pred std.priority.default
|
||||
protected definition prio : num := num.pred nat.prio
|
||||
|
||||
prefix [priority int.prio] - := int.neg
|
||||
infix [priority int.prio] + := int.add
|
||||
infix [priority int.prio] * := int.mul
|
||||
definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add
|
||||
definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
|
||||
definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
|
||||
|
||||
/- some basic functions and properties -/
|
||||
|
||||
|
|
@ -115,14 +116,14 @@ theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl
|
|||
theorem of_nat_mul (n m : ℕ) : of_nat (n * m) = of_nat n * of_nat m := rfl
|
||||
|
||||
theorem sub_nat_nat_of_ge {m n : ℕ} (H : m ≥ n) : sub_nat_nat m n = of_nat (m - n) :=
|
||||
show sub_nat_nat m n = nat.cases_on 0 (m - n) _, from (sub_eq_zero_of_le H) ▸ rfl
|
||||
show sub_nat_nat m n = nat.cases_on 0 (m - n : nat) _, from (sub_eq_zero_of_le H) ▸ rfl
|
||||
|
||||
section
|
||||
local attribute sub_nat_nat [reducible]
|
||||
theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) :
|
||||
sub_nat_nat m n = -[1+ pred (n - m)] :=
|
||||
have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹,
|
||||
show sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (m - n) _, from H1 ▸ rfl
|
||||
have H1 : n - m = succ (pred (n - m)), from eq.symm (succ_pred_of_pos (sub_pos_of_lt H)),
|
||||
show sub_nat_nat m n = nat.cases_on (succ (nat.pred (n - m))) (m - n : nat) _, from H1 ▸ rfl
|
||||
end
|
||||
|
||||
definition nat_abs (a : ℤ) : ℕ := int.cases_on a function.id succ
|
||||
|
|
@ -143,31 +144,31 @@ protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm
|
|||
|
||||
protected theorem equiv.symm [symm] {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
|
||||
calc
|
||||
pr1 q + pr2 p = pr2 p + pr1 q : add.comm
|
||||
pr1 q + pr2 p = pr2 p + pr1 q : by rewrite add.comm
|
||||
... = pr1 p + pr2 q : H⁻¹
|
||||
... = pr2 q + pr1 p : add.comm
|
||||
... = pr2 q + pr1 p : by rewrite add.comm
|
||||
|
||||
protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
|
||||
add.cancel_right (calc
|
||||
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : add.right_comm
|
||||
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite add.right_comm
|
||||
... = pr2 p + pr1 q + pr2 r : {H1}
|
||||
... = pr2 p + (pr1 q + pr2 r) : add.assoc
|
||||
... = pr2 p + (pr1 q + pr2 r) : by rewrite add.assoc
|
||||
... = pr2 p + (pr2 q + pr1 r) : {H2}
|
||||
... = pr2 p + pr2 q + pr1 r : add.assoc
|
||||
... = pr2 p + pr1 r + pr2 q : add.right_comm)
|
||||
... = pr2 p + pr2 q + pr1 r : by rewrite add.assoc
|
||||
... = pr2 p + pr1 r + pr2 q : by rewrite add.right_comm)
|
||||
|
||||
protected theorem equiv_equiv : is_equivalence int.equiv :=
|
||||
is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
|
||||
|
||||
protected theorem equiv_cases {p q : ℕ × ℕ} (H : p ≡ q) :
|
||||
(pr1 p ≥ pr2 p ∧ pr1 q ≥ pr2 q) ∨ (pr1 p < pr2 p ∧ pr1 q < pr2 q) :=
|
||||
or.elim (@le_or_gt (pr2 p) (pr1 p))
|
||||
or.elim (@le_or_gt _ _ (pr2 p) (pr1 p))
|
||||
(suppose pr1 p ≥ pr2 p,
|
||||
have pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_add_right this (pr2 q),
|
||||
or.inl (and.intro `pr1 p ≥ pr2 p` (le_of_add_le_add_left this)))
|
||||
(suppose pr1 p < pr2 p,
|
||||
have pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right this (pr2 q),
|
||||
or.inr (and.intro `pr1 p < pr2 p` (lt_of_add_lt_add_left this)))
|
||||
(suppose H₁ : pr1 p < pr2 p,
|
||||
have pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right H₁ (pr2 q),
|
||||
or.inr (and.intro H₁ (lt_of_add_lt_add_left this)))
|
||||
|
||||
protected theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl
|
||||
|
||||
|
|
@ -208,20 +209,20 @@ or.elim (int.equiv_cases Hequiv)
|
|||
(and.rec (assume (Hp : pr1 p ≥ pr2 p) (Hq : pr1 q ≥ pr2 q),
|
||||
have H : pr1 p - pr2 p = pr1 q - pr2 q, from
|
||||
calc pr1 p - pr2 p
|
||||
= pr1 p + pr2 q - pr2 q - pr2 p : add_sub_cancel
|
||||
= pr1 p + pr2 q - pr2 q - pr2 p : by rewrite add_sub_cancel
|
||||
... = pr2 p + pr1 q - pr2 q - pr2 p : Hequiv
|
||||
... = pr2 p + (pr1 q - pr2 q) - pr2 p : add_sub_assoc Hq
|
||||
... = pr1 q - pr2 q + pr2 p - pr2 p : add.comm
|
||||
... = pr1 q - pr2 q : add_sub_cancel,
|
||||
... = pr1 q - pr2 q + pr2 p - pr2 p : by rewrite add.comm
|
||||
... = pr1 q - pr2 q : by rewrite add_sub_cancel,
|
||||
abstr_of_ge Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_ge Hq)⁻¹))
|
||||
(and.rec (assume (Hp : pr1 p < pr2 p) (Hq : pr1 q < pr2 q),
|
||||
have H : pr2 p - pr1 p = pr2 q - pr1 q, from
|
||||
calc pr2 p - pr1 p
|
||||
= pr2 p + pr1 q - pr1 q - pr1 p : add_sub_cancel
|
||||
= pr2 p + pr1 q - pr1 q - pr1 p : by rewrite add_sub_cancel
|
||||
... = pr1 p + pr2 q - pr1 q - pr1 p : Hequiv
|
||||
... = pr1 p + (pr2 q - pr1 q) - pr1 p : add_sub_assoc (le_of_lt Hq)
|
||||
... = pr2 q - pr1 q + pr1 p - pr1 p : add.comm
|
||||
... = pr2 q - pr1 q : add_sub_cancel,
|
||||
... = pr2 q - pr1 q + pr1 p - pr1 p : by rewrite add.comm
|
||||
... = pr2 q - pr1 q : by rewrite add_sub_cancel,
|
||||
abstr_of_lt Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_lt Hq)⁻¹))
|
||||
|
||||
theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ (abstr p = abstr q) :=
|
||||
|
|
@ -280,8 +281,8 @@ definition padd (p q : ℕ × ℕ) : ℕ × ℕ := (pr1 p + pr1 q, pr2 p + pr2 q
|
|||
|
||||
theorem repr_add : Π (a b : ℤ), repr (add a b) ≡ padd (repr a) (repr b)
|
||||
| (of_nat m) (of_nat n) := !equiv.refl
|
||||
| (of_nat m) -[1+ n] := (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat
|
||||
| -[1+ m] (of_nat n) := (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat
|
||||
| (of_nat m) -[1+ n] := sorry -- begin end -- (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat
|
||||
| -[1+ m] (of_nat n) := sorry -- begin end -- (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat
|
||||
| -[1+ m] -[1+ n] := !repr_sub_nat_nat
|
||||
|
||||
theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' :=
|
||||
|
|
@ -293,13 +294,13 @@ calc pr1 p + pr1 q + (pr2 p' + pr2 q')
|
|||
|
||||
theorem padd_comm (p q : ℕ × ℕ) : padd p q = padd q p :=
|
||||
calc (pr1 p + pr1 q, pr2 p + pr2 q)
|
||||
= (pr1 q + pr1 p, pr2 p + pr2 q) : add.comm
|
||||
... = (pr1 q + pr1 p, pr2 q + pr2 p) : add.comm
|
||||
= (pr1 q + pr1 p, pr2 p + pr2 q) : by rewrite add.comm
|
||||
... = (pr1 q + pr1 p, pr2 q + pr2 p) : by rewrite (add.comm (pr2 p) (pr2 q))
|
||||
|
||||
theorem padd_assoc (p q r : ℕ × ℕ) : padd (padd p q) r = padd p (padd q r) :=
|
||||
calc (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r)
|
||||
= (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : add.assoc
|
||||
... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : add.assoc
|
||||
= (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : by rewrite add.assoc
|
||||
... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : by rewrite add.assoc
|
||||
|
||||
theorem add.comm (a b : ℤ) : a + b = b + a :=
|
||||
eq_of_repr_equiv_repr (equiv.trans !repr_add
|
||||
|
|
@ -349,7 +350,7 @@ calc pr1 p + pr1 q + pr2 q + pr2 p
|
|||
= pr1 p + (pr1 q + pr2 q) + pr2 p : nat.add.assoc
|
||||
... = pr1 p + (pr1 q + pr2 q + pr2 p) : nat.add.assoc
|
||||
... = pr1 p + (pr2 q + pr1 q + pr2 p) : nat.add.comm
|
||||
... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm
|
||||
... = pr1 p + (pr2 q + pr2 p + pr1 q) : by rewrite add.right_comm
|
||||
... = pr1 p + (pr2 p + pr2 q + pr1 q) : nat.add.comm
|
||||
... = pr2 p + pr2 q + pr1 q + pr1 p : nat.add.comm
|
||||
|
||||
|
|
@ -404,16 +405,16 @@ nat.cases_on m rfl (take m', rfl)
|
|||
-- note: we have =, not just ≡
|
||||
theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b)
|
||||
| (of_nat m) (of_nat n) := calc
|
||||
(m * n + 0 * 0, m * 0 + 0) = (m * n + 0 * 0, m * 0 + 0 * n) : zero_mul
|
||||
(m * n + 0 * 0, m * 0 + 0) = (m * n + 0 * 0, m * 0 + 0 * n) : by rewrite *zero_mul
|
||||
| (of_nat m) -[1+ n] := calc
|
||||
repr (m * -[1+ n]) = (m * 0 + 0, m * succ n + 0 * 0) : repr_neg_of_nat
|
||||
... = (m * 0 + 0 * succ n, m * succ n + 0 * 0) : zero_mul
|
||||
repr ((m : int) * -[1+ n]) = (m * 0 + 0, m * succ n + 0 * 0) : repr_neg_of_nat
|
||||
... = (m * 0 + 0 * succ n, m * succ n + 0 * 0) : by rewrite *zero_mul
|
||||
| -[1+ m] (of_nat n) := calc
|
||||
repr (-[1+ m] * n) = (0 + succ m * 0, succ m * n) : repr_neg_of_nat
|
||||
repr (-[1+ m] * (n:int)) = (0 + succ m * 0, succ m * n) : repr_neg_of_nat
|
||||
... = (0 + succ m * 0, 0 + succ m * n) : nat.zero_add
|
||||
... = (0 * n + succ m * 0, 0 + succ m * n) : zero_mul
|
||||
... = (0 * n + succ m * 0, 0 + succ m * n) : by rewrite zero_mul
|
||||
| -[1+ m] -[1+ n] := calc
|
||||
(succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : zero_mul
|
||||
(succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : by rewrite zero_mul
|
||||
... = (0 + succ m * succ n, 0 * succ n) : nat.zero_add
|
||||
|
||||
theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
|
||||
|
|
@ -421,16 +422,16 @@ theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
|
|||
: xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) :=
|
||||
nat.add.cancel_right (calc
|
||||
xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn))
|
||||
= xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : add.comm4
|
||||
... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : nat.add.comm
|
||||
... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : !congr_arg2 add.comm4 add.comm4
|
||||
... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym))
|
||||
: by rewrite[-+mul.left_distrib,-+mul.right_distrib]; exact H1 ▸ H2 ▸ rfl
|
||||
... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : !congr_arg2 add.comm4 add.comm4
|
||||
... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : !nat.add.comm ▸ !nat.add.comm ▸ rfl
|
||||
... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : add.comm4
|
||||
... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : nat.add.comm
|
||||
... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : add.comm4)
|
||||
= xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : by rewrite add.comm4
|
||||
... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : by rewrite {xb*ym+yb*xm +_}nat.add.comm
|
||||
... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : by exact !congr_arg2 add.comm4 add.comm4
|
||||
... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) : by rewrite[-+mul.left_distrib,-+mul.right_distrib]; exact H1 ▸ H2 ▸ rfl
|
||||
... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by exact !congr_arg2 add.comm4 add.comm4
|
||||
... = xa*yn+ya*xn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by rewrite {xa*yn + _}nat.add.comm
|
||||
... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : by rewrite {xb*yn + _}nat.add.comm
|
||||
... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : by rewrite add.comm4
|
||||
... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : by rewrite {xb*xn+yb*yn + _}nat.add.comm
|
||||
... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : by rewrite add.comm4)
|
||||
|
||||
theorem pmul_congr {p p' q q' : ℕ × ℕ} : p ≡ p' → q ≡ q' → pmul p q ≡ pmul p' q' := equiv_mul_prep
|
||||
|
||||
|
|
@ -498,41 +499,34 @@ assume H : 0 = 1, !succ_ne_zero (of_nat.inj H)⁻¹
|
|||
|
||||
theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 0 :=
|
||||
or.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero
|
||||
(eq_zero_or_eq_zero_of_mul_eq_zero (H ▸ (nat_abs_mul a b)⁻¹))
|
||||
(eq_zero_or_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H]))
|
||||
|
||||
section migrate_algebra
|
||||
open [classes] algebra
|
||||
protected definition integral_domain [reducible] [instance] : algebra.integral_domain int :=
|
||||
⦃algebra.integral_domain,
|
||||
add := int.add,
|
||||
add_assoc := add.assoc,
|
||||
zero := zero,
|
||||
zero_add := zero_add,
|
||||
add_zero := add_zero,
|
||||
neg := int.neg,
|
||||
add_left_inv := add.left_inv,
|
||||
add_comm := add.comm,
|
||||
mul := int.mul,
|
||||
mul_assoc := mul.assoc,
|
||||
one := 1,
|
||||
one_mul := one_mul,
|
||||
mul_one := mul_one,
|
||||
left_distrib := mul.left_distrib,
|
||||
right_distrib := mul.right_distrib,
|
||||
mul_comm := mul.comm,
|
||||
zero_ne_one := zero_ne_one,
|
||||
eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄
|
||||
|
||||
protected definition integral_domain [reducible] : algebra.integral_domain int :=
|
||||
⦃algebra.integral_domain,
|
||||
add := add,
|
||||
add_assoc := add.assoc,
|
||||
zero := zero,
|
||||
zero_add := zero_add,
|
||||
add_zero := add_zero,
|
||||
neg := neg,
|
||||
add_left_inv := add.left_inv,
|
||||
add_comm := add.comm,
|
||||
mul := mul,
|
||||
mul_assoc := mul.assoc,
|
||||
one := 1,
|
||||
one_mul := one_mul,
|
||||
mul_one := mul_one,
|
||||
left_distrib := mul.left_distrib,
|
||||
right_distrib := mul.right_distrib,
|
||||
mul_comm := mul.comm,
|
||||
zero_ne_one := zero_ne_one,
|
||||
eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄
|
||||
definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int :=
|
||||
has_sub.mk algebra.sub
|
||||
|
||||
local attribute int.integral_domain [instance]
|
||||
definition sub (a b : ℤ) : ℤ := algebra.sub a b
|
||||
infix [priority int.prio] - := int.sub
|
||||
definition dvd (a b : ℤ) : Prop := algebra.dvd a b
|
||||
notation [priority int.prio] a ∣ b := dvd a b
|
||||
|
||||
migrate from algebra with int
|
||||
replacing sub → sub, dvd → dvd
|
||||
end migrate_algebra
|
||||
definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int :=
|
||||
has_dvd.mk algebra.dvd
|
||||
|
||||
/- additional properties -/
|
||||
theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : m - n = sub m n :=
|
||||
|
|
@ -540,24 +534,28 @@ assert m - n + n = m, from nat.sub_add_cancel H,
|
|||
begin
|
||||
symmetry,
|
||||
apply sub_eq_of_eq_add,
|
||||
rewrite [-of_nat_add, this]
|
||||
rewrite this
|
||||
end
|
||||
|
||||
-- (sub_eq_of_eq_add (!congr_arg (nat.sub_add_cancel H)⁻¹))⁻¹
|
||||
|
||||
theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=
|
||||
by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add]
|
||||
by rewrite [neg_succ_of_nat_eq, neg_add]
|
||||
|
||||
definition succ (a : ℤ) := a + (succ zero)
|
||||
definition pred (a : ℤ) := a - (succ zero)
|
||||
theorem pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel
|
||||
theorem succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel
|
||||
|
||||
theorem neg_succ (a : ℤ) : -succ a = pred (-a) :=
|
||||
by rewrite [↑succ,neg_add]
|
||||
|
||||
theorem succ_neg_succ (a : ℤ) : succ (-succ a) = -a :=
|
||||
by rewrite [neg_succ,succ_pred]
|
||||
|
||||
theorem neg_pred (a : ℤ) : -pred a = succ (-a) :=
|
||||
by rewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm]
|
||||
by krewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm]
|
||||
|
||||
theorem pred_neg_pred (a : ℤ) : pred (-pred a) = -a :=
|
||||
by rewrite [neg_pred,pred_succ]
|
||||
|
||||
|
|
|
|||
|
|
@ -9,38 +9,50 @@ Following SSReflect and the SMTlib standard, we define a mod b so that 0 ≤ a m
|
|||
-/
|
||||
import data.int.order data.nat.div
|
||||
open [coercions] [reduce-hints] nat
|
||||
open [declarations] nat (succ)
|
||||
open [declarations] [classes] nat (succ)
|
||||
open - [notations] algebra
|
||||
open eq.ops
|
||||
|
||||
namespace int
|
||||
|
||||
/- definitions -/
|
||||
|
||||
definition divide (a b : ℤ) : ℤ :=
|
||||
protected definition divide (a b : ℤ) : ℤ :=
|
||||
sign b *
|
||||
(match a with
|
||||
| of_nat m := #nat m div (nat_abs b)
|
||||
| -[1+m] := -[1+ (#nat m div (nat_abs b))]
|
||||
| of_nat m := (m div (nat_abs b) : nat)
|
||||
| -[1+m] := -[1+ ((m:nat) div (nat_abs b))]
|
||||
end)
|
||||
notation [priority int.prio] a div b := divide a b
|
||||
|
||||
definition modulo (a b : ℤ) : ℤ := a - a div b * b
|
||||
notation [priority int.prio] a mod b := modulo a b
|
||||
definition int_has_divides [reducible] [instance] [priority int.prio] : has_divides int :=
|
||||
has_divides.mk int.divide
|
||||
|
||||
lemma divide_of_nat (a : nat) (b : ℤ) : (of_nat a) div b = sign b * (a div (nat_abs b) : nat) :=
|
||||
rfl
|
||||
|
||||
lemma divide_of_neg_succ (a : nat) (b : ℤ) : -[1+a] div b = sign b * -[1+ (a div (nat_abs b))] :=
|
||||
rfl
|
||||
|
||||
protected definition modulo (a b : ℤ) : ℤ := a - a div b * b
|
||||
|
||||
definition int_has_modulo [reducible] [instance] [priority int.prio] : has_modulo int :=
|
||||
has_modulo.mk int.modulo
|
||||
|
||||
notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
|
||||
|
||||
/- div -/
|
||||
|
||||
theorem of_nat_div (m n : nat) : of_nat (#nat m div n) = m div n :=
|
||||
theorem of_nat_div (m n : nat) : of_nat (m div n) = m div n :=
|
||||
nat.cases_on n
|
||||
(by rewrite [↑divide, sign_zero, zero_mul, nat.div_zero])
|
||||
(take n, by rewrite [↑divide, sign_of_succ, one_mul])
|
||||
(begin krewrite [divide_of_nat, sign_zero, zero_mul, nat.div_zero] end)
|
||||
(take (n : nat), by krewrite [divide_of_nat, sign_of_succ, one_mul])
|
||||
|
||||
theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) :
|
||||
-[1+m] div b = -(m div b + 1) :=
|
||||
calc
|
||||
-[1+m] div b = sign b * _ : rfl
|
||||
... = -[1+(#nat m div (nat_abs b))] : by rewrite [sign_of_pos H, one_mul]
|
||||
... = -(m div b + 1) : by rewrite [↑divide, sign_of_pos H, one_mul]
|
||||
... = -[1+(m div (nat_abs b))] : begin krewrite [sign_of_pos H, one_mul] end
|
||||
... = -(m div b + 1) : by krewrite [sign_of_pos H, one_mul]
|
||||
|
||||
theorem div_neg (a b : ℤ) : a div -b = -(a div b) :=
|
||||
by rewrite [↑divide, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg]
|
||||
|
|
|
|||
|
|
@ -8,19 +8,22 @@ and transfer the results.
|
|||
-/
|
||||
import .basic algebra.ordered_ring
|
||||
open nat
|
||||
open - [notations] algebra
|
||||
open decidable
|
||||
open int eq.ops
|
||||
|
||||
namespace int
|
||||
|
||||
private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false)
|
||||
definition le (a b : ℤ) : Prop := nonneg (b - a)
|
||||
definition lt (a b : ℤ) : Prop := le (a + 1) b
|
||||
protected definition le (a b : ℤ) : Prop := nonneg (b - a)
|
||||
|
||||
infix [priority int.prio] - := int.sub
|
||||
infix [priority int.prio] <= := int.le
|
||||
infix [priority int.prio] ≤ := int.le
|
||||
infix [priority int.prio] < := int.lt
|
||||
definition int_has_le [instance] [reducible] [priority int.prio]: has_le int :=
|
||||
has_le.mk int.le
|
||||
|
||||
protected definition lt (a b : ℤ) : Prop := (a + 1) ≤ b
|
||||
|
||||
definition int_has_lt [instance] [reducible] [priority int.prio]: has_lt int :=
|
||||
has_lt.mk int.lt
|
||||
|
||||
local attribute nonneg [reducible]
|
||||
private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := int.cases_on a _ _
|
||||
|
|
@ -34,7 +37,7 @@ private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
|
|||
int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
|
||||
|
||||
theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
|
||||
have n = b - a, from eq_add_neg_of_add_eq (!add.comm ▸ H),
|
||||
have n = b - a, from eq_add_neg_of_add_eq (begin rewrite [add.comm, H] end), -- !add.comm ▸ H),
|
||||
show nonneg (b - a), from this ▸ trivial
|
||||
|
||||
theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
|
||||
|
|
@ -64,7 +67,7 @@ theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
|
|||
le.intro (show a + 1 + n = a + succ n, from
|
||||
calc
|
||||
a + 1 + n = a + (1 + n) : add.assoc
|
||||
... = a + (n + 1) : nat.add.comm
|
||||
... = a + (n + 1) : by rewrite (add.comm 1 n)
|
||||
... = a + succ n : rfl)
|
||||
|
||||
theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
|
||||
|
|
@ -191,9 +194,9 @@ le.intro
|
|||
(eq.symm
|
||||
(calc
|
||||
a * b = (0 + n) * b : Hn
|
||||
... = n * b : nat.zero_add
|
||||
... = n * b : zero_add
|
||||
... = n * (0 + m) : {Hm⁻¹}
|
||||
... = n * m : nat.zero_add
|
||||
... = n * m : zero_add
|
||||
... = 0 + n * m : zero_add))
|
||||
|
||||
theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b :=
|
||||
|
|
@ -203,15 +206,14 @@ lt.intro
|
|||
(eq.symm
|
||||
(calc
|
||||
a * b = (0 + nat.succ n) * b : Hn
|
||||
... = nat.succ n * b : nat.zero_add
|
||||
... = nat.succ n * b : zero_add
|
||||
... = nat.succ n * (0 + nat.succ m) : {Hm⁻¹}
|
||||
... = nat.succ n * nat.succ m : nat.zero_add
|
||||
... = nat.succ n * nat.succ m : zero_add
|
||||
... = of_nat (nat.succ n * nat.succ m) : of_nat_mul
|
||||
... = of_nat (nat.succ n * m + nat.succ n) : nat.mul_succ
|
||||
... = of_nat (nat.succ (nat.succ n * m + n)) : nat.add_succ
|
||||
... = 0 + nat.succ (nat.succ n * m + n) : zero_add))
|
||||
|
||||
|
||||
theorem zero_lt_one : (0 : ℤ) < 1 := trivial
|
||||
|
||||
theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a :=
|
||||
|
|
@ -231,61 +233,32 @@ theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c :=
|
|||
(iff.mpr !lt_iff_le_and_ne) (and.intro Hac
|
||||
(assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab))
|
||||
|
||||
section migrate_algebra
|
||||
open [classes] algebra
|
||||
|
||||
protected definition linear_ordered_comm_ring [reducible] :
|
||||
protected definition linear_ordered_comm_ring [reducible] [instance] :
|
||||
algebra.linear_ordered_comm_ring int :=
|
||||
⦃algebra.linear_ordered_comm_ring, int.integral_domain,
|
||||
le := le,
|
||||
le_refl := le.refl,
|
||||
le_trans := @le.trans,
|
||||
le_antisymm := @le.antisymm,
|
||||
lt := lt,
|
||||
le_of_lt := @le_of_lt,
|
||||
lt_irrefl := lt.irrefl,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt,
|
||||
add_le_add_left := @add_le_add_left,
|
||||
mul_nonneg := @mul_nonneg,
|
||||
mul_pos := @mul_pos,
|
||||
le_iff_lt_or_eq := le_iff_lt_or_eq,
|
||||
le_total := le.total,
|
||||
zero_ne_one := zero_ne_one,
|
||||
zero_lt_one := zero_lt_one,
|
||||
add_lt_add_left := @add_lt_add_left⦄
|
||||
⦃algebra.linear_ordered_comm_ring, int.integral_domain,
|
||||
le := int.le,
|
||||
le_refl := le.refl,
|
||||
le_trans := @le.trans,
|
||||
le_antisymm := @le.antisymm,
|
||||
lt := int.lt,
|
||||
le_of_lt := @le_of_lt,
|
||||
lt_irrefl := lt.irrefl,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt,
|
||||
add_le_add_left := @add_le_add_left,
|
||||
mul_nonneg := @mul_nonneg,
|
||||
mul_pos := @mul_pos,
|
||||
le_iff_lt_or_eq := le_iff_lt_or_eq,
|
||||
le_total := le.total,
|
||||
zero_ne_one := zero_ne_one,
|
||||
zero_lt_one := zero_lt_one,
|
||||
add_lt_add_left := @add_lt_add_left⦄
|
||||
|
||||
protected definition decidable_linear_ordered_comm_ring [reducible] :
|
||||
protected definition decidable_linear_ordered_comm_ring [reducible] [instance] :
|
||||
algebra.decidable_linear_ordered_comm_ring int :=
|
||||
⦃algebra.decidable_linear_ordered_comm_ring,
|
||||
int.linear_ordered_comm_ring,
|
||||
decidable_lt := decidable_lt⦄
|
||||
|
||||
local attribute int.integral_domain [instance]
|
||||
local attribute int.linear_ordered_comm_ring [instance]
|
||||
local attribute int.decidable_linear_ordered_comm_ring [instance]
|
||||
|
||||
definition ge [reducible] (a b : ℤ) := algebra.has_le.ge a b
|
||||
definition gt [reducible] (a b : ℤ) := algebra.has_lt.gt a b
|
||||
infix [priority int.prio] >= := int.ge
|
||||
infix [priority int.prio] ≥ := int.ge
|
||||
infix [priority int.prio] > := int.gt
|
||||
definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) :=
|
||||
show decidable (b ≤ a), from _
|
||||
definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) :=
|
||||
show decidable (b < a), from _
|
||||
definition min : ℤ → ℤ → ℤ := algebra.min
|
||||
definition max : ℤ → ℤ → ℤ := algebra.max
|
||||
definition abs : ℤ → ℤ := algebra.abs
|
||||
definition sign : ℤ → ℤ := algebra.sign
|
||||
|
||||
migrate from algebra with int
|
||||
replacing dvd → dvd, sub → sub, has_le.ge → ge, has_lt.gt → gt, min → min, max → max,
|
||||
abs → abs, sign → sign
|
||||
|
||||
attribute le.trans ge.trans lt.trans gt.trans [trans]
|
||||
attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans]
|
||||
end migrate_algebra
|
||||
⦃algebra.decidable_linear_ordered_comm_ring,
|
||||
int.linear_ordered_comm_ring,
|
||||
decidable_lt := decidable_lt⦄
|
||||
|
||||
/- more facts specific to int -/
|
||||
|
||||
|
|
@ -325,12 +298,12 @@ theorem nat_abs_abs (a : ℤ) : nat_abs (abs a) = nat_abs a :=
|
|||
abs.by_cases rfl !nat_abs_neg
|
||||
|
||||
theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
|
||||
obtain n (H1 : a + 1 + n = b), from le.elim H,
|
||||
obtain (n : nat) (H1 : a + 1 + n = b), from le.elim H,
|
||||
have a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1],
|
||||
lt.intro this
|
||||
|
||||
theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b :=
|
||||
obtain n (H1 : a + succ n = b), from lt.elim H,
|
||||
obtain (n : nat) (H1 : a + succ n = b), from lt.elim H,
|
||||
have a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1],
|
||||
le.intro this
|
||||
|
||||
|
|
@ -342,7 +315,7 @@ have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H,
|
|||
le_of_add_le_add_right H1
|
||||
|
||||
theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b :=
|
||||
lt_of_add_one_le (!sub_add_cancel⁻¹ ▸ H)
|
||||
lt_of_add_one_le (begin rewrite algebra.sub_add_cancel, exact H end)
|
||||
|
||||
theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b :=
|
||||
!sub_add_cancel ▸ add_one_le_of_lt H
|
||||
|
|
@ -358,8 +331,8 @@ sign_of_pos (of_nat_pos !nat.succ_pos)
|
|||
|
||||
theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[1+m] :=
|
||||
int.cases_on a
|
||||
(take m H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H))
|
||||
(take m H, exists.intro m rfl)
|
||||
(take (m : nat) H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H))
|
||||
(take (m : nat) H, exists.intro m rfl)
|
||||
|
||||
theorem eq_one_of_mul_eq_one_right {a b : ℤ} (H : a ≥ 0) (H' : a * b = 1) : a = 1 :=
|
||||
have a * b > 0, by rewrite H'; apply trivial,
|
||||
|
|
@ -397,13 +370,13 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
|
|||
cases Hinh with [elt, Helt],
|
||||
existsi b + of_nat (least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b)))),
|
||||
have Heltb : elt > b, begin
|
||||
apply int.lt_of_not_ge,
|
||||
apply lt_of_not_ge,
|
||||
intro Hge,
|
||||
apply (Hb _ Hge) Helt
|
||||
end,
|
||||
have H' : P (b + of_nat (nat_abs (elt - b))), begin
|
||||
rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),
|
||||
int.add.comm, int.sub_add_cancel],
|
||||
rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)),
|
||||
add.comm, algebra.sub_add_cancel],
|
||||
apply Helt
|
||||
end,
|
||||
apply and.intro,
|
||||
|
|
@ -411,16 +384,16 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
|
|||
intros z Hz,
|
||||
cases em (z ≤ b) with [Hzb, Hzb],
|
||||
apply Hb _ Hzb,
|
||||
let Hzb' := int.lt_of_not_ge Hzb,
|
||||
let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb',
|
||||
let Hzb' := lt_of_not_ge Hzb,
|
||||
let Hpos := iff.mpr !sub_pos_iff_lt Hzb',
|
||||
have Hzbk : z = b + of_nat (nat_abs (z - b)),
|
||||
by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, int.sub_add_cancel],
|
||||
by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, algebra.sub_add_cancel],
|
||||
have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin
|
||||
let Hz' := iff.mp !int.lt_add_iff_sub_lt_left Hz,
|
||||
let Hz' := iff.mp !lt_add_iff_sub_lt_left Hz,
|
||||
rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
|
||||
apply lt_of_of_nat_lt_of_nat Hz'
|
||||
end,
|
||||
let Hk' := nat.not_le_of_gt Hk,
|
||||
let Hk' := algebra.not_le_of_gt Hk,
|
||||
rewrite Hzbk,
|
||||
apply λ p, mt (ge_least_of_lt _ p) Hk',
|
||||
apply nat.lt.trans Hk,
|
||||
|
|
@ -435,13 +408,13 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
|
|||
cases Hinh with [elt, Helt],
|
||||
existsi b - of_nat (least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt)))),
|
||||
have Heltb : elt < b, begin
|
||||
apply int.lt_of_not_ge,
|
||||
apply lt_of_not_ge,
|
||||
intro Hge,
|
||||
apply (Hb _ Hge) Helt
|
||||
end,
|
||||
have H' : P (b - of_nat (nat_abs (b - elt))), begin
|
||||
rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),
|
||||
int.sub_sub_self],
|
||||
rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)),
|
||||
sub_sub_self],
|
||||
apply Helt
|
||||
end,
|
||||
apply and.intro,
|
||||
|
|
@ -449,16 +422,16 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
|
|||
intros z Hz,
|
||||
cases em (z ≥ b) with [Hzb, Hzb],
|
||||
apply Hb _ Hzb,
|
||||
let Hzb' := int.lt_of_not_ge Hzb,
|
||||
let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb',
|
||||
let Hzb' := lt_of_not_ge Hzb,
|
||||
let Hpos := iff.mpr !sub_pos_iff_lt Hzb',
|
||||
have Hzbk : z = b - of_nat (nat_abs (b - z)),
|
||||
by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.sub_sub_self],
|
||||
by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), sub_sub_self],
|
||||
have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin
|
||||
let Hz' := iff.mp !int.lt_add_iff_sub_lt_left (iff.mpr !int.lt_add_iff_sub_lt_right Hz),
|
||||
let Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz),
|
||||
rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
|
||||
apply lt_of_of_nat_lt_of_nat Hz'
|
||||
end,
|
||||
let Hk' := nat.not_le_of_gt Hk,
|
||||
let Hk' := algebra.not_le_of_gt Hk,
|
||||
rewrite Hzbk,
|
||||
apply λ p, mt (ge_least_of_lt _ p) Hk',
|
||||
apply nat.lt.trans Hk,
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ Basic properties of lists.
|
|||
-/
|
||||
import logic tools.helper_tactics data.nat.order
|
||||
open eq.ops helper_tactics nat prod function option
|
||||
open - [notations] algebra
|
||||
|
||||
inductive list (T : Type) : Type :=
|
||||
| nil {} : list T
|
||||
|
|
@ -70,8 +71,8 @@ theorem length_cons [simp] (x : T) (t : list T) : length (x::t) = length t + 1
|
|||
|
||||
theorem length_append [simp] : ∀ (s t : list T), length (s ++ t) = length s + length t
|
||||
| [] t := calc
|
||||
length ([] ++ t) = length t : rfl
|
||||
... = length [] + length t : zero_add
|
||||
length ([] ++ t) = length t : rfl
|
||||
... = length [] + length t : by rewrite [length_nil, zero_add]
|
||||
| (a :: s) t := calc
|
||||
length (a :: s ++ t) = length (s ++ t) + 1 : rfl
|
||||
... = length s + length t + 1 : length_append
|
||||
|
|
|
|||
|
|
@ -211,7 +211,7 @@ nat.induction_on n
|
|||
|
||||
theorem succ_mul [simp] (n m : ℕ) : (succ n) * m = (n * m) + m :=
|
||||
nat.induction_on m
|
||||
(!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹)
|
||||
(by rewrite mul_zero)
|
||||
(take k IH, calc
|
||||
succ n * succ k = succ n * k + succ n : mul_succ
|
||||
... = n * k + k + succ n : IH
|
||||
|
|
@ -289,35 +289,31 @@ nat.cases_on n
|
|||
... = succ (succ n' * m' + n') : add_succ)⁻¹
|
||||
!succ_ne_zero))
|
||||
|
||||
section migrate_algebra
|
||||
open [classes] algebra
|
||||
open - [notations] algebra
|
||||
protected definition comm_semiring [reducible] [instance] : algebra.comm_semiring nat :=
|
||||
⦃algebra.comm_semiring,
|
||||
add := nat.add,
|
||||
add_assoc := add.assoc,
|
||||
zero := nat.zero,
|
||||
zero_add := zero_add,
|
||||
add_zero := add_zero,
|
||||
add_comm := add.comm,
|
||||
mul := nat.mul,
|
||||
mul_assoc := mul.assoc,
|
||||
one := nat.succ nat.zero,
|
||||
one_mul := one_mul,
|
||||
mul_one := mul_one,
|
||||
left_distrib := mul.left_distrib,
|
||||
right_distrib := mul.right_distrib,
|
||||
zero_mul := zero_mul,
|
||||
mul_zero := mul_zero,
|
||||
mul_comm := mul.comm⦄
|
||||
|
||||
protected definition comm_semiring [reducible] : algebra.comm_semiring nat :=
|
||||
⦃algebra.comm_semiring,
|
||||
add := add,
|
||||
add_assoc := add.assoc,
|
||||
zero := zero,
|
||||
zero_add := zero_add,
|
||||
add_zero := add_zero,
|
||||
add_comm := add.comm,
|
||||
mul := mul,
|
||||
mul_assoc := mul.assoc,
|
||||
one := succ zero,
|
||||
one_mul := one_mul,
|
||||
mul_one := mul_one,
|
||||
left_distrib := mul.left_distrib,
|
||||
right_distrib := mul.right_distrib,
|
||||
zero_mul := zero_mul,
|
||||
mul_zero := mul_zero,
|
||||
mul_comm := mul.comm⦄
|
||||
definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
|
||||
has_zero.mk zero
|
||||
|
||||
local attribute nat.comm_semiring [instance]
|
||||
definition dvd (a b : ℕ) : Prop := algebra.dvd a b
|
||||
notation a ∣ b := dvd a b
|
||||
|
||||
migrate from algebra with nat replacing dvd → dvd
|
||||
|
||||
end migrate_algebra
|
||||
definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat :=
|
||||
has_one.mk (succ zero)
|
||||
end nat
|
||||
|
||||
section
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ Definitions and properties of div and mod. Much of the development follows Isabe
|
|||
-/
|
||||
import data.nat.sub
|
||||
open eq.ops well_founded decidable prod
|
||||
open - [notations] algebra
|
||||
|
||||
namespace nat
|
||||
|
||||
|
|
@ -20,7 +21,9 @@ private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y :
|
|||
if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
|
||||
|
||||
definition divide := fix div.F
|
||||
notation a div b := divide a b
|
||||
|
||||
definition nat_has_divides [reducible] [instance] [priority nat.prio] : has_divides nat :=
|
||||
has_divides.mk divide
|
||||
|
||||
theorem divide_def (x y : nat) : divide x y = if 0 < y ∧ y ≤ x then divide (x - y) y + 1 else 0 :=
|
||||
congr_fun (fix_eq div.F x) y
|
||||
|
|
@ -76,8 +79,11 @@ theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n :=
|
|||
private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
|
||||
if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
|
||||
|
||||
definition modulo := fix mod.F
|
||||
notation a mod b := modulo a b
|
||||
protected definition modulo := fix mod.F
|
||||
|
||||
definition nat_has_modulo [reducible] [instance] [priority nat.prio] : has_modulo nat :=
|
||||
has_modulo.mk nat.modulo
|
||||
|
||||
notation a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
|
||||
|
||||
theorem modulo_def (x y : nat) : modulo x y = if 0 < y ∧ y ≤ x then modulo (x - y) y else x :=
|
||||
|
|
@ -150,41 +156,44 @@ have H1 : n mod 1 < 1, from !mod_lt !succ_pos,
|
|||
eq_zero_of_le_zero (le_of_lt_succ H1)
|
||||
|
||||
/- properties of div and mod -/
|
||||
set_option pp.all true
|
||||
|
||||
-- the quotient / remainder theorem
|
||||
theorem eq_div_mul_add_mod (x y : ℕ) : x = x div y * y + x mod y :=
|
||||
by_cases_zero_pos y
|
||||
(show x = x div 0 * 0 + x mod 0, from
|
||||
begin
|
||||
eapply by_cases_zero_pos y,
|
||||
show x = x div 0 * 0 + x mod 0, from
|
||||
(calc
|
||||
x div 0 * 0 + x mod 0 = 0 + x mod 0 : mul_zero
|
||||
... = x mod 0 : zero_add
|
||||
... = x : mod_zero)⁻¹)
|
||||
(take y,
|
||||
assume H : y > 0,
|
||||
show x = x div y * y + x mod y, from
|
||||
nat.case_strong_induction_on x
|
||||
(show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, zero_div, zero_mul])
|
||||
(take x,
|
||||
assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y,
|
||||
show succ x = succ x div y * y + succ x mod y, from
|
||||
if H1 : succ x < y then
|
||||
have H2 : succ x div y = 0, from div_eq_zero_of_lt H1,
|
||||
have H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
|
||||
H2⁻¹ ▸ H3⁻¹ ▸ !zero_mul⁻¹ ▸ !zero_add⁻¹
|
||||
else
|
||||
have H2 : y ≤ succ x, from le_of_not_gt H1,
|
||||
have H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2,
|
||||
have H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
|
||||
have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
|
||||
have H6 : succ x - y ≤ x, from le_of_lt_succ H5,
|
||||
(calc
|
||||
succ x div y * y + succ x mod y =
|
||||
succ ((succ x - y) div y) * y + succ x mod y : H3
|
||||
... = ((succ x - y) div y) * y + y + succ x mod y : succ_mul
|
||||
... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4
|
||||
... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm
|
||||
... = succ x - y + y : {!(IH _ H6)⁻¹}
|
||||
... = succ x : sub_add_cancel H2)⁻¹))
|
||||
... = x : mod_zero)⁻¹,
|
||||
intro y H,
|
||||
show x = x div y * y + x mod y,
|
||||
begin
|
||||
eapply nat.case_strong_induction_on x,
|
||||
show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, zero_div, zero_mul],
|
||||
intro x IH,
|
||||
show succ x = succ x div y * y + succ x mod y, from
|
||||
if H1 : succ x < y then
|
||||
assert H2 : succ x div y = 0, from div_eq_zero_of_lt H1,
|
||||
assert H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
|
||||
begin rewrite [H2, H3, zero_mul, zero_add] end
|
||||
else
|
||||
have H2 : y ≤ succ x, from le_of_not_gt H1,
|
||||
assert H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2,
|
||||
assert H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
|
||||
have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
|
||||
assert H6 : succ x - y ≤ x, from le_of_lt_succ H5,
|
||||
(calc
|
||||
succ x div y * y + succ x mod y =
|
||||
succ ((succ x - y) div y) * y + succ x mod y : by rewrite H3
|
||||
... = ((succ x - y) div y) * y + y + succ x mod y : by rewrite succ_mul
|
||||
... = ((succ x - y) div y) * y + y + (succ x - y) mod y : by rewrite H4
|
||||
... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm
|
||||
... = succ x - y + y : by rewrite -(IH _ H6)
|
||||
... = succ x : sub_add_cancel H2)⁻¹
|
||||
end
|
||||
end
|
||||
|
||||
theorem mod_eq_sub_div_mul (x y : ℕ) : x mod y = x - x div y * y :=
|
||||
eq_sub_of_add_eq (!add.comm ▸ !eq_div_mul_add_mod)⁻¹
|
||||
|
|
@ -244,7 +253,8 @@ have H6 : y > 0, from lt_of_le_of_lt !zero_le H1,
|
|||
show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
|
||||
|
||||
theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
if H : y = 0 then H⁻¹ ▸ !mul_zero⁻¹ ▸ !div_zero⁻¹ ▸ !div_zero
|
||||
if H : y = 0 then
|
||||
by rewrite [H, mul_zero, *div_zero]
|
||||
else
|
||||
have ypos : y > 0, from pos_of_ne_zero H,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
|
|
@ -533,15 +543,16 @@ iff.mp (!div_le_iff_le_mul_of_div H1 H2) H3
|
|||
-- needed for integer division
|
||||
theorem mul_sub_div_of_lt {m n k : ℕ} (H : k < m * n) :
|
||||
(m * n - (k + 1)) div m = n - k div m - 1 :=
|
||||
have H1 : k div m < n, from div_lt_of_lt_mul (!mul.comm ▸ H),
|
||||
have H2 : n - k div m ≥ 1, from
|
||||
le_sub_of_add_le (calc
|
||||
1 + k div m = succ (k div m) : add.comm
|
||||
... ≤ n : succ_le_of_lt H1),
|
||||
assert H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹,
|
||||
assert H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)),
|
||||
have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4),
|
||||
assert H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos,
|
||||
begin
|
||||
have H1 : k div m < n, from div_lt_of_lt_mul (!mul.comm ▸ H),
|
||||
have H2 : n - k div m ≥ 1, from
|
||||
le_sub_of_add_le (calc
|
||||
1 + k div m = succ (k div m) : add.comm
|
||||
... ≤ n : succ_le_of_lt H1),
|
||||
have H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹,
|
||||
have H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)),
|
||||
have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4),
|
||||
have H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos,
|
||||
calc
|
||||
(m * n - (k + 1)) div m = (m * n - (k div m * m + k mod m + 1)) div m : eq_div_mul_add_mod
|
||||
... = (m * n - k div m * m - (k mod m + 1)) div m : by rewrite [*sub_sub]
|
||||
|
|
@ -554,7 +565,7 @@ calc
|
|||
by rewrite [add.comm, (add_mul_div_self H4)]
|
||||
... = n - k div m - 1 :
|
||||
by rewrite [div_eq_zero_of_lt H6, zero_add]
|
||||
|
||||
end
|
||||
|
||||
private lemma div_div_aux (a b c : nat) : b > 0 → c > 0 → (a div b) div c = a div (b * c) :=
|
||||
suppose b > 0, suppose c > 0,
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Leonardo de Moura
|
|||
Factorial
|
||||
-/
|
||||
import data.nat.div
|
||||
open - [notations] algebra
|
||||
|
||||
namespace nat
|
||||
definition fact : nat → nat
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ Definitions and properties of gcd, lcm, and coprime.
|
|||
-/
|
||||
import .div
|
||||
open eq.ops well_founded decidable prod
|
||||
open - [notations] algebra
|
||||
|
||||
namespace nat
|
||||
|
||||
|
|
@ -341,7 +342,7 @@ theorem comprime_one_left : ∀ n, coprime 1 n :=
|
|||
theorem comprime_one_right : ∀ n, coprime n 1 :=
|
||||
λ n, !gcd_one_right
|
||||
|
||||
theorem exists_eq_prod_and_dvd_and_dvd {m n k} (H : k ∣ m * n) :
|
||||
theorem exists_eq_prod_and_dvd_and_dvd {m n k : nat} (H : k ∣ m * n) :
|
||||
∃ m' n', k = m' * n' ∧ m' ∣ m ∧ n' ∣ n :=
|
||||
or.elim (eq_zero_or_pos (gcd k m))
|
||||
(assume H1 : gcd k m = 0,
|
||||
|
|
|
|||
|
|
@ -135,92 +135,72 @@ else (eq_max_left h) ▸ !le.refl
|
|||
|
||||
/- nat is an instance of a linearly ordered semiring and a lattice -/
|
||||
|
||||
section migrate_algebra
|
||||
open [classes] algebra
|
||||
local attribute nat.comm_semiring [instance]
|
||||
open -[notations] algebra
|
||||
|
||||
protected definition decidable_linear_ordered_semiring [reducible] :
|
||||
algebra.decidable_linear_ordered_semiring nat :=
|
||||
⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring,
|
||||
add_left_cancel := @add.cancel_left,
|
||||
add_right_cancel := @add.cancel_right,
|
||||
lt := lt,
|
||||
le := le,
|
||||
le_refl := le.refl,
|
||||
le_trans := @le.trans,
|
||||
le_antisymm := @le.antisymm,
|
||||
le_total := @le.total,
|
||||
le_iff_lt_or_eq := @le_iff_lt_or_eq,
|
||||
le_of_lt := @le_of_lt,
|
||||
lt_irrefl := @lt.irrefl,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt,
|
||||
lt_of_add_lt_add_left := @lt_of_add_lt_add_left,
|
||||
add_lt_add_left := @add_lt_add_left,
|
||||
add_le_add_left := @add_le_add_left,
|
||||
le_of_add_le_add_left := @le_of_add_le_add_left,
|
||||
zero_lt_one := zero_lt_succ 0,
|
||||
mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1),
|
||||
mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1),
|
||||
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,
|
||||
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right,
|
||||
decidable_lt := nat.decidable_lt ⦄
|
||||
protected definition decidable_linear_ordered_semiring [reducible] [instance] :
|
||||
algebra.decidable_linear_ordered_semiring nat :=
|
||||
⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring,
|
||||
add_left_cancel := @add.cancel_left,
|
||||
add_right_cancel := @add.cancel_right,
|
||||
lt := nat.lt,
|
||||
le := nat.le,
|
||||
le_refl := le.refl,
|
||||
le_trans := @le.trans,
|
||||
le_antisymm := @le.antisymm,
|
||||
le_total := @le.total,
|
||||
le_iff_lt_or_eq := @le_iff_lt_or_eq,
|
||||
le_of_lt := @le_of_lt,
|
||||
lt_irrefl := @lt.irrefl,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt,
|
||||
lt_of_add_lt_add_left := @lt_of_add_lt_add_left,
|
||||
add_lt_add_left := @add_lt_add_left,
|
||||
add_le_add_left := @add_le_add_left,
|
||||
le_of_add_le_add_left := @le_of_add_le_add_left,
|
||||
zero_lt_one := zero_lt_succ 0,
|
||||
mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1),
|
||||
mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1),
|
||||
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,
|
||||
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right,
|
||||
decidable_lt := nat.decidable_lt ⦄
|
||||
|
||||
/-
|
||||
protected definition lattice [reducible] : algebra.lattice nat :=
|
||||
⦃ algebra.lattice, nat.linear_ordered_semiring,
|
||||
min := min,
|
||||
max := max,
|
||||
min_le_left := min_le_left,
|
||||
min_le_right := min_le_right,
|
||||
le_min := @le_min,
|
||||
le_max_left := le_max_left,
|
||||
le_max_right := le_max_right,
|
||||
max_le := @max_le ⦄
|
||||
|
||||
local attribute nat.linear_ordered_semiring [instance]
|
||||
local attribute nat.lattice [instance]
|
||||
-/
|
||||
local attribute nat.decidable_linear_ordered_semiring [instance]
|
||||
definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat :=
|
||||
has_dvd.mk algebra.dvd
|
||||
|
||||
definition min : ℕ → ℕ → ℕ := algebra.min
|
||||
definition max : ℕ → ℕ → ℕ := algebra.max
|
||||
theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
|
||||
@algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
|
||||
|
||||
migrate from algebra with nat
|
||||
replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, min → min, max → max
|
||||
hiding add_pos_of_pos_of_nonneg, add_pos_of_nonneg_of_pos,
|
||||
add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
|
||||
le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
|
||||
lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right,
|
||||
mul_lt_mul
|
||||
theorem add_pos_right {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < b + a :=
|
||||
by rewrite add.comm; apply add_pos_left H b
|
||||
|
||||
attribute le.trans ge.trans lt.trans gt.trans [trans]
|
||||
attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans]
|
||||
theorem add_eq_zero_iff_eq_zero_and_eq_zero {a b : ℕ} :
|
||||
a + b = 0 ↔ a = 0 ∧ b = 0 :=
|
||||
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
|
||||
|
||||
theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
|
||||
@algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
|
||||
theorem add_pos_right {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < b + a :=
|
||||
!add.comm ▸ add_pos_left H b
|
||||
theorem add_eq_zero_iff_eq_zero_and_eq_zero {a b : ℕ} :
|
||||
a + b = 0 ↔ a = 0 ∧ b = 0 :=
|
||||
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
|
||||
theorem le_add_of_le_left {a b c : ℕ} (H : b ≤ c) : b ≤ a + c :=
|
||||
@algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
|
||||
theorem le_add_of_le_right {a b c : ℕ} (H : b ≤ c) : b ≤ c + a :=
|
||||
@algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
|
||||
theorem lt_add_of_lt_left {b c : ℕ} (H : b < c) (a : ℕ) : b < a + c :=
|
||||
@algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
|
||||
theorem lt_add_of_lt_right {b c : ℕ} (H : b < c) (a : ℕ) : b < c + a :=
|
||||
@algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
|
||||
theorem lt_of_mul_lt_mul_left {a b c : ℕ} (H : c * a < c * b) : a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
|
||||
theorem lt_of_mul_lt_mul_right {a b c : ℕ} (H : a * c < b * c) : a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
|
||||
theorem pos_of_mul_pos_left {a b : ℕ} (H : 0 < a * b) : 0 < b :=
|
||||
@algebra.pos_of_mul_pos_left _ _ a b H !zero_le
|
||||
theorem pos_of_mul_pos_right {a b : ℕ} (H : 0 < a * b) : 0 < a :=
|
||||
@algebra.pos_of_mul_pos_right _ _ a b H !zero_le
|
||||
end migrate_algebra
|
||||
theorem le_add_of_le_left {a b c : ℕ} (H : b ≤ c) : b ≤ a + c :=
|
||||
@algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
|
||||
|
||||
theorem le_add_of_le_right {a b c : ℕ} (H : b ≤ c) : b ≤ c + a :=
|
||||
@algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
|
||||
|
||||
theorem lt_add_of_lt_left {b c : ℕ} (H : b < c) (a : ℕ) : b < a + c :=
|
||||
@algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
|
||||
|
||||
theorem lt_add_of_lt_right {b c : ℕ} (H : b < c) (a : ℕ) : b < c + a :=
|
||||
@algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
|
||||
|
||||
theorem lt_of_mul_lt_mul_left {a b c : ℕ} (H : c * a < c * b) : a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
|
||||
|
||||
theorem lt_of_mul_lt_mul_right {a b c : ℕ} (H : a * c < b * c) : a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
|
||||
|
||||
theorem pos_of_mul_pos_left {a b : ℕ} (H : 0 < a * b) : 0 < b :=
|
||||
@algebra.pos_of_mul_pos_left _ _ a b H !zero_le
|
||||
|
||||
theorem pos_of_mul_pos_right {a b : ℕ} (H : 0 < a * b) : 0 < a :=
|
||||
@algebra.pos_of_mul_pos_right _ _ a b H !zero_le
|
||||
|
||||
theorem zero_le_one : 0 ≤ 1 := dec_trivial
|
||||
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ Elegant pairing function.
|
|||
-/
|
||||
import data.nat.sqrt data.nat.div
|
||||
open prod decidable
|
||||
open - [notations] algebra
|
||||
|
||||
namespace nat
|
||||
definition mkpair (a b : nat) : nat :=
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ import data.nat.order data.nat.sub
|
|||
|
||||
namespace nat
|
||||
open decidable
|
||||
open - [notations] algebra
|
||||
|
||||
-- This is the simplest possible function that just performs a linear search
|
||||
definition sqrt_aux : nat → nat → nat
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
|
|||
|
||||
theorem add_sub_cancel (n m : ℕ) : n + m - m = n :=
|
||||
nat.induction_on m
|
||||
(!add_zero⁻¹ ▸ !sub_zero)
|
||||
(begin rewrite add_zero end)
|
||||
(take k : ℕ,
|
||||
assume IH : n + k - k = n,
|
||||
calc
|
||||
|
|
@ -72,7 +72,7 @@ nat.induction_on k
|
|||
n - m - succ l = pred (n - m - l) : !sub_succ
|
||||
... = pred (n - (m + l)) : IH
|
||||
... = n - succ (m + l) : sub_succ
|
||||
... = n - (m + succ l) : {!add_succ⁻¹})
|
||||
... = n - (m + succ l) : by rewrite add_succ)
|
||||
|
||||
theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k :=
|
||||
calc
|
||||
|
|
@ -206,7 +206,7 @@ theorem exists_sub_eq_of_le {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
|
|||
obtain (k : ℕ) (Hk : n + k = m), from le.elim H,
|
||||
exists.intro k
|
||||
(calc
|
||||
m - k = n + k - k : Hk⁻¹
|
||||
m - k = n + k - k : by rewrite Hk
|
||||
... = n : add_sub_cancel)
|
||||
|
||||
theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
|
||||
|
|
@ -289,9 +289,11 @@ sub.cases
|
|||
... = k - n + n : sub_add_cancel H3,
|
||||
le.intro (add.cancel_right H4))
|
||||
|
||||
open -[notations] algebra
|
||||
|
||||
theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 :=
|
||||
have H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹,
|
||||
have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H,
|
||||
assert H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹,
|
||||
have H2 : 0 + m < n - m + m, begin rewrite [zero_add, -H1], exact H end,
|
||||
!lt_of_add_lt_add_right H2
|
||||
|
||||
theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n :=
|
||||
|
|
@ -319,9 +321,9 @@ sub.cases
|
|||
assume Hmn : m + mn = n,
|
||||
sub.cases
|
||||
(assume H : m ≤ k,
|
||||
have H2 : n - k ≤ n - m, from sub_le_sub_left H n,
|
||||
have H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2,
|
||||
show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3)
|
||||
have H2 : n - k ≤ n - m, from sub_le_sub_left H n,
|
||||
assert H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2,
|
||||
show n - k ≤ mn + 0, begin rewrite add_zero, assumption end)
|
||||
(take km : ℕ,
|
||||
assume Hkm : k + km = m,
|
||||
have H : k + (mn + km) = n, from
|
||||
|
|
@ -444,7 +446,9 @@ theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
|
|||
|
||||
theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
|
||||
have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
|
||||
from (!add.comm ▸ !add.left_comm ▸ !add.assoc) ⬝ !add.assoc⁻¹,
|
||||
begin rewrite [add.comm (k - m) (m - n),
|
||||
{n - m + _ + _}add.assoc,
|
||||
{m - k + _}add.left_comm, -add.assoc] end,
|
||||
this ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
|
||||
|
||||
theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
|
||||
|
|
@ -457,7 +461,7 @@ assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl,
|
|||
by rewrite [this, this n m, mul.right_distrib, *mul_sub_right_distrib]
|
||||
|
||||
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
|
||||
!mul.comm ▸ !mul.comm ▸ !dist_mul_right ⬝ !mul.comm
|
||||
begin rewrite [mul.comm k n, mul.comm k m, dist_mul_right, mul.comm] end
|
||||
|
||||
theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
|
||||
have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ namespace quotient
|
|||
theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a)
|
||||
: Π (v w : A × A), map_pair2 f v w = map_pair2 f w v
|
||||
| (pair v₁ v₂) (pair w₁ w₂) :=
|
||||
!map_pair2_pair ⬝ by rewrite [Hcomm v₁ w₁, Hcomm v₂ w₂] ⬝ !map_pair2_pair⁻¹
|
||||
!map_pair2_pair ⬝ by rewrite [Hcomm v₁ w₁, Hcomm v₂ w₂] ⬝ (eq.symm !map_pair2_pair)
|
||||
|
||||
theorem map_pair2_assoc {A : Type} {f : A → A → A}
|
||||
(Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) :
|
||||
|
|
|
|||
|
|
@ -6,7 +6,8 @@ Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
|||
Sigma types, aka dependent sum.
|
||||
-/
|
||||
import logic.cast
|
||||
open inhabited eq.ops sigma.ops
|
||||
open inhabited sigma.ops
|
||||
override eq.ops
|
||||
|
||||
namespace sigma
|
||||
universe variables u v
|
||||
|
|
|
|||
|
|
@ -16,29 +16,30 @@ namespace nat
|
|||
| refl : le a a
|
||||
| step : Π {b}, le a b → le a (succ b)
|
||||
|
||||
infix ≤ := le
|
||||
attribute le.refl [refl]
|
||||
definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
|
||||
|
||||
definition lt [reducible] (n m : ℕ) := succ n ≤ m
|
||||
definition ge [reducible] (n m : ℕ) := m ≤ n
|
||||
definition gt [reducible] (n m : ℕ) := succ m ≤ n
|
||||
infix < := lt
|
||||
infix ≥ := ge
|
||||
infix > := gt
|
||||
lemma le_refl [refl] : ∀ a : nat, a ≤ a :=
|
||||
le.refl
|
||||
|
||||
protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
|
||||
definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
|
||||
|
||||
definition pred [unfold 1] (a : nat) : nat :=
|
||||
nat.cases_on a zero (λ a₁, a₁)
|
||||
|
||||
-- add is defined in init.num
|
||||
|
||||
definition sub (a b : nat) : nat :=
|
||||
protected definition sub (a b : nat) : nat :=
|
||||
nat.rec_on b a (λ b₁, pred)
|
||||
|
||||
definition mul (a b : nat) : nat :=
|
||||
protected definition mul (a b : nat) : nat :=
|
||||
nat.rec_on b zero (λ b₁ r, r + a)
|
||||
|
||||
notation a - b := sub a b
|
||||
notation a * b := mul a b
|
||||
definition nat_has_sub [instance] [reducible] [priority nat.prio] : has_sub nat :=
|
||||
has_sub.mk nat.sub
|
||||
|
||||
definition nat_has_mul [instance] [reducible] [priority nat.prio] : has_mul nat :=
|
||||
has_mul.mk nat.mul
|
||||
|
||||
/- properties of ℕ -/
|
||||
|
||||
|
|
@ -182,15 +183,14 @@ namespace nat
|
|||
theorem lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b :=
|
||||
le_of_succ_le_succ
|
||||
|
||||
definition decidable_le [instance] : decidable_rel le :=
|
||||
definition decidable_le [instance] : ∀ a b : nat, decidable (a ≤ b) :=
|
||||
nat.rec (λm, (decidable.inl !zero_le))
|
||||
(λn IH m, !nat.cases_on (decidable.inr (not_succ_le_zero n))
|
||||
(λm, decidable.rec (λH, inl (succ_le_succ H))
|
||||
(λH, inr (λa, H (le_of_succ_le_succ a))) (IH m)))
|
||||
|
||||
definition decidable_lt [instance] : decidable_rel lt := _
|
||||
definition decidable_gt [instance] : decidable_rel gt := _
|
||||
definition decidable_ge [instance] : decidable_rel ge := _
|
||||
definition decidable_lt [instance] : ∀ a b : nat, decidable (a < b) :=
|
||||
λ a b, decidable_le (succ a) b
|
||||
|
||||
theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b :=
|
||||
nat.rec (inr !zero_le) (λn, or.rec
|
||||
|
|
@ -220,7 +220,7 @@ namespace nat
|
|||
theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h
|
||||
|
||||
theorem succ_sub_succ_eq_sub [simp] (a b : ℕ) : succ a - succ b = a - b :=
|
||||
nat.rec rfl (λ b, congr_arg pred) b
|
||||
nat.rec (by esimp) (λ b, congr_arg pred) b
|
||||
|
||||
theorem sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b :=
|
||||
eq.symm !succ_sub_succ_eq_sub
|
||||
|
|
@ -248,9 +248,3 @@ namespace nat
|
|||
theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true :=
|
||||
iff_true_intro !sub_lt_succ
|
||||
end nat
|
||||
|
||||
namespace nat_esimp
|
||||
open nat
|
||||
attribute add mul sub [unfold 2]
|
||||
attribute of_num [unfold 1]
|
||||
end nat_esimp
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
|
||||
prelude
|
||||
import init.logic init.bool
|
||||
import init.logic init.bool init.priority
|
||||
open bool
|
||||
|
||||
definition pos_num.is_inhabited [instance] : inhabited pos_num :=
|
||||
|
|
@ -117,11 +117,12 @@ end num
|
|||
-- the coercion from num to nat is defined here,
|
||||
-- so that it can already be used in init.tactic
|
||||
namespace nat
|
||||
protected definition prio := num.add std.priority.default 100
|
||||
|
||||
definition add (a b : nat) : nat :=
|
||||
protected definition add (a b : nat) : nat :=
|
||||
nat.rec_on b a (λ b₁ r, succ r)
|
||||
|
||||
notation a + b := add a b
|
||||
definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat := has_add.mk nat.add
|
||||
|
||||
definition of_num [coercion] (n : num) : nat :=
|
||||
num.rec zero
|
||||
|
|
|
|||
|
|
@ -12,12 +12,6 @@ notation A × B := prod A B
|
|||
notation `(` h `, ` t:(foldl `, ` (e r, prod.mk r e) h) `)` := t
|
||||
|
||||
namespace prod
|
||||
notation [parsing-only] A * B := prod A B
|
||||
namespace low_precedence_times
|
||||
reserve infixr [parsing-only] `*`:30 -- conflicts with notation for multiplication
|
||||
infixr `*` := prod
|
||||
end low_precedence_times
|
||||
|
||||
notation `pr₁` := pr1
|
||||
notation `pr₂` := pr2
|
||||
|
||||
|
|
|
|||
|
|
@ -95,3 +95,43 @@ reserve infix ` ⊇ `:50
|
|||
reserve infix ` ∣ `:50
|
||||
reserve infixl ` ++ `:65
|
||||
reserve infixr ` :: `:65
|
||||
|
||||
structure has_add [class] (A : Type) := (add : A → A → A)
|
||||
structure has_mul [class] (A : Type) := (mul : A → A → A)
|
||||
structure has_inv [class] (A : Type) := (inv : A → A)
|
||||
structure has_neg [class] (A : Type) := (neg : A → A)
|
||||
structure has_sub [class] (A : Type) := (sub : A → A → A)
|
||||
structure has_division [class] (A : Type) := (division : A → A → A)
|
||||
structure has_divides [class] (A : Type) := (divides : A → A → A)
|
||||
structure has_modulo [class] (A : Type) := (modulo : A → A → A)
|
||||
structure has_dvd [class] (A : Type) := (dvd : A → A → Prop)
|
||||
structure has_le [class] (A : Type) := (le : A → A → Prop)
|
||||
structure has_lt [class] (A : Type) := (lt : A → A → Prop)
|
||||
|
||||
definition add {A : Type} [s : has_add A] : A → A → A := has_add.add
|
||||
definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul
|
||||
definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub
|
||||
definition division {A : Type} [s : has_division A] : A → A → A := has_division.division
|
||||
definition divides {A : Type} [s : has_divides A] : A → A → A := has_divides.divides
|
||||
definition modulo {A : Type} [s : has_modulo A] : A → A → A := has_modulo.modulo
|
||||
definition dvd {A : Type} [s : has_dvd A] : A → A → Prop := has_dvd.dvd
|
||||
definition neg {A : Type} [s : has_neg A] : A → A := has_neg.neg
|
||||
definition inv {A : Type} [s : has_inv A] : A → A := has_inv.inv
|
||||
definition le {A : Type} [s : has_le A] : A → A → Prop := has_le.le
|
||||
definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt
|
||||
definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a
|
||||
definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a
|
||||
|
||||
infix + := add
|
||||
infix * := mul
|
||||
infix - := sub
|
||||
infix / := division
|
||||
infix div := divides
|
||||
infix ∣ := dvd
|
||||
infix mod := modulo
|
||||
prefix - := neg
|
||||
postfix ⁻¹ := inv
|
||||
infix ≤ := le
|
||||
infix ≥ := ge
|
||||
infix < := lt
|
||||
infix > := gt
|
||||
|
|
|
|||
|
|
@ -131,8 +131,8 @@ section
|
|||
definition accessible {z} (ac: acc R z) : acc R⁺ z :=
|
||||
begin
|
||||
induction ac with x acx ih,
|
||||
constructor, intro y lt,
|
||||
induction lt with a b rab a b c rab rbc ih₁ ih₂,
|
||||
constructor, intro y rel,
|
||||
induction rel with a b rab a b c rab rbc ih₁ ih₂,
|
||||
{exact ih a rab},
|
||||
{exact acc.inv (ih₂ acx ih) rab}
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1551,10 +1551,10 @@ expr parser::parse_numeral_expr(bool user_notation) {
|
|||
"(solution: use 'import data.num', or define notation for the given numeral)", p);
|
||||
}
|
||||
buffer<expr> cs;
|
||||
if (*m_has_num)
|
||||
cs.push_back(save_pos(copy(from_num(n)), p));
|
||||
for (expr const & c : vals)
|
||||
cs.push_back(copy_with_new_pos(c, p));
|
||||
if (*m_has_num)
|
||||
cs.push_back(save_pos(copy(from_num(n)), p));
|
||||
// Remark: choices are processed from right to left.
|
||||
// We want to process user provided notation before the default 'num'.
|
||||
lean_assert(!cs.empty());
|
||||
|
|
|
|||
Loading…
Reference in a new issue