michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/nat): mark more arguments implicit

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-26 18:47:36 -07:00
parent b3615d5c8b
commit 6b7e79b62f
11 changed files with 695 additions and 767 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
doc/lean/calc.org
View file

@ -37,7 +37,7 @@ Here is an example
:= calc a = b : Ax1
... = c + 1 : Ax2
... = d + 1 : { Ax3 }
... = 1 + d : add_comm d 1
... = 1 + d : add_comm
... = e : symm Ax4.
#+END_SRC
@ -47,27 +47,8 @@ We can use =by <tactic>= or =by <solver>= to (try to) automatically construct th
proof expression using the given tactic or solver.
Even when tactics and solvers are not used, we can still use the elaboration engine to fill
gaps in our calculational proofs. In the previous examples, we can use =_= as arguments for the
=add_comm= theorem. The Lean elaboration engine will infer =d= and =1= for us.
Here is the same example using placeholders.
#+BEGIN_SRC lean
import data.nat
using nat
variables a b c d e : nat.
axiom Ax1 : a = b.
axiom Ax2 : b = c + 1.
axiom Ax3 : c = d.
axiom Ax4 : e = 1 + d.
theorem T : a = e
:= calc a = b : Ax1
... = c + 1 : Ax2
... = d + 1 : { Ax3 }
... = 1 + d : add_comm _ _
... = e : symm Ax4.
#+END_SRC
gaps in our calculational proofs. In the previous examples, the arguments for the
=add_comm= theorem are implicit. The Lean elaboration engine infers them automatically for us.
The =calc= command can be configured for any relation that supports
some form of transitivity. It can even combine different relations.
@ -79,8 +60,8 @@ some form of transitivity. It can even combine different relations.
theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0
:= calc a = b : H1
... = c + 1 : H2
... = succ c : add_one _
... ≠ 0 : succ_ne_zero _
... = succ c : add_one
... ≠ 0 : succ_ne_zero
#+END_SRC
The Lean simplifier can be used to reduce the size of calculational proofs.

4
doc/lean/tutorial.org
View file

@ -760,7 +760,7 @@ of two even numbers is an even number.
exists_intro (w1 + w2)
(calc a + b = 2*w1 + b : {Hw1}
... = 2*w1 + 2*w2 : {Hw2}
... = 2*(w1 + w2) : symm (mul_distr_left 2 w1 w2))))
... = 2*(w1 + w2) : symm mul_distr_left)))
#+END_SRC
@ -780,5 +780,5 @@ With this macro we can write the example above in a more natural way
exists_intro (w1 + w2)
(calc a + b = 2*w1 + b : {Hw1}
... = 2*w1 + 2*w2 : {Hw2}
... = 2*(w1 + w2) : symm (mul_distr_left 2 w1 w2))
... = 2*(w1 + w2) : symm mul_distr_left)
#+END_SRC

108
library/data/int/basic.lean
View file

@ -19,7 +19,7 @@ using relation
using decidable
using binary
using fake_simplifier
using eq_ops
namespace int
@ -34,34 +34,36 @@ H
-- add_rewrite rel_comp --local
theorem rel_refl (a : ℕ × ℕ) : rel a a :=
add_comm (pr1 a) (pr2 a)
theorem rel_refl {a : ℕ × ℕ} : rel a a :=
add_comm
theorem rel_symm {a b : ℕ × ℕ} (H : rel a b) : rel b a :=
calc
pr1 b + pr2 a = pr2 a + pr1 b : add_comm _ _
... = pr1 a + pr2 b : symm H
... = pr2 b + pr1 a : add_comm _ _
pr1 b + pr2 a = pr2 a + pr1 b : add_comm
... = pr1 a + pr2 b : H⁻¹
... = pr2 b + pr1 a : add_comm
theorem rel_trans {a b c : ℕ × ℕ} (H1 : rel a b) (H2 : rel b c) : rel a c :=
have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from
calc
pr1 a + pr2 c + pr2 b = pr1 a + pr2 b + pr2 c : by simp
... = pr2 a + pr1 b + pr2 c : {H1}
... = pr2 a + (pr1 b + pr2 c) : by simp
... = pr2 a + (pr2 b + pr1 c) : {H2}
... = pr2 a + pr1 c + pr2 b : by simp,
... = pr2 a + pr1 b + pr2 c : {H1}
... = pr2 a + (pr1 b + pr2 c) : by simp
... = pr2 a + (pr2 b + pr1 c) : {H2}
... = pr2 a + pr1 c + pr2 b : by simp,
show pr1 a + pr2 c = pr2 a + pr1 c, from add_cancel_right H3
theorem rel_equiv : is_equivalence rel :=
is_equivalence_mk (is_reflexive_mk rel_refl) (is_symmetric_mk @rel_symm)
(is_transitive_mk @rel_trans)
is_equivalence_mk
(is_reflexive_mk @rel_refl)
(is_symmetric_mk @rel_symm)
(is_transitive_mk @rel_trans)
theorem rel_flip {a b : ℕ × ℕ} (H : rel a b) : rel (flip a) (flip b) :=
calc
pr1 (flip a) + pr2 (flip b) = pr2 a + pr1 b : by simp
... = pr1 a + pr2 b : symm H
... = pr2 (flip a) + pr1 (flip b) : by simp
... = pr1 a + pr2 b : H⁻¹
... = pr2 (flip a) + pr1 (flip b) : by simp
-- ## The canonical representative of each equivalence class
@ -76,14 +78,14 @@ have H2 : ¬ pr1 a ≥ pr2 a, from lt_imp_not_ge H,
if_neg H2 _ _
theorem proj_le {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : proj a = pair 0 (pr2 a - pr1 a) :=
or_elim (le_or_gt (pr2 a) (pr1 a))
or_elim le_or_gt
(assume H2 : pr2 a ≤ pr1 a,
have H3 : pr1 a = pr2 a, from le_antisym H H2,
calc
proj a = pair (pr1 a - pr2 a) 0 : proj_ge H2
... = pair (pr1 a - pr2 a) (pr1 a - pr1 a) : {symm (sub_self (pr1 a))}
... = pair (pr1 a - pr2 a) (pr1 a - pr1 a) : {sub_self⁻¹}
... = pair (pr2 a - pr2 a) (pr2 a - pr1 a) : {H3}
... = pair 0 (pr2 a - pr1 a) : {sub_self (pr2 a)})
... = pair 0 (pr2 a - pr1 a) : {sub_self})
(assume H2 : pr1 a < pr2 a, proj_lt H2)
theorem proj_ge_pr1 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr1 (proj a) = pr1 a - pr2 a :=
@ -119,70 +121,70 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
have H4 : pr2 (proj (flip a)) = pr2 (flip (proj a)), from
calc
pr2 (proj (flip a)) = pr2 (flip a) - pr1 (flip a) : proj_le_pr2 H2
... = pr1 a - pr1 (flip a) : {flip_pr2 a}
... = pr1 a - pr2 a : {flip_pr1 a}
... = pr1 (proj a) : symm (proj_ge_pr1 H)
... = pr2 (flip (proj a)) : symm (flip_pr2 (proj a)),
... = pr1 a - pr1 (flip a) : {flip_pr2 a}
... = pr1 a - pr2 a : {flip_pr1 a}
... = pr1 (proj a) : (proj_ge_pr1 H)⁻¹
... = pr2 (flip (proj a)) : (flip_pr2 (proj a))⁻¹,
prod_eq H3 H4,
or_elim (le_total (pr2 a) (pr1 a))
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 H,
calc
proj (flip a) = flip (flip (proj (flip a))) : symm (flip_flip (proj (flip a)))
... = flip (proj (flip (flip a))) : {symm (special (flip a) H2)}
... = flip (proj a) : {flip_flip a})
... = flip (proj (flip (flip a))) : {symm (special (flip a) H2)}
... = flip (proj a) : {flip_flip a})
theorem proj_rel (a : ℕ × ℕ) : rel a (proj a) :=
or_elim (le_total (pr2 a) (pr1 a))
or_elim le_total
(assume H : pr2 a ≤ pr1 a,
calc
pr1 a + pr2 (proj a) = pr1 a + 0 : {proj_ge_pr2 H}
... = pr1 a : add_zero_right (pr1 a)
... = pr2 a + (pr1 a - pr2 a) : symm (add_sub_le H)
... = pr2 a + pr1 (proj a) : {symm (proj_ge_pr1 H)})
... = pr1 a : add_zero_right
... = pr2 a + (pr1 a - pr2 a) : (add_sub_le H)⁻¹
... = pr2 a + pr1 (proj a) : {(proj_ge_pr1 H)⁻¹})
(assume H : pr1 a ≤ pr2 a,
calc
pr1 a + pr2 (proj a) = pr1 a + (pr2 a - pr1 a) : {proj_le_pr2 H}
... = pr2 a : add_sub_le H
... = pr2 a + 0 : symm (add_zero_right (pr2 a))
... = pr2 a + pr1 (proj a) : {symm (proj_le_pr1 H)})
... = pr2 a : add_sub_le H
... = pr2 a + 0 : add_zero_right⁻¹
... = pr2 a + pr1 (proj a) : {(proj_le_pr1 H)⁻¹})
theorem proj_congr {a b : ℕ × ℕ} (H : rel a b) : proj a = proj b :=
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 subst H (le_refl (pr1 a + pr2 b)),
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
pr1 (proj a) = pr1 a - pr2 a : proj_ge_pr1 H2
... = pr1 a + pr2 b - pr2 b - pr2 a : {symm (sub_add_left (pr1 a) (pr2 b))}
pr1 (proj a) = pr1 a - pr2 a : proj_ge_pr1 H2
... = pr1 a + pr2 b - pr2 b - pr2 a : {sub_add_left⁻¹}
... = pr2 a + pr1 b - pr2 b - pr2 a : {H}
... = pr2 a + pr1 b - pr2 a - pr2 b : {sub_comm _ _ _}
... = pr1 b - pr2 b : {sub_add_left2 (pr2 a) (pr1 b)}
... = pr1 (proj b) : symm (proj_ge_pr1 H4),
... = pr2 a + pr1 b - pr2 a - pr2 b : {sub_comm}
... = pr1 b - pr2 b : {sub_add_left2}
... = pr1 (proj b) : (proj_ge_pr1 H4)⁻¹,
have H6 : pr2 (proj a) = pr2 (proj b), from
calc
pr2 (proj a) = 0 : proj_ge_pr2 H2
... = pr2 (proj b) : {symm (proj_ge_pr2 H4)},
prod_eq H5 H6,
or_elim (le_total (pr2 a) (pr1 a))
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 H2,
have H4 : proj (flip a) = proj (flip b), from special (flip a) (flip b) H3 (rel_flip H),
have H5 : flip (proj a) = flip (proj b), from subst (proj_flip a) (subst (proj_flip b) H4),
have H5 : flip (proj a) = flip (proj b), from proj_flip a ▸ proj_flip b ▸ H4,
show proj a = proj b, from flip_inj H5)
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 (pr2 a) (pr1 a))
(assume H : pr2 a ≤ pr1 a, or_intro_right _ (proj_ge_pr2 H))
(assume H : pr1 a ≤ pr2 a, or_intro_left _ (proj_le_pr1 H))
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))
theorem proj_idempotent (a : ℕ × ℕ) : proj (proj a) = proj a :=
representative_map_idempotent_equiv proj_rel @proj_congr a
@ -226,7 +228,7 @@ theorem to_nat_comp (n m : ℕ) : (to_nat (psub (pair n m))) = dist n m :=
have H : ∀v w : ℕ × ℕ, rel v w → dist (pr1 v) (pr2 v) = dist (pr1 w) (pr2 w),
from take v w H, dist_eq_intro H,
have H2 : ∀v : ℕ × ℕ, (to_nat (psub v)) = dist (pr1 v) (pr2 v),
from take v, (comp_constant quotient H (rel_refl v)),
from take v, (comp_constant quotient H rel_refl),
iff_mp (by simp) H2 (pair n m)
-- add_rewrite to_nat_comp --local
@ -266,7 +268,7 @@ notation `-` x:100 := neg x
theorem neg_comp (n m : ℕ) : -(psub (pair n m)) = psub (pair m n) :=
have H : ∀a, -(psub a) = psub (flip a),
from take a, comp_quotient_map quotient @rel_flip (rel_refl _),
from take a, comp_quotient_map quotient @rel_flip rel_refl,
calc
-(psub (pair n m)) = psub (flip (pair n m)) : H (pair n m)
... = psub (pair m n) : by simp
@ -295,12 +297,12 @@ by simp
theorem pos_eq_neg {n m : ℕ} (H : n = -m) : n = 0 ∧ m = 0 :=
have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl (n),
have H3 : psub (pair n 0) = psub (pair 0 m), from iff_mp (by simp) H,
have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H3,
have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient @rel_refl H3,
have H5 : n + m = 0, from
calc
n + m = pr1 (pair n 0) + pr2 (pair 0 m) : by simp
... = pr2 (pair n 0) + pr1 (pair 0 m) : H4
... = 0 : by simp,
... = 0 : by simp,
add_eq_zero H5
-- add_rewrite to_nat_neg
@ -356,7 +358,7 @@ or_elim (cases a)
(take k : ℕ,
assume H3 : n = succ k,
have H4 : a = -(of_nat (succ k)), from subst H3 H2,
or_intro_right _ (exists_intro k H4)))
or_inr (exists_intro k H4)))
theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ)
(H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-(of_nat (succ n)))) : P a :=
@ -370,7 +372,7 @@ have H2 : n = psub (pair 0 m), from
n = -m : H
... = -(psub (pair m 0)) : refl (-m)
... = psub (pair 0 m) : by simp,
have H3 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H2,
have H3 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient @rel_refl H2,
have H4 : n + m = 0, from
calc
n + m = pr1 (pair n 0) + pr2 (pair 0 m) : by simp
@ -396,8 +398,8 @@ infixl `+` := int.add
theorem add_comp (n m k l : ℕ) : psub (pair n m) + psub (pair k l) = psub (pair (n + k) (m + l)) :=
have H : ∀a b, psub a + psub b = psub (map_pair2 nat.add a b),
from comp_quotient_map_binary_refl rel_refl quotient @rel_add,
trans (H (pair n m) (pair k l)) (by simp)
from comp_quotient_map_binary_refl @rel_refl quotient @rel_add,
H (pair n m) (pair k l) ⬝ by simp
-- add_rewrite add_comp --local
@ -446,7 +448,7 @@ theorem to_nat_add_le (a b : ℤ) : to_nat (a + b) ≤ to_nat a + to_nat b :=
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
have H : dist (xa + xb) (ya + yb) ≤ dist xa ya + dist xb yb,
from dist_add_le_add_dist xa xb ya yb,
from dist_add_le_add_dist,
by simp
-- TODO: note, we have to add #nat to get the right interpretation
@ -635,7 +637,7 @@ theorem mul_comp (n m k l : ℕ) :
psub (pair n m) * psub (pair k l) = psub (pair (n * k + m * l) (n * l + m * k)) :=
have H : ∀u v,
psub u * psub v = psub (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v)),
from comp_quotient_map_binary_refl rel_refl quotient @rel_mul,
from comp_quotient_map_binary_refl @rel_refl quotient @rel_mul,
trans (H (pair n m) (pair k l)) (by simp)
-- add_rewrite mul_comp
@ -719,7 +721,7 @@ theorem mul_to_nat (a b : ℤ) : (to_nat (a * b)) = #nat (to_nat a) * (to_nat b)
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
have H : dist xa ya * dist xb yb = dist (xa * xb + ya * yb) (xa * yb + ya * xb),
from dist_mul_dist xa ya xb yb,
from dist_mul_dist,
by simp
-- add_rewrite mul_zero_left mul_zero_right mul_one_right mul_one_left

74
library/data/int/order.lean
View file

@ -118,17 +118,17 @@ discriminate
(assume H2 : n = 0,
have H3 : a = b, from
calc
a = a + 0 : symm (add_zero_right a)
... = a + n : {symm H2}
... = b : Hn,
a = a + 0 : symm (add_zero_right a)
... = a + n : {symm H2}
... = b : Hn,
or_intro_right _ H3)
(take k : ℕ,
assume H2 : n = succ k,
have H3 : a + 1 + k = b, from
calc
a + 1 + k = a + succ k : by simp
... = a + n : by simp
... = b : Hn,
a + 1 + k = a + succ k : by simp
... = a + n : by simp
... = b : Hn,
or_intro_left _ (le_intro H3))
-- ### interaction with neg and sub
@ -224,11 +224,11 @@ not_intro
obtain (n : ℕ) (Hn : a + succ n = a), from lt_elim H,
have H2 : a + succ n = a + 0, from
calc
a + succ n = a : Hn
... = a + 0 : by simp,
a + succ n = a : Hn
... = a + 0 : by simp,
have H3 : succ n = 0, from add_cancel_left H2,
have H4 : succ n = 0, from of_nat_inj H3,
absurd H4 (succ_ne_zero n))
absurd H4 succ_ne_zero)
theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b :=
not_intro (assume H2 : a = b, absurd (subst H2 H) (lt_irrefl b))
@ -366,24 +366,24 @@ int_by_cases a
(take n : ℕ,
int_by_cases_succ b
(take m : ℕ,
show of_nat n ≤ m ∨ of_nat n > m, by simp) -- from (by simp) ◂ (le_or_gt n m))
show of_nat n ≤ m ∨ of_nat n > m, by simp) -- from (by simp) ◂ (le_or_gt n m))
(take m : ℕ,
show n ≤ -succ m ∨ n > -succ m, from
have H0 : -succ m < -m, from lt_neg (subst (symm (of_nat_succ m)) (self_lt_succ m)),
have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n),
or_intro_right _ H))
show n ≤ -succ m ∨ n > -succ m, from
have H0 : -succ m < -m, from lt_neg (subst (symm (of_nat_succ m)) (self_lt_succ m)),
have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n),
or_intro_right _ H))
(take n : ℕ,
int_by_cases_succ b
(take m : ℕ,
show -n ≤ m ∨ -n > m, from
or_intro_left _ (neg_le_pos n m))
show -n ≤ m ∨ -n > m, from
or_intro_left _ (neg_le_pos n m))
(take m : ℕ,
show -n ≤ -succ m ∨ -n > -succ m, from
or_imp_or (le_or_gt (succ m) n)
(assume H : succ m ≤ n,
le_neg (iff_elim_left (iff_symm (le_of_nat (succ m) n)) H))
(assume H : succ m > n,
lt_neg (iff_elim_left (iff_symm (lt_of_nat n (succ m))) H))))
show -n ≤ -succ m ∨ -n > -succ m, from
or_imp_or le_or_gt
(assume H : succ m ≤ n,
le_neg (iff_elim_left (iff_symm (le_of_nat (succ m) n)) H))
(assume H : succ m > n,
lt_neg (iff_elim_left (iff_symm (lt_of_nat n (succ m))) H))))
theorem trichotomy_alt (a b : ℤ) : (a < b ∨ a = b) ∨ a > b :=
or_imp_or_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H)
@ -422,15 +422,15 @@ obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
subst (symm 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
theorem le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
have aux : ∀x, decidable (0 ≤ x), from
take x,
have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from
iff_intro
(assume H1, to_nat_nonneg_eq H1)
(assume H1, subst H1 (of_nat_nonneg (to_nat x))),
(assume H1, to_nat_nonneg_eq H1)
(assume H1, subst H1 (of_nat_nonneg (to_nat x))),
decidable_iff_equiv _ (iff_symm H),
decidable_iff_equiv (aux _) (iff_symm (le_iff_sub_nonneg a b))
@ -609,21 +609,21 @@ or_elim (em (a = 0))
or_elim (em (b = 0))
(assume Hb : b = 0, by simp)
(assume Hb : b ≠ 0,
have H : sign (a * b) * (to_nat (a * b)) = sign a * sign b * (to_nat (a * b)), from
calc
sign (a * b) * (to_nat (a * b)) = a * b : mul_sign_to_nat (a * b)
... = sign a * (to_nat a) * b : {symm (mul_sign_to_nat a)}
... = sign a * (to_nat a) * (sign b * (to_nat b)) : {symm (mul_sign_to_nat b)}
... = sign a * sign b * (to_nat (a * b)) : by simp,
have H2 : (to_nat (a * b)) ≠ 0, from
take H2', mul_ne_zero Ha Hb (to_nat_eq_zero H2'),
have H3 : (to_nat (a * b)) ≠ of_nat 0, from mt of_nat_inj H2,
mul_cancel_right H3 H))
have H : sign (a * b) * (to_nat (a * b)) = sign a * sign b * (to_nat (a * b)), from
calc
sign (a * b) * (to_nat (a * b)) = a * b : mul_sign_to_nat (a * b)
... = sign a * (to_nat a) * b : {symm (mul_sign_to_nat a)}
... = sign a * (to_nat a) * (sign b * (to_nat b)) : {symm (mul_sign_to_nat b)}
... = sign a * sign b * (to_nat (a * b)) : by simp,
have H2 : (to_nat (a * b)) ≠ 0, from
take H2', mul_ne_zero Ha Hb (to_nat_eq_zero H2'),
have H3 : (to_nat (a * b)) ≠ of_nat 0, from mt of_nat_inj H2,
mul_cancel_right H3 H))
--set_option pp::coercion true
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 0),
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)
@ -631,7 +631,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 n))
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 :=

18
library/data/list/basic.lean
View file

@ -76,23 +76,23 @@ list_induction_on s (refl _)
definition length : list T → ℕ := list_rec 0 (fun x l m, succ m)
theorem length_nil : length (@nil T) = 0 := refl _
theorem length_nil : length (@nil T) = 0 := rfl
theorem length_cons (x : T) (t : list T) : length (x :: t) = succ (length t) := refl _
theorem length_cons (x : T) (t : list T) : length (x :: t) = succ (length t) := rfl
theorem length_concat (s t : list T) : length (s ++ t) = length s + length t :=
list_induction_on s
(calc
length (concat nil t) = length t : refl _
... = zero + length t : {symm (add_zero_left (length t))}
... = length (@nil T) + length t : refl _)
length (concat nil t) = length t : rfl
... = zero + length t : {add_zero_left⁻¹}
... = length (@nil T) + length t : rfl)
(take x s,
assume H : length (concat s t) = length s + length t,
calc
length (concat (cons x s) t ) = succ (length (concat s t)) : refl _
... = succ (length s + length t) : { H }
... = succ (length s) + length t : {symm (add_succ_left _ _)}
... = length (cons x s) + length t : refl _)
length (concat (cons x s) t ) = succ (length (concat s t)) : rfl
... = succ (length s + length t) : { H }
... = succ (length s) + length t : {add_succ_left⁻¹}
... = length (cons x s) + length t : rfl)
-- add_rewrite length_nil length_cons

273
library/data/nat/basic.lean
View file

@ -12,10 +12,8 @@ import logic data.num tools.tactic struc.binary tools.helper_tactics
using num tactic binary eq_ops
using decidable (hiding induction_on rec_on)
using relation -- for subst_iff
using helper_tactics
-- Definition of the type
-- ----------------------
@ -53,7 +51,7 @@ num_rec zero
-- Successor and predecessor
-- -------------------------
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
theorem succ_ne_zero {n : ℕ} : succ n ≠ 0 :=
assume H : succ n = 0,
have H2 : true = false, from
let f := (nat_rec false (fun a b, true)) in
@ -97,10 +95,10 @@ calc
... = pred (succ m) : {H}
... = m : pred_succ m
theorem succ_ne_self (n : ℕ) : succ n ≠ n :=
theorem succ_ne_self {n : ℕ} : succ n ≠ n :=
induction_on n
(take H : 1 = 0,
have ne : 1 ≠ 0, from succ_ne_zero 0,
have ne : 1 ≠ 0, from succ_ne_zero,
absurd H ne)
(take k IH H, IH (succ_inj H))
@ -110,10 +108,10 @@ have general : ∀n, decidable (n = m), from
(take n,
rec_on n
(inl (refl 0))
(λ m iH, inr (succ_ne_zero m)))
(λ m iH, inr succ_ne_zero))
(λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')),
take n, rec_on n
(inr (ne_symm (succ_ne_zero m')))
(inr (ne_symm succ_ne_zero))
(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
have d1 : decidable (n' = m'), from iH1 n',
decidable.rec_on d1
@ -143,14 +141,10 @@ have general : ∀m, P n m, from induction_on n
assume IH : ∀m, P k m,
take m : ℕ,
discriminate
(assume Hm : m = 0,
Hm⁻¹ ▸ (H2 k))
(take l : ℕ,
assume Hm : m = succ l,
Hm⁻¹ ▸ (H3 k l (IH l)))),
(assume Hm : m = 0, Hm⁻¹ ▸ (H2 k))
(take l : ℕ, assume Hm : m = succ l, Hm⁻¹ ▸ (H3 k l (IH l)))),
general m
-- Addition
-- --------
@ -158,67 +152,57 @@ definition add (x y : ℕ) : ℕ := plus x y
infixl `+` := add
theorem add_zero_right (n : ℕ) : n + 0 = n
theorem add_zero_right {n : ℕ} : n + 0 = n
theorem add_succ_right (n m : ℕ) : n + succ m = succ (n + m)
theorem add_succ_right {n m : ℕ} : n + succ m = succ (n + m)
opaque_hint (hiding add)
theorem add_zero_left (n : ℕ) : 0 + n = n :=
theorem add_zero_left {n : ℕ} : 0 + n = n :=
induction_on n
(add_zero_right 0)
add_zero_right
(take m IH, show 0 + succ m = succ m, from
calc
0 + succ m = succ (0 + m) : add_succ_right _ _
0 + succ m = succ (0 + m) : add_succ_right
... = succ m : {IH})
theorem add_succ_left (n m : ℕ) : (succ n) + m = succ (n + m) :=
theorem add_succ_left {n m : ℕ} : (succ n) + m = succ (n + m) :=
induction_on m
(calc
succ n + 0 = succ n : add_zero_right (succ n)
... = succ (n + 0) : {symm (add_zero_right n)})
(take k IH,
calc
succ n + succ k = succ (succ n + k) : add_succ_right _ _
... = succ (succ (n + k)) : {IH}
... = succ (n + succ k) : {symm (add_succ_right _ _)})
(add_zero_right ▸ add_zero_right)
(take k IH, calc
succ n + succ k = succ (succ n + k) : add_succ_right
... = succ (succ (n + k)) : {IH}
... = succ (n + succ k) : {add_succ_right⁻¹})
theorem add_comm (n m : ℕ) : n + m = m + n :=
theorem add_comm {n m : ℕ} : n + m = m + n :=
induction_on m
(trans (add_zero_right _) (symm (add_zero_left _)))
(take k IH,
calc
n + succ k = succ (n+k) : add_succ_right _ _
... = succ (k + n) : {IH}
... = succ k + n : symm (add_succ_left _ _))
(add_zero_right ⬝ add_zero_left⁻¹)
(take k IH, calc
n + succ k = succ (n+k) : add_succ_right
... = succ (k + n) : {IH}
... = succ k + n : add_succ_left⁻¹)
theorem add_move_succ (n m : ℕ) : succ n + m = n + succ m :=
calc
succ n + m = succ (n + m) : add_succ_left n m
... = n +succ m : symm (add_succ_right n m)
theorem add_move_succ {n m : ℕ} : succ n + m = n + succ m :=
add_succ_left ⬝ add_succ_right⁻¹
theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n :=
calc
n + succ m = succ n + m : symm (add_move_succ n m)
... = m + succ n : add_comm (succ n) m
theorem add_comm_succ {n m : ℕ} : n + succ m = m + succ n :=
add_move_succ⁻¹ ⬝ add_comm
theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k) :=
theorem add_assoc {n m k : ℕ} : (n + m) + k = n + (m + k) :=
induction_on k
(calc
(n + m) + 0 = n + m : add_zero_right _
... = n + (m + 0) : {symm (add_zero_right m)})
(add_zero_right ▸ add_zero_right)
(take l IH,
calc
(n + m) + succ l = succ ((n + m) + l) : add_succ_right _ _
... = succ (n + (m + l)) : {IH}
... = n + succ (m + l) : symm (add_succ_right _ _)
... = n + (m + succ l) : {symm (add_succ_right _ _)})
(n + m) + succ l = succ ((n + m) + l) : add_succ_right
... = succ (n + (m + l)) : {IH}
... = n + succ (m + l) : add_succ_right⁻¹
... = n + (m + succ l) : {add_succ_right⁻¹})
theorem add_left_comm (n m k : ℕ) : n + (m + k) = m + (n + k) :=
left_comm add_comm add_assoc n m k
theorem add_left_comm {n m k : ℕ} : n + (m + k) = m + (n + k) :=
left_comm @add_comm @add_assoc n m k
theorem add_right_comm (n m k : ℕ) : n + m + k = n + k + m :=
right_comm add_comm add_assoc n m k
theorem add_right_comm {n m k : ℕ} : n + m + k = n + k + m :=
right_comm @add_comm @add_assoc n m k
-- add_rewrite add_zero_left add_zero_right
-- add_rewrite add_succ_left add_succ_right
@ -229,180 +213,157 @@ right_comm add_comm add_assoc n m k
theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k :=
induction_on n
(take H : 0 + m = 0 + k,
calc
m = 0 + m : symm (add_zero_left m)
... = 0 + k : H
... = k : add_zero_left k)
add_zero_left⁻¹ ⬝ H ⬝ add_zero_left)
(take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
have H2 : succ (n + m) = succ (n + k),
from calc
succ (n + m) = succ n + m : symm (add_succ_left n m)
... = succ n + k : H
... = succ (n + k) : add_succ_left n k,
succ (n + m) = succ n + m : add_succ_left⁻¹
... = succ n + k : H
... = succ (n + k) : add_succ_left,
have H3 : n + m = n + k, from succ_inj H2,
IH H3)
theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
have H2 : m + n = m + k,
from calc
m + n = n + m : add_comm m n
... = k + m : H
... = m + k : add_comm k m,
have H2 : m + n = m + k, from add_comm ⬝ H ⬝ add_comm,
add_cancel_left H2
theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0 :=
induction_on n
(take (H : 0 + m = 0), refl 0)
(take k IH,
assume (H : succ k + m = 0),
assume H : succ k + m = 0,
absurd
(show succ (k + m) = 0, from
calc
succ (k + m) = succ k + m : symm (add_succ_left k m)
... = 0 : H)
(succ_ne_zero (k + m)))
(show succ (k + m) = 0, from calc
succ (k + m) = succ k + m : add_succ_left⁻¹
... = 0 : H)
succ_ne_zero)
theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 :=
add_eq_zero_left (trans (add_comm m n) H)
add_eq_zero_left (add_comm ⬝ H)
theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 :=
and_intro (add_eq_zero_left H) (add_eq_zero_right H)
-- ### misc
theorem add_one (n : ℕ) : n + 1 = succ n :=
calc
n + 1 = succ (n + 0) : add_succ_right _ _
... = succ n : {add_zero_right _}
theorem add_one {n : ℕ} : n + 1 = succ n :=
add_zero_right ▸ add_succ_right
theorem add_one_left (n : ℕ) : 1 + n = succ n :=
calc
1 + n = succ (0 + n) : add_succ_left _ _
... = succ n : {add_zero_left _}
theorem add_one_left {n : ℕ} : 1 + n = succ n :=
add_zero_left ▸ add_succ_left
-- TODO: rename? remove?
theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0)
(H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a :=
nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
nat_rec H1 (take n IH, add_one ▸ (H2 n IH)) a
-- Multiplication
-- --------------
definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
infixl `*` := mul
theorem mul_zero_right (n:ℕ) : n * 0 = 0
theorem mul_zero_right {n : ℕ} : n * 0 = 0
theorem mul_succ_right (n m:ℕ) : n * succ m = n * m + n
theorem mul_succ_right {n m : ℕ} : n * succ m = n * m + n
opaque_hint (hiding mul)
-- ### commutativity, distributivity, associativity, identity
theorem mul_zero_left (n:ℕ) : 0 * n = 0 :=
theorem mul_zero_left {n : ℕ} : 0 * n = 0 :=
induction_on n
(mul_zero_right 0)
(take m IH,
calc
0 * succ m = 0 * m + 0 : mul_succ_right _ _
... = 0 * m : add_zero_right _
... = 0 : IH)
mul_zero_right
(take m IH, mul_succ_right ⬝ add_zero_right ⬝ IH)
theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m :=
theorem mul_succ_left {n m : ℕ} : (succ n) * m = (n * m) + m :=
induction_on m
(calc
succ n * 0 = 0 : mul_zero_right _
... = n * 0 : symm (mul_zero_right _)
... = n * 0 + 0 : symm (add_zero_right _))
(take k IH,
calc
succ n * succ k = (succ n * k) + succ n : mul_succ_right _ _
... = (n * k) + k + succ n : { IH }
... = (n * k) + (k + succ n) : add_assoc _ _ _
... = (n * k) + (n + succ k) : {add_comm_succ _ _}
... = (n * k) + n + succ k : symm (add_assoc _ _ _)
... = (n * succ k) + succ k : {symm (mul_succ_right n k)})
(mul_zero_right ⬝ mul_zero_right⁻¹ ⬝ add_zero_right⁻¹)
(take k IH, calc
succ n * succ k = (succ n * k) + succ n : mul_succ_right
... = (n * k) + k + succ n : {IH}
... = (n * k) + (k + succ n) : add_assoc
... = (n * k) + (n + succ k) : {add_comm_succ}
... = (n * k) + n + succ k : add_assoc⁻¹
... = (n * succ k) + succ k : {mul_succ_right⁻¹})
theorem mul_comm (n m:ℕ) : n * m = m * n :=
theorem mul_comm {n m : ℕ} : n * m = m * n :=
induction_on m
(trans (mul_zero_right _) (symm (mul_zero_left _)))
(take k IH,
calc
n * succ k = n * k + n : mul_succ_right _ _
... = k * n + n : {IH}
... = (succ k) * n : symm (mul_succ_left _ _))
(mul_zero_right ⬝ mul_zero_left⁻¹)
(take k IH, calc
n * succ k = n * k + n : mul_succ_right
... = k * n + n : {IH}
... = (succ k) * n : mul_succ_left⁻¹)
theorem mul_distr_right (n m k : ℕ) : (n + m) * k = n * k + m * k :=
theorem mul_distr_right {n m k : ℕ} : (n + m) * k = n * k + m * k :=
induction_on k
(calc
(n + m) * 0 = 0 : mul_zero_right _
... = 0 + 0 : symm (add_zero_right _)
... = n * 0 + 0 : {symm (mul_zero_right _)}
... = n * 0 + m * 0 : {symm (mul_zero_right _)})
(n + m) * 0 = 0 : mul_zero_right
... = 0 + 0 : add_zero_right⁻¹
... = n * 0 + 0 : {mul_zero_right⁻¹}
... = n * 0 + m * 0 : {mul_zero_right⁻¹})
(take l IH, calc
(n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _
... = n * l + m * l + (n + m) : {IH}
... = n * l + m * l + n + m : symm (add_assoc _ _ _)
... = n * l + n + m * l + m : {add_right_comm _ _ _}
... = n * l + n + (m * l + m) : add_assoc _ _ _
... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
(n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right
... = n * l + m * l + (n + m) : {IH}
... = n * l + m * l + n + m : add_assoc⁻¹
... = n * l + n + m * l + m : {add_right_comm}
... = n * l + n + (m * l + m) : add_assoc
... = n * succ l + (m * l + m) : {mul_succ_right⁻¹}
... = n * succ l + m * succ l : {mul_succ_right⁻¹})
theorem mul_distr_left (n m k : ℕ) : n * (m + k) = n * m + n * k :=
theorem mul_distr_left {n m k : ℕ} : n * (m + k) = n * m + n * k :=
calc
n * (m + k) = (m + k) * n : mul_comm _ _
... = m * n + k * n : mul_distr_right _ _ _
... = n * m + k * n : {mul_comm _ _}
... = n * m + n * k : {mul_comm _ _}
n * (m + k) = (m + k) * n : mul_comm
... = m * n + k * n : mul_distr_right
... = n * m + k * n : {mul_comm}
... = n * m + n * k : {mul_comm}
theorem mul_assoc (n m k:ℕ) : (n * m) * k = n * (m * k) :=
theorem mul_assoc {n m k : ℕ} : (n * m) * k = n * (m * k) :=
induction_on k
(calc
(n * m) * 0 = 0 : mul_zero_right _
... = n * 0 : symm (mul_zero_right _)
... = n * (m * 0) : {symm (mul_zero_right _)})
(n * m) * 0 = 0 : mul_zero_right
... = n * 0 : mul_zero_right⁻¹
... = n * (m * 0) : {mul_zero_right⁻¹})
(take l IH,
calc
(n * m) * succ l = (n * m) * l + n * m : mul_succ_right _ _
... = n * (m * l) + n * m : {IH}
... = n * (m * l + m) : symm (mul_distr_left _ _ _)
... = n * (m * succ l) : {symm (mul_succ_right _ _)})
(n * m) * succ l = (n * m) * l + n * m : mul_succ_right
... = n * (m * l) + n * m : {IH}
... = n * (m * l + m) : mul_distr_left⁻¹
... = n * (m * succ l) : {mul_succ_right⁻¹})
theorem mul_left_comm (n m k : ℕ) : n * (m * k) = m * (n * k) :=
left_comm mul_comm mul_assoc n m k
theorem mul_left_comm {n m k : ℕ} : n * (m * k) = m * (n * k) :=
left_comm @mul_comm @mul_assoc n m k
theorem mul_right_comm (n m k : ℕ) : n * m * k = n * k * m :=
right_comm mul_comm mul_assoc n m k
theorem mul_right_comm {n m k : ℕ} : n * m * k = n * k * m :=
right_comm @mul_comm @mul_assoc n m k
theorem mul_one_right (n : ℕ) : n * 1 = n :=
theorem mul_one_right {n : ℕ} : n * 1 = n :=
calc
n * 1 = n * 0 + n : mul_succ_right n 0
... = 0 + n : {mul_zero_right n}
... = n : add_zero_left n
n * 1 = n * 0 + n : mul_succ_right
... = 0 + n : {mul_zero_right}
... = n : add_zero_left
theorem mul_one_left (n : ℕ) : 1 * n = n :=
theorem mul_one_left {n : ℕ} : 1 * n = n :=
calc
1 * n = n * 1 : mul_comm _ _
... = n : mul_one_right n
1 * n = n * 1 : mul_comm
... = n : mul_one_right
theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 :=
discriminate
(take Hn : n = 0, or_intro_left _ Hn)
(take Hn : n = 0, or_inl Hn)
(take (k : ℕ),
assume (Hk : n = succ k),
discriminate
(take (Hm : m = 0), or_intro_right _ Hm)
(take (Hm : m = 0), or_inr Hm)
(take (l : ℕ),
assume (Hl : m = succ l),
have Heq : succ (k * succ l + l) = n * m, from
symm (calc
n * m = n * succ l : {Hl}
... = succ k * succ l : {Hk}
... = k * succ l + succ l : mul_succ_left _ _
... = succ (k * succ l + l) : add_succ_right _ _),
absurd (trans Heq H) (succ_ne_zero _)))
n * m = n * succ l : {Hl}
... = succ k * succ l : {Hk}
... = k * succ l + succ l : mul_succ_left
... = succ (k * succ l + l) : add_succ_right),
absurd (trans Heq H) succ_ne_zero))
---other inversion theorems appear below

244
library/data/nat/div.lean
View file

@ -16,6 +16,7 @@ import tools.fake_simplifier
using nat relation relation.iff_ops prod
using fake_simplifier decidable
using eq_ops
namespace nat
@ -79,7 +80,7 @@ case_strong_induction_on m
have H2 : restrict default measure f 0 = (λx, default), from
funext
(take x,
have H3 [fact]: ¬ measure x < 0, from not_lt_zero _,
have H3 [fact]: ¬ measure x < 0, from not_lt_zero,
show restrict default measure f 0 x = default, from if_neg H3 _ _),
show f' 0 = restrict default measure f 0, from trans H1 (symm H2))
(take m,
@ -93,7 +94,7 @@ case_strong_induction_on m
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
... = rec_val x (f' m) : if_pos H1 _ _
... = rec_val x (restrict default measure f m) : {IH m (le_refl m)}
... = rec_val x (restrict default measure f m) : {IH m le_refl}
... = rec_val x f : symm (rec_decreasing _ _ _ (lt_succ_imp_le H1)),
have H3 : restrict default measure f (succ m) x = rec_val x f, from
let m' := measure x in
@ -101,9 +102,9 @@ case_strong_induction_on m
restrict default measure f (succ m) x = f x : if_pos H1 _ _
... = f' (succ m') x : 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 (restrict default measure f m') : {IH m' (lt_succ_imp_le H1)}
... = rec_val x f : symm (rec_decreasing _ _ _ (le_refl _)),
... = rec_val x f : (rec_decreasing _ _ _ le_refl)⁻¹,
show f' (succ m) x = restrict default measure f (succ m) x,
from trans H2 (symm H3))
(assume H1 : ¬ measure x < succ m,
@ -127,11 +128,11 @@ let f' := rec_measure_aux default measure rec_val in
let f := rec_measure default measure rec_val in
let m := measure x in
calc
f x = f' (succ m) x : refl _
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 (restrict default measure f m) : {rec_measure_aux_spec _ _ _ rec_decreasing _}
... = rec_val x f : symm (rec_decreasing _ _ _ (le_refl _))
... = rec_val x f : (rec_decreasing _ _ _ le_refl)⁻¹
-- Div and mod
@ -174,7 +175,7 @@ definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x
infixl `div` := idivide -- copied from Isabelle
theorem div_zero (x : ℕ) : x div 0 = 0 :=
theorem div_zero {x : ℕ} : x div 0 = 0 :=
trans (div_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _)
-- add_rewrite div_zero
@ -184,8 +185,8 @@ trans (div_aux_spec _ _) (if_pos (or_intro_right _ H) _ _)
-- add_rewrite div_less
theorem zero_div (y : ℕ) : 0 div y = 0 :=
case y (div_zero 0) (take y', div_less (succ_pos _))
theorem zero_div {y : ℕ} : 0 div y = 0 :=
case y div_zero (take y', div_less succ_pos)
-- add_rewrite zero_div
@ -194,23 +195,23 @@ 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 _) (subst H5 H1))
(assume H5 : y = 0, not_elim lt_irrefl (subst H5 H1))
(assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
trans (div_aux_spec _ _) (if_neg H3 _ _)
theorem div_add_self_right (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
have H1 : z ≤ x + z, by simp,
let H2 := div_rec H H1 in
by simp
theorem div_add_mul_self_right (x y : ℕ) {z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
theorem div_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
induction_on y (by simp)
(take y,
assume IH : (x + y * z) div z = x div z + y,
calc
(x + succ y * z) div z = (x + y * z + z) div z : by simp
... = succ ((x + y * z) div z) : div_add_self_right _ H
... = x div z + succ y : by simp)
(x + succ y * z) div z = (x + y * z + z) div z : by simp
... = succ ((x + y * z) div z) : div_add_self_right H
... = x div z + succ y : by simp)
-- ### The definition of mod
@ -250,7 +251,7 @@ definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x
infixl `mod` := modulo
theorem mod_zero (x : ℕ) : x mod 0 = x :=
theorem mod_zero {x : ℕ} : x mod 0 = x :=
trans (mod_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _)
-- add_rewrite mod_zero
@ -260,8 +261,8 @@ trans (mod_aux_spec _ _) (if_pos (or_intro_right _ H) _ _)
-- add_rewrite mod_lt_eq
theorem zero_mod (y : ℕ) : 0 mod y = 0 :=
case y (mod_zero 0) (take y', mod_lt_eq (succ_pos _))
theorem zero_mod {y : ℕ} : 0 mod y = 0 :=
case y mod_zero (take y', mod_lt_eq succ_pos)
-- add_rewrite zero_mod
@ -270,64 +271,64 @@ 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 _) (subst H5 H1))
(assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
(assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
trans (mod_aux_spec _ _) (if_neg H3 _ _)
-- need more of these, add as rewrite rules
theorem mod_add_self_right (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) mod z = x mod z :=
theorem mod_add_self_right {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z :=
have H1 : z ≤ x + z, by simp,
let H2 := mod_rec H H1 in
by simp
theorem mod_add_mul_self_right (x y : ℕ) {z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
theorem mod_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
induction_on y (by simp)
(take y,
assume IH : (x + y * z) mod z = x mod z,
calc
(x + succ y * z) mod z = (x + y * z + z) mod z : by simp
... = (x + y * z) mod z : mod_add_self_right _ H
... = x mod z : IH)
... = (x + y * z) mod z : mod_add_self_right H
... = x mod z : IH)
theorem mod_mul_self_right (m n : ℕ) : (m * n) mod n = 0 :=
theorem mod_mul_self_right {m n : ℕ} : (m * n) mod n = 0 :=
case_zero_pos n (by simp)
(take n,
assume npos : n > 0,
subst (by simp) (mod_add_mul_self_right 0 m npos))
(by simp) ▸ (@mod_add_mul_self_right 0 m _ npos))
-- add_rewrite mod_mul_self_right
theorem mod_mul_self_left (m n : ℕ) : (m * n) mod m = 0 :=
subst (mul_comm _ _) (mod_mul_self_right _ _)
theorem mod_mul_self_left {m n : ℕ} : (m * n) mod m = 0 :=
mul_comm ▸ mod_mul_self_right
-- add_rewrite mod_mul_self_left
-- ### properties of div and mod together
theorem mod_lt (x : ℕ) {y : ℕ} (H : y > 0) : x mod y < y :=
theorem mod_lt {x y : ℕ} (H : y > 0) : x mod y < y :=
case_strong_induction_on x
(show 0 mod y < y, from subst (symm (zero_mod _)) H)
(show 0 mod y < y, from zero_mod⁻¹ ▸ H)
(take x,
assume IH : ∀x', x' ≤ x → x' mod y < y,
show succ x mod y < y, from
by_cases -- (succ x < y)
(assume H1 : succ x < y,
have H2 : succ x mod y = succ x, from mod_lt_eq H1,
show succ x mod y < y, from subst (symm H2) 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 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 subst (symm H3) (IH _ H5)))
theorem div_mod_eq (x y : ℕ) : x = x div y * y + x mod y :=
theorem div_mod_eq {x y : ℕ} : x = x div y * y + x mod y :=
case_zero_pos y
(show x = x div 0 * 0 + x mod 0, from
symm (calc
x div 0 * 0 + x mod 0 = 0 + x mod 0 : {mul_zero_right _}
... = x mod 0 : add_zero_left _
... = x : mod_zero _))
x div 0 * 0 + x mod 0 = 0 + x mod 0 : {mul_zero_right}
... = x mod 0 : add_zero_left
... = x : mod_zero))
(take y,
assume H : y > 0,
show x = x div y * y + x mod y, from
@ -345,94 +346,94 @@ 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,
symm (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 : {mul_succ_left _ _}
... = ((succ x - y) div y) * y + y + succ x mod y : {mul_succ_left}
... = ((succ x - y) div y) * y + y + (succ x - y) mod y : {H4}
... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add_right_comm _ _ _
... = succ x - y + y : {symm (IH _ H6)}
... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add_right_comm
... = succ x - y + y : {(IH _ H6)⁻¹}
... = succ x : add_sub_ge_left H2))))
theorem mod_le (x y : ℕ) : x mod y ≤ x :=
subst (symm (div_mod_eq _ _)) (le_add_left (x mod y) _)
theorem mod_le {x y : ℕ} : x mod y ≤ x :=
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)
(H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 :=
calc
r1 = r1 mod y : by simp
... = (r1 + q1 * y) mod y : symm (mod_add_mul_self_right _ _ H)
... = (q1 * y + r1) mod y : {add_comm _ _}
... = (r1 + q1 * y) mod y : (mod_add_mul_self_right H)⁻¹
... = (q1 * y + r1) mod y : {add_comm}
... = (r2 + q2 * y) mod y : by simp
... = r2 mod y : mod_add_mul_self_right _ _ H
... = r2 : by simp
... = r2 mod y : mod_add_mul_self_right H
... = r2 : by simp
theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y)
(H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
have H4 : q1 * y + r2 = q2 * y + r2, from subst (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 :=
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 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 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),
quotient_unique zypos H1 H2
(calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : symm (div_mod_eq _ _)
... = z * (x div y * y + x mod y) : {div_mod_eq _ _}
... = z * (x div y * y) + z * (x mod y) : mul_distr_left _ _ _
... = (x div y) * (z * y) + z * (x mod y) : {mul_left_comm _ _ _}))
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq⁻¹
... = z * (x div y * y + x mod y) : {div_mod_eq}
... = z * (x div y * y) + z * (x mod y) : mul_distr_left
... = (x div y) * (z * y) + z * (x mod y) : {mul_left_comm}))
--- something wrong with the term order
--- ... = (x div y) * (z * y) + z * (x mod y) : by simp))
theorem mod_mul_mul {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod y) :=
theorem mod_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod 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 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 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),
remainder_unique zypos H1 H2
(calc
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : symm (div_mod_eq _ _)
... = z * (x div y * y + x mod y) : {div_mod_eq _ _}
... = z * (x div y * y) + z * (x mod y) : mul_distr_left _ _ _
... = (x div y) * (z * y) + z * (x mod y) : {mul_left_comm _ _ _}))
((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq⁻¹
... = z * (x div y * y + x mod y) : {div_mod_eq}
... = z * (x div y * y) + z * (x mod y) : mul_distr_left
... = (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 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)
-- add_rewrite mod_one
theorem mod_self (n : ℕ) : n mod n = 0 :=
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 1 1 (succ_pos n),
subst (by simp) H)
from mod_mul_mul succ_pos,
(by simp) ▸ H)
-- add_rewrite mod_self
theorem div_one (n : ℕ) : n div 1 = n :=
have H : n div 1 * 1 + n mod 1 = n, from symm (div_mod_eq n 1),
subst (by simp) H
theorem div_one {n : ℕ} : n div 1 = n :=
have H : n div 1 * 1 + n mod 1 = n, from div_mod_eq⁻¹,
(by simp) ▸ H
-- add_rewrite div_one
theorem pos_div_self {n : ℕ} (H : n > 0) : n div n = 1 :=
have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul 1 1 H,
subst (by simp) H1
have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul H,
(by simp) ▸ H1
-- add_rewrite pos_div_self
@ -443,48 +444,49 @@ definition dvd (x y : ℕ) : Prop := y mod x = 0
infix `|` := dvd
theorem dvd_iff_mod_eq_zero (x y : ℕ) : x | y ↔ y mod x = 0 :=
theorem dvd_iff_mod_eq_zero {x y : ℕ} : x | y ↔ y mod x = 0 :=
refl _
theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x :=
symm (calc
x = x div y * y + x mod y : div_mod_eq _ _
... = x div y * y + 0 : {mp (dvd_iff_mod_eq_zero _ _) H}
... = x div y * y : add_zero_right _)
x = x div y * y + x mod y : div_mod_eq
... = x div y * y + 0 : {mp dvd_iff_mod_eq_zero H}
... = x div y * y : add_zero_right)
-- add_rewrite dvd_imp_div_mul_eq
theorem mul_eq_imp_dvd {z x y : ℕ} (H : z * y = x) : y | x :=
have H1 : z * y = x mod y + x div y * y, from trans (trans H (div_mod_eq x y)) (add_comm _ _),
have H1 : z * y = x mod y + x div y * y, from
H ⬝ div_mod_eq ⬝ add_comm,
have H2 : (z - x div y) * y = x mod y, from
calc
(z - x div y) * y = z * y - x div y * y : mul_sub_distr_right _ _ _
(z - x div y) * y = z * y - x div y * y : mul_sub_distr_right
... = x mod y + x div y * y - x div y * y : {H1}
... = x mod y : sub_add_left _ _,
... = x mod y : sub_add_left,
show x mod y = 0, from
by_cases -- (y = 0)
by_cases
(assume yz : y = 0,
have xz : x = 0, from
calc
x = z * y : symm H
x = z * y : H⁻¹
... = z * 0 : {yz}
... = 0 : mul_zero_right _,
... = 0 : mul_zero_right,
calc
x mod y = x mod 0 : {yz}
... = x : mod_zero _
... = 0 : xz)
... = x : mod_zero
... = 0 : xz)
(assume ynz : y ≠ 0,
have ypos : y > 0, from ne_zero_imp_pos ynz,
have H3 : (z - x div y) * y < y, from subst (symm H2) (mod_lt x ypos),
have H4 : (z - x div y) * y < 1 * y, from subst (symm (mul_one_left y)) H3,
have H3 : (z - x div y) * y < y, from H2⁻¹ ▸ mod_lt ypos,
have H4 : (z - x div y) * y < 1 * y, from mul_one_left⁻¹ ▸ 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),
calc
x mod y = (z - x div y) * y : symm H2
... = 0 * y : {H6}
... = 0 : mul_zero_left _)
x mod y = (z - x div y) * y : H2⁻¹
... = 0 * y : {H6}
... = 0 : mul_zero_left)
theorem dvd_iff_exists_mul (x y : ℕ) : x | y ↔ ∃z, z * x = y :=
theorem dvd_iff_exists_mul {x y : ℕ} : x | y ↔ ∃z, z * x = y :=
iff_intro
(assume H : x | y,
show ∃z, z * x = y, from exists_intro _ (dvd_imp_div_mul_eq H))
@ -492,7 +494,7 @@ iff_intro
obtain (z : ℕ) (zx_eq : z * x = y), from H,
show x | y, from mul_eq_imp_dvd zx_eq)
theorem dvd_zero (n : ℕ) : n | 0 := sorry
theorem dvd_zero {n : ℕ} : n | 0 := sorry
-- (by simp) (dvd_iff_mod_eq_zero n 0)
-- add_rewrite dvd_zero
@ -502,22 +504,22 @@ theorem zero_dvd_iff {n : ℕ} : (0 | n) = (n = 0) := sorry
-- add_rewrite zero_dvd_iff
theorem one_dvd (n : ℕ) : 1 | n := sorry
theorem one_dvd {n : ℕ} : 1 | n := sorry
-- (by simp) (dvd_iff_mod_eq_zero 1 n)
-- add_rewrite one_dvd
theorem dvd_self (n : ℕ) : n | n := sorry
theorem dvd_self {n : ℕ} : n | n := sorry
-- (by simp) (dvd_iff_mod_eq_zero n n)
-- add_rewrite dvd_self
theorem dvd_mul_self_left (m n : ℕ) : m | (m * n) := sorry
theorem dvd_mul_self_left {m n : ℕ} : m | (m * n) := sorry
-- (by simp) (dvd_iff_mod_eq_zero m (m * n))
-- add_rewrite dvd_mul_self_left
theorem dvd_mul_self_right (m n : ℕ) : m | (n * m) := sorry
theorem dvd_mul_self_right {m n : ℕ} : m | (n * m) := sorry
-- (by simp) (dvd_iff_mod_eq_zero m (n * m))
-- add_rewrite dvd_mul_self_left
@ -528,12 +530,12 @@ have H4 : k = k div n * (n div m) * m, from
calc
k = k div n * n : by simp
... = k div n * (n div m * m) : {H3}
... = k div n * (n div m) * m : symm (mul_assoc _ _ _),
mp (symm (dvd_iff_exists_mul _ _)) (exists_intro (k div n * (n div m)) (symm H4))
... = k div n * (n div m) * m : mul_assoc⁻¹,
mp (dvd_iff_exists_mul⁻¹) (exists_intro (k div n * (n div m)) (symm H4))
theorem dvd_add {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 + n2) :=
have H : (n1 div m + n2 div m) * m = n1 + n2, by simp,
mp (symm (dvd_iff_exists_mul _ _)) (exists_intro _ H)
mp (dvd_iff_exists_mul⁻¹) (exists_intro _ H)
theorem dvd_add_cancel_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n2 :=
case_zero_pos m
@ -551,25 +553,25 @@ case_zero_pos m
calc
n1 + n2 = (n1 + n2) div m * m : by simp
... = (n1 div m * m + n2) div m * m : by simp
... = (n2 + n1 div m * m) div m * m : {add_comm _ _}
... = (n2 div m + n1 div m) * m : {div_add_mul_self_right _ _ mpos}
... = n2 div m * m + n1 div m * m : mul_distr_right _ _ _
... = n1 div m * m + n2 div m * m : add_comm _ _
... = (n2 + n1 div m * m) div m * m : {add_comm}
... = (n2 div m + n1 div m) * m : {div_add_mul_self_right mpos}
... = n2 div m * m + n1 div m * m : mul_distr_right
... = n1 div m * m + n2 div m * m : add_comm
... = n1 + n2 div m * m : by simp,
have H4 : n2 = n2 div m * m, from add_cancel_left H3,
mp (symm (dvd_iff_exists_mul _ _)) (exists_intro _ (symm H4)))
mp (dvd_iff_exists_mul⁻¹) (exists_intro _ (H4⁻¹)))
theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m | n1 :=
dvd_add_cancel_left (subst (add_comm _ _) H)
dvd_add_cancel_left (add_comm ▸ H)
theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
by_cases
(assume H3 : n1 ≥ n2,
have H4 : n1 = n1 - n2 + n2, from symm (add_sub_ge_left H3),
show m | n1 - n2, from dvd_add_cancel_right (subst H4 H1) H2)
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)),
show m | n1 - n2, from subst (symm H4) (dvd_zero _))
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero)
-- Gcd and lcm
@ -596,17 +598,17 @@ show lhs = rhs, from
by_cases -- (y = 0)
(assume H1 : y = 0,
calc
lhs = x : if_pos H1 _ _
... = rhs : symm (if_pos H1 _ _))
lhs = x : if_pos H1 _ _
... = rhs : (if_pos H1 _ _)⁻¹)
(assume H1 : y ≠ 0,
have ypos : y > 0, from ne_zero_imp_pos H1,
have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _,
have H3 : gcd_aux_measure p' < gcd_aux_measure p, from subst (symm H2) (mod_lt _ ypos),
have H3 : gcd_aux_measure p' < gcd_aux_measure p, from H2⁻¹ ▸ (mod_lt ypos),
have H4: gcd_aux_measure p' < m, from lt_le_trans H3 H,
symm (calc
rhs = restrict 0 gcd_aux_measure g m p' : if_neg H1 _ _
... = g p' : restrict_lt_eq _ _ _ _ _ H4
... = lhs : symm (if_neg H1 _ _)))
... = lhs : (if_neg H1 _ _)⁻¹))
theorem gcd_aux_spec (p : ℕ × ℕ) : gcd_aux p =
let x := pr1 p, y := pr2 p in
@ -620,18 +622,18 @@ let x' := pr1 (pair x y), y' := pr2 (pair x y) in
calc
gcd x y = if y' = 0 then x' else gcd_aux (pair y' (x' mod y'))
: gcd_aux_spec (pair x y)
... = if y = 0 then x else gcd y (x mod y) : refl _
... = if y = 0 then x else gcd y (x mod y) : rfl
theorem gcd_zero (x : ℕ) : gcd x 0 = x :=
trans (gcd_def x 0) (if_pos (refl _) _ _)
(gcd_def x 0) ⬝ (if_pos rfl _ _)
-- add_rewrite gcd_zero
theorem gcd_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) :=
trans (gcd_def m n) (if_neg (pos_imp_ne_zero H) _ _)
(gcd_def m n) ⬝ (if_neg (pos_imp_ne_zero H) _ _)
theorem gcd_zero_left (x : ℕ) : gcd 0 x = x :=
case x (by simp) (take x, trans (gcd_def _ _) (by simp))
case x (by simp) (take x, (gcd_def _ _) ⬝ (by simp))
-- add_rewrite gcd_zero_left
@ -642,13 +644,13 @@ 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) :=
trans (gcd_def _ _) (if_neg (succ_ne_zero n) _ _)
gcd_def _ _ ⬝ if_neg succ_ne_zero _ _
theorem gcd_one (n : ℕ) : gcd n 1 = 1 := sorry
-- (by simp) (gcd_succ n 0)
@ -664,10 +666,10 @@ gcd_induct m n
assume npos : 0 < n,
assume IH : (gcd n (m mod n) | n) ∧ (gcd n (m mod n) | (m mod n)),
have H : gcd n (m mod n) | (m div n * n + m mod n), from
dvd_add (dvd_trans (and_elim_left IH) (dvd_mul_self_right _ _)) (and_elim_right IH),
have H1 : gcd n (m mod n) | m, from subst (symm (div_mod_eq m n)) H,
dvd_add (dvd_trans (and_elim_left IH) dvd_mul_self_right) (and_elim_right IH),
have H1 : gcd n (m mod n) | m, from div_mod_eq⁻¹ ▸ H,
have gcd_eq : gcd n (m mod n) = gcd m n, from symm (gcd_pos _ npos),
show (gcd m n | m) ∧ (gcd m n | n), from subst gcd_eq (and_intro H1 (and_elim_left IH)))
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and_intro H1 (and_elim_left IH)))
theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and_elim_left (gcd_dvd _ _)
@ -683,7 +685,7 @@ gcd_induct m n
assume IH : k | n → k | (m mod n) → k | gcd n (m mod n),
assume H1 : k | m,
assume H2 : k | n,
have H3 : k | m div n * n + m mod n, from subst (div_mod_eq m n) H1,
have H3 : k | m div n * n + m mod n, from div_mod_eq ▸ H1,
have H4 : k | m mod n, from dvd_add_cancel_left H3 (dvd_trans H2 (by simp)),
have gcd_eq : gcd n (m mod n) = gcd m n, from symm (gcd_pos _ npos),
show k | gcd m n, from subst gcd_eq (IH H2 H4))

285
library/data/nat/order.lean
View file

@ -35,30 +35,30 @@ opaque_hint (hiding le)
-- ### partial order (totality is part of less than)
theorem le_refl (n : ℕ) : n ≤ n :=
le_intro (add_zero_right n)
theorem le_refl {n : ℕ} : n ≤ n :=
le_intro add_zero_right
theorem zero_le (n : ℕ) : 0 ≤ n :=
le_intro (add_zero_left 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,
absurd H2 (succ_ne_zero n))
absurd H2 succ_ne_zero)
theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
obtain (l2 : ℕ) (Hl2 : m + l2 = k), from le_elim H2,
le_intro
(calc
n + (l1 + l2) = n + l1 + l2 : symm (add_assoc n l1 l2)
... = m + l2 : {Hl1}
... = k : Hl2)
n + (l1 + l2) = n + l1 + l2 : add_assoc⁻¹
... = m + l2 : {Hl1}
... = k : Hl2)
theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
obtain (k : ℕ) (Hk : n + k = m), from (le_elim H1),
@ -66,33 +66,33 @@ 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 : symm (add_assoc n k l)
... = m + l : {Hk}
... = n : Hl
... = n + 0 : symm (add_zero_right n)),
n + (k + l) = n + k + l : add_assoc⁻¹
... = m + l : {Hk}
... = n : Hl
... = n + 0 : add_zero_right⁻¹),
have L2 : k = 0, from add_eq_zero_left L1,
calc
n = n + 0 : symm (add_zero_right n)
... = n + k : {symm L2}
... = m : Hk
n = n + 0 : add_zero_right⁻¹
... = n + k : {L2⁻¹}
... = m : Hk
-- ### interaction with addition
theorem le_add_right (n m : ℕ) : n ≤ n + m :=
le_intro (refl (n + m))
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 n m)
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
(calc
k + n + l = k + (n + l) : add_assoc k n l
... = k + m : {Hl})
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 k m ▸ add_comm k n ▸ add_le_left H k
add_comm ▸ add_comm ▸ add_le_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)
@ -102,33 +102,33 @@ 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
(calc
k + (n + l) = k + n + l : symm (add_assoc k n l)
... = k + m : Hl))
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 m k ▸ add_comm n k ▸ H)
add_le_cancel_left (add_comm ▸ add_comm ▸ H)
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 k a m) ▸ (symm Ha) ▸ H1,
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 m a) H4
show m ≤ l, from le_trans le_add_left H4
-- add_rewrite le_add_right le_add_left
-- ### interaction with successor and predecessor
theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
add_one m ▸ add_one n ▸ add_le_right H 1
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 m⁻¹ ▸ add_one n⁻¹ ▸ H)
add_le_cancel_right (add_one⁻¹ ▸ add_one⁻¹ ▸ H)
theorem self_le_succ (n : ℕ) : n ≤ succ n :=
le_intro (add_one 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 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),
@ -136,19 +136,19 @@ discriminate
(assume H3 : k = 0,
have Heq : n = m,
from calc
n = n + 0 : symm (add_zero_right n)
... = n + k : {symm H3}
... = m : Hk,
or_intro_right _ Heq)
n = n + 0 : add_zero_right⁻¹
... = 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 : add_move_succ n l
... = n + k : {symm H3}
... = m : Hk)),
or_intro_left _ Hlt)
succ n + l = n + succ l : add_move_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 :=
resolve_left (le_imp_succ_le_or_eq H1) H2
@ -162,18 +162,18 @@ 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 : symm (add_move_succ n k)
... = m : H2,
n + succ k = succ n + k : add_move_succ⁻¹
... = m : H2,
show n ≤ m, from le_intro H3)
(assume H3 : n = m,
have H4 : succ n ≤ n, from subst (symm H3) H,
have H5 : succ n = n, from le_antisym H4 (self_le_succ n),
show false, from absurd H5 (succ_ne_self n))
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 :=
theorem le_pred_self {n : ℕ} : pred n ≤ n :=
case n
(subst (symm pred_zero) (le_refl 0))
(take k : ℕ, subst (symm (pred_succ k)) (self_le_succ k))
(pred_zero⁻¹ ▸ le_refl)
(take k : ℕ, (pred_succ k)⁻¹ ▸ self_le_succ)
theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
discriminate
@ -182,24 +182,24 @@ discriminate
from calc
pred n = pred 0 : {Hn}
... = 0 : pred_zero,
subst (symm H2) (zero_le (pred m)))
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 k}
... = pred (succ (k + l)) : symm (pred_succ (k + l))
... = pred (succ k + l) : {symm (add_succ_left k l)}
... = pred (n + l) : {symm Hn}
... = pred m : {Hl},
pred n + l = pred (succ k) + l : {Hn}
... = k + l : {pred_succ k}
... = pred (succ (k + l)) : (pred_succ (k + l))⁻¹
... = 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 (subst (symm Hn) (zero_le m)))
or_inl (Hn⁻¹ ▸ zero_le))
(take k : ℕ,
assume Hn : n = succ k,
have H2 : pred n = k,
@ -210,9 +210,8 @@ discriminate
have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3,
show n ≤ m ∨ n = succ m, from
or_imp_or H4
(take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5)
(take H5 : k = m, show n = succ m, from subst H5 Hn))
(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
@ -221,11 +220,11 @@ 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) : by simp
... = k * m : {Hl},
... = k * m : {Hl},
le_intro H2
theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
mul_comm k m ▸ mul_comm k n ▸ (mul_le_left H k)
mul_comm ▸ mul_comm ▸ (mul_le_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)
@ -237,11 +236,11 @@ have general : ∀n, decidable (n ≤ m), from
rec_on m
(take n,
rec_on n
(inl (le_refl 0))
(take m iH, inr (not_succ_zero_le m)))
(inl le_refl)
(take m iH, inr not_succ_zero_le))
(take (m' : ℕ) (iH1 : ∀n, decidable (n ≤ m')) (n : ℕ),
rec_on n
(inl (zero_le (succ m')))
(inl zero_le)
(take (n' : ℕ) (iH2 : decidable (n' ≤ succ m')),
have d1 : decidable (n' ≤ m'), from iH1 n',
decidable.rec_on d1
@ -279,25 +278,25 @@ theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
le_elim H
theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
lt_intro (add_move_succ n m)
lt_intro add_move_succ
-- ### basic facts
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 :=
not_intro (assume H : n < n, absurd (refl n) (lt_imp_ne H))
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 n)
theorem succ_pos {n : ℕ} : 0 < succ n :=
succ_le zero_le
theorem not_lt_zero (n : ℕ) : ¬ n < 0 :=
not_succ_zero_le n
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 (subst Hm H) (not_lt_zero n))
(take (Hm : m = 0), absurd (Hm ▸ H) not_lt_zero)
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
-- ### interaction with le
@ -308,8 +307,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 (succ n)
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)
@ -338,10 +337,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 n))
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 n))
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)
@ -349,10 +348,10 @@ 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 :=
add_succ_right k n ▸ add_le_left H k
add_succ_right ▸ add_le_left H k
theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
add_comm k m ▸ add_comm k n ▸ add_lt_left H 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 :=
le_lt_trans (add_le_right H1 m) (add_lt_left H2 k)
@ -364,27 +363,27 @@ 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 :=
add_le_cancel_left (add_succ_right k n⁻¹ ▸ H)
add_le_cancel_left (add_succ_right⁻¹ ▸ H)
theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m :=
add_lt_cancel_left (add_comm m k ▸ add_comm n k ▸ H)
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 m ▸ add_one n ▸ add_lt_right H 1
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 m⁻¹ ▸ add_one n⁻¹ ▸ H)
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 m)
:= lt_trans H self_lt_succ
-- ### totality of lt and le
theorem le_or_gt (n m : ℕ) : n ≤ m ∨ n > m :=
theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m :=
induction_on n
(or_inl (zero_le m))
(or_inl zero_le)
(take (k : ℕ),
assume IH : k ≤ m ∨ m < k,
or_elim IH
@ -394,35 +393,35 @@ induction_on n
(assume H2 : l = 0,
have H3 : m = k,
from calc
m = k + l : symm Hl
m = k + l : Hl⁻¹
... = k + 0 : {H2}
... = k : add_zero_right k,
have H4 : m < succ k, from subst H3 (self_lt_succ m),
... = k : add_zero_right,
have H4 : m < succ k, from subst H3 self_lt_succ,
or_inr H4)
(take l2 : ℕ,
assume H2 : l = succ l2,
have H3 : succ k + l2 = m,
from calc
succ k + l2 = k + succ l2 : add_move_succ k l2
... = k + l : {symm H2}
... = m : Hl,
succ k + l2 = k + succ l2 : add_move_succ
... = k + l : {H2⁻¹}
... = m : Hl,
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 :=
or_imp_or_left (le_or_gt n m) (assume H : n ≤ m, le_imp_lt_or_eq H)
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 n m)
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 :=
or_imp_or_right (le_or_gt n m) (assume H : m < n, lt_imp_le H)
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 :=
resolve_left (le_or_gt m n) H
resolve_left le_or_gt H
theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
resolve_right (le_or_gt n m) H
resolve_right le_or_gt H
-- The following three theorems are automatically proved using the instance le_decidable
theorem lt_decidable [instance] (n m : ℕ) : decidable (n < m)
@ -434,20 +433,20 @@ theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m)
-- ### misc
theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
have H1 : ∀n, ∀m, m < n → P m, from
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, m < n' → P m,
have H2: P n', from H n' IH,
assume IH : ∀ {m : nat}, m < n' → P m,
have H2: P n', from H n' @IH,
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))
(assume H4: m < n', IH _ H4)
(assume H4: m < n', IH H4)
(assume H4: m = n', H4⁻¹ ▸ H2)),
H1 _ _ (self_lt_succ n)
H1 self_lt_succ
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 :=
@ -469,17 +468,17 @@ strong_induction_on a (
-- ### basic
theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y :=
case y H0 (take y', H1 _ (succ_pos _))
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)
theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 :=
or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H)
theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 :=
or_imp_or_left (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 m)
H⁻¹ ▸ succ_pos
theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
or_elim (zero_or_pos n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
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)
@ -487,11 +486,11 @@ ne_symm (lt_imp_ne H)
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l :=
lt_imp_eq_succ H
theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n :=
(add_zero_right n) ▸ (add_lt_left H n)
theorem add_pos_right {n k : ℕ} (H : k > 0) : n + k > n :=
add_zero_right ▸ add_lt_left H n
theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n :=
(add_comm n k) ▸ (add_pos_right n H)
theorem add_pos_left {n : ℕ} {k : ℕ} (H : k > 0) : k + n > n :=
add_comm ▸ add_pos_right H
-- ### multiplication
@ -499,10 +498,10 @@ 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_right (succ k) l
... = succ (succ k * l + k) : add_succ_right _ _)
n * m = succ k * m : {Hk}
... = succ k * succ l : {Hl}
... = succ k * l + succ k : mul_succ_right
... = succ (succ k * l + k) : add_succ_right)
theorem mul_pos_imp_pos_left {n m : ℕ} (H : n * m > 0) : n > 0 :=
discriminate
@ -510,25 +509,25 @@ discriminate
have H3 : n * m = 0,
from calc
n * m = 0 * m : {H2}
... = 0 : mul_zero_left m,
... = 0 : mul_zero_left,
have H4 : 0 > 0, from H3 ▸ H,
absurd H4 (lt_irrefl 0))
absurd H4 lt_irrefl)
(take l : nat,
assume Hl : n = succ l,
Hl⁻¹ ▸ (succ_pos 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 n m) ▸ H)
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 (k * n) Hk,
have H3 : k * n + k ≤ k * m, from (mul_succ_right k n) ▸ (mul_le_left H k),
have H2 : k * n < k * n + k, from add_pos_right Hk,
have H3 : k * n + k ≤ k * m, from mul_succ_right ▸ mul_le_left H k,
lt_le_trans H2 H3
theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m) : n * k < m * k :=
subst (mul_comm k m) (subst (mul_comm k n) (mul_lt_left Hk H))
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 :=
le_lt_trans (mul_le_right H1 m) (mul_lt_left Hk H2)
@ -538,58 +537,58 @@ 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 n) 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 :=
or_elim (le_or_gt m n)
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 mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
mul_lt_cancel_left ((mul_comm m k) ▸ (mul_comm n k) ▸ H)
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 le_lt_trans H (add_pos_right _ Hk),
have H3 : k * n < k * succ m, from (mul_succ_right k m)⁻¹ ▸ H2,
have H2 : k * n < k * m + k, from le_lt_trans H (add_pos_right Hk),
have H3 : k * n < k * succ m, from mul_succ_right⁻¹ ▸ 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 k m) ▸ (mul_comm n m) ▸ H)
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 (n * m)),
have H3 : n * k ≤ n * m, from H ▸ (le_refl (n * m)),
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 :=
or_imp_or_right (zero_or_pos n)
or_imp_or_right zero_or_pos
(assume Hn : n > 0, mul_cancel_left Hn H)
theorem mul_cancel_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
mul_cancel_left Hm (subst (subst H (mul_comm n m)) (mul_comm k m))
mul_cancel_left Hm ((H ▸ mul_comm) ▸ mul_comm)
theorem mul_cancel_right_or {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k :=
mul_cancel_left_or (subst (subst H (mul_comm n m)) (mul_comm k m))
mul_cancel_left_or ((H ▸ mul_comm) ▸ mul_comm)
theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, from H⁻¹ ▸ succ_pos 0,
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 n 1)
or_elim le_or_gt
(assume H5 : n ≤ 1,
show n = 1, from le_antisym H5 H3)
(assume H5 : n > 1,
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
have H7 : 1 ≥ 2, from mul_one_right 2 ▸ H ▸ H6,
absurd (self_lt_succ 1) (le_imp_not_gt H7))
have H7 : 1 ≥ 2, from mul_one_right ▸ H ▸ H6,
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 n m) ▸ H)
mul_eq_one_left (mul_comm ▸ H)
end nat

421
library/data/nat/sub.lean
View file

@ -23,167 +23,152 @@ namespace nat
definition sub (n m : ℕ) : nat := nat_rec n (fun m x, pred x) m
infixl `-` := sub
theorem sub_zero_right (n : ℕ) : n - 0 = n
theorem sub_zero_right {n : ℕ} : n - 0 = n
theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
theorem sub_succ_right {n m : ℕ} : n - succ m = pred (n - m)
opaque_hint (hiding sub)
theorem sub_zero_left (n : ℕ) : 0 - n = 0 :=
induction_on n (sub_zero_right 0)
theorem sub_zero_left {n : ℕ} : 0 - n = 0 :=
induction_on n sub_zero_right
(take k : nat,
assume IH : 0 - k = 0,
calc
0 - succ k = pred (0 - k) : sub_succ_right 0 k
... = pred 0 : {IH}
... = 0 : pred_zero)
--(
--theorem sub_succ_left (n m : ℕ) : pred (succ n - m) = n - m
-- :=
-- induction_on m
-- (calc
-- pred (succ n - 0) = pred (succ n) : {sub_zero_right (succ n)}
-- ... = n : pred_succ n
-- ... = n - 0 : symm (sub_zero_right n))
-- (take k : nat,
-- assume IH : pred (succ n - k) = n - k,
-- _)
--)
0 - succ k = pred (0 - k) : sub_succ_right
... = pred 0 : {IH}
... = 0 : pred_zero)
--succ_sub_succ
theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m :=
theorem sub_succ_succ {n m : ℕ} : succ n - succ m = n - m :=
induction_on m
(calc
succ n - 1 = pred (succ n - 0) : sub_succ_right (succ n) 0
... = pred (succ n) : {sub_zero_right (succ n)}
... = n : pred_succ n
... = n - 0 : symm (sub_zero_right n))
succ n - 1 = pred (succ n - 0) : sub_succ_right
... = pred (succ n) : {sub_zero_right}
... = n : pred_succ _
... = n - 0 : sub_zero_right⁻¹)
(take k : nat,
assume IH : succ n - succ k = n - k,
calc
succ n - succ (succ k) = pred (succ n - succ k) : sub_succ_right (succ n) (succ k)
... = pred (n - k) : {IH}
... = n - succ k : symm (sub_succ_right n k))
succ n - succ (succ k) = pred (succ n - succ k) : sub_succ_right
... = pred (n - k) : {IH}
... = n - succ k : sub_succ_right⁻¹)
theorem sub_self (n : ℕ) : n - n = 0 :=
induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH)
theorem sub_self {n : ℕ} : n - n = 0 :=
induction_on n sub_zero_right (take k IH, trans sub_succ_succ IH)
-- TODO: add_sub_add_right
theorem sub_add_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m :=
theorem sub_add_add_right {n k m : ℕ} : (n + k) - (m + k) = n - m :=
induction_on k
(calc
(n + 0) - (m + 0) = n - (m + 0) : {add_zero_right _}
... = n - m : {add_zero_right _})
(n + 0) - (m + 0) = n - (m + 0) : {add_zero_right}
... = n - m : {add_zero_right})
(take l : nat,
assume IH : (n + l) - (m + l) = n - m,
calc
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right _ _}
... = succ (n + l) - succ (m + l) : {add_succ_right _ _}
... = (n + l) - (m + l) : sub_succ_succ _ _
... = n - m : IH)
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right}
... = succ (n + l) - succ (m + l) : {add_succ_right}
... = (n + l) - (m + l) : sub_succ_succ
... = n - m : IH)
theorem sub_add_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
add_comm m k ▸ add_comm n k ▸ sub_add_add_right n k m
theorem sub_add_add_left {k n m : ℕ} : (k + n) - (k + m) = n - m :=
add_comm ▸ add_comm ▸ sub_add_add_right
-- TODO: add_sub_inv
theorem sub_add_left (n m : ℕ) : n + m - m = n :=
theorem sub_add_left {n m : ℕ} : n + m - m = n :=
induction_on m
((add_zero_right n)⁻¹ ▸ sub_zero_right n)
(add_zero_right⁻¹ ▸ sub_zero_right)
(take k : ℕ,
assume IH : n + k - k = n,
calc
n + succ k - succ k = succ (n + k) - succ k : {add_succ_right n k}
... = n + k - k : sub_succ_succ _ _
... = n : IH)
n + succ k - succ k = succ (n + k) - succ k : {add_succ_right}
... = n + k - k : sub_succ_succ
... = n : IH)
-- TODO: add_sub_inv'
theorem sub_add_left2 (n m : ℕ) : n + m - n = m :=
add_comm m n ▸ sub_add_left m n
theorem sub_add_left2 {n m : ℕ} : n + m - n = m :=
add_comm ▸ sub_add_left
theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) :=
theorem sub_sub {n m k : ℕ} : n - m - k = n - (m + k) :=
induction_on k
(calc
n - m - 0 = n - m : sub_zero_right _
... = n - (m + 0) : {symm (add_zero_right m)})
n - m - 0 = n - m : sub_zero_right
... = n - (m + 0) : {add_zero_right⁻¹})
(take l : nat,
assume IH : n - m - l = n - (m + l),
calc
n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l
... = pred (n - (m + l)) : {IH}
... = n - succ (m + l) : symm (sub_succ_right n (m + l))
... = n - (m + succ l) : {symm (add_succ_right m l)})
n - m - succ l = pred (n - m - l) : sub_succ_right
... = pred (n - (m + l)) : {IH}
... = n - succ (m + l) : sub_succ_right⁻¹
... = n - (m + succ l) : {add_succ_right⁻¹})
theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k :=
theorem succ_sub_sub {n m k : ℕ} : succ n - m - succ k = n - m - k :=
calc
succ n - m - succ k = succ n - (m + succ k) : sub_sub _ _ _
... = succ n - succ (m + k) : {add_succ_right m k}
... = n - (m + k) : sub_succ_succ _ _
... = n - m - k : symm (sub_sub n m k)
succ n - m - succ k = succ n - (m + succ k) : sub_sub
... = succ n - succ (m + k) : {add_succ_right}
... = n - (m + k) : sub_succ_succ
... = n - m - k : sub_sub⁻¹
theorem sub_add_right_eq_zero (n m : ℕ) : n - (n + m) = 0 :=
theorem sub_add_right_eq_zero {n m : ℕ} : n - (n + m) = 0 :=
calc
n - (n + m) = n - n - m : symm (sub_sub n n m)
... = 0 - m : {sub_self n}
... = 0 : sub_zero_left m
n - (n + m) = n - n - m : sub_sub⁻¹
... = 0 - m : {sub_self}
... = 0 : sub_zero_left
theorem sub_comm (m n k : ℕ) : m - n - k = m - k - n :=
theorem sub_comm {m n k : ℕ} : m - n - k = m - k - n :=
calc
m - n - k = m - (n + k) : sub_sub m n k
... = m - (k + n) : {add_comm n k}
... = m - k - n : symm (sub_sub m k n)
m - n - k = m - (n + k) : sub_sub
... = m - (k + n) : {add_comm}
... = m - k - n : sub_sub⁻¹
theorem sub_one (n : ℕ) : n - 1 = pred n :=
theorem sub_one {n : ℕ} : n - 1 = pred n :=
calc
n - 1 = pred (n - 0) : sub_succ_right n 0
... = pred n : {sub_zero_right n}
n - 1 = pred (n - 0) : sub_succ_right
... = pred n : {sub_zero_right}
theorem succ_sub_one (n : ℕ) : succ n - 1 = n :=
trans (sub_succ_succ n 0) (sub_zero_right n)
theorem succ_sub_one {n : ℕ} : succ n - 1 = n :=
sub_succ_succ ⬝ sub_zero_right
-- add_rewrite sub_add_left
-- ### interaction with multiplication
theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m :=
theorem mul_pred_left {n m : ℕ} : pred n * m = n * m - m :=
induction_on n
(calc
pred 0 * m = 0 * m : {pred_zero}
... = 0 : mul_zero_left _
... = 0 - m : symm (sub_zero_left m)
... = 0 * m - m : {symm (mul_zero_left m)})
pred 0 * m = 0 * m : {pred_zero}
... = 0 : mul_zero_left
... = 0 - m : sub_zero_left⁻¹
... = 0 * m - m : {mul_zero_left⁻¹})
(take k : nat,
assume IH : pred k * m = k * m - m,
calc
pred (succ k) * m = k * m : {pred_succ k}
... = k * m + m - m : symm (sub_add_left _ _)
... = succ k * m - m : {symm (mul_succ_left k m)})
pred (succ k) * m = k * m : {pred_succ _}
... = k * m + m - m : sub_add_left⁻¹
... = succ k * m - m : {mul_succ_left⁻¹})
theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
calc n * pred m = pred m * n : mul_comm _ _
... = m * n - n : mul_pred_left m n
... = n * m - n : {mul_comm m n}
theorem mul_pred_right {n m : ℕ} : n * pred m = n * m - n :=
calc n * pred m = pred m * n : mul_comm
... = m * n - n : mul_pred_left
... = n * m - n : {mul_comm}
theorem mul_sub_distr_right (n m k : ℕ) : (n - m) * k = n * k - m * k :=
theorem mul_sub_distr_right {n m k : ℕ} : (n - m) * k = n * k - m * k :=
induction_on m
(calc
(n - 0) * k = n * k : {sub_zero_right n}
... = n * k - 0 : symm (sub_zero_right _)
... = n * k - 0 * k : {symm (mul_zero_left _)})
(n - 0) * k = n * k : {sub_zero_right}
... = n * k - 0 : sub_zero_right⁻¹
... = n * k - 0 * k : {mul_zero_left⁻¹})
(take l : nat,
assume IH : (n - l) * k = n * k - l * k,
calc
(n - succ l) * k = pred (n - l) * k : {sub_succ_right n l}
... = (n - l) * k - k : mul_pred_left _ _
... = n * k - l * k - k : {IH}
... = n * k - (l * k + k) : sub_sub _ _ _
... = n * k - (succ l * k) : {symm (mul_succ_left l k)})
(n - succ l) * k = pred (n - l) * k : {sub_succ_right}
... = (n - l) * k - k : mul_pred_left
... = n * k - l * k - k : {IH}
... = n * k - (l * k + k) : sub_sub
... = n * k - (succ l * k) : {mul_succ_left⁻¹})
theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k :=
theorem mul_sub_distr_left {n m k : ℕ} : n * (m - k) = n * m - n * k :=
calc
n * (m - k) = (m - k) * n : mul_comm _ _
... = m * n - k * n : mul_sub_distr_right _ _ _
... = n * m - k * n : {mul_comm _ _}
... = n * m - n * k : {mul_comm _ _}
n * (m - k) = (m - k) * n : mul_comm
... = m * n - k * n : mul_sub_distr_right
... = n * m - k * n : {mul_comm}
... = n * m - n * k : {mul_comm}
-- ### interaction with inequalities
@ -192,76 +177,76 @@ sub_induction n m
(take k,
assume H : 0 ≤ k,
calc
succ k - 0 = succ k : sub_zero_right (succ k)
... = succ (k - 0) : {symm (sub_zero_right k)})
succ k - 0 = succ k : sub_zero_right
... = succ (k - 0) : {sub_zero_right⁻¹})
(take k,
assume H : succ k ≤ 0,
absurd H (not_succ_zero_le k))
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,
calc
succ (succ l) - succ k = succ l - k : sub_succ_succ (succ l) k
... = succ (l - k) : IH (succ_le_cancel H)
... = succ (succ l - succ k) : {symm (sub_succ_succ l k)})
succ (succ l) - succ k = succ l - k : sub_succ_succ
... = succ (l - k) : IH (succ_le_cancel 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 n k
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
(take k,
assume H : 0 ≤ k,
calc
0 + (k - 0) = k - 0 : add_zero_left (k - 0)
... = k : sub_zero_right k)
(take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k))
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 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 l k}
... = succ (k + (l - k)) : add_succ_left k (l - k)
... = succ l : {IH (succ_le_cancel H)})
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)})
theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n :=
add_comm m (n - m) ▸ add_sub_le
add_comm ▸ add_sub_le
theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
calc
n + (m - n) = n + 0 : {le_imp_sub_eq_zero H}
... = n : add_zero_right n
... = n : add_zero_right
theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m :=
add_comm m (n - m) ▸ add_sub_ge
add_comm ▸ add_sub_ge
theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) :=
or_elim (le_total n m)
theorem le_add_sub_left {n m : ℕ} : n ≤ n + (m - n) :=
or_elim le_total
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H)
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ le_refl n)
(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 n m)
(assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m))
(assume H : m ≤ n, subst (symm (add_sub_ge H)) H)
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)
(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 n m)
(assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3))
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 :=
theorem sub_le_self {n m : ℕ} : n - m ≤ n :=
sub_split
(assume H : n ≤ m, zero_le n)
(take k : ℕ, assume H : m + k = n, le_intro (subst (add_comm m k) H))
(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 :=
theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
exists_intro k
(calc
m - k = n + k - k : {symm Hk}
... = n : sub_add_left n k)
m - k = n + k - k : {Hk⁻¹}
... = n : sub_add_left)
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
@ -269,17 +254,17 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
(take m : ℕ,
assume H : 0 ≤ m,
calc
n + m - 0 = n + m : sub_zero_right (n + m)
... = n + (m - 0) : {symm (sub_zero_right m)})
(take k : ℕ, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k))
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 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_right n m}
... = n + m - k : sub_succ_succ (n + m) k
... = n + (m - k) : IH (succ_le_cancel H)
... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}),
n + succ m - succ k = succ (n + m) - succ k : {add_succ_right}
... = n + m - k : sub_succ_succ
... = n + (m - k) : IH (succ_le_cancel H)
... = n + (succ m - succ k) : {sub_succ_succ⁻¹}),
l1 H
theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m :=
@ -288,12 +273,12 @@ sub_split
(take k : ℕ,
assume H1 : m + k = n,
assume H2 : k = 0,
have H3 : n = m, from subst (add_zero_right m) (subst H2 (symm H1)),
subst H3 (le_refl n))
have H3 : n = m, from add_zero_right ▸ H2 ▸ H1⁻¹,
subst 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 n m)
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,
@ -302,9 +287,9 @@ or_elim (le_total n m)
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)
... = n + m : symm H
... = m + n : add_comm n m,
k - n + n = k : add_sub_ge_left (le_intro H)
... = n + m : H⁻¹
... = m + n : add_comm,
add_cancel_right H2
theorem sub_lt {x y : ℕ} (xpos : x > 0) (ypos : y > 0) : x - y < x :=
@ -312,39 +297,39 @@ obtain (x' : ℕ) (xeq : x = succ x'), from pos_imp_eq_succ xpos,
obtain (y' : ℕ) (yeq : y = succ y'), from pos_imp_eq_succ ypos,
have xsuby_eq : x - y = x' - y', from
calc
x - y = succ x' - y : {xeq}
x - y = succ x' - y : {xeq}
... = 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 _,
... = x' - y' : sub_succ_succ,
have H1 : x' - y' ≤ x', from sub_le_self,
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 n k)
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le (m - k))
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
n - k + l = l + (n - k) : by simp
... = l + n - k : symm (add_sub_assoc H2 l)
... = n + l - k : {add_comm l n}
... = m - k : {Hl},
n - k + l = l + (n - k) : by simp
... = l + n - k : (add_sub_assoc H2 l)⁻¹
... = n + l - k : {add_comm}
... = m - k : {Hl},
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,
sub_split
(assume H2 : k ≤ m, zero_le (k - n))
(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 H4 : m' + l + n = k - n + n, from
calc
m' + l + n = n + l + m' : by simp
... = m + m' : {Hl}
... = k : Hm
... = k - n + n : symm (add_sub_ge_left H3),
m' + l + n = n + l + m' : by simp
... = m + m' : {Hl}
... = k : Hm
... = k - n + n : (add_sub_ge_left H3)⁻¹,
le_intro (add_cancel_right H4))
-- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
@ -355,25 +340,25 @@ sub_split
-- :=
-- _
theorem sub_triangle_inequality (n m k : ℕ) : n - k ≤ (n - m) + (m - k) :=
theorem sub_triangle_inequality {n m k : ℕ} : n - k ≤ (n - m) + (m - k) :=
sub_split
(assume H : n ≤ m, (add_zero_left (m - k))⁻¹ ▸ sub_le_right H k)
(assume H : n ≤ m, add_zero_left⁻¹ ▸ sub_le_right H k)
(take mn : ℕ,
assume Hmn : m + mn = n,
sub_split
(assume H : m ≤ k,
have H2 : n - k ≤ n - m, from sub_le_left H n,
have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2,
show n - k ≤ mn + 0, from (add_zero_right mn)⁻¹ ▸ H3)
have H2 : n - k ≤ n - m, from sub_le_left H n,
have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2,
show n - k ≤ mn + 0, from add_zero_right⁻¹ ▸ H3)
(take km : ℕ,
assume Hkm : k + km = m,
have H : k + (mn + km) = n, from
calc
k + (mn + km) = k + km + mn : by simp
... = m + mn : {Hkm}
... = n : Hmn,
have H2 : n - k = mn + km, from sub_intro H,
H2 ▸ (le_refl (n - k))))
assume Hkm : k + km = m,
have H : k + (mn + km) = n, from
calc
k + (mn + km) = k + km + mn : by simp
... = m + mn : {Hkm}
... = n : Hmn,
have H2 : n - k = mn + km, from sub_intro H,
H2 ▸ le_refl))
-- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
@ -389,9 +374,9 @@ theorem max_le {n m : ℕ} (H : n ≤ m) : n + (m - n) = m := add_sub_le H
theorem max_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n := add_sub_ge H
theorem left_le_max (n m : ℕ) : n ≤ n + (m - n) := le_add_sub_left n m
theorem left_le_max {n m : ℕ} : n ≤ n + (m - n) := le_add_sub_left
theorem right_le_max (n m : ℕ) : m ≤ max n m := le_add_sub_right n m
theorem right_le_max {n m : ℕ} : m ≤ max n m := le_add_sub_right
-- ### absolute difference
@ -399,13 +384,13 @@ theorem right_le_max (n m : ℕ) : m ≤ max n m := le_add_sub_right n m
definition dist (n m : ℕ) := (n - m) + (m - n)
theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
add_comm (n - m) (m - n)
theorem dist_comm {n m : ℕ} : dist n m = dist m n :=
add_comm
theorem dist_self (n : ℕ) : dist n n = 0 :=
theorem dist_self {n : ℕ} : dist n n = 0 :=
calc
(n - n) + (n - n) = 0 + 0 : by simp
... = 0 : by simp
... = 0 : by simp
theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
have H2 : n - m = 0, from add_eq_zero_left H,
@ -417,97 +402,95 @@ le_antisym H3 H5
theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
calc
dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H}
... = m - n : add_zero_left (m - n)
... = m - n : add_zero_left
theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
dist_comm m n ▸ dist_le H
dist_comm ▸ dist_le H
theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
trans (dist_ge (zero_le n)) (sub_zero_right n)
theorem dist_zero_right {n : ℕ} : dist n 0 = n :=
dist_ge zero_le ⬝ sub_zero_right
theorem dist_zero_left (n : ℕ) : dist 0 n = n :=
trans (dist_le (zero_le n)) (sub_zero_right n)
theorem dist_zero_left {n : ℕ} : dist 0 n = n :=
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)
... = m : sub_intro H
... = m : sub_intro H
theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
theorem dist_add_right {n k m : ℕ} : dist (n + k) (m + k) = dist n m :=
calc
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : refl _
... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right _ _ _}
... = (n - m) + (m - n) : {sub_add_add_right _ _ _}
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : rfl
... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right}
... = (n - m) + (m - n) : {sub_add_add_right}
theorem dist_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m :=
add_comm m k ▸ add_comm n k ▸ dist_add_right n k m
theorem dist_add_left {k n m : ℕ} : dist (k + n) (k + m) = dist n m :=
add_comm ▸ add_comm ▸ dist_add_right
-- add_rewrite dist_self dist_add_right dist_add_left dist_zero_left dist_zero_right
theorem dist_ge_add_right {n m : ℕ} (H : n ≥ m) : dist n m + m = n :=
calc
dist n m + m = n - m + m : {dist_ge H}
... = n : add_sub_ge_left H
... = n : add_sub_ge_left H
theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m :=
calc
dist n k = dist (n + m) (k + m) : symm (dist_add_right n m k)
... = dist (k + l) (k + m) : {H}
... = dist l m : dist_add_left k l m
dist n k = dist (n + m) (k + m) : dist_add_right⁻¹
... = dist (k + l) (k + m) : {H}
... = dist l m : dist_add_left
theorem dist_sub_move_add {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 : by simp
... = n + k : {add_sub_ge_left H}
... = k + n : by simp,
... = n + k : {add_sub_ge_left H}
... = k + n : by simp,
dist_eq_intro H2
theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m) = dist (n + m) k :=
subst (subst (dist_sub_move_add H n) (dist_comm (k - m) n)) (dist_comm k (n + m))
(dist_sub_move_add H n ▸ dist_comm) ▸ dist_comm
--triangle inequality formulated with dist
theorem triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
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 n m k) (sub_triangle_inequality k m n)
H ▸ add_le 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 :=
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
calc
_ = dist n k + dist (k + m) (k + l) : {dist_add_right n m k}
... = _ : {dist_add_left k m l},
H ▸ (triangle_inequality (n + m) (k + m) (k + l))
dist_add_left ▸ dist_add_right ▸ rfl,
H ▸ triangle_inequality
--interaction with multiplication
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
have H : ∀n m, dist n m = n - m + (m - n), from take n m, refl _,
theorem dist_mul_left {k n m : ℕ} : dist (k * n) (k * m) = k * dist n m :=
have H : ∀n m, dist n m = n - m + (m - n), from take n m, rfl,
by simp
theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k :=
have H : ∀n m, dist n m = n - m + (m - n), from take n m, refl _,
theorem dist_mul_right {n k m : ℕ} : dist (n * k) (m * k) = dist n m * k :=
have H : ∀n m, dist n m = n - m + (m - n), from take n m, rfl,
by simp
-- add_rewrite dist_mul_right dist_mul_left dist_comm
--needed to prove of_nat a * of_nat b = of_nat (a * b) in int
theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
theorem dist_mul_dist {n m k l : ℕ} : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
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)) : symm (dist_mul_right n (k - l) m)
... = 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) (n * l + (m * k - m * l)) : {add_comm _ _}
... = dist (n * k) (n * l + m * k - m * l) : {symm (add_sub_assoc H2 (n * l))}
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _,
or_elim (le_total k l)
(assume H : k ≤ l, dist_comm l k ▸ dist_comm _ _ ▸ aux l k H)
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) (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
(assume H : k ≤ l, dist_comm ▸ dist_comm ▸ aux l k H)
(assume H : l ≤ k, aux k l H)
end nat

2
tests/lean/run/occurs_check_bug1.lean
View file

@ -14,4 +14,4 @@ theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (decidable_eq (pr2 (pair x
sorry
theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
trans (gcd_def _ _) (if_neg (succ_ne_zero n) _ _)
trans (gcd_def _ _) (if_neg succ_ne_zero _ _)

4
tests/lean/slow/list_elab2.lean
View file

@ -108,14 +108,14 @@ theorem length_concat (s t : list T) : length (s ++ t) = length s + length t :=
list_induction_on s
(calc
length (concat nil t) = length t : refl _
... = zero + length t : {symm (add_zero_left (length t))}
... = zero + length t : {symm add_zero_left}
... = length (@nil T) + length t : refl _)
(take x s,
assume H : length (concat s t) = length s + length t,
calc
length (concat (cons x s) t ) = succ (length (concat s t)) : refl _
... = succ (length s + length t) : { H }
... = succ (length s) + length t : {symm (add_succ_left _ _)}
... = succ (length s) + length t : {symm add_succ_left}
... = length (cons x s) + length t : refl _)
-- Reverse