refactor(data/nat/order): use new policy for marking implicit arguments and '!' operator
This commit is contained in:
Leonardo de Moura
parent
e91a64fb38
commit
a0d4d82f3f
6 changed files with 97 additions and 97 deletions
|
|
@ -119,7 +119,7 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
|
|||
... = pr1 (proj a) : (proj_ge_pr1 H)⁻¹
|
||||
... = pr2 (flip (proj a)) : (flip_pr2 (proj a))⁻¹,
|
||||
prod.equal H3 H4,
|
||||
or.elim le_total
|
||||
or.elim !le_total
|
||||
(assume H : pr2 a ≤ pr1 a, special a H)
|
||||
(assume H : pr1 a ≤ pr2 a,
|
||||
have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip a H,
|
||||
|
|
@ -129,7 +129,7 @@ or.elim le_total
|
|||
... = flip (proj a) : {flip_flip a})
|
||||
|
||||
theorem proj_rel (a : ℕ × ℕ) : rel a (proj a) :=
|
||||
or.elim le_total
|
||||
or.elim !le_total
|
||||
(assume H : pr2 a ≤ pr1 a,
|
||||
calc
|
||||
pr1 a + pr2 (proj a) = pr1 a + 0 : {proj_ge_pr2 H}
|
||||
|
|
@ -148,7 +148,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
|
|||
take a b,
|
||||
assume H2 : pr2 a ≤ pr1 a,
|
||||
assume H : rel a b,
|
||||
have H3 : pr1 a + pr2 b ≤ pr2 a + pr1 b, from H ▸ le_refl,
|
||||
have H3 : pr1 a + pr2 b ≤ pr2 a + pr1 b, from H ▸ !le_refl,
|
||||
have H4 : pr2 b ≤ pr1 b, from add_le_inv H3 H2,
|
||||
have H5 : pr1 (proj a) = pr1 (proj b), from
|
||||
calc
|
||||
|
|
@ -163,7 +163,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
|
|||
pr2 (proj a) = 0 : proj_ge_pr2 H2
|
||||
... = pr2 (proj b) : {(proj_ge_pr2 H4)⁻¹},
|
||||
prod.equal H5 H6,
|
||||
or.elim le_total
|
||||
or.elim !le_total
|
||||
(assume H2 : pr2 a ≤ pr1 a, special a b H2 H)
|
||||
(assume H2 : pr1 a ≤ pr2 a,
|
||||
have H3 : pr2 (flip a) ≤ pr1 (flip a), from P_flip a H2,
|
||||
|
|
@ -175,7 +175,7 @@ theorem proj_inj {a b : ℕ × ℕ} (H : proj a = proj b) : rel a b :=
|
|||
representative_map_equiv_inj rel_equiv proj_rel @proj_congr H
|
||||
|
||||
theorem proj_zero_or (a : ℕ × ℕ) : pr1 (proj a) = 0 ∨ pr2 (proj a) = 0 :=
|
||||
or.elim le_total
|
||||
or.elim !le_total
|
||||
(assume H : pr2 a ≤ pr1 a, or.inr (proj_ge_pr2 H))
|
||||
(assume H : pr1 a ≤ pr2 a, or.inl (proj_le_pr1 H))
|
||||
|
||||
|
|
|
|||
|
|
@ -420,7 +420,7 @@ obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
|
|||
Hn⁻¹ ▸ congr_arg of_nat (to_nat_of_nat n)
|
||||
|
||||
theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
|
||||
iff.mp (iff.symm (le_of_nat _ _)) zero_le
|
||||
iff.mp (iff.symm !le_of_nat) !zero_le
|
||||
|
||||
definition le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
|
||||
have aux : Πx, decidable (0 ≤ x), from
|
||||
|
|
@ -615,7 +615,7 @@ or.elim (em (a = 0))
|
|||
mul_cancel_right H3 H))
|
||||
|
||||
theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a :=
|
||||
have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) succ_pos,
|
||||
have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) !succ_pos,
|
||||
--this should be done with simp
|
||||
or.elim3 (trichotomy a 0) sorry sorry sorry
|
||||
-- (by simp)
|
||||
|
|
@ -623,7 +623,7 @@ or.elim3 (trichotomy a 0) sorry sorry sorry
|
|||
-- (by simp)
|
||||
|
||||
theorem sign_succ (n : ℕ) : sign (succ n) = 1 :=
|
||||
sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) succ_pos)
|
||||
sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) !succ_pos)
|
||||
--this should be done with simp
|
||||
|
||||
theorem sign_neg (a : ℤ) : sign (-a) = - sign a :=
|
||||
|
|
|
|||
|
|
@ -73,7 +73,7 @@ let f := rec_measure default measure rec_val in
|
|||
case_strong_induction_on m
|
||||
(take x,
|
||||
have H1 : f' 0 x = default, from rfl,
|
||||
have H2 : ¬ measure x < 0, from not_lt_zero,
|
||||
have H2 : ¬ measure x < 0, from !not_lt_zero,
|
||||
have H3 : restrict default measure f 0 x = default, from if_neg H2,
|
||||
show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
|
||||
(take m,
|
||||
|
|
@ -86,7 +86,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 m le_refl z
|
||||
f' m z = restrict default measure f m z : IH m !le_refl z
|
||||
... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1)),
|
||||
have H2 : f' (succ m) x = rec_val x f, from
|
||||
calc
|
||||
|
|
@ -105,7 +105,7 @@ case_strong_induction_on m
|
|||
restrict default measure f (succ m) x = f x : if_pos H1
|
||||
... = f' (succ m') x : eq.refl _
|
||||
... = if measure x < succ m' then rec_val x (f' m') else default : rfl
|
||||
... = rec_val x (f' m') : if_pos self_lt_succ
|
||||
... = rec_val x (f' m') : if_pos !self_lt_succ
|
||||
... = rec_val x f : rec_decreasing _ _ _ H3a,
|
||||
show f' (succ m) x = restrict default measure f (succ m) x,
|
||||
from H2 ⬝ H3⁻¹)
|
||||
|
|
@ -138,7 +138,7 @@ have H : ∀z, measure z < measure x → f' m z = f z, from
|
|||
calc
|
||||
f x = f' (succ m) x : rfl
|
||||
... = if measure x < succ m then rec_val x (f' m) else default : rfl
|
||||
... = rec_val x (f' m) : if_pos (self_lt_succ)
|
||||
... = rec_val x (f' m) : if_pos !self_lt_succ
|
||||
... = rec_val x f : rec_decreasing _ _ _ H
|
||||
|
||||
|
||||
|
|
@ -193,7 +193,7 @@ div_aux_spec _ _ ⬝ if_pos (or.inr H)
|
|||
-- add_rewrite div_less
|
||||
|
||||
theorem zero_div {y : ℕ} : 0 div y = 0 :=
|
||||
case y div_zero (take y', div_less succ_pos)
|
||||
case y div_zero (take y', div_less !succ_pos)
|
||||
|
||||
-- add_rewrite zero_div
|
||||
|
||||
|
|
@ -202,7 +202,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from
|
|||
not_intro
|
||||
(assume H4 : y = 0 ∨ x < y,
|
||||
or.elim H4
|
||||
(assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
|
||||
(assume H5 : y = 0, not_elim !lt_irrefl (H5 ▸ H1))
|
||||
(assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
|
||||
div_aux_spec _ _ ⬝ if_neg H3
|
||||
|
||||
|
|
@ -269,7 +269,7 @@ mod_aux_spec _ _ ⬝ if_pos (or.inr H)
|
|||
-- add_rewrite mod_lt_eq
|
||||
|
||||
theorem zero_mod {y : ℕ} : 0 mod y = 0 :=
|
||||
case y mod_zero (take y', mod_lt_eq succ_pos)
|
||||
case y mod_zero (take y', mod_lt_eq !succ_pos)
|
||||
|
||||
-- add_rewrite zero_mod
|
||||
|
||||
|
|
@ -278,7 +278,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from
|
|||
not_intro
|
||||
(assume H4 : y = 0 ∨ x < y,
|
||||
or.elim H4
|
||||
(assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
|
||||
(assume H5 : y = 0, not_elim !lt_irrefl (H5 ▸ H1))
|
||||
(assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
|
||||
mod_aux_spec _ _ ⬝ if_neg H3
|
||||
|
||||
|
|
@ -325,7 +325,7 @@ case_strong_induction_on x
|
|||
(assume H1 : ¬ succ x < y,
|
||||
have H2 : y ≤ succ x, from not_lt_imp_ge 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 H4 : succ x - y < succ x, from sub_lt !succ_pos H,
|
||||
have H5 : succ x - y ≤ x, from lt_succ_imp_le H4,
|
||||
show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
|
||||
|
||||
|
|
@ -353,7 +353,7 @@ case_zero_pos y
|
|||
have H2 : y ≤ succ x, from not_lt_imp_ge 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 H5 : succ x - y < succ x, from sub_lt !succ_pos H,
|
||||
have H6 : succ x - y ≤ x, from lt_succ_imp_le H5,
|
||||
(calc
|
||||
succ x div y * y + succ x mod y = succ ((succ x - y) div y) * y + succ x mod y :
|
||||
|
|
@ -365,7 +365,7 @@ case_zero_pos y
|
|||
... = succ x : add_sub_ge_left H2)⁻¹)))
|
||||
|
||||
theorem mod_le {x y : ℕ} : x mod y ≤ x :=
|
||||
div_mod_eq⁻¹ ▸ le_add_left
|
||||
div_mod_eq⁻¹ ▸ !le_add_left
|
||||
|
||||
--- a good example where simplifying using the context causes problems
|
||||
theorem remainder_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y)
|
||||
|
|
@ -382,7 +382,7 @@ theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y)
|
|||
(H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
|
||||
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 le_lt_trans zero_le H1,
|
||||
have H6 : y > 0, from le_lt_trans !zero_le H1,
|
||||
show q1 = q2, from mul_cancel_right H6 H5
|
||||
|
||||
theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
|
|
@ -418,7 +418,7 @@ by_cases -- (y = 0)
|
|||
... = (x div y) * (z * y) + z * (x mod y) : {!mul.left_comm}))
|
||||
|
||||
theorem mod_one {x : ℕ} : x mod 1 = 0 :=
|
||||
have H1 : x mod 1 < 1, from mod_lt succ_pos,
|
||||
have H1 : x mod 1 < 1, from mod_lt !succ_pos,
|
||||
le_zero (lt_succ_imp_le H1)
|
||||
|
||||
-- add_rewrite mod_one
|
||||
|
|
@ -427,7 +427,7 @@ theorem mod_self {n : ℕ} : n mod n = 0 :=
|
|||
case n (by simp)
|
||||
(take n,
|
||||
have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
|
||||
from mod_mul_mul succ_pos,
|
||||
from mod_mul_mul !succ_pos,
|
||||
(by simp) ▸ H)
|
||||
|
||||
-- add_rewrite mod_self
|
||||
|
|
@ -651,9 +651,9 @@ have aux : ∀m, P m n, from
|
|||
(take n,
|
||||
assume IH : ∀k, k ≤ n → ∀m, P m k,
|
||||
take m,
|
||||
have H2 : m mod succ n ≤ n, from lt_succ_imp_le (mod_lt succ_pos),
|
||||
have H2 : m mod succ n ≤ n, from lt_succ_imp_le (mod_lt !succ_pos),
|
||||
have H3 : P (succ n) (m mod succ n), from IH _ H2 _,
|
||||
show P m (succ n), from H1 _ _ succ_pos H3),
|
||||
show P m (succ n), from H1 _ _ !succ_pos H3),
|
||||
aux m
|
||||
|
||||
theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
|
||||
|
|
|
|||
|
|
@ -34,17 +34,17 @@ irreducible le
|
|||
|
||||
-- ### partial order (totality is part of less than)
|
||||
|
||||
theorem le_refl {n : ℕ} : n ≤ n :=
|
||||
theorem le_refl (n : ℕ) : n ≤ n :=
|
||||
le_intro !add.zero_right
|
||||
|
||||
theorem zero_le {n : ℕ} : 0 ≤ n :=
|
||||
theorem zero_le (n : ℕ) : 0 ≤ n :=
|
||||
le_intro !add.zero_left
|
||||
|
||||
theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
|
||||
obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
|
||||
add.eq_zero_left Hk
|
||||
|
||||
theorem not_succ_zero_le {n : ℕ} : ¬ succ n ≤ 0 :=
|
||||
theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 :=
|
||||
not_intro
|
||||
(assume H : succ n ≤ 0,
|
||||
have H2 : succ n = 0, from le_zero H,
|
||||
|
|
@ -77,10 +77,10 @@ calc
|
|||
|
||||
-- ### interaction with addition
|
||||
|
||||
theorem le_add_right {n m : ℕ} : n ≤ n + m :=
|
||||
theorem le_add_right (n m : ℕ) : n ≤ n + m :=
|
||||
le_intro rfl
|
||||
|
||||
theorem le_add_left {n m : ℕ} : n ≤ m + n :=
|
||||
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 :=
|
||||
|
|
@ -111,7 +111,7 @@ theorem add_le_inv {n m k l : ℕ} (H1 : n + m ≤ k + l) (H2 : k ≤ n) : m ≤
|
|||
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
|
||||
show m ≤ l, from le_trans !le_add_left H4
|
||||
|
||||
-- add_rewrite le_add_right le_add_left
|
||||
|
||||
|
|
@ -123,11 +123,11 @@ theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
|
|||
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 :=
|
||||
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
|
||||
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),
|
||||
|
|
@ -166,13 +166,13 @@ obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H),
|
|||
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,
|
||||
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 :=
|
||||
theorem le_pred_self (n : ℕ) : pred n ≤ n :=
|
||||
case n
|
||||
(pred.zero⁻¹ ▸ le_refl)
|
||||
(take k : ℕ, !pred.succ⁻¹ ▸ self_le_succ)
|
||||
(pred.zero⁻¹ ▸ !le_refl)
|
||||
(take k : ℕ, !pred.succ⁻¹ ▸ !self_le_succ)
|
||||
|
||||
theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
|
||||
discriminate
|
||||
|
|
@ -181,7 +181,7 @@ discriminate
|
|||
from calc
|
||||
pred n = pred 0 : {Hn}
|
||||
... = 0 : pred.zero,
|
||||
H2⁻¹ ▸ zero_le)
|
||||
H2⁻¹ ▸ !zero_le)
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
|
|
@ -198,7 +198,7 @@ discriminate
|
|||
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))
|
||||
or.inl (Hn⁻¹ ▸ !zero_le))
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
have H2 : pred n = k,
|
||||
|
|
@ -235,11 +235,11 @@ have general : ∀n, decidable (n ≤ m), from
|
|||
rec_on m
|
||||
(take n,
|
||||
rec_on n
|
||||
(decidable.inl le_refl)
|
||||
(take m iH, decidable.inr not_succ_zero_le))
|
||||
(decidable.inl !le_refl)
|
||||
(take m iH, decidable.inr !not_succ_zero_le))
|
||||
(take (m' : ℕ) (iH1 : ∀n, decidable (n ≤ m')) (n : ℕ),
|
||||
rec_on n
|
||||
(decidable.inl zero_le)
|
||||
(decidable.inl !zero_le)
|
||||
(take (n' : ℕ) (iH2 : decidable (n' ≤ succ m')),
|
||||
decidable.by_cases
|
||||
(assume Hp : n' ≤ m', decidable.inl (succ_le Hp))
|
||||
|
|
@ -283,18 +283,18 @@ lt_intro !add.move_succ
|
|||
theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
|
||||
and.elim_right (succ_le_imp_le_and_ne H)
|
||||
|
||||
theorem lt_irrefl {n : ℕ} : ¬ n < n :=
|
||||
theorem lt_irrefl (n : ℕ) : ¬ n < n :=
|
||||
not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
|
||||
|
||||
theorem succ_pos {n : ℕ} : 0 < succ n :=
|
||||
succ_le zero_le
|
||||
theorem succ_pos (n : ℕ) : 0 < succ n :=
|
||||
succ_le !zero_le
|
||||
|
||||
theorem not_lt_zero {n : ℕ} : ¬ n < 0 :=
|
||||
not_succ_zero_le
|
||||
theorem not_lt_zero (n : ℕ) : ¬ n < 0 :=
|
||||
!not_succ_zero_le
|
||||
|
||||
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
|
||||
discriminate
|
||||
(take (Hm : m = 0), absurd (Hm ▸ H) not_lt_zero)
|
||||
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
|
||||
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
|
||||
|
||||
-- ### interaction with le
|
||||
|
|
@ -305,8 +305,8 @@ H
|
|||
theorem le_succ_imp_lt {n m : ℕ} (H : succ n ≤ m) : n < m :=
|
||||
H
|
||||
|
||||
theorem self_lt_succ {n : ℕ} : n < succ n :=
|
||||
le_refl
|
||||
theorem self_lt_succ (n : ℕ) : n < succ n :=
|
||||
!le_refl
|
||||
|
||||
theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
|
||||
and.elim_left (succ_le_imp_le_and_ne H)
|
||||
|
|
@ -335,10 +335,10 @@ theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
|
|||
lt_le_trans H1 (lt_imp_le H2)
|
||||
|
||||
theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
|
||||
not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) lt_irrefl)
|
||||
not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) !lt_irrefl)
|
||||
|
||||
theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m :=
|
||||
not_intro (assume H2 : m ≤ n, absurd (lt_le_trans H H2) lt_irrefl)
|
||||
not_intro (assume H2 : m ≤ n, absurd (lt_le_trans H H2) !lt_irrefl)
|
||||
|
||||
theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
|
||||
le_imp_not_gt (lt_imp_le H)
|
||||
|
|
@ -375,13 +375,13 @@ 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_trans H self_lt_succ
|
||||
:= lt_trans H !self_lt_succ
|
||||
|
||||
-- ### totality of lt and le
|
||||
|
||||
theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m :=
|
||||
induction_on n
|
||||
(or.inl zero_le)
|
||||
(or.inl !zero_le)
|
||||
(take (k : ℕ),
|
||||
assume IH : k ≤ m ∨ m < k,
|
||||
or.elim IH
|
||||
|
|
@ -394,7 +394,7 @@ induction_on n
|
|||
m = k + l : Hl⁻¹
|
||||
... = k + 0 : {H2}
|
||||
... = k : !add.zero_right,
|
||||
have H4 : m < succ k, from H3 ▸ self_lt_succ,
|
||||
have H4 : m < succ k, from H3 ▸ !self_lt_succ,
|
||||
or.inr H4)
|
||||
(take l2 : ℕ,
|
||||
assume H2 : l = succ l2,
|
||||
|
|
@ -406,13 +406,13 @@ induction_on n
|
|||
or.inl (le_intro H3)))
|
||||
(assume H : m < k, or.inr (lt_imp_lt_succ H)))
|
||||
|
||||
theorem trichotomy_alt {n m : ℕ} : (n < m ∨ n = m) ∨ n > m :=
|
||||
theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m :=
|
||||
or.imp_or_left le_or_gt (assume H : n ≤ m, le_imp_lt_or_eq H)
|
||||
|
||||
theorem trichotomy {n m : ℕ} : n < m ∨ n = m ∨ n > m :=
|
||||
iff.elim_left or.assoc trichotomy_alt
|
||||
theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ n > m :=
|
||||
iff.elim_left or.assoc !trichotomy_alt
|
||||
|
||||
theorem le_total {n m : ℕ} : n ≤ m ∨ m ≤ n :=
|
||||
theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n :=
|
||||
or.imp_or_right le_or_gt (assume H : m < n, lt_imp_le H)
|
||||
|
||||
theorem not_lt_imp_ge {n m : ℕ} (H : ¬ n < m) : n ≥ m :=
|
||||
|
|
@ -434,7 +434,7 @@ protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (
|
|||
have H1 : ∀ {n m : nat}, m < n → P m, from
|
||||
take n,
|
||||
induction_on n
|
||||
(show ∀m, m < 0 → P m, from take m H, absurd H not_lt_zero)
|
||||
(show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero)
|
||||
(take n',
|
||||
assume IH : ∀ {m : nat}, m < n' → P m,
|
||||
have H2: P n', from H n' @IH,
|
||||
|
|
@ -444,7 +444,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from
|
|||
or.elim (le_imp_lt_or_eq (lt_succ_imp_le H3))
|
||||
(assume H4: m < n', IH H4)
|
||||
(assume H4: m = n', H4⁻¹ ▸ H2)),
|
||||
H1 self_lt_succ
|
||||
H1 !self_lt_succ
|
||||
|
||||
protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
|
||||
(Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
|
||||
|
|
@ -466,15 +466,15 @@ strong_induction_on a (
|
|||
-- ### basic
|
||||
|
||||
theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
|
||||
case y H0 (take y, H1 succ_pos)
|
||||
case y H0 (take y, H1 !succ_pos)
|
||||
|
||||
theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 :=
|
||||
or.imp_or_left
|
||||
(or.swap (le_imp_lt_or_eq zero_le))
|
||||
(or.swap (le_imp_lt_or_eq !zero_le))
|
||||
(take H : 0 = n, H⁻¹)
|
||||
|
||||
theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
|
||||
H⁻¹ ▸ succ_pos
|
||||
H⁻¹ ▸ !succ_pos
|
||||
|
||||
theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
or.elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
|
||||
|
|
@ -510,10 +510,10 @@ discriminate
|
|||
n * m = 0 * m : {H2}
|
||||
... = 0 : !mul.zero_left,
|
||||
have H4 : 0 > 0, from H3 ▸ H,
|
||||
absurd H4 lt_irrefl)
|
||||
absurd H4 !lt_irrefl)
|
||||
(take l : nat,
|
||||
assume Hl : n = succ l,
|
||||
Hl⁻¹ ▸ succ_pos)
|
||||
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)
|
||||
|
|
@ -536,7 +536,7 @@ le_lt_trans (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 (le_lt_trans zero_le H1) H2,
|
||||
have H4 : k * m < k * l, from mul_lt_left (le_lt_trans !zero_le H1) H2,
|
||||
le_lt_trans H3 H4
|
||||
|
||||
theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
|
||||
|
|
@ -559,8 +559,8 @@ theorem mul_le_cancel_right {n k m : ℕ} (Hm : m > 0) (H : n * m ≤ k * m) : n
|
|||
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 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
|
||||
|
|
@ -576,7 +576,7 @@ 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 mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 :=
|
||||
have H2 : n * m > 0, from H⁻¹ ▸ succ_pos,
|
||||
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
|
||||
|
|
@ -585,7 +585,7 @@ or.elim le_or_gt
|
|||
(assume H5 : n > 1,
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
|
||||
have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6,
|
||||
absurd self_lt_succ (le_imp_not_gt H7))
|
||||
absurd !self_lt_succ (le_imp_not_gt H7))
|
||||
|
||||
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
|
||||
mul_eq_one_left (!mul.comm ▸ H)
|
||||
|
|
|
|||
|
|
@ -180,7 +180,7 @@ 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_zero_le)
|
||||
(take k l,
|
||||
assume IH : k ≤ l → succ l - k = succ (l - k),
|
||||
take H : succ k ≤ succ l,
|
||||
|
|
@ -199,7 +199,7 @@ sub_induction n m
|
|||
calc
|
||||
0 + (k - 0) = k - 0 : !add.zero_left
|
||||
... = 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_zero_le)
|
||||
(take k l,
|
||||
assume IH : k ≤ l → k + (l - k) = l,
|
||||
take H : succ k ≤ succ l,
|
||||
|
|
@ -209,7 +209,7 @@ sub_induction n m
|
|||
... = succ l : {IH (succ_le_cancel H)})
|
||||
|
||||
theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n :=
|
||||
!add.comm ▸ add_sub_le
|
||||
!add.comm ▸ !add_sub_le
|
||||
|
||||
theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
|
||||
calc
|
||||
|
|
@ -220,24 +220,24 @@ 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 sub_le_self {n m : ℕ} : n - m ≤ n :=
|
||||
sub_split
|
||||
(assume H : n ≤ m, zero_le)
|
||||
(assume H : n ≤ m, !zero_le)
|
||||
(take k : ℕ, assume H : m + k = n, le_intro (!add.comm ▸ H))
|
||||
|
||||
theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
|
||||
|
|
@ -255,7 +255,7 @@ 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_zero_le)
|
||||
(take k m,
|
||||
assume IH : k ≤ m → n + m - k = n + (m - k),
|
||||
take H : succ k ≤ succ m,
|
||||
|
|
@ -273,11 +273,11 @@ sub_split
|
|||
assume H1 : m + k = n,
|
||||
assume H2 : k = 0,
|
||||
have H3 : n = m, from !add.zero_right ▸ 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,
|
||||
|
|
@ -300,13 +300,13 @@ obtain (x' : ℕ) (xeq : x = succ x'), from pos_imp_eq_succ xpos,
|
|||
... = succ x' - succ y' : {yeq}
|
||||
... = x' - y' : sub_succ_succ,
|
||||
have H1 : x' - y' ≤ x', from sub_le_self,
|
||||
have H2 : x' < succ x', from self_lt_succ,
|
||||
have H2 : x' < succ x', from !self_lt_succ,
|
||||
show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt_trans H1 H2
|
||||
|
||||
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
|
||||
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le)
|
||||
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
|
||||
calc
|
||||
|
|
@ -319,7 +319,7 @@ or.elim le_total
|
|||
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,
|
||||
sub_split
|
||||
(assume H2 : k ≤ m, zero_le)
|
||||
(assume H2 : k ≤ m, !zero_le)
|
||||
(take m' : ℕ,
|
||||
assume Hm : m + m' = k,
|
||||
have H3 : n ≤ k, from le_trans H (le_intro Hm),
|
||||
|
|
@ -357,7 +357,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
|
||||
|
|
@ -407,10 +407,10 @@ theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
|
|||
dist_comm ▸ dist_le H
|
||||
|
||||
theorem dist_zero_right {n : ℕ} : dist n 0 = n :=
|
||||
dist_ge zero_le ⬝ sub_zero_right
|
||||
dist_ge !zero_le ⬝ sub_zero_right
|
||||
|
||||
theorem dist_zero_left {n : ℕ} : dist 0 n = n :=
|
||||
dist_le zero_le ⬝ sub_zero_right
|
||||
dist_le !zero_le ⬝ sub_zero_right
|
||||
|
||||
theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m :=
|
||||
calc
|
||||
|
|
@ -479,7 +479,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
|
|||
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 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⁻¹
|
||||
|
|
@ -488,7 +488,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
|
|||
... = 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)
|
||||
|
||||
|
|
|
|||
|
|
@ -63,7 +63,7 @@ let f := rec_measure default measure rec_val in
|
|||
case_strong_induction_on m
|
||||
(take x,
|
||||
have H1 : f' 0 x = default, from rfl,
|
||||
have H2 : ¬ measure x < 0, from not_lt_zero,
|
||||
have H2 : ¬ measure x < 0, from !not_lt_zero,
|
||||
have H3 : restrict default measure f 0 x = default, from if_neg H2,
|
||||
show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
|
||||
(take m,
|
||||
|
|
@ -77,8 +77,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_le_trans 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_le_trans Hzx (lt_succ_imp_le H1))
|
||||
∎,
|
||||
have H2 : f' (succ m) x = rec_val x f,
|
||||
proof
|
||||
|
|
@ -94,15 +94,15 @@ case_strong_induction_on m
|
|||
assume Hzx : measure z < measure x,
|
||||
calc
|
||||
f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _
|
||||
... = f z : restrict_lt_eq _ _ _ _ _ Hzx
|
||||
... = f z : !restrict_lt_eq Hzx
|
||||
qed,
|
||||
have H3 : restrict default measure f (succ m) x = rec_val x f,
|
||||
proof
|
||||
calc
|
||||
restrict default measure f (succ m) x = f x : if_pos H1
|
||||
... = f' (succ m') x : eq.refl _
|
||||
... = f' (succ m') x : !eq.refl
|
||||
... = if measure x < succ m' then rec_val x (f' m') else default : rfl
|
||||
... = rec_val x (f' m') : if_pos self_lt_succ
|
||||
... = rec_val x (f' m') : if_pos !self_lt_succ
|
||||
... = rec_val x f : rec_decreasing _ _ _ H3a
|
||||
qed,
|
||||
show f' (succ m) x = restrict default measure f (succ m) x,
|
||||
|
|
|
|||
Loading…
Reference in a new issue