refactor(library/data/nat/order): make nat order an instance of linear_ordered_semigroup, rename various theorems
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
7b9758ac14
commit
50f03c5a09
12 changed files with 418 additions and 490 deletions
|
|
@ -211,7 +211,7 @@ section group
|
|||
... = a * 1 : mul.right_inv
|
||||
... = a : mul_one
|
||||
|
||||
theorem inv_mul_eq (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
|
||||
theorem inv_mul (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
|
||||
inv_eq_of_mul_eq_one
|
||||
(calc
|
||||
a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul.assoc
|
||||
|
|
@ -346,7 +346,7 @@ section add_group
|
|||
... = a + 0 : add.right_inv
|
||||
... = a : add_zero
|
||||
|
||||
theorem neg_add_eq (a b : A) : -(a + b) = -b + -a :=
|
||||
theorem neg_add (a b : A) : -(a + b) = -b + -a :=
|
||||
neg_eq_of_add_eq_zero
|
||||
(calc
|
||||
a + b + (-b + -a) = a + (b + (-b + -a)) : add.assoc
|
||||
|
|
@ -425,24 +425,24 @@ section add_group
|
|||
theorem eq_iff_sub_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
|
||||
iff.intro (assume H, H ▸ !sub_self) (assume H, eq_of_sub_eq_zero H)
|
||||
|
||||
theorem zero_sub_eq (a : A) : 0 - a = -a := !zero_add
|
||||
theorem zero_sub (a : A) : 0 - a = -a := !zero_add
|
||||
|
||||
theorem sub_zero_eq (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
|
||||
theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
|
||||
|
||||
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 :=
|
||||
theorem neg_sub (a b : A) : -(a - b) = b - a :=
|
||||
neg_eq_of_add_eq_zero
|
||||
(calc
|
||||
a - b + (b - a) = a - b + b - a : !add.assoc⁻¹
|
||||
... = a - a : sub_add_cancel
|
||||
... = 0 : sub_self)
|
||||
|
||||
theorem add_sub_eq (a b c : A) : a + (b - c) = a + b - c := !add.assoc⁻¹
|
||||
theorem add_sub (a b c : A) : a + (b - c) = a + b - c := !add.assoc⁻¹
|
||||
|
||||
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_eq
|
||||
a - (b + c) = a + (-c - b) : neg_add
|
||||
... = a - c - b : !add.assoc⁻¹
|
||||
|
||||
theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
|
||||
|
|
@ -471,11 +471,11 @@ include s
|
|||
|
||||
theorem neg_add_eq_sub (a b : A) : -a + b = b - a := !add.comm
|
||||
|
||||
theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add_eq a b
|
||||
theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add a b
|
||||
|
||||
theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add.right_comm
|
||||
|
||||
theorem sub_sub_eq (a b c : A) : a - b - c = a - (b + c) :=
|
||||
theorem sub_sub (a b c : A) : a - b - c = a - (b + c) :=
|
||||
calc
|
||||
a - b - c = a + (-b + -c) : add.assoc
|
||||
... = a + -(b + c) : {(neg_add_distrib b c)⁻¹}
|
||||
|
|
|
|||
|
|
@ -293,14 +293,23 @@ section
|
|||
(assume H1 : a = b, or.inl (H1 ▸ !le.refl))
|
||||
(assume H1 : b < a, or.inr (le_of_lt H1)))
|
||||
|
||||
definition le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=
|
||||
theorem le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=
|
||||
lt.by_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
|
||||
|
||||
definition lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
|
||||
theorem lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
|
||||
lt.by_cases
|
||||
(assume H', absurd (le_of_lt H') H)
|
||||
(assume H', absurd (H' ▸ !le.refl) H)
|
||||
(assume H', H')
|
||||
|
||||
theorem lt_or_ge (a b : A) : a < b ∨ a ≥ b :=
|
||||
lt.by_cases
|
||||
(assume H1 : a < b, or.inl H1)
|
||||
(assume H1 : a = b, or.inr (H1 ▸ le.refl a))
|
||||
(assume H1 : a > b, or.inr (le_of_lt H1))
|
||||
|
||||
theorem le_or_gt (a b : A) : a ≤ b ∨ a > b :=
|
||||
!or.swap (lt_or_ge b a)
|
||||
end
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ namespace fin
|
|||
... < n+1 : succ_pos n,
|
||||
to_nat_lt (@fs n f) := calc
|
||||
to_nat (fs f) = (to_nat f)+1 : rfl
|
||||
... < n+1 : succ_lt (to_nat_lt f)
|
||||
... < n+1 : succ_lt_succ (to_nat_lt f)
|
||||
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n),
|
||||
@lift ⌞n+1⌟ (fz n) m := fz (m + n),
|
||||
|
|
|
|||
|
|
@ -175,11 +175,11 @@ 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) :=
|
||||
or.elim (@le_or_gt (pr2 p) (pr1 p))
|
||||
(assume H1: pr1 p ≥ pr2 p,
|
||||
have H2 : pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_right H1 (pr2 q),
|
||||
or.inl (and.intro H1 (add_le_cancel_left H2)))
|
||||
have H2 : pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_add_right H1 (pr2 q),
|
||||
or.inl (and.intro H1 (le_of_add_le_add_left H2)))
|
||||
(assume H1: pr1 p < pr2 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)))
|
||||
have H2 : pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right H1 (pr2 q),
|
||||
or.inr (and.intro H1 (lt_of_add_lt_add_left H2)))
|
||||
|
||||
theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl
|
||||
|
||||
|
|
@ -222,7 +222,7 @@ or.elim (@le_or_gt n m)
|
|||
H1⁻¹ ▸
|
||||
(calc
|
||||
0 + n = n : zero_add
|
||||
... = n - m + m : add_sub_ge_left (lt_imp_le H)
|
||||
... = n - m + m : add_sub_ge_left (le.of_lt H)
|
||||
... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_gt H))⁻¹))
|
||||
|
||||
theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p :=
|
||||
|
|
@ -251,7 +251,7 @@ or.elim (equiv_cases Hequiv)
|
|||
calc
|
||||
pr2 p = pr2 p + pr1 q - pr1 q : sub_add_left
|
||||
... = pr1 p + pr2 q - pr1 q : Hequiv
|
||||
... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (lt_imp_le H4)
|
||||
... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le.of_lt H4)
|
||||
... = pr2 q - pr1 q + pr1 p : add.comm,
|
||||
have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from
|
||||
calc
|
||||
|
|
@ -290,7 +290,7 @@ or.elim (@le_or_gt n m)
|
|||
nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H
|
||||
... = succ (pred (n - m)) : rfl
|
||||
... = n - m : succ_pred_of_pos (sub_pos_of_gt H)
|
||||
... = dist m n : dist_le (lt_imp_le H))
|
||||
... = dist m n : dist_le (le.of_lt H))
|
||||
|
||||
theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) :=
|
||||
cases_on a
|
||||
|
|
@ -629,7 +629,7 @@ section port_algebra
|
|||
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 neg_add : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add
|
||||
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 :=
|
||||
|
|
@ -657,11 +657,11 @@ section port_algebra
|
|||
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
|
||||
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 zero_sub : ∀a : ℤ, 0 - a = -a := algebra.zero_sub
|
||||
theorem sub_zero : ∀a : ℤ, a - 0 = a := algebra.sub_zero
|
||||
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 neg_sub : ∀a b : ℤ, -(a - b) = b - a := algebra.neg_sub
|
||||
theorem add_sub : ∀a b c : ℤ, a + (b - c) = a + b - c := algebra.add_sub
|
||||
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
|
||||
|
|
@ -672,7 +672,7 @@ section port_algebra
|
|||
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 sub_sub_ : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub
|
||||
theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b :=
|
||||
algebra.add_sub_add_left_eq_sub
|
||||
theorem ne_zero_of_mul_ne_zero_right : ∀{a b : ℤ}, a * b ≠ 0 → a ≠ 0 :=
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
|
|||
or.elim (nonneg_or_nonneg_neg (b - a))
|
||||
(assume H, or.inl H)
|
||||
(assume H : nonneg (-(b - a)),
|
||||
have H0 : -(b - a) = a - b, from neg_sub_eq b a,
|
||||
have H0 : -(b - a) = a - b, from neg_sub b a,
|
||||
have H1 : nonneg (a - b), from H0 ▸ H, -- too bad: can't do it in one step
|
||||
or.inr H1)
|
||||
|
||||
|
|
@ -59,9 +59,9 @@ iff.intro
|
|||
(assume H : of_nat n ≤ of_nat m,
|
||||
obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le.elim H,
|
||||
have H2 : n + k = m, from of_nat_inj ((add_of_nat n k)⁻¹ ⬝ Hk),
|
||||
nat.le_intro H2)
|
||||
nat.le.intro H2)
|
||||
(assume H : n ≤ m,
|
||||
obtain (k : ℕ) (Hk : n + k = m), from nat.le_elim H,
|
||||
obtain (k : ℕ) (Hk : n + k = m), from nat.le.elim H,
|
||||
have H2 : of_nat n + of_nat k = of_nat m, from Hk ▸ add_of_nat n k,
|
||||
le.intro H2)
|
||||
|
||||
|
|
@ -252,8 +252,10 @@ section port_algebra
|
|||
theorem lt.trichotomy : ∀a b : ℤ, a < b ∨ a = b ∨ b < a := algebra.lt.trichotomy
|
||||
theorem lt.by_cases : ∀{a b : ℤ} {P : Prop}, (a < b → P) → (a = b → P) → (b < a → P) → P :=
|
||||
@algebra.lt.by_cases _ _
|
||||
definition le_of_not_lt : ∀{a b : ℤ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
|
||||
definition lt_of_not_le : ∀{a b : ℤ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
|
||||
theorem le_of_not_lt : ∀{a b : ℤ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
|
||||
theorem lt_of_not_le : ∀{a b : ℤ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
|
||||
theorem lt_or_ge : ∀a b : ℤ, a < b ∨ a ≥ b := @algebra.lt_or_ge _ _
|
||||
theorem le_or_gt : ∀a b : ℤ, a ≤ b ∨ a > b := @algebra.le_or_gt _ _
|
||||
|
||||
theorem add_le_add_right : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, a + c ≤ b + c :=
|
||||
@algebra.add_le_add_right _ _
|
||||
|
|
@ -421,8 +423,8 @@ section port_algebra
|
|||
@algebra.mul_neg_of_pos_of_neg _ _
|
||||
theorem mul_neg_of_neg_of_pos : ∀{a b : ℤ}, a < 0 → b > 0 → a * b < 0 :=
|
||||
@algebra.mul_neg_of_neg_of_pos _ _
|
||||
theorem lt_of_mul_lt_mul_left : ∀{a b c : ℤ}, c * a < c * b → c ≥ zero → a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_left int _
|
||||
theorem lt_of_mul_lt_mul_left : ∀{a b c : ℤ}, c * a < c * b → c ≥ 0 → a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_left _ _
|
||||
theorem lt_of_mul_lt_mul_right : ∀{a b c : ℤ}, a * c < b * c → c ≥ 0 → a < b :=
|
||||
@algebra.lt_of_mul_lt_mul_right _ _
|
||||
theorem le_of_mul_le_mul_left : ∀{a b c : ℤ}, c * a ≤ c * b → c > 0 → a ≤ b :=
|
||||
|
|
|
|||
|
|
@ -294,8 +294,8 @@ section
|
|||
|
||||
protected definition comm_semiring [instance] : algebra.comm_semiring nat :=
|
||||
algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
|
||||
mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
|
||||
zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
|
||||
mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
|
||||
zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
|
||||
end
|
||||
|
||||
section port_algebra
|
||||
|
|
|
|||
|
|
@ -5,8 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Module: data.nat.div
|
||||
Authors: Jeremy Avigad, Leonardo de Moura
|
||||
|
||||
This is a continuation of the development of the natural numbers, with a general way of
|
||||
defining recursive functions, and definitions of div, mod, and gcd.
|
||||
Definitions of div, mod, and gcd on the natural numbers.
|
||||
-/
|
||||
|
||||
import data.nat.sub logic
|
||||
|
|
@ -38,7 +37,7 @@ theorem div_zero (a : ℕ) : a div 0 = 0 :=
|
|||
divide_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
|
||||
|
||||
theorem div_less {a b : ℕ} (h : a < b) : a div b = 0 :=
|
||||
divide_def a b ⬝ if_neg (!not_and_of_not_right (lt_imp_not_ge h))
|
||||
divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
|
||||
|
||||
theorem zero_div (b : ℕ) : 0 div b = 0 :=
|
||||
divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt.of_lt_of_le l r) (lt.irrefl 0)))
|
||||
|
|
@ -78,7 +77,7 @@ theorem mod_zero (a : ℕ) : a mod 0 = a :=
|
|||
modulo_def a 0 ⬝ if_neg (!not_and_of_not_left (lt.irrefl 0))
|
||||
|
||||
theorem mod_less {a b : ℕ} (h : a < b) : a mod b = a :=
|
||||
modulo_def a b ⬝ if_neg (!not_and_of_not_right (lt_imp_not_ge h))
|
||||
modulo_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
|
||||
|
||||
theorem zero_mod (b : ℕ) : 0 mod b = 0 :=
|
||||
modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt.of_lt_of_le l r) (lt.irrefl 0)))
|
||||
|
|
@ -105,7 +104,7 @@ induction_on y
|
|||
... = x mod z : IH)
|
||||
|
||||
theorem mod_mul_self_right {m n : ℕ} : (m * n) mod n = 0 :=
|
||||
case_zero_pos n (by simp)
|
||||
by_cases_zero_pos n (by simp)
|
||||
(take n,
|
||||
assume npos : n > 0,
|
||||
(by simp) ▸ (@mod_add_mul_self_right 0 m _ npos))
|
||||
|
|
@ -130,14 +129,14 @@ case_strong_induction_on x
|
|||
have H2 : succ x mod y = succ x, from mod_less H1,
|
||||
show succ x mod y < y, from H2⁻¹ ▸ H1)
|
||||
(assume H1 : ¬ succ x < y,
|
||||
have H2 : y ≤ succ x, from not_lt_imp_ge H1,
|
||||
have H2 : y ≤ succ x, from le_of_not_lt H1,
|
||||
have H3 : succ x mod y = (succ x - y) mod y, from mod_rec H H2,
|
||||
have H4 : succ x - y < succ x, from sub_lt !succ_pos H,
|
||||
have H5 : succ x - y ≤ x, from lt_succ_imp_le H4,
|
||||
have H5 : succ x - y ≤ x, from le_of_lt_succ H4,
|
||||
show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
|
||||
|
||||
theorem div_mod_eq {x y : ℕ} : x = x div y * y + x mod y :=
|
||||
case_zero_pos y
|
||||
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
|
||||
|
|
@ -157,11 +156,11 @@ case_zero_pos y
|
|||
have H3 : succ x mod y = succ x, from mod_less H1,
|
||||
by simp)
|
||||
(assume H1 : ¬ succ x < y,
|
||||
have H2 : y ≤ succ x, from not_lt_imp_ge H1,
|
||||
have H2 : y ≤ succ x, from le_of_not_lt H1,
|
||||
have H3 : succ x div y = succ ((succ x - y) div y), from div_rec H H2,
|
||||
have H4 : succ x mod y = (succ x - y) mod y, from mod_rec H H2,
|
||||
have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
|
||||
have H6 : succ x - y ≤ x, from lt_succ_imp_le H5,
|
||||
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
|
||||
|
|
@ -189,16 +188,16 @@ theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y)
|
|||
have H4 : q1 * y + r2 = q2 * y + r2, from (remainder_unique H H1 H2 H3) ▸ H3,
|
||||
have H5 : q1 * y = q2 * y, from add.cancel_right H4,
|
||||
have H6 : y > 0, from lt.of_le_of_lt !zero_le H1,
|
||||
show q1 = q2, from mul_cancel_right H6 H5
|
||||
show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
|
||||
|
||||
theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
by_cases -- (y = 0)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume H : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_imp_pos H,
|
||||
have ypos : y > 0, from pos_of_ne_zero H,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos,
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_left zpos (mod_lt ypos),
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
|
||||
quotient_unique zypos H1 H2
|
||||
(calc
|
||||
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq
|
||||
|
|
@ -212,10 +211,10 @@ theorem mod_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) mod (z * y) = z * (x
|
|||
by_cases -- (y = 0)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume H : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_imp_pos H,
|
||||
have ypos : y > 0, from pos_of_ne_zero H,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
have H1 : (z * x) mod (z * y) < z * y, from mod_lt zypos,
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_left zpos (mod_lt ypos),
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (mod_lt ypos) zpos,
|
||||
remainder_unique zypos H1 H2
|
||||
(calc
|
||||
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq
|
||||
|
|
@ -225,7 +224,7 @@ by_cases -- (y = 0)
|
|||
|
||||
theorem mod_one (x : ℕ) : x mod 1 = 0 :=
|
||||
have H1 : x mod 1 < 1, from mod_lt !succ_pos,
|
||||
le_zero (lt_succ_imp_le H1)
|
||||
eq_zero_of_le_zero (le_of_lt_succ H1)
|
||||
|
||||
-- add_rewrite mod_one
|
||||
|
||||
|
|
@ -289,11 +288,11 @@ show x mod y = 0, from
|
|||
... = x : mod_zero
|
||||
... = 0 : xz)
|
||||
(assume ynz : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_imp_pos ynz,
|
||||
have ypos : y > 0, from pos_of_ne_zero ynz,
|
||||
have H3 : (z - x div y) * y < y, from H2⁻¹ ▸ mod_lt ypos,
|
||||
have H4 : (z - x div y) * y < 1 * y, from !one_mul⁻¹ ▸ H3,
|
||||
have H5 : z - x div y < 1, from mul_lt_cancel_right H4,
|
||||
have H6 : z - x div y = 0, from le_zero (lt_succ_imp_le H5),
|
||||
have H5 : z - x div y < 1, from lt_of_mul_lt_mul_right H4,
|
||||
have H6 : z - x div y = 0, from eq_zero_of_le_zero (le_of_lt_succ H5),
|
||||
calc
|
||||
x mod y = (z - x div y) * y : H2
|
||||
... = 0 * y : H6
|
||||
|
|
@ -318,7 +317,7 @@ theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x :=
|
|||
mod_eq_zero_imp_div_mul_eq (mod_eq_zero_of_dvd H)
|
||||
|
||||
theorem dvd_of_dvd_add_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n2 :=
|
||||
case_zero_pos m
|
||||
by_cases_zero_pos m
|
||||
(assume (H1 : 0 | n1 + n2) (H2 : 0 | n1),
|
||||
have H3 : n1 + n2 = 0, from eq_zero_of_zero_dvd H1,
|
||||
have H4 : n1 = 0, from eq_zero_of_zero_dvd H2,
|
||||
|
|
@ -352,7 +351,7 @@ by_cases
|
|||
have H4 : n1 = n1 - n2 + n2, from (add_sub_ge_left H3)⁻¹,
|
||||
show m | n1 - n2, from dvd_add_cancel_right (H4 ▸ H1) H2)
|
||||
(assume H3 : ¬ (n1 ≥ n2),
|
||||
have H4 : n1 - n2 = 0, from le_imp_sub_eq_zero (lt_imp_le (not_le_imp_gt H3)),
|
||||
have H4 : n1 - n2 = 0, from le_imp_sub_eq_zero (le.of_lt (lt_of_not_le H3)),
|
||||
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _)
|
||||
|
||||
-- Gcd and lcm
|
||||
|
|
@ -395,7 +394,7 @@ cases_on y
|
|||
... = if succ y₁ = 0 then x else gcd (succ y₁) (x mod succ y₁) : (if_neg (succ_ne_zero y₁))⁻¹)
|
||||
|
||||
theorem gcd_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
|
||||
gcd_def m n ⬝ if_neg (pos_imp_ne_zero H)
|
||||
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
|
||||
|
||||
theorem gcd_self (n : ℕ) : gcd n n = n :=
|
||||
cases_on n
|
||||
|
|
|
|||
|
|
@ -1,40 +1,66 @@
|
|||
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Floris van Doorn, Leonardo de Moura
|
||||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
-- data.nat.order
|
||||
-- ==============
|
||||
--
|
||||
-- The ordering on the natural numbers
|
||||
Module: data.nat.order
|
||||
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import .basic
|
||||
The order relation on the natural numbers.
|
||||
-/
|
||||
|
||||
import .basic algebra.ordered_ring
|
||||
open eq.ops
|
||||
|
||||
namespace nat
|
||||
|
||||
-- TODO: move this
|
||||
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
|
||||
iff.intro succ_le_of_lt lt_of_succ_le
|
||||
/- lt and le -/
|
||||
|
||||
-- Less than or equal
|
||||
-- ------------------
|
||||
theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
|
||||
or.elim H (take H1, le.of_lt H1) (take H1, H1 ▸ !le.refl)
|
||||
|
||||
theorem le.succ_right {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
|
||||
theorem lt.by_cases {a b : ℕ} {P : Prop}
|
||||
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
|
||||
or.elim !lt.trichotomy
|
||||
(assume H, H1 H)
|
||||
(assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
|
||||
|
||||
theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
|
||||
lt.by_cases
|
||||
(assume H1 : m < n, or.inl H1)
|
||||
(assume H1 : m = n, or.inr H1)
|
||||
(assume H1 : m > n, absurd (lt.of_le_of_lt H H1) !lt.irrefl)
|
||||
|
||||
theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n :=
|
||||
iff.intro lt_or_eq_of_le le_of_lt_or_eq
|
||||
|
||||
theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
|
||||
or.elim (lt_or_eq_of_le H1)
|
||||
(take H3 : m < n, H3)
|
||||
(take H3 : m = n, absurd H3 H2)
|
||||
|
||||
theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n :=
|
||||
iff.intro
|
||||
(take H, and.intro (le.of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
|
||||
(take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H))
|
||||
|
||||
theorem le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
|
||||
lt.step h
|
||||
|
||||
theorem le.add_right (n k : ℕ) : n ≤ n + k :=
|
||||
theorem le_add_right (n k : ℕ) : n ≤ n + k :=
|
||||
induction_on k
|
||||
(calc n ≤ n : le.refl n
|
||||
... = n + zero : add_zero)
|
||||
(λ k (ih : n ≤ n + k), calc
|
||||
n ≤ succ (n + k) : le.succ_right ih
|
||||
n ≤ succ (n + k) : le_succ_of_le ih
|
||||
... = n + succ k : add_succ)
|
||||
|
||||
theorem le_intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
|
||||
h ▸ le.add_right n k
|
||||
theorem le_add_left (n m : ℕ): n ≤ m + n :=
|
||||
!add.comm ▸ !le_add_right
|
||||
|
||||
theorem le_elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m :=
|
||||
theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
|
||||
h ▸ le_add_right n k
|
||||
|
||||
theorem le.elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m :=
|
||||
le.rec_on h
|
||||
(exists.intro 0 rfl)
|
||||
(λ m (h : n < m), lt.rec_on h
|
||||
|
|
@ -45,326 +71,279 @@ le.rec_on h
|
|||
n + succ k = succ (n + k) : add_succ
|
||||
... = succ b : h)))
|
||||
|
||||
-- ### partial order (totality is part of less than)
|
||||
theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
|
||||
lt.by_cases
|
||||
(assume H : m < n, or.inl (le.of_lt H))
|
||||
(assume H : m = n, or.inl (H ▸ !le.refl))
|
||||
(assume H : m > n, or.inr (le.of_lt H))
|
||||
|
||||
theorem le_refl (n : ℕ) : n ≤ n :=
|
||||
le.refl n
|
||||
/- addition -/
|
||||
|
||||
theorem zero_le (n : ℕ) : 0 ≤ n :=
|
||||
le_intro !zero_add
|
||||
|
||||
theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
|
||||
obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
|
||||
eq_zero_of_add_eq_zero_right Hk
|
||||
|
||||
theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 :=
|
||||
(assume H : succ n ≤ 0,
|
||||
have H2 : succ n = 0, from le_zero H,
|
||||
absurd H2 !succ_ne_zero)
|
||||
|
||||
theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
|
||||
le.trans H1 H2
|
||||
|
||||
theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from (le_elim H1),
|
||||
obtain (l : ℕ) (Hl : m + l = n), from (le_elim H2),
|
||||
have L1 : k + l = 0, from
|
||||
add.cancel_left
|
||||
(calc
|
||||
n + (k + l) = n + k + l : !add.assoc⁻¹
|
||||
... = m + l : {Hk}
|
||||
... = n : Hl
|
||||
... = n + 0 : !add_zero⁻¹),
|
||||
have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
|
||||
calc
|
||||
n = n + 0 : !add_zero⁻¹
|
||||
... = n + k : {L2⁻¹}
|
||||
... = m : Hk
|
||||
|
||||
-- ### interaction with addition
|
||||
|
||||
theorem le_add_right (n m : ℕ) : n ≤ n + m :=
|
||||
le_intro rfl
|
||||
|
||||
theorem le_add_left (n m : ℕ): n ≤ m + n :=
|
||||
le_intro !add.comm
|
||||
|
||||
theorem add_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
|
||||
le_intro
|
||||
theorem add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
|
||||
le.intro
|
||||
(calc
|
||||
k + n + l = k + (n + l) : !add.assoc
|
||||
... = k + m : {Hl})
|
||||
|
||||
theorem add_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
|
||||
!add.comm ▸ !add.comm ▸ add_le_left H k
|
||||
theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
|
||||
!add.comm ▸ !add.comm ▸ add_le_add_left H k
|
||||
|
||||
theorem add_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n + m ≤ k + l :=
|
||||
le_trans (add_le_right H1 m) (add_le_left H2 k)
|
||||
|
||||
|
||||
theorem add_le_cancel_left {n m k : ℕ} (H : k + n ≤ k + m) : n ≤ m :=
|
||||
obtain (l : ℕ) (Hl : k + n + l = k + m), from (le_elim H),
|
||||
le_intro (add.cancel_left
|
||||
theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m :=
|
||||
obtain (l : ℕ) (Hl : k + n + l = k + m), from (le.elim H),
|
||||
le.intro (add.cancel_left
|
||||
(calc
|
||||
k + (n + l) = k + n + l : !add.assoc⁻¹
|
||||
k + (n + l) = k + n + l : (!add.assoc)⁻¹
|
||||
... = k + m : Hl))
|
||||
|
||||
theorem add_le_cancel_right {n m k : ℕ} (H : n + k ≤ m + k) : n ≤ m :=
|
||||
add_le_cancel_left (!add.comm ▸ !add.comm ▸ H)
|
||||
theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
|
||||
lt_of_succ_le (!add_succ ▸ add_le_add_left (succ_le_of_lt H) k)
|
||||
|
||||
theorem add_le_inv {n m k l : ℕ} (H1 : n + m ≤ k + l) (H2 : k ≤ n) : m ≤ l :=
|
||||
obtain (a : ℕ) (Ha : k + a = n), from le_elim H2,
|
||||
have H3 : k + (a + m) ≤ k + l, from !add.assoc ▸ Ha⁻¹ ▸ H1,
|
||||
have H4 : a + m ≤ l, from add_le_cancel_left H3,
|
||||
show m ≤ l, from le_trans !le_add_left H4
|
||||
theorem add_lt_add_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
|
||||
!add.comm ▸ !add.comm ▸ add_lt_add_left H k
|
||||
|
||||
-- add_rewrite le_add_right le_add_left
|
||||
theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k :=
|
||||
!add_zero ▸ add_lt_add_left H n
|
||||
|
||||
-- ### interaction with successor and predecessor
|
||||
/- multiplication -/
|
||||
|
||||
theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
|
||||
!add_one ▸ !add_one ▸ add_le_right H 1
|
||||
|
||||
theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
|
||||
add_le_cancel_right (!add_one⁻¹ ▸ !add_one⁻¹ ▸ H)
|
||||
|
||||
theorem self_le_succ (n : ℕ) : n ≤ succ n :=
|
||||
le_intro !add_one
|
||||
|
||||
theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m :=
|
||||
le_trans H !self_le_succ
|
||||
|
||||
theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from (le_elim H),
|
||||
discriminate
|
||||
(assume H3 : k = 0,
|
||||
have Heq : n = m,
|
||||
from calc
|
||||
n = n + 0 : !add_zero⁻¹
|
||||
... = n + k : {H3⁻¹}
|
||||
... = m : Hk,
|
||||
or.inr Heq)
|
||||
(take l : nat,
|
||||
assume H3 : k = succ l,
|
||||
have Hlt : succ n ≤ m, from
|
||||
(le_intro
|
||||
(calc
|
||||
succ n + l = n + succ l : !succ_add_eq_add_succ
|
||||
... = n + k : {H3⁻¹}
|
||||
... = m : Hk)),
|
||||
or.inl Hlt)
|
||||
|
||||
theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m :=
|
||||
or_resolve_left (le_imp_succ_le_or_eq H1) H2
|
||||
|
||||
theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m :=
|
||||
or_of_or_of_imp_left (le_imp_succ_le_or_eq H)
|
||||
(take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2)
|
||||
|
||||
theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m :=
|
||||
obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H),
|
||||
and.intro
|
||||
(have H3 : n + succ k = m,
|
||||
from calc
|
||||
n + succ k = succ n + k : !succ_add_eq_add_succ⁻¹
|
||||
... = m : H2,
|
||||
show n ≤ m, from le_intro H3)
|
||||
(assume H3 : n = m,
|
||||
have H4 : succ n ≤ n, from H3⁻¹ ▸ H,
|
||||
have H5 : succ n = n, from le_antisym H4 !self_le_succ,
|
||||
show false, from absurd H5 succ.ne_self)
|
||||
|
||||
theorem le_pred_self (n : ℕ) : pred n ≤ n :=
|
||||
cases_on n
|
||||
(pred.zero⁻¹ ▸ !le_refl)
|
||||
(take k : ℕ, !pred.succ⁻¹ ▸ !self_le_succ)
|
||||
|
||||
theorem pred_le_pre_of_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
|
||||
discriminate
|
||||
(take Hn : n = 0,
|
||||
have H2 : pred n = 0,
|
||||
from calc
|
||||
pred n = pred 0 : {Hn}
|
||||
... = 0 : pred.zero,
|
||||
H2⁻¹ ▸ !zero_le)
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
have H2 : pred n + l = pred m,
|
||||
from calc
|
||||
pred n + l = pred (succ k) + l : {Hn}
|
||||
... = k + l : {!pred.succ}
|
||||
... = pred (succ (k + l)) : !pred.succ⁻¹
|
||||
... = pred (succ k + l) : {!add.succ_left⁻¹}
|
||||
... = pred (n + l) : {Hn⁻¹}
|
||||
... = pred m : {Hl},
|
||||
le_intro H2)
|
||||
|
||||
theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m :=
|
||||
discriminate
|
||||
(take Hn : n = 0,
|
||||
or.inl (Hn⁻¹ ▸ !zero_le))
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
have H2 : pred n = k,
|
||||
from calc
|
||||
pred n = pred (succ k) : {Hn}
|
||||
... = k : !pred.succ,
|
||||
have H3 : k ≤ m, from H2 ▸ H,
|
||||
have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3,
|
||||
show n ≤ m ∨ n = succ m, from
|
||||
or_of_or_of_imp_of_imp H4
|
||||
(take H5 : succ k ≤ m, show n ≤ m, from Hn⁻¹ ▸ H5)
|
||||
(take H5 : k = m, show n = succ m, from H5 ▸ Hn))
|
||||
|
||||
-- ### interaction with multiplication
|
||||
|
||||
theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
|
||||
theorem mul_le_mul_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
|
||||
have H2 : k * n + k * l = k * m, from
|
||||
calc
|
||||
k * n + k * l = k * (n + l) : mul.left_distrib
|
||||
... = k * m : {Hl},
|
||||
le_intro H2
|
||||
le.intro H2
|
||||
|
||||
theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ (mul_le_left H k)
|
||||
theorem mul_le_mul_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ (mul_le_mul_left H k)
|
||||
|
||||
theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
|
||||
le_trans (mul_le_right H1 m) (mul_le_left H2 k)
|
||||
theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
|
||||
le.trans (mul_le_mul_right H1 m) (mul_le_mul_left H2 k)
|
||||
|
||||
-- Less than, Greater than, Greater than or equal
|
||||
-- ----------------------------------------------
|
||||
theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m :=
|
||||
have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk,
|
||||
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left (succ_le_of_lt H) k,
|
||||
lt.of_lt_of_le H2 H3
|
||||
|
||||
theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
|
||||
|
||||
theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from (le.elim H1),
|
||||
obtain (l : ℕ) (Hl : m + l = n), from (le.elim H2),
|
||||
have L1 : k + l = 0, from
|
||||
add.cancel_left
|
||||
(calc
|
||||
n + (k + l) = n + k + l : (!add.assoc)⁻¹
|
||||
... = m + l : {Hk}
|
||||
... = n : Hl
|
||||
... = n + 0 : (!add_zero)⁻¹),
|
||||
have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
|
||||
calc
|
||||
n = n + 0 : (!add_zero)⁻¹
|
||||
... = n + k : {L2⁻¹}
|
||||
... = m : Hk
|
||||
|
||||
theorem zero_le (n : ℕ) : 0 ≤ n :=
|
||||
le.intro !zero_add
|
||||
|
||||
/- nat is an instance of a linearly ordered semiring -/
|
||||
|
||||
section
|
||||
open [classes] algebra
|
||||
|
||||
protected definition linear_ordered_semiring [instance] : algebra.linear_ordered_semiring nat :=
|
||||
algebra.linear_ordered_semiring.mk add add.assoc zero zero_add add_zero add.comm
|
||||
mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
|
||||
zero_mul mul_zero (ne.symm (succ_ne_zero zero)) @add.cancel_left @add.cancel_right le le.refl
|
||||
@le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left @le_of_add_le_add_left
|
||||
(take a b c H1 H2, mul_le_mul_left H1 c) (take a b c H1 H2, mul_le_mul_right H1 c)
|
||||
@mul_lt_mul_of_pos_left @mul_lt_mul_of_pos_right @le_iff_lt_or_eq @le.total
|
||||
end
|
||||
|
||||
section port_algebra
|
||||
theorem ne_of_lt : ∀{a b : ℕ}, a < b → a ≠ b := @algebra.ne_of_lt _ _
|
||||
theorem lt_of_le_of_ne : ∀{a b : ℕ}, a ≤ b → a ≠ b → a < b :=
|
||||
@algebra.lt_of_le_of_ne _ _
|
||||
|
||||
theorem not_le_of_lt : ∀{a b : ℕ}, a < b → ¬ b ≤ a := @algebra.not_le_of_lt _ _
|
||||
theorem not_lt_of_le : ∀{a b : ℕ}, a ≤ b → ¬ b < a := @algebra.not_lt_of_le _ _
|
||||
|
||||
theorem le_of_not_lt : ∀{a b : ℕ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
|
||||
theorem lt_of_not_le : ∀{a b : ℕ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
|
||||
theorem lt_or_ge : ∀a b : ℕ, a < b ∨ a ≥ b := @algebra.lt_or_ge _ _
|
||||
theorem le_or_gt : ∀a b : ℕ, a ≤ b ∨ a > b := @algebra.le_or_gt _ _
|
||||
|
||||
theorem add_le_add : ∀{a b c d : ℕ}, a ≤ b → c ≤ d → a + c ≤ b + d := @algebra.add_le_add _ _
|
||||
theorem add_lt_add : ∀{a b c d : ℕ}, a < b → c < d → a + c < b + d := @algebra.add_lt_add _ _
|
||||
theorem add_lt_add_of_le_of_lt : ∀{a b c d : ℕ}, a ≤ b → c < d → a + c < b + d :=
|
||||
@algebra.add_lt_add_of_le_of_lt _ _
|
||||
theorem add_lt_add_of_lt_of_le : ∀{a b c d : ℕ}, a < b → c ≤ d → a + c < b + d :=
|
||||
@algebra.add_lt_add_of_lt_of_le _ _
|
||||
theorem lt_add_of_pos_left : ∀{a b : ℕ}, b > 0 → a < b + a := @algebra.lt_add_of_pos_left _ _
|
||||
|
||||
theorem le_of_add_le_add_right : ∀{a b c : ℕ}, a + b ≤ c + b → a ≤ c :=
|
||||
@algebra.le_of_add_le_add_right _ _
|
||||
theorem lt_of_add_lt_add_left : ∀{a b c : ℕ}, a + b < a + c → b < c :=
|
||||
@algebra.lt_of_add_lt_add_left _ _
|
||||
theorem lt_of_add_lt_add_right : ∀{a b c : ℕ}, a + b < c + b → a < c :=
|
||||
@algebra.lt_of_add_lt_add_right _ _
|
||||
theorem add_le_add_left_iff : ∀a b c : ℕ, a + b ≤ a + c ↔ b ≤ c := algebra.add_le_add_left_iff
|
||||
theorem add_le_add_right_iff : ∀a b c : ℕ, a + b ≤ c + b ↔ a ≤ c := algebra.add_le_add_right_iff
|
||||
theorem add_lt_add_left_iff : ∀a b c : ℕ, a + b < a + c ↔ b < c := algebra.add_lt_add_left_iff
|
||||
theorem add_lt_add_right_iff : ∀a b c : ℕ, a + b < c + b ↔ a < c := algebra.add_lt_add_right_iff
|
||||
|
||||
theorem add_pos_left : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < a + b :=
|
||||
take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
|
||||
theorem add_pos_right : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < b + a :=
|
||||
take a H b, !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 :=
|
||||
take a b : ℕ,
|
||||
@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 : ℕ}, b ≤ c → b ≤ a + c :=
|
||||
take a b c H, @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
|
||||
theorem le_add_of_le_right : ∀{a b c : ℕ}, b ≤ c → b ≤ c + a :=
|
||||
take a b c H, @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
|
||||
theorem lt_add_of_pos_of_le : ∀{a b c : ℕ}, 0 < a → b ≤ c → b < a + c :=
|
||||
@algebra.lt_add_of_pos_of_le _ _
|
||||
theorem lt_add_of_le_of_pos : ∀{a b c : ℕ}, b ≤ c → 0 < a → b < c + a :=
|
||||
@algebra.lt_add_of_le_of_pos _ _
|
||||
|
||||
theorem lt_add_of_lt_left : ∀{b c : ℕ}, b < c → ∀a, b < a + c :=
|
||||
take b c H a, @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
|
||||
theorem lt_add_of_lt_right : ∀{b c : ℕ}, b < c → ∀a, b < c + a :=
|
||||
take b c H a, @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
|
||||
theorem lt_add_of_pos_of_lt : ∀{a b c : ℕ}, 0 < a → b < c → b < a + c :=
|
||||
@algebra.lt_add_of_pos_of_lt _ _
|
||||
theorem lt_add_of_lt_of_pos : ∀{a b c : ℕ}, b < c → 0 < a → b < c + a :=
|
||||
@algebra.lt_add_of_lt_of_pos _ _
|
||||
|
||||
theorem mul_pos : ∀{a b : ℕ}, 0 < a → 0 < b → 0 < a * b := @algebra.mul_pos _ _
|
||||
|
||||
theorem lt_of_mul_lt_mul_left : ∀{a b c : ℕ}, c * a < c * b → a < b :=
|
||||
take a b c H, @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
|
||||
theorem lt_of_mul_lt_mul_right : ∀{a b c : ℕ}, a * c < b * c → a < b :=
|
||||
take a b c H, @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
|
||||
theorem le_of_mul_le_mul_left : ∀{a b c : ℕ}, c * a ≤ c * b → c > 0 → a ≤ b :=
|
||||
@algebra.le_of_mul_le_mul_left _ _
|
||||
theorem le_of_mul_le_mul_right : ∀{a b c : ℕ}, a * c ≤ b * c → c > 0 → a ≤ b :=
|
||||
@algebra.le_of_mul_le_mul_right _ _
|
||||
theorem pos_of_mul_pos_left : ∀{a b : ℕ}, 0 < a * b → 0 < b :=
|
||||
take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le
|
||||
theorem pos_of_mul_pos_right : ∀{a b : ℕ}, 0 < a * b → 0 < a :=
|
||||
take a b H, @algebra.pos_of_mul_pos_right _ _ a b H !zero_le
|
||||
end port_algebra
|
||||
|
||||
theorem zero_le_one : 0 ≤ 1 := dec_trivial
|
||||
theorem zero_lt_one : 0 < 1 := dec_trivial
|
||||
|
||||
/- properties specific to nat -/
|
||||
|
||||
theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
|
||||
lt_of_succ_le (le_intro H)
|
||||
lt_of_succ_le (le.intro H)
|
||||
|
||||
theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
|
||||
le_elim (succ_le_of_lt H)
|
||||
theorem lt_elim {n m : ℕ} (H : n < m) : ∃k, succ n + k = m :=
|
||||
le.elim (succ_le_of_lt H)
|
||||
|
||||
theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
|
||||
lt_intro !succ_add_eq_add_succ
|
||||
|
||||
-- ### basic facts
|
||||
theorem eq_zero_of_le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
|
||||
obtain (k : ℕ) (Hk : n + k = 0), from le.elim H,
|
||||
eq_zero_of_add_eq_zero_right Hk
|
||||
|
||||
theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
|
||||
λ heq : n = m, absurd H (heq ▸ !lt.irrefl)
|
||||
/- succ and pred -/
|
||||
|
||||
theorem lt_irrefl (n : ℕ) : ¬ n < n :=
|
||||
(assume H : n < n, absurd rfl (lt_imp_ne H))
|
||||
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
|
||||
iff.intro succ_le_of_lt lt_of_succ_le
|
||||
|
||||
theorem lt_def (n m : ℕ) : n < m ↔ succ n ≤ m :=
|
||||
iff.intro
|
||||
(λ h, succ_le_of_lt h)
|
||||
(λ h, lt_of_succ_le h)
|
||||
theorem not_succ_le_zero (n : ℕ) : ¬ succ n ≤ 0 :=
|
||||
(assume H : succ n ≤ 0,
|
||||
have H2 : succ n = 0, from eq_zero_of_le_zero H,
|
||||
absurd H2 !succ_ne_zero)
|
||||
|
||||
theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
|
||||
!add_one ▸ !add_one ▸ add_le_add_right H 1
|
||||
|
||||
theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
|
||||
le_of_add_le_add_right ((!add_one)⁻¹ ▸ (!add_one)⁻¹ ▸ H)
|
||||
|
||||
theorem self_le_succ (n : ℕ) : n ≤ succ n :=
|
||||
le.intro !add_one
|
||||
|
||||
theorem succ_le_or_eq_of_le {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m :=
|
||||
or.elim (lt_or_eq_of_le H)
|
||||
(assume H1 : n < m, or.inl (succ_le_of_lt H1))
|
||||
(assume H1 : n = m, or.inr H1)
|
||||
|
||||
theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
|
||||
nat.cases_on n
|
||||
(assume H : pred 0 ≤ m, !zero_le)
|
||||
(take n',
|
||||
assume H : pred (succ n') ≤ m,
|
||||
have H1 : n' ≤ m, from pred.succ n' ▸ H,
|
||||
succ_le_succ H1)
|
||||
|
||||
theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m :=
|
||||
nat.cases_on n
|
||||
(assume H, !pred.zero⁻¹ ▸ zero_le m)
|
||||
(take n',
|
||||
assume H : succ n' ≤ succ m,
|
||||
have H1 : n' ≤ m, from le_of_succ_le_succ H,
|
||||
!pred.succ⁻¹ ▸ H1)
|
||||
|
||||
theorem succ_le_of_le_pred {n m : ℕ} : succ n ≤ m → n ≤ pred m :=
|
||||
nat.cases_on m
|
||||
(assume H, absurd H !not_succ_le_zero)
|
||||
(take m',
|
||||
assume H : succ n ≤ succ m',
|
||||
have H1 : n ≤ m', from le_of_succ_le_succ H,
|
||||
!pred.succ⁻¹ ▸ H1)
|
||||
|
||||
theorem pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
|
||||
nat.cases_on n
|
||||
(assume H, pred.zero⁻¹ ▸ zero_le (pred m))
|
||||
(take n',
|
||||
assume H : succ n' ≤ m,
|
||||
!pred.succ⁻¹ ▸ succ_le_of_le_pred H)
|
||||
|
||||
theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m :=
|
||||
or_of_or_of_imp_left (succ_le_or_eq_of_le H)
|
||||
(take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2)
|
||||
|
||||
theorem le_pred_self (n : ℕ) : pred n ≤ n :=
|
||||
cases_on n
|
||||
(pred.zero⁻¹ ▸ !le.refl)
|
||||
(take k : ℕ, (!pred.succ)⁻¹ ▸ !self_le_succ)
|
||||
|
||||
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 (eq_zero_or_eq_succ_pred n) (ne.symm (lt_imp_ne H))⁻¹)
|
||||
(or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))⁻¹
|
||||
|
||||
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
|
||||
theorem exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : exists k, m = succ k :=
|
||||
discriminate
|
||||
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
|
||||
(take (l : ℕ) (Hm : m = succ l), exists.intro l Hm)
|
||||
|
||||
-- ### interaction with le
|
||||
|
||||
theorem self_lt_succ (n : ℕ) : n < succ n :=
|
||||
lt.base n
|
||||
|
||||
theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
|
||||
le.of_lt H
|
||||
theorem le_of_lt_succ {n m : ℕ} (H : n < succ m) : n ≤ m :=
|
||||
le_of_succ_le_succ (succ_le_of_lt H)
|
||||
|
||||
theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m :=
|
||||
or.swap (eq_or_lt_of_le H)
|
||||
theorem succ_lt_succ {n m : ℕ} (H : n < m) : succ n < succ m :=
|
||||
!add_one ▸ !add_one ▸ add_lt_add_right H 1
|
||||
|
||||
theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m :=
|
||||
or_resolve_left (le_imp_lt_or_eq H1) H2
|
||||
/- other forms of induction -/
|
||||
|
||||
theorem lt_succ_imp_le {n m : ℕ} (H : n < succ m) : n ≤ m :=
|
||||
succ_le_cancel (succ_le_of_lt H)
|
||||
|
||||
theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
|
||||
le.rec_on H
|
||||
!lt.irrefl
|
||||
(λ m (h : n < m), lt.asymm h)
|
||||
|
||||
theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m :=
|
||||
(assume H2 : m ≤ n, absurd (lt.of_lt_of_le H H2) !lt_irrefl)
|
||||
|
||||
theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
|
||||
lt.asymm H
|
||||
|
||||
-- le_imp_not_gt (lt_imp_le H)
|
||||
|
||||
-- ### interaction with addition
|
||||
|
||||
theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
|
||||
lt_of_succ_le (!add_succ ▸ add_le_left (succ_le_of_lt H) k)
|
||||
|
||||
theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
|
||||
!add.comm ▸ !add.comm ▸ add_lt_left H k
|
||||
|
||||
theorem add_le_lt {n m k l : ℕ} (H1 : n ≤ k) (H2 : m < l) : n + m < k + l :=
|
||||
lt.of_le_of_lt (add_le_right H1 m) (add_lt_left H2 k)
|
||||
|
||||
theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l :=
|
||||
lt.of_lt_of_le (add_lt_right H1 m) (add_le_left H2 k)
|
||||
|
||||
theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l :=
|
||||
add_lt_le H1 (lt_imp_le H2)
|
||||
|
||||
theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m :=
|
||||
lt_of_succ_le (add_le_cancel_left (!add_succ⁻¹ ▸ (succ_le_of_lt H)))
|
||||
|
||||
theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m :=
|
||||
add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H)
|
||||
|
||||
-- ### interaction with successor (see also the interaction with le)
|
||||
|
||||
theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m :=
|
||||
!add_one ▸ !add_one ▸ add_lt_right H 1
|
||||
|
||||
theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) : n < m :=
|
||||
add_lt_cancel_right (!add_one⁻¹ ▸ !add_one⁻¹ ▸ H)
|
||||
|
||||
theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m :=
|
||||
lt.step H
|
||||
|
||||
-- ### totality of lt and le
|
||||
|
||||
theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m :=
|
||||
or.rec_on (lt.trichotomy n m)
|
||||
(λ h : n < m, or.inl (le.of_lt h))
|
||||
(λ h : n = m ∨ m < n, or.rec_on h
|
||||
(λ h : n = m, eq.rec_on h (or.inl !le.refl))
|
||||
(λ h : m < n, or.inr h))
|
||||
|
||||
theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m :=
|
||||
or.rec_on (lt.trichotomy n m)
|
||||
(λ h, or.inl (or.inl h))
|
||||
(λ h, or.rec_on h
|
||||
(λ h, or.inl (or.inr h))
|
||||
(λ h, or.inr h))
|
||||
|
||||
theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ n > m :=
|
||||
lt.trichotomy n m
|
||||
|
||||
theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n :=
|
||||
or_of_or_of_imp_right le_or_gt (assume H : m < n, lt_imp_le H)
|
||||
|
||||
theorem not_lt_imp_ge {n m : ℕ} (H : ¬ n < m) : n ≥ m :=
|
||||
or_resolve_left le_or_gt H
|
||||
|
||||
theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
|
||||
or_resolve_right le_or_gt H
|
||||
|
||||
-- ### misc
|
||||
|
||||
protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
|
||||
protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) :
|
||||
P n :=
|
||||
have H1 : ∀ {n m : nat}, m < n → P m, from
|
||||
take n,
|
||||
induction_on n
|
||||
|
|
@ -375,7 +354,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from
|
|||
show ∀m, m < succ n' → P m, from
|
||||
take m,
|
||||
assume H3 : m < succ n',
|
||||
or.elim (le_imp_lt_or_eq (lt_succ_imp_le H3))
|
||||
or.elim (lt_or_eq_of_le (le_of_lt_succ H3))
|
||||
(assume H4: m < n', IH H4)
|
||||
(assume H4: m = n', H4⁻¹ ▸ H2)),
|
||||
H1 !self_lt_succ
|
||||
|
|
@ -392,136 +371,70 @@ strong_induction_on a (
|
|||
show P (succ n), from
|
||||
Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
|
||||
|
||||
-- Positivity
|
||||
-- ---------
|
||||
--
|
||||
-- Writing "t > 0" is the preferred way to assert that a natural number is positive.
|
||||
/- pos -/
|
||||
|
||||
-- ### basic
|
||||
|
||||
theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
|
||||
theorem by_cases_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
|
||||
cases_on y H0 (take y, H1 !succ_pos)
|
||||
|
||||
theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 :=
|
||||
or_of_or_of_imp_left
|
||||
(or.swap (le_imp_lt_or_eq !zero_le))
|
||||
(or.swap (lt_or_eq_of_le !zero_le))
|
||||
(take H : 0 = n, H⁻¹)
|
||||
|
||||
theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
|
||||
H⁻¹ ▸ !succ_pos
|
||||
|
||||
theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
theorem pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
or.elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
|
||||
|
||||
theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
|
||||
ne.symm (lt_imp_ne H)
|
||||
theorem ne_zero_of_pos {n : ℕ} (H : n > 0) : n ≠ 0 :=
|
||||
ne.symm (ne_of_lt H)
|
||||
|
||||
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l :=
|
||||
lt_imp_eq_succ H
|
||||
theorem exists_eq_succ_of_pos {n : ℕ} (H : n > 0) : exists l, n = succ l :=
|
||||
exists_eq_succ_of_lt H
|
||||
|
||||
theorem add_pos_right {n k : ℕ} (H : k > 0) : n + k > n :=
|
||||
!add_zero ▸ add_lt_left H n
|
||||
/- multiplication -/
|
||||
|
||||
theorem add_pos_left {n : ℕ} {k : ℕ} (H : k > 0) : k + n > n :=
|
||||
!add.comm ▸ add_pos_right H
|
||||
theorem mul_lt_mul_of_le_of_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) :
|
||||
n * m < k * l :=
|
||||
lt.of_le_of_lt (mul_le_mul_right H1 m) (mul_lt_mul_of_pos_left H2 Hk)
|
||||
|
||||
-- ### multiplication
|
||||
theorem mul_lt_mul_of_lt_of_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) :
|
||||
n * m < k * l :=
|
||||
lt.of_le_of_lt (mul_le_mul_left H2 n) (mul_lt_mul_of_pos_right H1 Hl)
|
||||
|
||||
theorem mul_pos {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0 :=
|
||||
obtain (k : ℕ) (Hk : n = succ k), from pos_imp_eq_succ Hn,
|
||||
obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm,
|
||||
succ_imp_pos (calc
|
||||
n * m = succ k * m : {Hk}
|
||||
... = succ k * succ l : {Hl}
|
||||
... = succ k * l + succ k : !mul_succ
|
||||
... = succ (succ k * l + k) : !add_succ)
|
||||
|
||||
theorem mul_pos_imp_pos_left {n m : ℕ} (H : n * m > 0) : n > 0 :=
|
||||
discriminate
|
||||
(assume H2 : n = 0,
|
||||
have H3 : n * m = 0,
|
||||
from calc
|
||||
n * m = 0 * m : {H2}
|
||||
... = 0 : !zero_mul,
|
||||
have H4 : 0 > 0, from H3 ▸ H,
|
||||
absurd H4 !lt_irrefl)
|
||||
(take l : nat,
|
||||
assume Hl : n = succ l,
|
||||
Hl⁻¹ ▸ !succ_pos)
|
||||
|
||||
theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0 :=
|
||||
mul_pos_imp_pos_left (!mul.comm ▸ H)
|
||||
|
||||
-- ### interaction of mul with le and lt
|
||||
|
||||
theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m :=
|
||||
have H2 : k * n < k * n + k, from add_pos_right Hk,
|
||||
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_left (succ_le_of_lt H) k,
|
||||
lt.of_lt_of_le H2 H3
|
||||
|
||||
theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m) : n * k < m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ mul_lt_left Hk H
|
||||
|
||||
theorem mul_le_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l :=
|
||||
lt.of_le_of_lt (mul_le_right H1 m) (mul_lt_left Hk H2)
|
||||
|
||||
theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l :=
|
||||
lt.of_le_of_lt (mul_le_left H2 n) (mul_lt_right Hl H1)
|
||||
|
||||
theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
|
||||
have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
|
||||
have H4 : k * m < k * l, from mul_lt_left (lt.of_le_of_lt !zero_le H1) H2,
|
||||
theorem mul_lt_mul_of_le_of_le {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
|
||||
have H3 : n * m ≤ k * m, from mul_le_mul_right (le.of_lt H1) m,
|
||||
have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt.of_le_of_lt !zero_le H1),
|
||||
lt.of_le_of_lt H3 H4
|
||||
|
||||
theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
|
||||
or.elim le_or_gt
|
||||
(assume H2 : m ≤ n,
|
||||
have H3 : k * m ≤ k * n, from mul_le_left H2 k,
|
||||
absurd H3 (lt_imp_not_ge H))
|
||||
(assume H2 : n < m, H2)
|
||||
theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
|
||||
have H2 : n * m ≤ n * k, from H ▸ !le.refl,
|
||||
have H3 : n * k ≤ n * m, from H ▸ !le.refl,
|
||||
have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn,
|
||||
have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn,
|
||||
le.antisymm H4 H5
|
||||
|
||||
theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
|
||||
mul_lt_cancel_left (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m :=
|
||||
have H2 : k * n < k * m + k, from lt.of_le_of_lt H (add_pos_right Hk),
|
||||
have H3 : k * n < k * succ m, from !mul_succ⁻¹ ▸ H2,
|
||||
have H4 : n < succ m, from mul_lt_cancel_left H3,
|
||||
show n ≤ m, from lt_succ_imp_le H4
|
||||
|
||||
theorem mul_le_cancel_right {n k m : ℕ} (Hm : m > 0) (H : n * m ≤ k * m) : n ≤ k :=
|
||||
mul_le_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_cancel_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
|
||||
have H2 : n * m ≤ n * k, from H ▸ !le_refl,
|
||||
have H3 : n * k ≤ n * m, from H ▸ !le_refl,
|
||||
have H4 : m ≤ k, from mul_le_cancel_left Hn H2,
|
||||
have H5 : k ≤ m, from mul_le_cancel_left Hn H3,
|
||||
le_antisym H4 H5
|
||||
|
||||
theorem mul_cancel_left_or {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k :=
|
||||
theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k :=
|
||||
or_of_or_of_imp_right zero_or_pos
|
||||
(assume Hn : n > 0, mul_cancel_left Hn H)
|
||||
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
|
||||
|
||||
theorem mul_cancel_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
|
||||
mul_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H)
|
||||
theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
|
||||
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_cancel_right_or {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k :=
|
||||
mul_cancel_left_or (!mul.comm ▸ !mul.comm ▸ H)
|
||||
theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k :=
|
||||
eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 :=
|
||||
theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 :=
|
||||
have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos,
|
||||
have H3 : n > 0, from mul_pos_imp_pos_left H2,
|
||||
have H4 : m > 0, from mul_pos_imp_pos_right H2,
|
||||
or.elim le_or_gt
|
||||
have H3 : n > 0, from pos_of_mul_pos_right H2,
|
||||
have H4 : m > 0, from pos_of_mul_pos_left H2,
|
||||
or.elim (le_or_gt n 1)
|
||||
(assume H5 : n ≤ 1,
|
||||
show n = 1, from le_antisym H5 (succ_le_of_lt H3))
|
||||
show n = 1, from le.antisymm H5 (succ_le_of_lt H3))
|
||||
(assume H5 : n > 1,
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le (succ_le_of_lt H5) (succ_le_of_lt H4),
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt H4),
|
||||
have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
|
||||
absurd !self_lt_succ (le_imp_not_gt H7))
|
||||
absurd !self_lt_succ (not_lt_of_le H7))
|
||||
|
||||
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
|
||||
mul_eq_one_left (!mul.comm ▸ H)
|
||||
theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
|
||||
eq_one_of_mul_eq_one_left (!mul.comm ▸ H)
|
||||
|
||||
end nat
|
||||
|
|
|
|||
|
|
@ -167,17 +167,17 @@ sub_induction n m
|
|||
... = succ (k - 0) : {!sub_zero_right⁻¹})
|
||||
(take k,
|
||||
assume H : succ k ≤ 0,
|
||||
absurd H !not_succ_zero_le)
|
||||
absurd H !not_succ_le_zero)
|
||||
(take k l,
|
||||
assume IH : k ≤ l → succ l - k = succ (l - k),
|
||||
take H : succ k ≤ succ l,
|
||||
calc
|
||||
succ (succ l) - succ k = succ l - k : !sub_succ_succ
|
||||
... = succ (l - k) : IH (succ_le_cancel H)
|
||||
... = succ (l - k) : IH (le_of_succ_le_succ H)
|
||||
... = succ (succ l - succ k) : {!sub_succ_succ⁻¹})
|
||||
|
||||
theorem le_imp_sub_eq_zero {n m : ℕ} (H : n ≤ m) : n - m = 0 :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le_elim H, Hk ▸ !sub_add_right_eq_zero
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le.elim H, Hk ▸ !sub_add_right_eq_zero
|
||||
|
||||
theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m :=
|
||||
sub_induction n m
|
||||
|
|
@ -186,14 +186,14 @@ sub_induction n m
|
|||
calc
|
||||
0 + (k - 0) = k - 0 : !zero_add
|
||||
... = k : !sub_zero_right)
|
||||
(take k, assume H : succ k ≤ 0, absurd H !not_succ_zero_le)
|
||||
(take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
|
||||
(take k l,
|
||||
assume IH : k ≤ l → k + (l - k) = l,
|
||||
take H : succ k ≤ succ l,
|
||||
calc
|
||||
succ k + (succ l - succ k) = succ k + (l - k) : {!sub_succ_succ}
|
||||
... = succ (k + (l - k)) : !add.succ_left
|
||||
... = succ l : {IH (succ_le_cancel H)})
|
||||
... = succ l : {IH (le_of_succ_le_succ H)})
|
||||
|
||||
theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n :=
|
||||
!add.comm ▸ !add_sub_le
|
||||
|
|
@ -207,23 +207,23 @@ theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m :=
|
|||
!add.comm ▸ add_sub_ge
|
||||
|
||||
theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) :=
|
||||
or.elim !le_total
|
||||
or.elim !le.total
|
||||
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H)
|
||||
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ !le_refl)
|
||||
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ !le.refl)
|
||||
|
||||
theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n) :=
|
||||
or.elim !le_total
|
||||
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ !le_refl)
|
||||
or.elim !le.total
|
||||
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ !le.refl)
|
||||
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ H)
|
||||
|
||||
theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k)
|
||||
: P (n - m) :=
|
||||
or.elim !le_total
|
||||
or.elim !le.total
|
||||
(assume H3 : n ≤ m, (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 H3))
|
||||
(assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3))
|
||||
|
||||
theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le.elim H,
|
||||
exists.intro k
|
||||
(calc
|
||||
m - k = n + k - k : {Hk⁻¹}
|
||||
|
|
@ -237,14 +237,14 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
|
|||
calc
|
||||
n + m - 0 = n + m : !sub_zero_right
|
||||
... = n + (m - 0) : {!sub_zero_right⁻¹})
|
||||
(take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_zero_le)
|
||||
(take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
|
||||
(take k m,
|
||||
assume IH : k ≤ m → n + m - k = n + (m - k),
|
||||
take H : succ k ≤ succ m,
|
||||
calc
|
||||
n + succ m - succ k = succ (n + m) - succ k : {!add_succ}
|
||||
... = n + m - k : !sub_succ_succ
|
||||
... = n + (m - k) : IH (succ_le_cancel H)
|
||||
... = n + (m - k) : IH (le_of_succ_le_succ H)
|
||||
... = n + (succ m - succ k) : {!sub_succ_succ⁻¹}),
|
||||
l1 H
|
||||
|
||||
|
|
@ -255,11 +255,11 @@ sub_split
|
|||
assume H1 : m + k = n,
|
||||
assume H2 : k = 0,
|
||||
have H3 : n = m, from !add_zero ▸ H2 ▸ H1⁻¹,
|
||||
H3 ▸ !le_refl)
|
||||
H3 ▸ !le.refl)
|
||||
|
||||
theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
|
||||
(H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) :=
|
||||
or.elim !le_total
|
||||
or.elim !le.total
|
||||
(assume H3 : n ≤ m,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹)))
|
||||
(assume H3 : m ≤ n,
|
||||
|
|
@ -268,7 +268,7 @@ or.elim !le_total
|
|||
theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m :=
|
||||
have H2 : k - n + n = m + n, from
|
||||
calc
|
||||
k - n + n = k : add_sub_ge_left (le_intro H)
|
||||
k - n + n = k : add_sub_ge_left (le.intro H)
|
||||
... = n + m : H⁻¹
|
||||
... = m + n : !add.comm,
|
||||
add.cancel_right H2
|
||||
|
|
@ -277,8 +277,8 @@ theorem sub_lt {x y : ℕ} (xpos : x > 0) (ypos : y > 0) : x - y < x :=
|
|||
sub.lt xpos ypos
|
||||
|
||||
theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
or.elim !le_total
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
|
||||
or.elim !le.total
|
||||
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ !zero_le)
|
||||
(assume H2 : k ≤ n,
|
||||
have H3 : n - k + l = m - k, from
|
||||
|
|
@ -287,15 +287,15 @@ or.elim !le_total
|
|||
... = l + n - k : (add_sub_assoc H2 l)⁻¹
|
||||
... = n + l - k : {!add.comm}
|
||||
... = m - k : {Hl},
|
||||
le_intro H3)
|
||||
le.intro H3)
|
||||
|
||||
theorem sub_le_left {n m : ℕ} (H : n ≤ m) (k : nat) : k - m ≤ k - n :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
|
||||
sub_split
|
||||
(assume H2 : k ≤ m, !zero_le)
|
||||
(take m' : ℕ,
|
||||
assume Hm : m + m' = k,
|
||||
have H3 : n ≤ k, from le_trans H (le_intro Hm),
|
||||
have H3 : n ≤ k, from le.trans H (le.intro Hm),
|
||||
have H4 : m' + l + n = k - n + n, from
|
||||
calc
|
||||
m' + l + n = n + (m' + l) : add.comm
|
||||
|
|
@ -304,12 +304,12 @@ sub_split
|
|||
... = m + m' : {Hl}
|
||||
... = k : Hm
|
||||
... = k - n + n : (add_sub_ge_left H3)⁻¹,
|
||||
le_intro (add.cancel_right H4))
|
||||
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 H1 : n = n - m + m, from (add_sub_ge_left (le.of_lt H))⁻¹,
|
||||
have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H,
|
||||
!add_lt_cancel_right H2
|
||||
!lt_of_add_lt_add_right H2
|
||||
|
||||
-- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
|
||||
-- :=
|
||||
|
|
@ -338,7 +338,7 @@ sub_split
|
|||
... = m + mn : Hkm
|
||||
... = n : Hmn,
|
||||
have H2 : n - k = mn + km, from sub_intro H,
|
||||
H2 ▸ !le_refl))
|
||||
H2 ▸ !le.refl))
|
||||
|
||||
|
||||
-- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
|
||||
|
|
@ -367,7 +367,7 @@ have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
|
|||
have H3 : n ≤ m, from sub_eq_zero_imp_le H2,
|
||||
have H4 : m - n = 0, from eq_zero_of_add_eq_zero_left H,
|
||||
have H5 : m ≤ n, from sub_eq_zero_imp_le H4,
|
||||
le_antisym H3 H5
|
||||
le.antisymm H3 H5
|
||||
|
||||
theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
|
||||
calc
|
||||
|
|
@ -385,7 +385,7 @@ dist_le !zero_le ⬝ !sub_zero_right
|
|||
|
||||
theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m :=
|
||||
calc
|
||||
dist k n = k - n : dist_ge (le_intro H)
|
||||
dist k n = k - n : dist_ge (le.intro H)
|
||||
... = m : sub_intro H
|
||||
|
||||
theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
|
||||
|
|
@ -426,7 +426,7 @@ theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m)
|
|||
theorem triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
|
||||
have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
|
||||
by simp,
|
||||
H ▸ add_le !sub_triangle_inequality !sub_triangle_inequality
|
||||
H ▸ add_le_add !sub_triangle_inequality !sub_triangle_inequality
|
||||
|
||||
theorem dist_add_le_add_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
|
||||
have H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, from
|
||||
|
|
@ -450,17 +450,17 @@ theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m *
|
|||
have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
|
||||
take k l : ℕ,
|
||||
assume H : k ≥ l,
|
||||
have H2 : m * k ≥ m * l, from mul_le_left H m,
|
||||
have H3 : n * l + m * k ≥ m * l, from le_trans H2 !le_add_left,
|
||||
have H2 : m * k ≥ m * l, from mul_le_mul_left H m,
|
||||
have H3 : n * l + m * k ≥ m * l, from le.trans H2 !le_add_left,
|
||||
calc
|
||||
dist n m * dist k l = dist n m * (k - l) : {dist_ge H}
|
||||
... = dist (n * (k - l)) (m * (k - l)) : !dist_mul_right⁻¹
|
||||
... = dist (n * k - n * l) (m * k - m * l) : by simp
|
||||
... = dist (n * k) (m * k - m * l + n * l) : dist_sub_move_add (mul_le_left H n) _
|
||||
... = dist (n * k) (m * k - m * l + n * l) : dist_sub_move_add (mul_le_mul_left H n) _
|
||||
... = dist (n * k) (n * l + (m * k - m * l)) : {!add.comm}
|
||||
... = dist (n * k) (n * l + m * k - m * l) : {(add_sub_assoc H2 (n * l))⁻¹}
|
||||
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _,
|
||||
or.elim !le_total
|
||||
or.elim !le.total
|
||||
(assume H : k ≤ l, !dist_comm ▸ !dist_comm ▸ aux l k H)
|
||||
(assume H : l ≤ k, aux k l H)
|
||||
|
||||
|
|
|
|||
|
|
@ -42,9 +42,13 @@ intro : a → b → and a b
|
|||
definition and.elim_left {a b : Prop} (H : and a b) : a :=
|
||||
and.rec (λa b, a) H
|
||||
|
||||
definition and.left := @and.elim_left
|
||||
|
||||
definition and.elim_right {a b : Prop} (H : and a b) : b :=
|
||||
and.rec (λa b, b) H
|
||||
|
||||
definition and.right := @and.elim_right
|
||||
|
||||
inductive sum (A B : Type) : Type :=
|
||||
inl {} : A → sum A B,
|
||||
inr {} : B → sum A B
|
||||
|
|
|
|||
|
|
@ -271,7 +271,6 @@ namespace decidable
|
|||
by_cases
|
||||
(assume H1 : p, H1)
|
||||
(assume H1 : ¬p, false.rec _ (H H1))
|
||||
|
||||
end decidable
|
||||
|
||||
section
|
||||
|
|
@ -405,6 +404,8 @@ if c then false else true
|
|||
theorem of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
|
||||
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, !false.rec (if_neg Hnc ▸ H₂))
|
||||
|
||||
notation `dec_trivial` := of_is_true trivial
|
||||
|
||||
theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c :=
|
||||
decidable.rec_on H₁ (λ Hc, absurd true.intro (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
|
||||
|
||||
|
|
|
|||
|
|
@ -79,8 +79,8 @@ case_strong_induction_on m
|
|||
take z,
|
||||
assume Hzx : measure z < measure x,
|
||||
calc
|
||||
f' m z = restrict default measure f m z : IH m !le_refl z
|
||||
... = f z : !restrict_lt_eq (lt.of_lt_of_le Hzx (lt_succ_imp_le H1))
|
||||
f' m z = restrict default measure f m z : IH m !le.refl z
|
||||
... = f z : !restrict_lt_eq (lt.of_lt_of_le Hzx (le_of_lt_succ H1))
|
||||
∎,
|
||||
have H2 : f' (succ m) x = rec_val x f,
|
||||
proof
|
||||
|
|
@ -95,7 +95,7 @@ case_strong_induction_on m
|
|||
take z,
|
||||
assume Hzx : measure z < measure x,
|
||||
calc
|
||||
f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _
|
||||
f' m' z = restrict default measure f m' z : IH _ (le_of_lt_succ H1) _
|
||||
... = f z : !restrict_lt_eq Hzx
|
||||
qed,
|
||||
have H3 : restrict default measure f (succ m) x = rec_val x f,
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue