refactor(library): cleanup nat/int proofs
This commit is contained in:
Leonardo de Moura
parent
a307a0691b
commit
7462874a4a
4 changed files with 78 additions and 194 deletions
|
|
@ -169,20 +169,15 @@ local infix ≡ := int.equiv
|
|||
|
||||
protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm
|
||||
|
||||
local attribute int.equiv [reducible]
|
||||
|
||||
protected theorem equiv.symm [symm] {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
|
||||
calc
|
||||
pr1 q + pr2 p = pr2 p + pr1 q : by rewrite add.comm
|
||||
... = pr1 p + pr2 q : H⁻¹
|
||||
... = pr2 q + pr1 p : by rewrite add.comm
|
||||
by simp
|
||||
|
||||
protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
|
||||
add.right_cancel (calc
|
||||
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) : by rewrite add.assoc
|
||||
... = pr2 p + (pr2 q + pr1 r) : {H2}
|
||||
... = pr2 p + pr2 q + pr1 r : by rewrite add.assoc
|
||||
... = pr2 p + pr1 r + pr2 q : by rewrite add.right_comm)
|
||||
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by simp_nohyps
|
||||
... = pr2 p + pr1 r + pr2 q : by simp)
|
||||
|
||||
protected theorem equiv_equiv : is_equivalence int.equiv :=
|
||||
is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
|
||||
|
|
@ -239,7 +234,7 @@ or.elim (int.equiv_cases Hequiv)
|
|||
= pr1 p + pr2 q - pr2 q - pr2 p : by rewrite nat.add_sub_cancel
|
||||
... = pr2 p + pr1 q - pr2 q - pr2 p : Hequiv
|
||||
... = pr2 p + (pr1 q - pr2 q) - pr2 p : nat.add_sub_assoc Hq
|
||||
... = pr1 q - pr2 q + pr2 p - pr2 p : by rewrite add.comm
|
||||
... = pr1 q - pr2 q + pr2 p - pr2 p : by simp
|
||||
... = pr1 q - pr2 q : by rewrite nat.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),
|
||||
|
|
@ -324,20 +319,16 @@ theorem repr_add : Π (a b : ℤ), repr (add a b) ≡ padd (repr a) (repr b)
|
|||
|
||||
theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' :=
|
||||
calc pr1 p + pr1 q + (pr2 p' + pr2 q')
|
||||
= pr1 p + pr2 p' + (pr1 q + pr2 q') : add.comm4
|
||||
... = pr2 p + pr1 p' + (pr1 q + pr2 q') : {Ha}
|
||||
... = pr2 p + pr1 p' + (pr2 q + pr1 q') : {Hb}
|
||||
... = pr2 p + pr2 q + (pr1 p' + pr1 q') : add.comm4
|
||||
= pr1 p + pr2 p' + (pr1 q + pr2 q') : by simp_nohyps
|
||||
... = pr2 p + pr1 p' + (pr2 q + pr1 q') : by simp
|
||||
... = pr2 p + pr2 q + (pr1 p' + pr1 q') : by simp_nohyps
|
||||
|
||||
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) : by rewrite add.comm
|
||||
... = (pr1 q + pr1 p, pr2 q + pr2 p) : by rewrite (add.comm (pr2 p) (pr2 q))
|
||||
calc (pr1 p + pr1 q, pr2 p + pr2 q) = (pr1 q + pr1 p, pr2 q + pr2 p) : by simp
|
||||
|
||||
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) : by rewrite 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 simp
|
||||
|
||||
protected theorem add_comm (a b : ℤ) : a + b = b + a :=
|
||||
eq_of_repr_equiv_repr (equiv.trans !repr_add
|
||||
|
|
@ -383,13 +374,7 @@ theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) :=
|
|||
show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add_comm ▸ rfl
|
||||
|
||||
theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
|
||||
calc pr1 p + pr1 q + pr2 q + pr2 p
|
||||
= pr1 p + (pr1 q + pr2 q) + pr2 p : add.assoc
|
||||
... = pr1 p + (pr1 q + pr2 q + pr2 p) : add.assoc
|
||||
... = pr1 p + (pr2 q + pr1 q + pr2 p) : add.comm
|
||||
... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm
|
||||
... = pr1 p + (pr2 p + pr2 q + pr1 q) : add.comm
|
||||
... = pr2 p + pr2 q + pr1 q + pr1 p : add.comm
|
||||
by unfold [padd, pneg]; simp
|
||||
|
||||
protected theorem add_left_inv (a : ℤ) : -a + a = 0 :=
|
||||
have H : repr (-a + a) ≡ repr 0, from
|
||||
|
|
@ -457,31 +442,19 @@ theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b)
|
|||
(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
|
||||
|
||||
local attribute left_distrib right_distrib [simp]
|
||||
theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
|
||||
(H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
|
||||
: xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) :=
|
||||
nat.add_right_cancel (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)) : 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[-+left_distrib,-+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)
|
||||
(H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm) : xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) :=
|
||||
nat.add_right_cancel (
|
||||
calc xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn))
|
||||
= (xa + yb)*xn + (ya + xb)*yn + (xb*(xn + ym)) + (yb*(yn + xm)) : by simp_nohyps
|
||||
... = (ya + xb)*xn + (xa + yb)*yn + (xb*(yn + xm)) + (yb*(xn + ym)) : by simp
|
||||
... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : by simp_nohyps)
|
||||
|
||||
theorem pmul_congr {p p' q q' : ℕ × ℕ} : p ≡ p' → q ≡ q' → pmul p q ≡ pmul p' q' := equiv_mul_prep
|
||||
|
||||
theorem pmul_comm (p q : ℕ × ℕ) : pmul p q = pmul q p :=
|
||||
show (_,_) = (_,_),
|
||||
begin
|
||||
congruence,
|
||||
{ congruence, repeat rewrite mul.comm },
|
||||
{ rewrite add.comm, congruence, repeat rewrite mul.comm }
|
||||
end
|
||||
by unfold pmul; simp
|
||||
|
||||
protected theorem mul_comm (a b : ℤ) : a * b = b * a :=
|
||||
eq_of_repr_equiv_repr
|
||||
|
|
@ -493,13 +466,7 @@ eq_of_repr_equiv_repr
|
|||
private theorem pmul_assoc_prep {p1 p2 q1 q2 r1 r2 : ℕ} :
|
||||
((p1*q1+p2*q2)*r1+(p1*q2+p2*q1)*r2, (p1*q1+p2*q2)*r2+(p1*q2+p2*q1)*r1) =
|
||||
(p1*(q1*r1+q2*r2)+p2*(q1*r2+q2*r1), p1*(q1*r2+q2*r1)+p2*(q1*r1+q2*r2)) :=
|
||||
begin
|
||||
rewrite [+left_distrib, +right_distrib, *mul.assoc],
|
||||
rewrite (add.comm4 (p1 * (q1 * r1)) (p2 * (q2 * r1)) (p1 * (q2 * r2)) (p2 * (q1 * r2))),
|
||||
rewrite (add.comm (p2 * (q2 * r1)) (p2 * (q1 * r2))),
|
||||
rewrite (add.comm4 (p1 * (q1 * r2)) (p2 * (q2 * r2)) (p1 * (q2 * r1)) (p2 * (q1 * r1))),
|
||||
rewrite (add.comm (p2 * (q2 * r2)) (p2 * (q1 * r1)))
|
||||
end
|
||||
by simp
|
||||
|
||||
theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) := pmul_assoc_prep
|
||||
|
||||
|
|
@ -522,11 +489,7 @@ int.mul_comm a 1 ▸ int.mul_one a
|
|||
private theorem mul_distrib_prep {a1 a2 b1 b2 c1 c2 : ℕ} :
|
||||
((a1+b1)*c1+(a2+b2)*c2, (a1+b1)*c2+(a2+b2)*c1) =
|
||||
(a1*c1+a2*c2+(b1*c1+b2*c2), a1*c2+a2*c1+(b1*c2+b2*c1)) :=
|
||||
begin
|
||||
rewrite +right_distrib, congruence,
|
||||
{rewrite add.comm4},
|
||||
{rewrite add.comm4}
|
||||
end
|
||||
by simp
|
||||
|
||||
protected theorem right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c :=
|
||||
eq_of_repr_equiv_repr
|
||||
|
|
|
|||
|
|
@ -255,8 +255,6 @@ protected definition comm_semiring [reducible] [trans_instance] : comm_semiring
|
|||
mul_zero := nat.mul_zero,
|
||||
mul_comm := nat.mul_comm⦄
|
||||
|
||||
attribute succ_eq_add_one [simp]
|
||||
|
||||
end nat
|
||||
|
||||
section
|
||||
|
|
|
|||
|
|
@ -12,144 +12,86 @@ namespace nat
|
|||
|
||||
/- subtraction -/
|
||||
|
||||
protected theorem sub_zero (n : ℕ) : n - 0 = n :=
|
||||
protected theorem sub_zero [simp] (n : ℕ) : n - 0 = n :=
|
||||
rfl
|
||||
|
||||
theorem sub_succ (n m : ℕ) : n - succ m = pred (n - m) :=
|
||||
theorem sub_succ [simp] (n m : ℕ) : n - succ m = pred (n - m) :=
|
||||
rfl
|
||||
|
||||
protected theorem zero_sub (n : ℕ) : 0 - n = 0 :=
|
||||
nat.induction_on n !nat.sub_zero
|
||||
(take k : nat,
|
||||
assume IH : 0 - k = 0,
|
||||
calc
|
||||
0 - succ k = pred (0 - k) : sub_succ
|
||||
... = pred 0 : IH
|
||||
... = 0 : pred_zero)
|
||||
protected theorem zero_sub [simp] (n : ℕ) : 0 - n = 0 :=
|
||||
nat.induction_on n (by simp) (by simp)
|
||||
|
||||
theorem succ_sub_succ (n m : ℕ) : succ n - succ m = n - m :=
|
||||
theorem succ_sub_succ [simp] (n m : ℕ) : succ n - succ m = n - m :=
|
||||
succ_sub_succ_eq_sub n m
|
||||
|
||||
protected theorem sub_self (n : ℕ) : n - n = 0 :=
|
||||
nat.induction_on n !nat.sub_zero (take k IH, !succ_sub_succ ⬝ IH)
|
||||
protected theorem sub_self [simp] (n : ℕ) : n - n = 0 :=
|
||||
nat.induction_on n (by simp) (by simp)
|
||||
|
||||
protected theorem add_sub_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m :=
|
||||
nat.induction_on k
|
||||
(calc
|
||||
(n + 0) - (m + 0) = n - (m + 0) : {!add_zero}
|
||||
... = n - m : {!add_zero})
|
||||
(take l : nat,
|
||||
assume IH : (n + l) - (m + l) = n - m,
|
||||
local attribute nat.add_succ [simp]
|
||||
|
||||
protected theorem add_sub_add_right [simp] (n k m : ℕ) : (n + k) - (m + k) = n - m :=
|
||||
nat.induction_on k (by simp) (by simp)
|
||||
|
||||
protected theorem add_sub_add_left [simp] (k n m : ℕ) : (k + n) - (k + m) = n - m :=
|
||||
nat.induction_on k (by simp) (by simp)
|
||||
|
||||
protected theorem add_sub_cancel [simp] (n m : ℕ) : n + m - m = n :=
|
||||
nat.induction_on m (by simp) (by simp)
|
||||
|
||||
protected theorem add_sub_cancel_left [simp] (n m : ℕ) : n + m - n = m :=
|
||||
nat.induction_on n (by simp) (by simp)
|
||||
|
||||
protected theorem sub_sub [simp] (n m k : ℕ) : n - m - k = n - (m + k) :=
|
||||
nat.induction_on k (by simp) (by simp)
|
||||
|
||||
theorem succ_sub_sub_succ [simp] (n m k : ℕ) : succ n - m - succ k = n - m - k :=
|
||||
by simp
|
||||
|
||||
theorem sub_self_add [simp] (n m : ℕ) : n - (n + m) = 0 :=
|
||||
calc
|
||||
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add_succ}
|
||||
... = succ (n + l) - succ (m + l) : {!add_succ}
|
||||
... = (n + l) - (m + l) : !succ_sub_succ
|
||||
... = n - m : IH)
|
||||
protected theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
|
||||
add.comm n k ▸ add.comm m k ▸ nat.add_sub_add_right n k m
|
||||
|
||||
protected theorem add_sub_cancel (n m : ℕ) : n + m - m = n :=
|
||||
nat.induction_on m
|
||||
(begin rewrite add_zero end)
|
||||
(take k : ℕ,
|
||||
assume IH : n + k - k = n,
|
||||
calc
|
||||
n + succ k - succ k = succ (n + k) - succ k : add_succ
|
||||
... = n + k - k : succ_sub_succ
|
||||
... = n : IH)
|
||||
|
||||
protected theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m :=
|
||||
!add.comm ▸ !nat.add_sub_cancel
|
||||
|
||||
protected theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) :=
|
||||
nat.induction_on k
|
||||
(calc
|
||||
n - m - 0 = n - m : nat.sub_zero
|
||||
... = n - (m + 0) : add_zero)
|
||||
(take l : nat,
|
||||
assume IH : n - m - l = n - (m + l),
|
||||
calc
|
||||
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) : by rewrite add_succ)
|
||||
|
||||
theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k :=
|
||||
calc
|
||||
succ n - m - succ k = succ n - (m + succ k) : nat.sub_sub
|
||||
... = succ n - succ (m + k) : add_succ
|
||||
... = n - (m + k) : succ_sub_succ
|
||||
... = n - m - k : nat.sub_sub
|
||||
|
||||
theorem sub_self_add (n m : ℕ) : n - (n + m) = 0 :=
|
||||
calc
|
||||
n - (n + m) = n - n - m : nat.sub_sub
|
||||
... = 0 - m : nat.sub_self
|
||||
... = 0 : nat.zero_sub
|
||||
n - (n + m) = n - n - m : by topdown_simp
|
||||
... = 0 : by simp
|
||||
|
||||
protected theorem sub.right_comm (m n k : ℕ) : m - n - k = m - k - n :=
|
||||
calc
|
||||
m - n - k = m - (n + k) : !nat.sub_sub
|
||||
... = m - (k + n) : {!add.comm}
|
||||
... = m - k - n : !nat.sub_sub⁻¹
|
||||
by simp
|
||||
|
||||
theorem sub_one (n : ℕ) : n - 1 = pred n :=
|
||||
rfl
|
||||
|
||||
theorem succ_sub_one (n : ℕ) : succ n - 1 = n :=
|
||||
theorem succ_sub_one [simp] (n : ℕ) : succ n - 1 = n :=
|
||||
rfl
|
||||
|
||||
local attribute nat.succ_mul nat.mul_succ [simp]
|
||||
|
||||
/- interaction with multiplication -/
|
||||
|
||||
theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m :=
|
||||
nat.induction_on n
|
||||
(calc
|
||||
pred 0 * m = 0 * m : pred_zero
|
||||
... = 0 : zero_mul
|
||||
... = 0 - m : nat.zero_sub
|
||||
... = 0 * m - m : zero_mul)
|
||||
(take k : nat,
|
||||
assume IH : pred k * m = k * m - m,
|
||||
calc
|
||||
pred (succ k) * m = k * m : pred_succ
|
||||
... = k * m + m - m : nat.add_sub_cancel
|
||||
... = succ k * m - m : succ_mul)
|
||||
nat.induction_on n (by simp) (by simp)
|
||||
|
||||
theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
|
||||
calc
|
||||
n * pred m = pred m * n : mul.comm
|
||||
n * pred m = pred m * n : by simp
|
||||
... = m * n - n : mul_pred_left
|
||||
... = n * m - n : mul.comm
|
||||
... = n * m - n : by simp
|
||||
|
||||
protected theorem mul_sub_right_distrib (n m k : ℕ) : (n - m) * k = n * k - m * k :=
|
||||
nat.induction_on m
|
||||
(calc
|
||||
(n - 0) * k = n * k : nat.sub_zero
|
||||
... = n * k - 0 : nat.sub_zero
|
||||
... = n * k - 0 * k : zero_mul)
|
||||
(take l : nat,
|
||||
assume IH : (n - l) * k = n * k - l * k,
|
||||
calc
|
||||
(n - succ l) * k = pred (n - l) * k : sub_succ
|
||||
... = (n - l) * k - k : mul_pred_left
|
||||
... = n * k - l * k - k : IH
|
||||
... = n * k - (l * k + k) : nat.sub_sub
|
||||
... = n * k - (succ l * k) : succ_mul)
|
||||
attribute mul_pred_left mul_pred_right [simp]
|
||||
|
||||
protected theorem mul_sub_left_distrib (n m k : ℕ) : n * (m - k) = n * m - n * k :=
|
||||
protected theorem mul_sub_right_distrib [simp] (n m k : ℕ) : (n - m) * k = n * k - m * k :=
|
||||
nat.induction_on m (by simp) (by simp)
|
||||
|
||||
protected theorem mul_sub_left_distrib [simp] (n m k : ℕ) : n * (m - k) = n * m - n * k :=
|
||||
calc
|
||||
n * (m - k) = (m - k) * n : !mul.comm
|
||||
... = m * n - k * n : !nat.mul_sub_right_distrib
|
||||
... = n * m - k * n : {!mul.comm}
|
||||
... = n * m - n * k : {!mul.comm}
|
||||
n * (m - k) = (m - k) * n : by rewrite mul.comm
|
||||
... = n * m - n * k : by simp
|
||||
|
||||
protected theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) :=
|
||||
by rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b),
|
||||
nat.add_sub_add_left]
|
||||
|
||||
local attribute succ_eq_add_one right_distrib left_distrib [simp]
|
||||
|
||||
theorem succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 :=
|
||||
calc succ a * succ a = (a+1)*(a+1) : by rewrite [add_one]
|
||||
... = a*a + a + a + 1 : by rewrite [right_distrib, left_distrib, one_mul, mul_one]
|
||||
by simp
|
||||
|
||||
/- interaction with inequalities -/
|
||||
|
||||
|
|
@ -213,11 +155,7 @@ exists.intro k
|
|||
protected theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
|
||||
have l1 : k ≤ m → n + m - k = n + (m - k), from
|
||||
sub_induction k m
|
||||
(take m : ℕ,
|
||||
assume H : 0 ≤ m,
|
||||
calc
|
||||
n + m - 0 = n + m : nat.sub_zero
|
||||
... = n + (m - 0) : nat.sub_zero)
|
||||
(by simp)
|
||||
(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),
|
||||
|
|
@ -267,10 +205,9 @@ or.elim !le.total
|
|||
(assume H2 : k ≤ n,
|
||||
have H3 : n - k + l = m - k, from
|
||||
calc
|
||||
n - k + l = l + (n - k) : add.comm
|
||||
n - k + l = l + (n - k) : by simp
|
||||
... = l + n - k : nat.add_sub_assoc H2 l
|
||||
... = n + l - k : add.comm
|
||||
... = m - k : Hl,
|
||||
... = m - k : by simp,
|
||||
le.intro H3)
|
||||
|
||||
protected theorem sub_le_sub_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k - m ≤ k - n :=
|
||||
|
|
@ -280,14 +217,7 @@ sub.cases
|
|||
(take m' : ℕ,
|
||||
assume Hm : m + m' = k,
|
||||
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
|
||||
... = n + (l + m') : add.comm
|
||||
... = n + l + m' : add.assoc
|
||||
... = m + m' : Hl
|
||||
... = k : Hm
|
||||
... = k - n + n : nat.sub_add_cancel H3,
|
||||
have H4 : m' + l + n = k - n + n, by simp,
|
||||
le.intro (add.right_cancel H4))
|
||||
|
||||
protected theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 :=
|
||||
|
|
@ -327,8 +257,7 @@ sub.cases
|
|||
assume Hkm : k + km = m,
|
||||
have H : k + (mn + km) = n, from
|
||||
calc
|
||||
k + (mn + km) = k + (km + mn): add.comm
|
||||
... = k + km + mn : add.assoc
|
||||
k + (mn + km) = k + km + mn : by simp
|
||||
... = m + mn : Hkm
|
||||
... = n : Hmn,
|
||||
have H2 : n - k = mn + km, from nat.sub_eq_of_add_eq H,
|
||||
|
|
@ -366,13 +295,10 @@ lt_of_succ_le this
|
|||
definition dist [reducible] (n m : ℕ) := (n - m) + (m - n)
|
||||
|
||||
theorem dist.comm (n m : ℕ) : dist n m = dist m n :=
|
||||
!add.comm
|
||||
by simp
|
||||
|
||||
theorem dist_self (n : ℕ) : dist n n = 0 :=
|
||||
calc
|
||||
(n - n) + (n - n) = 0 + (n - n) : nat.sub_self
|
||||
... = 0 + 0 : nat.sub_self
|
||||
... = 0 : rfl
|
||||
by simp
|
||||
|
||||
theorem eq_of_dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
|
||||
have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
|
||||
|
|
@ -433,10 +359,9 @@ theorem dist_sub_eq_dist_add_left {n m : ℕ} (H : n ≥ m) (k : ℕ) :
|
|||
dist (n - m) k = dist n (k + m) :=
|
||||
have H2 : n - m + (k + m) = k + n, from
|
||||
calc
|
||||
n - m + (k + m) = n - m + (m + k) : add.comm
|
||||
... = n - m + m + k : add.assoc
|
||||
n - m + (k + m) = n - m + m + k : by simp
|
||||
... = n + k : nat.sub_add_cancel H
|
||||
... = k + n : add.comm,
|
||||
... = k + n : by simp,
|
||||
dist_eq_intro H2
|
||||
|
||||
theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
|
||||
|
|
@ -444,10 +369,7 @@ theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
|
|||
dist.comm (k - m) n ▸ dist.comm k (n + m) ▸ dist_sub_eq_dist_add_left H 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)),
|
||||
begin rewrite [add.comm (k - m) (m - n),
|
||||
{n - m + _ + _}add.assoc,
|
||||
{m - k + _}add.left_comm, -add.assoc] end,
|
||||
have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)), by simp,
|
||||
this ▸ add_le_add !nat.sub_lt_sub_add_sub !nat.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 :=
|
||||
|
|
|
|||
|
|
@ -109,6 +109,7 @@ definition with_attributes_tac (o : expr) (n : identifier_list) (t : tactic) : t
|
|||
|
||||
definition simp : tactic := #tactic with_options [blast.strategy "simp"] blast
|
||||
definition simp_nohyps : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
|
||||
definition topdown_simp : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
|
||||
|
||||
definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue