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

refactor(library): replace assert-exprs with have-exprs

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-29 11:47:33 -08:00
parent 101cf1ec4c
commit deb1b3dc79
77 changed files with 655 additions and 651 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/algebra/complete_lattice.lean
View file

@ -89,7 +89,7 @@ le_Inf (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(suppose x = a, begin subst x, exact h₁ end)
(suppose x ∈ '{b},
assert x = b, from !eq_of_mem_singleton this,
have x = b, from !eq_of_mem_singleton this,
begin subst x, exact h₂ end))
lemma le_sup_left (a b : A) : a ≤ a ⊔ b :=
@ -104,7 +104,7 @@ Sup_le (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(suppose x = a, by subst x; assumption)
(suppose x ∈ '{b},
assert x = b, from !eq_of_mem_singleton this,
have x = b, from !eq_of_mem_singleton this,
by subst x; assumption))
end complete_lattice_Inf
@ -152,7 +152,7 @@ le_Inf (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(suppose x = a, begin subst x, exact h₁ end)
(suppose x ∈ '{b},
assert x = b, from !eq_of_mem_singleton this,
have x = b, from !eq_of_mem_singleton this,
begin subst x, exact h₂ end))
lemma le_sup_left (a b : A) : a ≤ a ⊔ b :=
@ -167,7 +167,7 @@ Sup_le (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(assume H : x = a, by subst x; exact h₁)
(suppose x ∈ '{b},
assert x = b, from !eq_of_mem_singleton this,
have x = b, from !eq_of_mem_singleton this,
by subst x; exact h₂))
end complete_lattice_Sup
@ -265,12 +265,12 @@ lemma Inf_singleton {a : A} : ⨅'{a} = a :=
have ⨅'{a} ≤ a, from
Inf_le !mem_insert,
have a ≤ ⨅'{a}, from
le_Inf (take b, suppose b ∈ '{a}, assert b = a, from eq_of_mem_singleton this, by rewrite this; apply le.refl),
le_Inf (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this; apply le.refl),
le.antisymm `⨅'{a} ≤ a` `a ≤ ⨅'{a}`
lemma Sup_singleton {a : A} : ⨆'{a} = a :=
have ⨆'{a} ≤ a, from
Sup_le (take b, suppose b ∈ '{a}, assert b = a, from eq_of_mem_singleton this, by rewrite this; apply le.refl),
Sup_le (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this; apply le.refl),
have a ≤ ⨆'{a}, from
le_Sup !mem_insert,
le.antisymm `⨆'{a} ≤ a` `a ≤ ⨆'{a}`

10
library/algebra/field.lean
View file

@ -80,15 +80,15 @@ section division_ring
division_ring.mul_ne_zero (and.right H2) (and.left H2)
theorem eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a :=
assert a ≠ 0, from
have a ≠ 0, from
suppose a = 0,
have 0 = (1:A), by inst_simp,
absurd this zero_ne_one,
assert b = (1 / a) * a * b, by inst_simp,
have b = (1 / a) * a * b, by inst_simp,
show b = 1 / a, by inst_simp
theorem eq_one_div_of_mul_eq_one_left (H : b * a = 1) : b = 1 / a :=
assert a ≠ 0, from
have a ≠ 0, from
suppose a = 0,
have 0 = (1:A), by inst_simp,
absurd this zero_ne_one,
@ -205,7 +205,7 @@ section field
by rewrite [(division_ring.one_div_mul_one_div Ha Hb), mul.comm b]
theorem field.div_mul_right (Hb : b ≠ 0) (H : a * b ≠ 0) : a / (a * b) = 1 / b :=
assert a ≠ 0, from and.left (ne_zero_and_ne_zero_of_mul_ne_zero H),
have a ≠ 0, from and.left (ne_zero_and_ne_zero_of_mul_ne_zero H),
symm (calc
1 / b = a * ((1 / a) * (1 / b)) : by inst_simp
... = a * (1 / (b * a)) : division_ring.one_div_mul_one_div this Hb
@ -222,7 +222,7 @@ section field
by rewrite [mul.comm, (!div_mul_cancel Hb)]
theorem one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
assert a * b ≠ 0, from (division_ring.mul_ne_zero Ha Hb),
have a * b ≠ 0, from (division_ring.mul_ne_zero Ha Hb),
by rewrite [add.comm, -(field.div_mul_left Ha this), -(field.div_mul_right Hb this), *division.def,
-right_distrib]

34
library/algebra/group.lean
View file

@ -156,7 +156,7 @@ section group
by simp
theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
assert a⁻¹ * 1 = b, by inst_simp,
have a⁻¹ * 1 = b, by inst_simp,
by inst_simp
theorem one_inv [simp] : 1⁻¹ = (1 : A) :=
@ -166,14 +166,14 @@ section group
inv_eq_of_mul_eq_one (mul.left_inv a)
theorem inv.inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
assert a = a⁻¹⁻¹, by simp_nohyps,
have a = a⁻¹⁻¹, by simp_nohyps,
by inst_simp
theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
iff.intro (assume H, inv.inj H) (by simp)
theorem inv_eq_one_iff_eq_one (a : A) : a⁻¹ = 1 ↔ a = 1 :=
assert a⁻¹ = 1⁻¹ ↔ a = 1, from inv_eq_inv_iff_eq a 1,
have a⁻¹ = 1⁻¹ ↔ a = 1, from inv_eq_inv_iff_eq a 1,
by simp
theorem eq_one_of_inv_eq_one (a : A) : a⁻¹ = 1 → a = 1 :=
@ -186,11 +186,11 @@ section group
iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv
theorem eq_inv_of_mul_eq_one {a b : A} (H : a * b = 1) : a = b⁻¹ :=
assert a⁻¹ = b, from inv_eq_of_mul_eq_one H,
have a⁻¹ = b, from inv_eq_of_mul_eq_one H,
by inst_simp
theorem mul.right_inv [simp] (a : A) : a * a⁻¹ = 1 :=
assert a = a⁻¹⁻¹, by simp,
have a = a⁻¹⁻¹, by simp,
by inst_simp
theorem mul_inv_cancel_left [simp] (a b : A) : a * (a⁻¹ * b) = b :=
@ -203,7 +203,7 @@ section group
inv_eq_of_mul_eq_one (by inst_simp)
theorem eq_of_mul_inv_eq_one {a b : A} (H : a * b⁻¹ = 1) : a = b :=
assert a⁻¹ * 1 = a⁻¹, by inst_simp,
have a⁻¹ * 1 = a⁻¹, by inst_simp,
by inst_simp
theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * c = b) : a = b * c⁻¹ :=
@ -237,11 +237,11 @@ section group
iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
theorem mul_left_cancel {a b c : A} (H : a * b = a * c) : b = c :=
assert a⁻¹ * (a * b) = b, by inst_simp,
have a⁻¹ * (a * b) = b, by inst_simp,
by inst_simp
theorem mul_right_cancel {a b c : A} (H : a * b = c * b) : a = c :=
assert a * b * b⁻¹ = a, by inst_simp,
have a * b * b⁻¹ = a, by inst_simp,
by inst_simp
theorem mul_eq_one_of_mul_eq_one {a b : A} (H : b * a = 1) : a * b = 1 :=
@ -277,7 +277,7 @@ section group
lemma is_conj.symm (a b : A) : a ~ b → b ~ a :=
assume Pab, obtain x (Pconj : x ∘c b = a), from Pab,
assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, by simp,
have Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, by simp,
exists.intro x⁻¹ (by simp)
lemma is_conj.trans (a b c : A) : a ~ b → b ~ c → a ~ c :=
@ -324,7 +324,7 @@ section add_group
by simp
theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b :=
assert -a + 0 = b, by inst_simp,
have -a + 0 = b, by inst_simp,
by inst_simp
theorem neg_zero [simp] : -0 = (0 : A) := neg_eq_of_add_eq_zero (zero_add 0)
@ -332,11 +332,11 @@ section add_group
theorem neg_neg [simp] (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
theorem eq_neg_of_add_eq_zero {a b : A} (H : a + b = 0) : a = -b :=
assert -a = b, from neg_eq_of_add_eq_zero H,
have -a = b, from neg_eq_of_add_eq_zero H,
by inst_simp
theorem neg.inj {a b : A} (H : -a = -b) : a = b :=
assert a = -(-a), by simp_nohyps,
have a = -(-a), by simp_nohyps,
by inst_simp
theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
@ -346,7 +346,7 @@ section add_group
iff.mp !neg_eq_neg_iff_eq
theorem neg_eq_zero_iff_eq_zero (a : A) : -a = 0 ↔ a = 0 :=
assert -a = -0 ↔ a = 0, from neg_eq_neg_iff_eq a 0,
have -a = -0 ↔ a = 0, from neg_eq_neg_iff_eq a 0,
by simp
theorem eq_zero_of_neg_eq_zero {a : A} : -a = 0 → a = 0 :=
@ -359,7 +359,7 @@ section add_group
iff.intro !eq_neg_of_eq_neg !eq_neg_of_eq_neg
theorem add.right_inv [simp] (a : A) : a + -a = 0 :=
assert a = -(-a), by simp,
have a = -(-a), by simp,
by inst_simp
theorem add_neg_cancel_left [simp] (a b : A) : a + (-a + b) = b :=
@ -403,11 +403,11 @@ section add_group
iff.intro eq_add_neg_of_add_eq add_eq_of_eq_add_neg
theorem add_left_cancel {a b c : A} (H : a + b = a + c) : b = c :=
assert -a + (a + b) = b, by inst_simp,
have -a + (a + b) = b, by inst_simp,
by inst_simp
theorem add_right_cancel {a b c : A} (H : a + b = c + b) : a = c :=
assert a + b + -b = a, by inst_simp,
have a + b + -b = a, by inst_simp,
by inst_simp
definition add_group.to_left_cancel_semigroup [trans_instance] : add_left_cancel_semigroup A :=
@ -459,7 +459,7 @@ section add_group
by rewrite [sub_eq_add_neg, add.assoc, -sub_eq_add_neg]
theorem eq_of_sub_eq_zero {a b : A} (H : a - b = 0) : a = b :=
assert -a + 0 = -a, by inst_simp,
have -a + 0 = -a, by inst_simp,
by inst_simp
theorem eq_iff_sub_eq_zero (a b : A) : a = b ↔ a - b = 0 :=

12
library/algebra/group_bigops.lean
View file

@ -136,7 +136,7 @@ section monoid
∀ {l : list A} b, (∀ a, a ∈ l → f a = b) → Prodl l f = b ^ length l
| nil := take b, assume Pconst, by rewrite [length_nil, {b^0}pow_zero]
| (a::l) := take b, assume Pconst,
assert Pconstl : ∀ a', a' ∈ l → f a' = b,
have Pconstl : ∀ a', a' ∈ l → f a' = b,
from take a' Pa'in, Pconst a' (mem_cons_of_mem a Pa'in),
by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons,
add_one, pow_succ b]
@ -304,9 +304,9 @@ namespace finset
(take x s', assume H1 : x ∉ s',
assume IH : (∀ {x : A}, x ∈ s' → f x = g x) → Prod s' f = Prod s' g,
assume H2 : ∀{y}, y ∈ insert x s' → f y = g y,
assert H3 : ∀y, y ∈ s' → f y = g y, from
have H3 : ∀y, y ∈ s' → f y = g y, from
take y, assume H', H2 (mem_insert_of_mem _ H'),
assert H4 : f x = g x, from H2 !mem_insert,
have H4 : f x = g x, from H2 !mem_insert,
by rewrite [Prod_insert_of_not_mem f H1, Prod_insert_of_not_mem g H1, IH H3, H4])
theorem Prod_singleton (a : A) (f : A → B) : Prod '{a} f = f a :=
@ -412,15 +412,15 @@ section Prod
Prod (insert a s) f = Prod s f :=
by_cases
(suppose finite s,
assert (#finset a ∈ set.to_finset s), by rewrite mem_to_finset_eq; apply H,
have (#finset a ∈ set.to_finset s), by rewrite mem_to_finset_eq; apply H,
by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_mem f this])
(assume nfs : ¬ finite s,
assert ¬ finite (insert a s), from assume H, nfs (finite_of_finite_insert H),
have ¬ finite (insert a s), from assume H, nfs (finite_of_finite_insert H),
by rewrite [Prod_of_not_finite nfs, Prod_of_not_finite this])
theorem Prod_insert_of_not_mem (f : A → B) {a : A} {s : set A} [finite s] (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f :=
assert (#finset a ∉ set.to_finset s), by rewrite mem_to_finset_eq; apply H,
have (#finset a ∉ set.to_finset s), by rewrite mem_to_finset_eq; apply H,
by rewrite [↑Prod, to_finset_insert, finset.Prod_insert_of_not_mem f this]
theorem Prod_union (f : A → B) {s₁ s₂ : set A} [finite s₁] [finite s₂]

4
library/algebra/group_power.lean
View file

@ -108,7 +108,7 @@ theorem inv_pow (a : A) : ∀n, (a⁻¹)^n = (a^n)⁻¹
| (succ n) := by rewrite [pow_succ, pow_succ', inv_pow, mul_inv]
theorem pow_sub (a : A) {m n : ℕ} (H : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ :=
assert H1 : m - n + n = m, from nat.sub_add_cancel H,
have H1 : m - n + n = m, from nat.sub_add_cancel H,
have H2 : a^(m - n) * a^n = a^m, by rewrite [-pow_add, H1],
eq_mul_inv_of_mul_eq H2
@ -132,7 +132,7 @@ private lemma gpow_add_aux (a : A) (m n : nat) :
gpow a ((of_nat m) + -[1+n]) = gpow a (of_nat m) * gpow a (-[1+n]) :=
or.elim (nat.lt_or_ge m (nat.succ n))
(assume H : (m < nat.succ n),
assert H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
have H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
calc
gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n)) : rfl
... = gpow a (-[1+ nat.pred (nat.sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H}

18
library/algebra/ordered_field.lean
View file

@ -170,16 +170,16 @@ section linear_ordered_field
theorem div_lt_div_of_mul_sub_mul_div_neg (Hc : c ≠ 0) (Hd : d ≠ 0)
(H : (a * d - b * c) / (c * d) < 0) : a / c < b / d :=
assert H1 : (a * d - c * b) / (c * d) < 0, by rewrite [mul.comm c b]; exact H,
assert H2 : a / c - b / d < 0, by rewrite [!div_sub_div Hc Hd]; exact H1,
assert H3 : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _,
have H1 : (a * d - c * b) / (c * d) < 0, by rewrite [mul.comm c b]; exact H,
have H2 : a / c - b / d < 0, by rewrite [!div_sub_div Hc Hd]; exact H1,
have H3 : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _,
begin rewrite [zero_add at H3, sub_eq_add_neg at H3, neg_add_cancel_right at H3], exact H3 end
theorem div_le_div_of_mul_sub_mul_div_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0)
(H : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d :=
assert H1 : (a * d - c * b) / (c * d) ≤ 0, by rewrite [mul.comm c b]; exact H,
assert H2 : a / c - b / d ≤ 0, by rewrite [!div_sub_div Hc Hd]; exact H1,
assert H3 : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _,
have H1 : (a * d - c * b) / (c * d) ≤ 0, by rewrite [mul.comm c b]; exact H,
have H2 : a / c - b / d ≤ 0, by rewrite [!div_sub_div Hc Hd]; exact H1,
have H3 : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _,
begin rewrite [zero_add at H3, sub_eq_add_neg at H3, neg_add_cancel_right at H3], exact H3 end
theorem div_pos_of_pos_of_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a / b :=
@ -351,12 +351,12 @@ section linear_ordered_field
theorem exists_add_lt_and_pos_of_lt (H : b < a) : ∃ c : A, b + c < a ∧ c > 0 :=
exists.intro ((a - b) / (1 + 1))
(and.intro (assert H2 : a + a > (b + b) + (a - b), from calc
(and.intro (have H2 : a + a > (b + b) + (a - b), from calc
a + a > b + a : add_lt_add_right H
... = b + a + b - b : add_sub_cancel
... = b + b + a - b : add.right_comm
... = (b + b) + (a - b) : add_sub,
assert H3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
have H3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
from div_lt_div_of_lt_of_pos H2 two_pos,
by rewrite [one_add_one_eq_two, sub_eq_add_neg, add_self_div_two at H3, -div_add_div_same at H3, add_self_div_two at H3];
exact H3)
@ -423,7 +423,7 @@ section discrete_linear_ordered_field
), le_of_one_le_div Hb H'
theorem le_of_one_div_le_one_div_of_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
assert Ha : a ≠ 0, from ne_of_lt (neg_of_one_div_neg (calc
have Ha : a ≠ 0, from ne_of_lt (neg_of_one_div_neg (calc
1 / a ≤ 1 / b : Hl
... < 0 : one_div_neg_of_neg H)),
have H' : -b > 0, from neg_pos_of_neg H,

26
library/algebra/ordered_group.lean
View file

@ -241,12 +241,12 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
theorem ordered_comm_group.le_of_add_le_add_left [ordered_comm_group A] {a b c : A}
(H : a + b ≤ a + c) : b ≤ c :=
assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
by rewrite *neg_add_cancel_left at H'; exact H'
theorem ordered_comm_group.lt_of_add_lt_add_left [ordered_comm_group A] {a b c : A}
(H : a + b < a + c) : b < c :=
assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
have H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
by rewrite *neg_add_cancel_left at H'; exact H'
definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
@ -386,7 +386,7 @@ section
iff.mp !add_le_iff_le_sub_right
theorem le_add_iff_neg_add_le : a ≤ b + c ↔ -b + a ≤ c :=
assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
have H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
theorem le_add_of_neg_add_le {a b c : A} : -b + a ≤ c → a ≤ b + c :=
@ -405,7 +405,7 @@ section
iff.mp !le_add_iff_sub_left_le
theorem le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b :=
assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
have H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
by rewrite [sub_eq_add_neg (b+c) c at H, add_neg_cancel_right at H]; exact H
theorem le_add_of_sub_right_le {a b c : A} : a - c ≤ b → a ≤ b + c :=
@ -415,7 +415,7 @@ section
iff.mp !le_add_iff_sub_right_le
theorem le_add_iff_neg_add_le_left : a ≤ b + c ↔ -b + a ≤ c :=
assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
have H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
theorem le_add_of_neg_add_le_left {a b c : A} : -b + a ≤ c → a ≤ b + c :=
@ -434,8 +434,8 @@ section
iff.mp !le_add_iff_neg_add_le_right
theorem le_add_iff_neg_le_sub_left : c ≤ a + b ↔ -a ≤ b - c :=
assert H : c ≤ a + b ↔ -a + c ≤ b, from !le_add_iff_neg_add_le,
assert H' : -a + c ≤ b ↔ -a ≤ b - c, from !add_le_iff_le_sub_right,
have H : c ≤ a + b ↔ -a + c ≤ b, from !le_add_iff_neg_add_le,
have H' : -a + c ≤ b ↔ -a ≤ b - c, from !add_le_iff_le_sub_right,
iff.trans H H'
theorem le_add_of_neg_le_sub_left {a b c : A} : -a ≤ b - c → c ≤ a + b :=
@ -454,7 +454,7 @@ section
iff.mp !le_add_iff_neg_le_sub_right
theorem add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c :=
assert H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff),
have H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff),
begin rewrite neg_add_cancel_left at H, exact H end
theorem add_lt_of_lt_neg_add_left {a b c : A} : b < -a + c → a + b < c :=
@ -485,7 +485,7 @@ section
iff.mp !add_lt_iff_lt_sub_left
theorem add_lt_iff_lt_sub_right : a + b < c ↔ a < c - b :=
assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
have H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
by rewrite [sub_eq_add_neg at H, add_neg_cancel_right at H]; exact H
theorem add_lt_of_lt_sub_right {a b c : A} : a < c - b → a + b < c :=
@ -495,7 +495,7 @@ section
iff.mp !add_lt_iff_lt_sub_right
theorem lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c :=
assert H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff),
have H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
theorem lt_add_of_neg_add_lt_left {a b c : A} : -b + a < c → a < b + c :=
@ -760,7 +760,7 @@ section
... = abs a + b : by rewrite (abs_of_nonneg H2)
... = abs a + abs b : by rewrite (abs_of_nonneg H3))
(assume H3 : ¬ b ≥ 0,
assert H4 : b ≤ 0, from le_of_lt (lt_of_not_ge H3),
have H4 : b ≤ 0, from le_of_lt (lt_of_not_ge H3),
calc
abs (a + b) = a + b : by rewrite (abs_of_nonneg H1)
... = abs a + b : by rewrite (abs_of_nonneg H2)
@ -791,8 +791,8 @@ section
or.elim (le.total 0 (a + b))
(assume H2 : 0 ≤ a + b, aux2 H2)
(assume H2 : a + b ≤ 0,
assert H3 : -a + -b = -(a + b), by rewrite neg_add,
assert H4 : -(a + b) ≥ 0, from iff.mpr (neg_nonneg_iff_nonpos (a+b)) H2,
have H3 : -a + -b = -(a + b), by rewrite neg_add,
have H4 : -(a + b) ≥ 0, from iff.mpr (neg_nonneg_iff_nonpos (a+b)) H2,
have H5 : -a + -b ≥ 0, begin rewrite -H3 at H4, exact H4 end,
calc
abs (a + b) = abs (-a + -b) : by rewrite [-abs_neg, neg_add]

16
library/algebra/ordered_ring.lean
View file

@ -209,7 +209,7 @@ structure ordered_ring [class] (A : Type)
theorem ordered_ring.mul_le_mul_of_nonneg_left [s : ordered_ring A] {a b c : A}
(Hab : a ≤ b) (Hc : 0 ≤ c) : c * a ≤ c * b :=
have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
assert H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1,
have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1,
begin
rewrite mul_sub_left_distrib at H2,
exact (iff.mp !sub_nonneg_iff_le H2)
@ -218,7 +218,7 @@ end
theorem ordered_ring.mul_le_mul_of_nonneg_right [s : ordered_ring A] {a b c : A}
(Hab : a ≤ b) (Hc : 0 ≤ c) : a * c ≤ b * c :=
have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
assert H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc,
have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc,
begin
rewrite mul_sub_right_distrib at H2,
exact (iff.mp !sub_nonneg_iff_le H2)
@ -227,7 +227,7 @@ end
theorem ordered_ring.mul_lt_mul_of_pos_left [s : ordered_ring A] {a b c : A}
(Hab : a < b) (Hc : 0 < c) : c * a < c * b :=
have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
assert H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1,
have H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1,
begin
rewrite mul_sub_left_distrib at H2,
exact (iff.mp !sub_pos_iff_lt H2)
@ -236,7 +236,7 @@ end
theorem ordered_ring.mul_lt_mul_of_pos_right [s : ordered_ring A] {a b c : A}
(Hab : a < b) (Hc : 0 < c) : a * c < b * c :=
have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
assert H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc,
have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc,
begin
rewrite mul_sub_right_distrib at H2,
exact (iff.mp !sub_pos_iff_lt H2)
@ -264,7 +264,7 @@ section
theorem mul_le_mul_of_nonpos_left (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b :=
have Hc' : -c ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos Hc,
assert H1 : -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left H Hc',
have H1 : -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left H Hc',
have H2 : -(c * b) ≤ -(c * a),
begin
rewrite [-*neg_mul_eq_neg_mul at H1],
@ -274,7 +274,7 @@ section
theorem mul_le_mul_of_nonpos_right (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c :=
have Hc' : -c ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos Hc,
assert H1 : b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right H Hc',
have H1 : b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right H Hc',
have H2 : -(b * c) ≤ -(a * c),
begin
rewrite [-*neg_mul_eq_mul_neg at H1],
@ -291,7 +291,7 @@ section
theorem mul_lt_mul_of_neg_left (H : b < a) (Hc : c < 0) : c * a < c * b :=
have Hc' : -c > 0, from iff.mpr !neg_pos_iff_neg Hc,
assert H1 : -c * b < -c * a, from mul_lt_mul_of_pos_left H Hc',
have H1 : -c * b < -c * a, from mul_lt_mul_of_pos_left H Hc',
have H2 : -(c * b) < -(c * a),
begin
rewrite [-*neg_mul_eq_neg_mul at H1],
@ -301,7 +301,7 @@ section
theorem mul_lt_mul_of_neg_right (H : b < a) (Hc : c < 0) : a * c < b * c :=
have Hc' : -c > 0, from iff.mpr !neg_pos_iff_neg Hc,
assert H1 : b * -c < a * -c, from mul_lt_mul_of_pos_right H Hc',
have H1 : b * -c < a * -c, from mul_lt_mul_of_pos_right H Hc',
have H2 : -(b * c) < -(a * c),
begin
rewrite [-*neg_mul_eq_mul_neg at H1],

4
library/algebra/ring.lean
View file

@ -374,7 +374,7 @@ section
(suppose a * a = b * b,
have (a - b) * (a + b) = 0,
by rewrite [mul.comm, -mul_self_sub_mul_self_eq, this, sub_self],
assert a - b = 0 ∨ a + b = 0, from !eq_zero_or_eq_zero_of_mul_eq_zero this,
have a - b = 0 ∨ a + b = 0, from !eq_zero_or_eq_zero_of_mul_eq_zero this,
or.elim this
(suppose a - b = 0, or.inl (eq_of_sub_eq_zero this))
(suppose a + b = 0, or.inr (eq_neg_of_add_eq_zero this)))
@ -383,7 +383,7 @@ section
(suppose a = -b, by rewrite [this, neg_mul_neg]))
theorem mul_self_eq_one_iff (a : A) : a * a = 1 ↔ a = 1 ∨ a = -1 :=
assert a * a = 1 * 1 ↔ a = 1 ∨ a = -1, from mul_self_eq_mul_self_iff a 1,
have a * a = 1 * 1 ↔ a = 1 ∨ a = -1, from mul_self_eq_mul_self_iff a 1,
by rewrite mul_one at this; exact this
-- TODO: c - b * c → c = 0 ∨ b = 1 and variants

4
library/algebra/ring_power.lean
View file

@ -110,11 +110,11 @@ begin
end
theorem pow_ge_one {x : A} (i : ℕ) (xge1 : x ≥ 1) : x^i ≥ 1 :=
assert H : x^i ≥ 1^i, from pow_le_pow_of_le i (le_of_lt zero_lt_one) xge1,
have H : x^i ≥ 1^i, from pow_le_pow_of_le i (le_of_lt zero_lt_one) xge1,
by rewrite one_pow at H; exact H
theorem pow_gt_one {x : A} {i : ℕ} (xgt1 : x > 1) (ipos : i > 0) : x^i > 1 :=
assert xpos : x > 0, from lt.trans zero_lt_one xgt1,
have xpos : x > 0, from lt.trans zero_lt_one xgt1,
begin
induction i with [i, ih],
{exfalso, exact !lt.irrefl ipos},

68
library/data/bag.lean
View file

@ -107,17 +107,17 @@ protected lemma ext {b₁ b₂ : bag A} : (∀ a, count a b₁ = count a b₂)
quot.induction_on₂ b₁ b₂ (λ l₁ l₂ (h : ∀ a, count a ⟦l₁⟧ = count a ⟦l₂⟧),
have gen : ∀ (l₁ l₂ : list A), (∀ a, list.count a l₁ = list.count a l₂) → l₁ ~ l₂
| [] [] h₁ := !perm.refl
| [] (a₂::s₂) h₁ := assert list.count a₂ [] = list.count a₂ (a₂::s₂), from h₁ a₂, by rewrite [count_nil at this, count_cons_eq at this]; contradiction
| [] (a₂::s₂) h₁ := have list.count a₂ [] = list.count a₂ (a₂::s₂), from h₁ a₂, by rewrite [count_nil at this, count_cons_eq at this]; contradiction
| (a::s₁) s₂ h₁ :=
assert g₁ : list.count a (a::s₁) > 0, from count_gt_zero_of_mem !mem_cons,
assert list.count a (a::s₁) = list.count a s₂, from h₁ a,
assert list.count a s₂ > 0, by rewrite [-this]; exact g₁,
have g₁ : list.count a (a::s₁) > 0, from count_gt_zero_of_mem !mem_cons,
have list.count a (a::s₁) = list.count a s₂, from h₁ a,
have list.count a s₂ > 0, by rewrite [-this]; exact g₁,
have a ∈ s₂, from mem_of_count_gt_zero this,
have ∃ l r, s₂ = l++(a::r), from mem_split this,
obtain l r (e₁ : s₂ = l++(a::r)), from this,
have ∀ a, list.count a s₁ = list.count a (l++r), from
take a₁,
assert e₂ : list.count a₁ (a::s₁) = list.count a₁ (l++(a::r)), by rewrite -e₁; exact h₁ a₁,
have e₂ : list.count a₁ (a::s₁) = list.count a₁ (l++(a::r)), by rewrite -e₁; exact h₁ a₁,
by_cases
(suppose a₁ = a, begin
rewrite [-this at e₂, list.count_append at e₂, *count_cons_eq at e₂, add_succ at e₂],
@ -134,7 +134,7 @@ quot.induction_on₂ b₁ b₂ (λ l₁ l₂ (h : ∀ a, count a ⟦l₁⟧ = co
definition insert.inj {a : A} {b₁ b₂ : bag A} : insert a b₁ = insert a b₂ → b₁ = b₂ :=
assume h, bag.ext (take x,
assert e : count x (insert a b₁) = count x (insert a b₂), by rewrite h,
have e : count x (insert a b₁) = count x (insert a b₂), by rewrite h,
by_cases
(suppose x = a, begin subst x, rewrite [*count_insert at e], injection e, assumption end)
(suppose x ≠ a, begin rewrite [*count_insert_of_ne this at e], assumption end))
@ -274,8 +274,8 @@ private definition min_count (l₁ l₂ : list A) : list A → list A
private lemma not_mem_max_count_of_not_mem (l₁ l₂ : list A) : ∀ {a l}, a ∉ l → a ∉ max_count l₁ l₂ l
| a [] h := !not_mem_nil
| a (b::l) h :=
assert ih : a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem (not_mem_of_not_mem_cons h),
assert a ≠ b, from ne_of_not_mem_cons h,
have ih : a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem (not_mem_of_not_mem_cons h),
have a ≠ b, from ne_of_not_mem_cons h,
by_cases
(suppose list.count b l₁ ≥ list.count b l₂, begin
unfold max_count, rewrite [if_pos this],
@ -289,12 +289,12 @@ private lemma not_mem_max_count_of_not_mem (l₁ l₂ : list A) : ∀ {a l}, a
private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a ∈ l → nodup l → list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂)
| a [] h₁ h₂ := absurd h₁ !not_mem_nil
| a (b::l) h₁ h₂ :=
assert nodup l, from nodup_of_nodup_cons h₂,
assert b ∉ l, from not_mem_of_nodup_cons h₂,
have nodup l, from nodup_of_nodup_cons h₂,
have b ∉ l, from not_mem_of_nodup_cons h₂,
or.elim (eq_or_mem_of_mem_cons h₁)
(suppose a = b,
have a ∉ l, by rewrite this; assumption,
assert a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem l₁ l₂ this,
have a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem l₁ l₂ this,
by_cases
(suppose i : list.count a l₁ ≥ list.count a l₂, begin
unfold max_count, subst b,
@ -305,8 +305,8 @@ private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
rewrite [if_neg i, list.count_append, count_gen, max_eq_right_of_lt (lt_of_not_ge i), count_eq_zero_of_not_mem `a ∉ max_count l₁ l₂ l`]
end))
(suppose a ∈ l,
assert a ≠ b, from suppose a = b, begin subst b, contradiction end,
assert ih : list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂), from
have a ≠ b, from suppose a = b, begin subst b, contradiction end,
have ih : list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂), from
max_count_eq `a ∈ l` `nodup l`,
by_cases
(suppose i : list.count b l₁ ≥ list.count b l₂, begin
@ -321,8 +321,8 @@ private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
private lemma not_mem_min_count_of_not_mem (l₁ l₂ : list A) : ∀ {a l}, a ∉ l → a ∉ min_count l₁ l₂ l
| a [] h := !not_mem_nil
| a (b::l) h :=
assert ih : a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem (not_mem_of_not_mem_cons h),
assert a ≠ b, from ne_of_not_mem_cons h,
have ih : a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem (not_mem_of_not_mem_cons h),
have a ≠ b, from ne_of_not_mem_cons h,
by_cases
(suppose list.count b l₁ ≤ list.count b l₂, begin
unfold min_count, rewrite [if_pos this],
@ -336,12 +336,12 @@ private lemma not_mem_min_count_of_not_mem (l₁ l₂ : list A) : ∀ {a l}, a
private lemma min_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a ∈ l → nodup l → list.count a (min_count l₁ l₂ l) = min (list.count a l₁) (list.count a l₂)
| a [] h₁ h₂ := absurd h₁ !not_mem_nil
| a (b::l) h₁ h₂ :=
assert nodup l, from nodup_of_nodup_cons h₂,
assert b ∉ l, from not_mem_of_nodup_cons h₂,
have nodup l, from nodup_of_nodup_cons h₂,
have b ∉ l, from not_mem_of_nodup_cons h₂,
or.elim (eq_or_mem_of_mem_cons h₁)
(suppose a = b,
have a ∉ l, by rewrite this; assumption,
assert a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem l₁ l₂ this,
have a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem l₁ l₂ this,
by_cases
(suppose i : list.count a l₁ ≤ list.count a l₂, begin
unfold min_count, subst b,
@ -352,8 +352,8 @@ private lemma min_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
rewrite [if_neg i, list.count_append, count_gen, min_eq_right (le_of_lt (lt_of_not_ge i)), count_eq_zero_of_not_mem `a ∉ min_count l₁ l₂ l`]
end))
(suppose a ∈ l,
assert a ≠ b, from suppose a = b, by subst b; contradiction,
assert ih : list.count a (min_count l₁ l₂ l) = min (list.count a l₁) (list.count a l₂), from min_count_eq `a ∈ l` `nodup l`,
have a ≠ b, from suppose a = b, by subst b; contradiction,
have ih : list.count a (min_count l₁ l₂ l) = min (list.count a l₁) (list.count a l₂), from min_count_eq `a ∈ l` `nodup l`,
by_cases
(suppose i : list.count b l₁ ≤ list.count b l₂, begin
unfold min_count,
@ -367,8 +367,8 @@ private lemma min_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
private lemma perm_max_count_left {l₁ l₂ l₃ l₄ : list A} (h₁ : l₁ ~ l₃) (h₂ : l₂ ~ l₄) : ∀ l, max_count l₁ l₂ l ~ max_count l₃ l₄ l
| [] := by esimp
| (a::l) :=
assert e₁ : list.count a l₁ = list.count a l₃, from count_eq_of_perm h₁ a,
assert e₂ : list.count a l₂ = list.count a l₄, from count_eq_of_perm h₂ a,
have e₁ : list.count a l₁ = list.count a l₃, from count_eq_of_perm h₁ a,
have e₂ : list.count a l₂ = list.count a l₄, from count_eq_of_perm h₂ a,
by_cases
(suppose list.count a l₁ ≥ list.count a l₂,
begin unfold max_count, rewrite [-e₁, -e₂, *if_pos this], exact perm_app !perm.refl !perm_max_count_left end)
@ -408,8 +408,8 @@ calc max_count l₁ l₂ l₃ ~ max_count r₁ r₂ l₃ : perm_max_count_left p
private lemma perm_min_count_left {l₁ l₂ l₃ l₄ : list A} (h₁ : l₁ ~ l₃) (h₂ : l₂ ~ l₄) : ∀ l, min_count l₁ l₂ l ~ min_count l₃ l₄ l
| [] := by esimp
| (a::l) :=
assert e₁ : list.count a l₁ = list.count a l₃, from count_eq_of_perm h₁ a,
assert e₂ : list.count a l₂ = list.count a l₄, from count_eq_of_perm h₂ a,
have e₁ : list.count a l₁ = list.count a l₃, from count_eq_of_perm h₁ a,
have e₂ : list.count a l₂ = list.count a l₄, from count_eq_of_perm h₂ a,
by_cases
(suppose list.count a l₁ ≤ list.count a l₂,
begin unfold min_count, rewrite [-e₁, -e₂, *if_pos this], exact perm_app !perm.refl !perm_min_count_left end)
@ -455,9 +455,9 @@ lemma count_union (a : A) (b₁ b₂ : bag A) : count a (b₁ ∪ b₂) = max (c
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, by_cases
(suppose a ∈ union_list l₁ l₂, !max_count_eq this !nodup_union_list)
(suppose ¬ a ∈ union_list l₁ l₂,
assert ¬ a ∈ l₁, from not_mem_of_not_mem_union_list_left `¬ a ∈ union_list l₁ l₂`,
assert ¬ a ∈ l₂, from not_mem_of_not_mem_union_list_right `¬ a ∈ union_list l₁ l₂`,
assert n : ¬ a ∈ max_count l₁ l₂ (union_list l₁ l₂), from not_mem_max_count_of_not_mem l₁ l₂ `¬ a ∈ union_list l₁ l₂`,
have ¬ a ∈ l₁, from not_mem_of_not_mem_union_list_left `¬ a ∈ union_list l₁ l₂`,
have ¬ a ∈ l₂, from not_mem_of_not_mem_union_list_right `¬ a ∈ union_list l₁ l₂`,
have n : ¬ a ∈ max_count l₁ l₂ (union_list l₁ l₂), from not_mem_max_count_of_not_mem l₁ l₂ `¬ a ∈ union_list l₁ l₂`,
begin
unfold [union, count],
rewrite [count_eq_zero_of_not_mem `¬ a ∈ l₁`, count_eq_zero_of_not_mem `¬ a ∈ l₂`, max_self],
@ -468,9 +468,9 @@ lemma count_inter (a : A) (b₁ b₂ : bag A) : count a (b₁ ∩ b₂) = min (c
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, by_cases
(suppose a ∈ union_list l₁ l₂, !min_count_eq this !nodup_union_list)
(suppose ¬ a ∈ union_list l₁ l₂,
assert ¬ a ∈ l₁, from not_mem_of_not_mem_union_list_left `¬ a ∈ union_list l₁ l₂`,
assert ¬ a ∈ l₂, from not_mem_of_not_mem_union_list_right `¬ a ∈ union_list l₁ l₂`,
assert n : ¬ a ∈ min_count l₁ l₂ (union_list l₁ l₂), from not_mem_min_count_of_not_mem l₁ l₂ `¬ a ∈ union_list l₁ l₂`,
have ¬ a ∈ l₁, from not_mem_of_not_mem_union_list_left `¬ a ∈ union_list l₁ l₂`,
have ¬ a ∈ l₂, from not_mem_of_not_mem_union_list_right `¬ a ∈ union_list l₁ l₂`,
have n : ¬ a ∈ min_count l₁ l₂ (union_list l₁ l₂), from not_mem_min_count_of_not_mem l₁ l₂ `¬ a ∈ union_list l₁ l₂`,
begin
unfold [inter, count],
rewrite [count_eq_zero_of_not_mem `¬ a ∈ l₁`, count_eq_zero_of_not_mem `¬ a ∈ l₂`, min_self],
@ -653,10 +653,10 @@ private lemma all_of_subcount_eq_tt : ∀ {l₁ l₂ : list A}, subcount l₁ l
| [] l₂ h := take x, !zero_le
| (a::l₁) l₂ h := take x,
have subcount l₁ l₂ = tt, from by_contradiction (suppose subcount l₁ l₂ ≠ tt,
assert subcount l₁ l₂ = ff, from eq_ff_of_ne_tt this,
have subcount l₁ l₂ = ff, from eq_ff_of_ne_tt this,
begin unfold subcount at h, rewrite [this at h, if_t_t at h], contradiction end),
assert ih : ∀ a, list.count a l₁ ≤ list.count a l₂, from all_of_subcount_eq_tt this,
assert i : list.count a (a::l₁) ≤ list.count a l₂, from by_contradiction (suppose ¬ list.count a (a::l₁) ≤ list.count a l₂,
have ih : ∀ a, list.count a l₁ ≤ list.count a l₂, from all_of_subcount_eq_tt this,
have i : list.count a (a::l₁) ≤ list.count a l₂, from by_contradiction (suppose ¬ list.count a (a::l₁) ≤ list.count a l₂,
begin unfold subcount at h, rewrite [if_neg this at h], contradiction end),
by_cases
(suppose x = a, by rewrite this; apply i)
@ -667,7 +667,7 @@ private lemma ex_of_subcount_eq_ff : ∀ {l₁ l₂ : list A}, subcount l₁ l
| (a::l₁) l₂ h := by_cases
(suppose i : list.count a (a::l₁) ≤ list.count a l₂,
have subcount l₁ l₂ = ff, from by_contradiction (suppose subcount l₁ l₂ ≠ ff,
assert subcount l₁ l₂ = tt, from eq_tt_of_ne_ff this,
have subcount l₁ l₂ = tt, from eq_tt_of_ne_ff this,
begin
unfold subcount at h,
rewrite [if_pos i at h, this at h],

18
library/data/encodable.lean
View file

@ -19,7 +19,7 @@ definition countable_of_encodable {A : Type} : encodable A → countable A :=
assume e : encodable A,
have injective encode, from
λ (a₁ a₂ : A) (h : encode a₁ = encode a₂),
assert decode A (encode a₁) = decode A (encode a₂), by rewrite h,
have decode A (encode a₁) = decode A (encode a₂), by rewrite h,
by rewrite [*encodek at this]; injection this; assumption,
exists.intro encode this
@ -71,16 +71,16 @@ else
open decidable
private theorem decode_encode_sum : ∀ s : sum A B, decode_sum (encode_sum s) = some s
| (sum.inl a) :=
assert aux : 2 > (0:nat), from dec_trivial,
have aux : 2 > (0:nat), from dec_trivial,
begin
esimp [encode_sum, decode_sum],
rewrite [mul_mod_right, if_pos (eq.refl (0 : nat)), nat.mul_div_cancel_left _ aux,
encodable.encodek]
end
| (sum.inr b) :=
assert aux₁ : 2 > (0:nat), from dec_trivial,
assert aux₂ : 1 % 2 = (1:nat), by rewrite [nat.mod_def],
assert aux₃ : 1 ≠ (0:nat), from dec_trivial,
have aux₁ : 2 > (0:nat), from dec_trivial,
have aux₂ : 1 % 2 = (1:nat), by rewrite [nat.mod_def],
have aux₃ : 1 ≠ (0:nat), from dec_trivial,
begin
esimp [encode_sum, decode_sum],
rewrite [add.comm, add_mul_mod_self_left, aux₂, if_neg aux₃, nat.add_sub_cancel_left,
@ -225,9 +225,9 @@ private lemma enle.total (a b : A) : enle a b ∨ enle b a :=
private lemma enle.antisymm (a b : A) : enle a b → enle b a → a = b :=
assume h₁ h₂,
assert encode a = encode b, from le.antisymm h₁ h₂,
assert decode A (encode a) = decode A (encode b), by rewrite this,
assert some a = some b, by rewrite [*encodek at this]; exact this,
have encode a = encode b, from le.antisymm h₁ h₂,
have decode A (encode a) = decode A (encode b), by rewrite this,
have some a = some b, by rewrite [*encodek at this]; exact this,
option.no_confusion this (λ e, e)
private definition decidable_enle [instance] (a b : A) : decidable (enle a b) :=
@ -248,7 +248,7 @@ quot.lift_on s
(λ l, encode (ensort (elt_of l)))
(λ l₁ l₂ p,
have elt_of l₁ ~ elt_of l₂, from p,
assert ensort (elt_of l₁) = ensort (elt_of l₂), from sorted_eq_of_perm this,
have ensort (elt_of l₁) = ensort (elt_of l₂), from sorted_eq_of_perm this,
by rewrite this)
private definition decode_finset (n : nat) : option (finset A) :=

10
library/data/equiv.lean
View file

@ -32,9 +32,9 @@ definition inv {A B : Type} [e : equiv A B] : B → A :=
lemma eq_of_to_fun_eq {A B : Type} : ∀ {e₁ e₂ : equiv A B}, fn e₁ = fn e₂ → e₁ = e₂
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) h :=
assert f₁ = f₂, from h,
assert g₁ = g₂, from funext (λ x,
assert f₁ (g₁ x) = f₂ (g₂ x), from eq.trans (r₁ x) (eq.symm (r₂ x)),
have f₁ = f₂, from h,
have g₁ = g₂, from funext (λ x,
have f₁ (g₁ x) = f₂ (g₂ x), from eq.trans (r₁ x) (eq.symm (r₂ x)),
have f₁ (g₁ x) = f₁ (g₂ x), begin subst f₂, exact this end,
show g₁ x = g₂ x, from injective_of_left_inverse l₁ this),
by congruence; repeat assumption
@ -295,7 +295,7 @@ open decidable
definition decidable_eq_of_equiv {A B : Type} [h : decidable_eq A] : A ≃ B → decidable_eq B
| (mk f g l r) :=
take b₁ b₂, match h (g b₁) (g b₂) with
| inl he := inl (assert aux : f (g b₁) = f (g b₂), from congr_arg f he,
| inl he := inl (have aux : f (g b₁) = f (g b₂), from congr_arg f he,
begin rewrite *r at aux, exact aux end)
| inr hn := inr (λ b₁eqb₂, by subst b₁eqb₂; exact absurd rfl hn)
end
@ -330,7 +330,7 @@ by_cases
(suppose r = a, by_cases
(suppose r = b, begin unfold swap_core, rewrite [if_pos `r = a`, if_pos (eq.refl b), -`r = a`, -`r = b`, if_pos (eq.refl r)] end)
(suppose ¬ r = b,
assert b ≠ a, from assume h, begin rewrite h at this, contradiction end,
have b ≠ a, from assume h, begin rewrite h at this, contradiction end,
begin unfold swap_core, rewrite [*if_pos `r = a`, if_pos (eq.refl b), if_neg `b ≠ a`, `r = a`] end))
(suppose ¬ r = a, by_cases
(suppose r = b, begin unfold swap_core, rewrite [if_neg `¬ r = a`, *if_pos `r = b`, if_pos (eq.refl a), this] end)

8
library/data/examples/vector.lean
View file

@ -257,11 +257,11 @@ namespace vector
| 0 (m+1) [] (y::ys) h₁ h₂ := by contradiction
| (n+1) 0 (x::xs) [] h₁ h₂ := by contradiction
| (n+1) (m+1) (x::xs) (y::ys) h₁ h₂ :=
assert e₁ : n = m, from succ.inj h₂,
assert e₂ : x = y, begin unfold to_list at h₁, injection h₁, assumption end,
have e₁ : n = m, from succ.inj h₂,
have e₂ : x = y, begin unfold to_list at h₁, injection h₁, assumption end,
have e₃ : to_list xs = to_list ys, begin unfold to_list at h₁, injection h₁, assumption end,
assert xs == ys, from heq_of_list_eq e₃ e₁,
assert y :: xs == y :: ys, begin clear heq_of_list_eq h₁ h₂ e₃, revert xs ys this, induction e₁, intro xs ys h, rewrite [eq_of_heq h] end,
have xs == ys, from heq_of_list_eq e₃ e₁,
have y :: xs == y :: ys, begin clear heq_of_list_eq h₁ h₂ e₃, revert xs ys this, induction e₁, intro xs ys h, rewrite [eq_of_heq h] end,
show x :: xs == y :: ys, by rewrite e₂; exact this
theorem list_eq_of_heq {n m} {v₁ : vector A n} {v₂ : vector A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ :=

26
library/data/fin.lean
View file

@ -54,7 +54,7 @@ dmap_nodup_of_dinj (dinj_lt n) (list.nodup_upto n)
lemma mem_upto (n : nat) : ∀ (i : fin n), i ∈ upto n :=
take i, fin.destruct i
(take ival Piltn,
assert ival ∈ list.upto n, from mem_upto_of_lt Piltn,
have ival ∈ list.upto n, from mem_upto_of_lt Piltn,
mem_dmap Piltn this)
lemma upto_zero : upto 0 = [] :=
@ -138,7 +138,7 @@ by intro hlt he; substvars; exact absurd hlt (lt.irrefl n)
lemma lt_max_of_ne_max {i : fin (succ n)} : i ≠ maxi → i < n :=
assume hne : i ≠ maxi,
assert vne : val i ≠ n, from
have vne : val i ≠ n, from
assume he,
have val (@maxi n) = n, from rfl,
have val i = val (@maxi n), from he ⬝ this⁻¹,
@ -160,7 +160,7 @@ take i j, destruct i (destruct j (take iv ilt jv jlt Pmkeq,
lemma lt_of_inj_of_max (f : fin (succ n) → fin (succ n)) :
injective f → (f maxi = maxi) → ∀ i : fin (succ n), i < n → f i < n :=
assume Pinj Peq, take i, assume Pilt,
assert P1 : f i = f maxi → i = maxi, from assume Peq, Pinj i maxi Peq,
have P1 : f i = f maxi → i = maxi, from assume Peq, Pinj i maxi Peq,
have f i ≠ maxi, from
begin rewrite -Peq, intro P2, apply absurd (P1 P2) (ne_max_of_lt_max Pilt) end,
lt_max_of_ne_max this
@ -188,7 +188,7 @@ end
lemma lift_fun_of_inj {f : fin n → fin n} : injective f → injective (lift_fun f) :=
assume Pinj, take i j,
assert Pdi : decidable (i = maxi), from _, assert Pdj : decidable (j = maxi), from _,
have Pdi : decidable (i = maxi), from _, have Pdj : decidable (j = maxi), from _,
begin
cases Pdi with Pimax Pinmax,
cases Pdj with Pjmax Pjnmax,
@ -205,7 +205,7 @@ end
lemma lift_fun_inj : injective (@lift_fun n) :=
take f₁ f₂ Peq, funext (λ i,
assert lift_fun f₁ (lift_succ i) = lift_fun f₂ (lift_succ i), from congr_fun Peq _,
have lift_fun f₁ (lift_succ i) = lift_fun f₂ (lift_succ i), from congr_fun Peq _,
begin revert this, rewrite [*lift_fun_eq], apply lift_succ_inj end)
lemma lower_inj_apply {f Pinj Pmax} (i : fin n) :
@ -299,7 +299,7 @@ begin
let vj := nat.pred vk in
have vk = vj+1, from
eq.symm (succ_pred_of_pos HT),
assert vj < n, from
have vj < n, from
lt_of_succ_lt_succ (eq.subst `vk = vj+1` pk),
have succ (mk vj `vj < n`) = mk vk pk, from
val_inj (eq.symm `vk = vj+1`),
@ -405,7 +405,7 @@ definition fin_one_equiv_unit : fin 1 ≃ unit :=
⦄
definition fin_sum_equiv (n m : nat) : (fin n + fin m) ≃ fin (n+m) :=
assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
have aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
take v, suppose v < m, calc
v + n < m + n : add_lt_add_of_lt_of_le this !le.refl
... = n + m : add.comm,
@ -425,7 +425,7 @@ assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
{ cases f₂ with v hlt, esimp,
have ¬ v + n < n, from
suppose v + n < n,
assert v < n - n, from nat.lt_sub_of_add_lt this !le.refl,
have v < n - n, from nat.lt_sub_of_add_lt this !le.refl,
have v < 0, by rewrite [nat.sub_self at this]; exact this,
absurd this !not_lt_zero,
rewrite [dif_neg this], congruence, congruence, rewrite [nat.add_sub_cancel] }
@ -439,17 +439,17 @@ assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
definition fin_prod_equiv_of_pos (n m : nat) : n > 0 → (fin n × fin m) ≃ fin (n*m) :=
suppose n > 0,
assert aux₁ : ∀ {v₁ v₂}, v₁ < n → v₂ < m → v₁ + v₂ * n < n*m, from
have aux₁ : ∀ {v₁ v₂}, v₁ < n → v₂ < m → v₁ + v₂ * n < n*m, from
take v₁ v₂, assume h₁ h₂,
have nat.succ v₂ ≤ m, from succ_le_of_lt h₂,
assert nat.succ v₂ * n ≤ m * n, from mul_le_mul_right _ this,
have nat.succ v₂ * n ≤ m * n, from mul_le_mul_right _ this,
have v₂ * n + n ≤ n * m, by rewrite [-add_one at this, right_distrib at this, one_mul at this, mul.comm m n at this]; exact this,
assert v₁ + (v₂ * n + n) < n + n * m, from add_lt_add_of_lt_of_le h₁ this,
have v₁ + (v₂ * n + n) < n + n * m, from add_lt_add_of_lt_of_le h₁ this,
have v₁ + v₂ * n + n < n * m + n, by rewrite [add.assoc, add.comm (n*m) n]; exact this,
lt_of_add_lt_add_right this,
assert aux₂ : ∀ v, v % n < n, from
have aux₂ : ∀ v, v % n < n, from
take v, mod_lt _ `n > 0`,
assert aux₃ : ∀ {v}, v < n * m → v / n < m, from
have aux₃ : ∀ {v}, v < n * m → v / n < m, from
take v, assume h, by rewrite mul.comm at h; exact nat.div_lt_of_lt_mul h,
⦃ equiv,
to_fun := λ p : (fin n × fin m), match p with (mk v₁ hlt₁, mk v₂ hlt₂) := mk (v₁ + v₂ * n) (aux₁ hlt₁ hlt₂) end,

14
library/data/finset/basic.lean
View file

@ -52,7 +52,7 @@ definition to_finset [decidable_eq A] (l : list A) : finset A :=
lemma to_finset_eq_of_nodup [decidable_eq A] {l : list A} (n : nodup l) :
to_finset_of_nodup l n = to_finset l :=
assert P : to_nodup_list_of_nodup n = to_nodup_list l, from
have P : to_nodup_list_of_nodup n = to_nodup_list l, from
begin
rewrite [↑to_nodup_list, ↑to_nodup_list_of_nodup],
congruence,
@ -237,11 +237,11 @@ quot.induction_on s
(assume nodup_l, H1)
(take a l',
assume IH nodup_al',
assert aux₁: a ∉ l', from not_mem_of_nodup_cons nodup_al',
assert e : list.insert a l' = a :: l', from insert_eq_of_not_mem aux₁,
assert nodup l', from nodup_of_nodup_cons nodup_al',
assert P (quot.mk (subtype.tag l' this)), from IH this,
assert P (insert a (quot.mk (subtype.tag l' _))), from H2 aux₁ this,
have aux₁: a ∉ l', from not_mem_of_nodup_cons nodup_al',
have e : list.insert a l' = a :: l', from insert_eq_of_not_mem aux₁,
have nodup l', from nodup_of_nodup_cons nodup_al',
have P (quot.mk (subtype.tag l' this)), from IH this,
have P (insert a (quot.mk (subtype.tag l' _))), from H2 aux₁ this,
begin
revert nodup_al',
rewrite [-e],
@ -319,7 +319,7 @@ theorem erase_insert {a : A} {s : finset A} : a ∉ s → erase a (insert a s) =
(λ bin, by subst b; contradiction))
(λ bnea : b ≠ a, iff.intro
(λ bin,
assert b ∈ insert a s, from mem_of_mem_erase bin,
have b ∈ insert a s, from mem_of_mem_erase bin,
mem_of_mem_insert_of_ne this bnea)
(λ bin,
have b ∈ insert a s, from mem_insert_of_mem _ bin,

16
library/data/finset/card.lean
View file

@ -22,7 +22,7 @@ begin
show card s₁ + card (insert a s₂) = card (s₁ ∪ (insert a s₂)) + card (s₁ ∩ (insert a s₂)),
from decidable.by_cases
(assume as1 : a ∈ s₁,
assert H : a ∉ s₁ ∩ s₂, from assume H', ans2 (mem_of_mem_inter_right H'),
have H : a ∉ s₁ ∩ s₂, from assume H', ans2 (mem_of_mem_inter_right H'),
begin
rewrite [card_insert_of_not_mem ans2, union_comm, -insert_union, union_comm],
rewrite [insert_union, insert_eq_of_mem as1, insert_eq, inter_distrib_left, inter_comm],
@ -30,7 +30,7 @@ begin
rewrite IH
end)
(assume ans1 : a ∉ s₁,
assert H : a ∉ s₁ ∪ s₂, from assume H',
have H : a ∉ s₁ ∪ s₂, from assume H',
or.elim (mem_or_mem_of_mem_union H') (assume as1, ans1 as1) (assume as2, ans2 as2),
begin
rewrite [card_insert_of_not_mem ans2, union_comm, -insert_union, union_comm],
@ -92,8 +92,8 @@ lemma card_le_of_inj_on (a : finset A) (b : finset B)
(Pex : ∃ f : A → B, set.inj_on f (ts a) ∧ (image f a ⊆ b)):
card a ≤ card b :=
obtain f Pinj, from Pex,
assert Psub : _, from and.right Pinj,
assert Ple : card (image f a) ≤ card b, from card_le_card_of_subset Psub,
have Psub : _, from and.right Pinj,
have Ple : card (image f a) ≤ card b, from card_le_card_of_subset Psub,
by rewrite [(card_image_eq_of_inj_on (and.left Pinj))⁻¹]; exact Ple
theorem card_image_le (f : A → B) (s : finset A) : card (image f s) ≤ card s :=
@ -167,7 +167,7 @@ theorem eq_of_card_eq_of_subset {s₁ s₂ : finset A} (Hcard : card s₁ = card
s₁ = s₂ :=
have H : card s₁ + 0 = card s₁ + card (s₂ \ s₁),
by rewrite [Hcard at {1}, card_eq_card_add_card_diff Hsub],
assert H1 : s₂ \ s₁ = ∅, from eq_empty_of_card_eq_zero (add.left_cancel H)⁻¹,
have H1 : s₂ \ s₁ = ∅, from eq_empty_of_card_eq_zero (add.left_cancel H)⁻¹,
by rewrite [-union_diff_cancel Hsub, H1, union_empty]
lemma exists_two_of_card_gt_one {s : finset A} : 1 < card s → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
@ -210,12 +210,12 @@ finset.induction_on s
have H2 : ∀ a₁ a₂ : A, a₁ ∈ s' → a₂ ∈ s' → a₁ ≠ a₂ → f a₁ ∩ f a₂ = ∅, from
take a₁ a₂, assume H3 H4 H5,
H1 (!mem_insert_of_mem H3) (!mem_insert_of_mem H4) H5,
assert H6 : card (⋃ (x : A) ∈ s', f x) = ∑ (x : A) ∈ s', card (f x), from IH H2,
assert H7 : ∀ x, x ∈ s' → f a ∩ f x = ∅, from
have H6 : card (⋃ (x : A) ∈ s', f x) = ∑ (x : A) ∈ s', card (f x), from IH H2,
have H7 : ∀ x, x ∈ s' → f a ∩ f x = ∅, from
take x, assume xs',
have anex : a ≠ x, from assume aex, (eq.subst aex H) xs',
H1 !mem_insert (!mem_insert_of_mem xs') anex,
assert H8 : f a ∩ (⋃ (x : A) ∈ s', f x) = ∅, from
have H8 : f a ∩ (⋃ (x : A) ∈ s', f x) = ∅, from
calc
f a ∩ (⋃ (x : A) ∈ s', f x) = (⋃ (x : A) ∈ s', f a ∩ f x) : by rewrite inter_Union
... = (⋃ (x : A) ∈ s', ∅) : by rewrite [Union_ext H7]

2
library/data/finset/comb.lean
View file

@ -460,7 +460,7 @@ begin
apply yps
end))
(assume H : x ⊆ insert a s,
assert H' : erase a x ⊆ s, from erase_subset_of_subset_insert H,
have H' : erase a x ⊆ s, from erase_subset_of_subset_insert H,
decidable.by_cases
(suppose a ∈ x,
or.inr (exists.intro (erase a x)

30
library/data/finset/equiv.lean
View file

@ -35,8 +35,8 @@ private lemma mem_of_nat_of_odd {n : nat} {s : nat} : odd (s / 2^n) → n ∈ of
assume h,
have 2^n < succ s, from by_contradiction
(suppose ¬(2^n < succ s),
assert 2^n > s, from lt_of_succ_le (le_of_not_gt this),
assert s / 2^n = 0, from div_eq_zero_of_lt this,
have 2^n > s, from lt_of_succ_le (le_of_not_gt this),
have s / 2^n = 0, from div_eq_zero_of_lt this,
by rewrite this at h; exact absurd h dec_trivial),
have n < succ s, from calc
n ≤ 2^n : le_pow_self dec_trivial n
@ -47,12 +47,12 @@ mem_sep_of_mem this h
private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n ∈ of_nat (s / 2) :=
iff.intro
(suppose succ n ∈ of_nat s,
assert odd (s / 2^(succ n)), from odd_of_mem_of_nat this,
have odd (s / 2^(succ n)), from odd_of_mem_of_nat this,
have odd ((s / 2) / (2 ^ n)), by rewrite [pow_succ' at this, nat.div_div_eq_div_mul, mul.comm]; assumption,
show n ∈ of_nat (s / 2), from mem_of_nat_of_odd this)
(suppose n ∈ of_nat (s / 2),
assert odd ((s / 2) / (2 ^ n)), from odd_of_mem_of_nat this,
assert odd (s / 2^(succ n)), by rewrite [pow_succ', mul.comm, -nat.div_div_eq_div_mul]; assumption,
have odd ((s / 2) / (2 ^ n)), from odd_of_mem_of_nat this,
have odd (s / 2^(succ n)), by rewrite [pow_succ', mul.comm, -nat.div_div_eq_div_mul]; assumption,
show succ n ∈ of_nat s, from mem_of_nat_of_odd this)
private lemma odd_of_zero_mem (s : nat) : 0 ∈ of_nat s ↔ odd s :=
@ -78,7 +78,7 @@ finset.induction_on s dec_trivial
suppose even (2^a + to_nat s), by_cases
(suppose e : even (2^a), by_cases
(suppose even (to_nat s),
assert 0 ∉ s, from iff.mp ih this,
have 0 ∉ s, from iff.mp ih this,
suppose 0 ∈ insert a s, or.elim (eq_or_mem_of_mem_insert this)
(suppose 0 = a, begin rewrite [-this at e], exact absurd e not_even_one end)
(by contradiction))
@ -90,7 +90,7 @@ finset.induction_on s dec_trivial
have even (to_nat s), from iff.mpr ih (by rewrite -this at nains; exact nains),
absurd this `odd (to_nat s)`)
(suppose 0 ∈ s,
assert a ≠ 0, from suppose a = 0, by subst a; contradiction,
have a ≠ 0, from suppose a = 0, by subst a; contradiction,
begin
cases a with a, exact absurd rfl `0 ≠ 0`,
have odd (2*2^a), by rewrite [pow_succ' at o, mul.comm]; exact o,
@ -111,9 +111,9 @@ finset.induction_on s dec_trivial
private lemma of_nat_eq_insert_zero {s : nat} : 0 ∉ of_nat s → of_nat (2^0 + s) = insert 0 (of_nat s) :=
assume h : 0 ∉ of_nat s,
assert even s, from iff.mp (even_of_not_zero_mem s) h,
have even s, from iff.mp (even_of_not_zero_mem s) h,
have odd (s+1), from odd_succ_of_even this,
assert zmem : 0 ∈ of_nat (s+1), from iff.mpr (odd_of_zero_mem (s+1)) this,
have zmem : 0 ∈ of_nat (s+1), from iff.mpr (odd_of_zero_mem (s+1)) this,
obtain w (hw : s = 2*w), from exists_of_even `even s`,
begin
rewrite [pow_zero, add.comm, hw],
@ -122,8 +122,8 @@ begin
match n with
| 0 := iff.intro (λ h, !mem_insert) (λ h, by rewrite [hw at zmem]; exact zmem)
| succ m :=
assert d₁ : 1 / 2 = (0:nat), from dec_trivial,
assert aux : _, from calc
have d₁ : 1 / 2 = (0:nat), from dec_trivial,
have aux : _, from calc
succ m ∈ of_nat (2 * w + 1) ↔ m ∈ of_nat ((2*w+1) / 2) : succ_mem_of_nat
... ↔ m ∈ of_nat w : by rewrite [add.comm, add_mul_div_self_left _ _ (dec_trivial : 2 > 0), d₁, zero_add]
... ↔ m ∈ of_nat (2*w / 2) : by rewrite [mul.comm, nat.mul_div_cancel _ (dec_trivial : 2 > 0)]
@ -141,7 +141,7 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n
| (succ n) s h :=
have n ∉ of_nat (s / 2),
from iff.mp (not_iff_not_of_iff !succ_mem_of_nat) h,
assert ih : of_nat (2^n + s / 2) = insert n (of_nat (s / 2)), from of_nat_eq_insert this,
have ih : of_nat (2^n + s / 2) = insert n (of_nat (s / 2)), from of_nat_eq_insert this,
finset.ext (λ x,
have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s)
| zero :=
@ -163,13 +163,13 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n
... ↔ odd s : aux₁
... ↔ 0 ∈ insert (succ n) (of_nat s) : aux₂
| (succ m) :=
assert aux : m ∈ insert n (of_nat (s / 2)) ↔ succ m ∈ insert (succ n) (of_nat s), from iff.intro
have aux : m ∈ insert n (of_nat (s / 2)) ↔ succ m ∈ insert (succ n) (of_nat s), from iff.intro
(assume hl, or.elim (eq_or_mem_of_mem_insert hl)
(suppose m = n, by subst m; apply mem_insert)
(suppose m ∈ of_nat (s / 2), finset.mem_insert_of_mem _ (iff.mpr !succ_mem_of_nat this)))
(assume hr, or.elim (eq_or_mem_of_mem_insert hr)
(suppose succ m = succ n,
assert m = n, by injection this; assumption,
have m = n, by injection this; assumption,
by subst m; apply mem_insert)
(suppose succ m ∈ of_nat s, finset.mem_insert_of_mem _ (iff.mp !succ_mem_of_nat this))),
calc
@ -189,7 +189,7 @@ private definition predimage (s : finset nat) : finset nat :=
private lemma mem_image_pred_of_succ_mem {n : nat} {s : finset nat} : succ n ∈ s → n ∈ image pred s :=
assume h,
assert pred (succ n) ∈ image pred s, from mem_image_of_mem _ h,
have pred (succ n) ∈ image pred s, from mem_image_of_mem _ h,
begin rewrite [pred_succ at this], assumption end
private lemma mem_predimage_of_succ_mem {n : nat} {s : finset nat} : succ n ∈ s → n ∈ predimage s :=

6
library/data/finset/partition.lean
View file

@ -32,8 +32,8 @@ lemma equiv_class_disjoint (f : partition) (a1 a2 : finset A) (Pa1 : a1 ∈ equi
(Pa2 : a2 ∈ equiv_classes f) :
a1 ≠ a2 → a1 ∩ a2 = ∅ :=
assume Pne,
assert Pe1 : _, from exists_of_mem_image Pa1, obtain g1 Pg1, from Pe1,
assert Pe2 : _, from exists_of_mem_image Pa2, obtain g2 Pg2, from Pe2,
have Pe1 : _, from exists_of_mem_image Pa1, obtain g1 Pg1, from Pe1,
have Pe2 : _, from exists_of_mem_image Pa2, obtain g2 Pg2, from Pe2,
begin
apply inter_eq_empty_of_disjoint,
apply disjoint.intro,
@ -99,7 +99,7 @@ lemma binary_inter_empty_Union_disjoint_sets {P : finset A → Prop} [decP : dec
assume Pds, inter_eq_empty (take a, assume Pa nPa,
obtain s Psin Pains, from iff.elim_left !mem_Union_iff Pa,
obtain t Ptin Paint, from iff.elim_left !mem_Union_iff nPa,
assert s ≠ t,
have s ≠ t,
from assume Peq, absurd (Peq ▸ of_mem_sep Psin) (of_mem_sep Ptin),
have e₁ : s ∩ t = empty, from Pds s t (mem_of_mem_sep Psin) (mem_of_mem_sep Ptin) `s ≠ t`,
have a ∈ s ∩ t, from mem_inter Pains Paint,

6
library/data/fintype/basic.lean
View file

@ -23,7 +23,7 @@ definition fintype_of_equiv {A B : Type} [h : fintype A] : A ≃ B → fintype B
(nodup_map (injective_of_left_inverse l) !fintype.unique)
(λ b,
have g b ∈ elements_of A, from fintype.complete (g b),
assert f (g b) ∈ map f (elements_of A), from mem_map f this,
have f (g b) ∈ map f (elements_of A), from mem_map f this,
by rewrite r at this; exact this)
end
@ -70,7 +70,7 @@ theorem ne_of_find_discr_eq_some {f g : A → B} {a : A} : ∀ {l}, find_discr f
have find_discr f g l = some a, by rewrite [find_discr_cons_of_eq l this at e]; exact e,
ne_of_find_discr_eq_some this)
(assume h : f x ≠ g x,
assert some x = some a, by rewrite [find_discr_cons_of_ne l h at e]; exact e,
have some x = some a, by rewrite [find_discr_cons_of_ne l h at e]; exact e,
by clear ne_of_find_discr_eq_some; injection this; subst a; exact h)
theorem all_eq_of_find_discr_eq_none {f g : A → B} : ∀ {l}, find_discr f g l = none → ∀ a, a ∈ l → f a = g a
@ -151,7 +151,7 @@ match h₁ with
obtain x px, from ex,
absurd px (all_of_check_pred_eq_tt h (c x)))
| ff := λ h : check_pred (λ a, ¬ p a) e = ff, inl (
assert ∃ x, ¬¬p x, from ex_of_check_pred_eq_ff h,
have ∃ x, ¬¬p x, from ex_of_check_pred_eq_ff h,
obtain x nnpx, from this, exists.intro x (not_not_elim nnpx))
end rfl
end

16
library/data/fintype/card.lean
View file

@ -25,25 +25,25 @@ lemma card_le_of_inj (A : Type) [finA : fintype A] [deceqA : decidable_eq A]
(B : Type) [finB : fintype B] [deceqB : decidable_eq B] :
(∃ f : A → B, injective f) → card A ≤ card B :=
assume Pex, obtain f Pinj, from Pex,
assert Pinj_on_univ : _, from iff.mp !set.injective_iff_inj_on_univ Pinj,
assert Pinj_ts : set.inj_on f (ts univ), from to_set_univ⁻¹ ▸ Pinj_on_univ,
assert Psub : (image f univ) ⊆ univ, from !subset_univ,
have Pinj_on_univ : _, from iff.mp !set.injective_iff_inj_on_univ Pinj,
have Pinj_ts : set.inj_on f (ts univ), from to_set_univ⁻¹ ▸ Pinj_on_univ,
have Psub : (image f univ) ⊆ univ, from !subset_univ,
finset.card_le_of_inj_on univ univ (exists.intro f (and.intro Pinj_ts Psub))
-- used to prove that inj ∧ eq card => surj
lemma univ_of_card_eq_univ {A : Type} [finA : fintype A] [deceqA : decidable_eq A] {s : finset A} :
finset.card s = card A → s = univ :=
assume Pcardeq, ext (take a,
assert D : decidable (a ∈ s), from decidable_mem a s, begin
have D : decidable (a ∈ s), from decidable_mem a s, begin
apply iff.intro,
intro ain, apply mem_univ,
intro ain, cases D with Pin Pnin,
exact Pin,
assert Pplus1 : finset.card (insert a s) = finset.card s + 1,
exact card_insert_of_not_mem Pnin,
have Pplus1 : finset.card (insert a s) = finset.card s + 1,
from card_insert_of_not_mem Pnin,
rewrite Pcardeq at Pplus1,
assert Ple : finset.card (insert a s) ≤ card A,
apply card_le_card_of_subset, apply subset_univ,
have Ple : finset.card (insert a s) ≤ card A,
begin apply card_le_card_of_subset, apply subset_univ end,
rewrite Pplus1 at Ple,
exact false.elim (not_succ_le_self Ple)
end)

58
library/data/fintype/function.lean
View file

@ -75,12 +75,12 @@ lemma nodup_mem_all_nodups [deceqA : decidable_eq A] {n : nat} ⦃l : list A⦄
lemma length_mem_all_lists : ∀ {n : nat} ⦃l : list A⦄,
l ∈ all_lists_of_len n → length l = n
| 0 [] := assume P, rfl
| 0 (a::l) := assume Pin, assert Peq : (a::l) = [], from mem_singleton Pin,
| 0 (a::l) := assume Pin, have Peq : (a::l) = [], from mem_singleton Pin,
by contradiction
| (succ n) [] := assume Pin, obtain pr Pprin Ppr, from exists_of_mem_map Pin,
by contradiction
| (succ n) (a::l) := assume Pin, obtain pr Pprin Ppr, from exists_of_mem_map Pin,
assert Pl : l ∈ all_lists_of_len n,
have Pl : l ∈ all_lists_of_len n,
from mem_of_mem_product_right ((pair_of_cons Ppr) ▸ Pprin),
by rewrite [length_cons, length_mem_all_lists Pl]
@ -138,8 +138,8 @@ lemma eq_of_kth_eq [deceqA : decidable_eq A]
rewrite *kth_succ_of_cons at keq,
exact keq
end,
assert ih : l₁ = l₂, from eq_of_kth_eq ih₁ ih₂,
assert k₁ : a₁ = a₂,
have ih : l₁ = l₂, from eq_of_kth_eq ih₁ ih₂,
have k₁ : a₁ = a₂,
begin
have lt₁ : 0 < length (a₁::l₁), from !zero_lt_succ,
have lt₂ : 0 < length (a₂::l₂), from !zero_lt_succ,
@ -163,7 +163,7 @@ lemma kth_find [deceqA : decidable_eq A] :
∀ {l : list A} {a} P, kth (find a l) l P = a
| [] := take a, assume P, absurd P !not_lt_zero
| (x::l) := take a, begin
assert Pd : decidable (a = x), {apply deceqA},
have Pd : decidable (a = x), begin apply deceqA end,
cases Pd with Pe Pne,
rewrite [find_cons_of_eq l Pe], intro P, rewrite [kth_zero_of_cons, Pe],
rewrite [find_cons_of_ne l Pne], intro P, rewrite [kth_succ_of_cons],
@ -179,8 +179,8 @@ lemma find_kth [deceqA : decidable_eq A] :
end
| (succ k) (a::l) := assume P, begin
rewrite [kth_succ_of_cons],
assert Pd : decidable ((kth k l (lt_of_succ_lt_succ P)) = a),
{apply deceqA},
have Pd : decidable ((kth k l (lt_of_succ_lt_succ P)) = a),
begin apply deceqA end,
cases Pd with Pe Pne,
rewrite [find_cons_of_eq l Pe], apply zero_lt_succ,
rewrite [find_cons_of_ne l Pne], apply succ_lt_succ, apply find_kth
@ -193,10 +193,10 @@ lemma find_kth_of_nodup [deceqA : decidable_eq A] :
by rewrite [kth_zero_of_cons, find_cons_of_eq l rfl]
| (succ k) (a::l) := assume Plt Pnodup, begin
rewrite [kth_succ_of_cons],
assert Pd : decidable ((kth k l (lt_of_succ_lt_succ Plt)) = a),
{apply deceqA},
have Pd : decidable ((kth k l (lt_of_succ_lt_succ Plt)) = a),
begin apply deceqA end,
cases Pd with Pe Pne,
assert Pin : a ∈ l, {rewrite -Pe, apply kth_mem},
have Pin : a ∈ l, begin rewrite -Pe, apply kth_mem end,
exact absurd Pin (not_mem_of_nodup_cons Pnodup),
rewrite [find_cons_of_ne l Pne], apply congr (eq.refl succ),
apply find_kth_of_nodup (lt_of_succ_lt_succ Plt) (nodup_of_nodup_cons Pnodup)
@ -265,10 +265,10 @@ include deceqB
lemma fun_eq_list_to_fun_map (f : A → B) : ∀ P, f = list_to_fun (map f (elems A)) P :=
assume Pleq, funext (take a,
assert Plt : _, from Pleq⁻¹ ▸ find_lt_length (complete a), begin
have Plt : _, from Pleq⁻¹ ▸ find_lt_length (complete a), begin
rewrite [list_to_fun_apply _ Pleq a (Pleq⁻¹ ▸ find_lt_length (complete a))],
assert Pmlt : find a (elems A) < length (map f (elems A)),
{rewrite length_map, exact Plt},
have Pmlt : find a (elems A) < length (map f (elems A)),
begin rewrite length_map, exact Plt end,
rewrite [@kth_of_map A B f (find a (elems A)) (elems A) Plt _, kth_find]
end)
@ -277,9 +277,9 @@ lemma list_eq_map_list_to_fun (l : list B) (leq : length l = card A)
begin
apply eq_of_kth_eq, rewrite length_map, apply leq,
intro k Plt Plt2,
assert Plt1 : k < length (elems A), {apply leq ▸ Plt},
assert Plt3 : find (kth k (elems A) Plt1) (elems A) < length l,
{rewrite leq, apply find_kth},
have Plt1 : k < length (elems A), begin apply leq ▸ Plt end,
have Plt3 : find (kth k (elems A) Plt1) (elems A) < length l,
begin rewrite leq, apply find_kth end,
rewrite [kth_of_map Plt1 Plt2, list_to_fun_apply l leq _ Plt3],
congruence,
rewrite [find_kth_of_nodup Plt1 (unique A)]
@ -303,9 +303,9 @@ lemma nodup_all_funs : nodup (@all_funs A B _ _ _) :=
dmap_nodup_of_dinj dinj_list_to_fun nodup_all_lists
lemma all_funs_complete (f : A → B) : f ∈ all_funs :=
assert Plin : map f (elems A) ∈ all_lists_of_len (card A),
have Plin : map f (elems A) ∈ all_lists_of_len (card A),
from mem_all_lists (by rewrite length_map),
assert Plfin : list_to_fun (map f (elems A)) (length_map_of_fintype f) ∈ all_funs,
have Plfin : list_to_fun (map f (elems A)) (length_map_of_fintype f) ∈ all_funs,
from mem_dmap _ Plin,
begin rewrite [fun_eq_list_to_fun_map f (length_map_of_fintype f)], apply Plfin end
@ -342,7 +342,7 @@ lemma found_of_surj {f : A → B} (surj : surjective f) :
∀ b, let elts := elems A, k := find b (map f elts) in k < length elts :=
λ b, let elts := elems A, img := map f elts, k := find b img in
have Pin : b ∈ img, from mem_map_of_surj surj b,
assert Pfound : k < length img, from find_lt_length (mem_map_of_surj surj b),
have Pfound : k < length img, from find_lt_length (mem_map_of_surj surj b),
length_map f elts ▸ Pfound
definition right_inv {f : A → B} (surj : surjective f) : B → A :=
@ -395,12 +395,12 @@ decidable.rec_on decidable_forall_finite
(assume P : surjective f, P)
(assume Pnsurj : ¬surjective f,
obtain b Pne, from exists_not_of_not_forall Pnsurj,
assert Pall : ∀ a, f a ≠ b, from forall_not_of_not_exists Pne,
assert Pbnin : b ∉ image f univ, from λ Pin,
have Pall : ∀ a, f a ≠ b, from forall_not_of_not_exists Pne,
have Pbnin : b ∉ image f univ, from λ Pin,
obtain a Pa, from exists_of_mem_image Pin, absurd (and.right Pa) (Pall a),
assert Puniv : finset.card (image f univ) = card A, from card_eq_card_image_of_inj Pinj,
assert Punivb : finset.card (image f univ) = card B, from eq.trans Puniv Peqcard,
assert P : image f univ = univ, from univ_of_card_eq_univ Punivb,
have Puniv : finset.card (image f univ) = card A, from card_eq_card_image_of_inj Pinj,
have Punivb : finset.card (image f univ) = card B, from eq.trans Puniv Peqcard,
have P : image f univ = univ, from univ_of_card_eq_univ Punivb,
absurd (P⁻¹▸ mem_univ b) Pbnin)
end inj
@ -422,9 +422,9 @@ lemma nodup_all_injs : nodup (all_injs A) :=
lemma all_injs_complete {f : A → A} : injective f → f ∈ (all_injs A) :=
assume Pinj,
assert Plin : map f (elems A) ∈ all_nodups_of_len (card A),
have Plin : map f (elems A) ∈ all_nodups_of_len (card A),
from begin apply mem_all_nodups, apply length_map, apply nodup_of_inj Pinj end,
assert Plfin : list_to_fun (map f (elems A)) (length_map_of_fintype f) ∈ !all_injs,
have Plfin : list_to_fun (map f (elems A)) (length_map_of_fintype f) ∈ !all_injs,
from mem_dmap _ Plin,
begin rewrite [fun_eq_list_to_fun_map f (length_map_of_fintype f)], apply Plfin end
@ -439,13 +439,13 @@ lemma univ_of_leq_univ_of_nodup {l : list A} (n : nodup l) (leq : length l = car
lemma inj_of_mem_all_injs {f : A → A} : f ∈ (all_injs A) → injective f :=
assume Pfin, obtain l Pex, from exists_of_mem_dmap Pfin,
obtain leq Pin Peq, from Pex,
assert Pmap : map f (elems A) = l, from Peq⁻¹ ▸ list_to_fun_to_list l leq,
have Pmap : map f (elems A) = l, from Peq⁻¹ ▸ list_to_fun_to_list l leq,
begin apply inj_of_nodup, rewrite Pmap, apply nodup_mem_all_nodups Pin end
lemma perm_of_inj {f : A → A} : injective f → perm (map f (elems A)) (elems A) :=
assume Pinj,
assert P1 : univ = to_finset_of_nodup (elems A) (unique A), from rfl,
assert P2 : to_finset_of_nodup (map f (elems A)) (nodup_of_inj Pinj) = univ,
have P1 : univ = to_finset_of_nodup (elems A) (unique A), from rfl,
have P2 : to_finset_of_nodup (map f (elems A)) (nodup_of_inj Pinj) = univ,
from univ_of_leq_univ_of_nodup _ !length_map,
quot.exact (P1 ▸ P2)

18
library/data/hf.lean
View file

@ -113,8 +113,8 @@ begin unfold [mem, insert], rewrite to_finset_of_finset, intros, apply mem_of_me
protected theorem ext {s₁ s₂ : hf} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ :=
assume h,
assert to_finset s₁ = to_finset s₂, from finset.ext h,
assert of_finset (to_finset s₁) = of_finset (to_finset s₂), by rewrite this,
have to_finset s₁ = to_finset s₂, from finset.ext h,
have of_finset (to_finset s₁) = of_finset (to_finset s₂), by rewrite this,
by rewrite [*of_finset_to_finset at this]; exact this
theorem insert_eq_of_mem {a : hf} {s : hf} : a ∈ s → insert a s = s :=
@ -122,7 +122,7 @@ begin unfold mem, intro h, unfold [mem, insert], rewrite (finset.insert_eq_of_me
protected theorem induction [recursor 4] {P : hf → Prop}
(h₁ : P empty) (h₂ : ∀ (a s : hf), a ∉ s → P s → P (insert a s)) (s : hf) : P s :=
assert P (of_finset (to_finset s)), from
have P (of_finset (to_finset s)), from
@finset.induction _ _ _ h₁
(λ a s nain ih,
begin
@ -388,16 +388,16 @@ begin
revert s₂, induction s₁ with a s₁ nain ih,
take s₂, suppose ∅ ⊆ s₂, !zero_le,
take s₂, suppose insert a s₁ ⊆ s₂,
assert a ∈ s₂, from mem_of_subset_of_mem this !mem_insert,
have a ∉ erase a s₂, from !not_mem_erase,
have s₁ ⊆ erase a s₂, from subset_of_forall
have a ∈ s₂, from mem_of_subset_of_mem this !mem_insert,
have a ∉ erase a s₂, from !not_mem_erase,
have s₁ ⊆ erase a s₂, from subset_of_forall
(take x xin, by_cases
(suppose x = a, by subst x; contradiction)
(suppose x ≠ a,
have x ∈ s₂, from mem_of_subset_of_mem `insert a s₁ ⊆ s₂` (mem_insert_of_mem _ `x ∈ s₁`),
mem_erase_of_ne_of_mem `x ≠ a` `x ∈ s₂`)),
have s₁ ≤ erase a s₂, from ih _ this,
assert insert a s₁ ≤ insert a (erase a s₂), from
have s₁ ≤ erase a s₂, from ih _ this,
have insert a s₁ ≤ insert a (erase a s₂), from
insert_le_insert_of_le (or.inr `a ∉ erase a s₂`) this,
by rewrite [insert_erase `a ∈ s₂` at this]; exact this
end
@ -465,7 +465,7 @@ begin
obtain w h₁ h₂, from this,
begin subst x, rewrite to_finset_of_finset, exact iff.mp !finset.mem_powerset_iff_subset h₁ end,
suppose finset.subset (to_finset x) (to_finset s),
assert finset.mem (to_finset x) (finset.powerset (to_finset s)), from iff.mpr !finset.mem_powerset_iff_subset this,
have finset.mem (to_finset x) (finset.powerset (to_finset s)), from iff.mpr !finset.mem_powerset_iff_subset this,
exists.intro (to_finset x) (and.intro this (of_finset_to_finset x))
end

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

@ -544,7 +544,7 @@ has_dvd.mk has_dvd.dvd
/- additional properties -/
theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : of_nat (m - n) = of_nat m - of_nat n :=
assert m - n + n = m, from nat.sub_add_cancel H,
have m - n + n = m, from nat.sub_add_cancel H,
begin
symmetry,
apply sub_eq_of_eq_add,

12
library/data/int/div.lean
View file

@ -105,7 +105,7 @@ protected theorem div_zero (a : ℤ) : a / 0 = 0 :=
by rewrite [div_def, sign_zero, zero_mul]
protected theorem div_one (a : ℤ) : a / 1 = a :=
assert (1 : int) > 0, from dec_trivial,
have (1 : int) > 0, from dec_trivial,
int.cases_on a
(take m : nat, by rewrite [-of_nat_one, -of_nat_div, nat.div_one])
(take m : nat, by rewrite [!neg_succ_of_nat_div this, -of_nat_one, -of_nat_div, nat.div_one])
@ -133,7 +133,7 @@ int.cases_on a
theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a / b = 0 :=
lt.by_cases
(suppose b < 0,
assert a < -b, from abs_of_neg this ▸ H2,
have a < -b, from abs_of_neg this ▸ H2,
calc
a / b = - (a / -b) : by rewrite [int.div_neg, neg_neg]
... = 0 : by rewrite [div_eq_zero_of_lt H1 this, neg_zero])
@ -155,8 +155,8 @@ private theorem add_mul_div_self_aux2 {a : ℤ} {k : ℕ} (n : ℕ) (H1 : a < 0)
obtain m (Hm : a = -[1+m]), from exists_eq_neg_succ_of_nat H1,
or.elim (nat.lt_or_ge m (n * k))
(assume m_lt_nk : m < n * k,
assert H3 : m + 1 ≤ n * k, from nat.succ_le_of_lt m_lt_nk,
assert H4 : m / k + 1 ≤ n,
have H3 : m + 1 ≤ n * k, from nat.succ_le_of_lt m_lt_nk,
have H4 : m / k + 1 ≤ n,
from nat.succ_le_of_lt (nat.div_lt_of_lt_mul m_lt_nk),
have (-[1+m] + n * k) / k = -[1+m] / k + n, from calc
(-[1+m] + n * k) / k
@ -371,7 +371,7 @@ by rewrite [add.comm, add_mod_eq_add_mod_right _ H, add.comm]
theorem mod_eq_mod_of_add_mod_eq_add_mod_right {m n k i : ℤ}
(H : (m + i) % n = (k + i) % n) :
m % n = k % n :=
assert H1 : (m + i + (-i)) % n = (k + i + (-i)) % n, from add_mod_eq_add_mod_right _ H,
have H1 : (m + i + (-i)) % n = (k + i + (-i)) % n, from add_mod_eq_add_mod_right _ H,
by rewrite [*add_neg_cancel_right at H1]; apply H1
theorem mod_eq_mod_of_add_mod_eq_add_mod_left {m n k i : ℤ} :
@ -666,7 +666,7 @@ lt_of_mul_lt_mul_right
(le_of_lt H)
protected theorem lt_mul_of_div_lt {a b c : ℤ} (H1 : c > 0) (H2 : a / c < b) : a < b * c :=
assert H3 : (a / c + 1) * c ≤ b * c,
have H3 : (a / c + 1) * c ≤ b * c,
from !mul_le_mul_of_nonneg_right (add_one_le_of_lt H2) (le_of_lt H1),
have H4 : a / c * c + c ≤ b * c, by rewrite [right_distrib at H3, one_mul at H3]; apply H3,
calc

12
library/data/int/gcd.lean
View file

@ -46,7 +46,7 @@ open nat
theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a % abs b) :=
have nat_abs b ≠ 0, from assume H', H (eq_zero_of_nat_abs_eq_zero H'),
have nat_abs b > 0, from pos_of_ne_zero this,
assert nat.gcd (nat_abs a) (nat_abs b) = (nat.gcd (nat_abs b) (nat_abs a % nat_abs b)),
have nat.gcd (nat_abs a) (nat_abs b) = (nat.gcd (nat_abs b) (nat_abs a % nat_abs b)),
from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this,
calc
gcd a b = nat.gcd (nat_abs b) (nat_abs a % nat_abs b) : by rewrite [↑gcd, this]
@ -156,8 +156,8 @@ or.elim (le_or_gt 0 a₁)
div_gcd_eq_div_gcd_of_nonneg H (ne_of_gt H1) (ne_of_gt H2) H3 H5)
(assume H3 : a₁ < 0,
have H4 : a₂ * b₁ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
assert H5 : a₂ < 0, from neg_of_mul_neg_right H4 (le_of_lt H1),
assert H6 : abs a₁ / (gcd (abs a₁) (abs b₁)) = abs a₂ / (gcd (abs a₂) (abs b₂)),
have H5 : a₂ < 0, from neg_of_mul_neg_right H4 (le_of_lt H1),
have H6 : abs a₁ / (gcd (abs a₁) (abs b₁)) = abs a₂ / (gcd (abs a₂) (abs b₂)),
begin
apply div_gcd_eq_div_gcd_of_nonneg,
rewrite [abs_of_pos H1, abs_of_pos H2, abs_of_neg H3, abs_of_neg H5],
@ -249,12 +249,12 @@ theorem coprime_swap {a b : ℤ} (H : coprime b a) : coprime a b :=
!gcd.comm ▸ H
theorem dvd_of_coprime_of_dvd_mul_right {a b c : ℤ} (H1 : coprime c b) (H2 : c ∣ a * b) : c ∣ a :=
assert H3 : gcd (a * c) (a * b) = abs a, from
have H3 : gcd (a * c) (a * b) = abs a, from
calc
gcd (a * c) (a * b) = abs a * gcd c b : gcd_mul_left
... = abs a * 1 : H1
... = abs a : mul_one,
assert H4 : (c ∣ gcd (a * c) (a * b)), from dvd_gcd !dvd_mul_left H2,
have H4 : (c ∣ gcd (a * c) (a * b)), from dvd_gcd !dvd_mul_left H2,
by rewrite [-dvd_abs_iff, -H3]; apply H4
theorem dvd_of_coprime_of_dvd_mul_left {a b c : ℤ} (H1 : coprime c a) (H2 : c ∣ a * b) : c ∣ b :=
@ -291,7 +291,7 @@ calc
theorem not_coprime_of_dvd_of_dvd {m n d : ℤ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) :
¬ coprime m n :=
assume co : coprime m n,
assert d ∣ gcd m n, from dvd_gcd Hm Hn,
have d ∣ gcd m n, from dvd_gcd Hm Hn,
have d ∣ 1, by rewrite [↑coprime at co, co at this]; apply this,
have d ≤ 1, from le_of_dvd dec_trivial this,
show false, from not_lt_of_ge `d ≤ 1` `d > 1`

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

@ -122,7 +122,7 @@ have a + of_nat (n + m) = a + 0, from
... = a + 0 : by rewrite add_zero,
have of_nat (n + m) = of_nat 0, from add.left_cancel this,
have n + m = 0, from of_nat.inj this,
assert n = 0, from nat.eq_zero_of_add_eq_zero_right this,
have n = 0, from nat.eq_zero_of_add_eq_zero_right this,
show a = b, from
calc
a = a + 0 : add_zero
@ -341,7 +341,7 @@ or.elim (le_or_gt a 1)
(suppose a ≤ 1,
show a = 1, from le.antisymm this (add_one_le_of_lt `a > 0`))
(suppose a > 1,
assert a * b ≥ 2 * 1,
have a * b ≥ 2 * 1,
from mul_le_mul (add_one_le_of_lt `a > 1`) (add_one_le_of_lt `b > 0`) trivial H,
have false, by rewrite [H' at this]; exact this,
false.elim this)

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

@ -559,7 +559,7 @@ list.induction_on l
(λ h : a ∈ nil, absurd h (not_mem_nil a))
(λ x xs r ainxxs, or.elim (eq_or_mem_of_mem_cons ainxxs)
(λ aeqx : a = x,
assert aux : ∃ l, x::xs≈x|l, from
have aux : ∃ l, x::xs≈x|l, from
exists.intro xs (qhead x xs),
by rewrite aeqx; exact aux)
(λ ainxs : a ∈ xs,

24
library/data/list/comb.lean
View file

@ -424,14 +424,14 @@ theorem product_nil : ∀ (l : list A), product l (@nil B) = []
theorem eq_of_mem_map_pair₁ {a₁ a : A} {b₁ : B} {l : list B} : (a₁, b₁) ∈ map (λ b, (a, b)) l → a₁ = a :=
assume ain,
assert pr1 (a₁, b₁) ∈ map pr1 (map (λ b, (a, b)) l), from mem_map pr1 ain,
assert a₁ ∈ map (λb, a) l, by revert this; rewrite [map_map, ↑pr1]; intro this; assumption,
have pr1 (a₁, b₁) ∈ map pr1 (map (λ b, (a, b)) l), from mem_map pr1 ain,
have a₁ ∈ map (λb, a) l, by revert this; rewrite [map_map, ↑pr1]; intro this; assumption,
eq_of_map_const this
theorem mem_of_mem_map_pair₁ {a₁ a : A} {b₁ : B} {l : list B} : (a₁, b₁) ∈ map (λ b, (a, b)) l → b₁ ∈ l :=
assume ain,
assert pr2 (a₁, b₁) ∈ map pr2 (map (λ b, (a, b)) l), from mem_map pr2 ain,
assert b₁ ∈ map (λx, x) l, by rewrite [map_map at this, ↑pr2 at this]; exact this,
have pr2 (a₁, b₁) ∈ map pr2 (map (λ b, (a, b)) l), from mem_map pr2 ain,
have b₁ ∈ map (λx, x) l, by rewrite [map_map at this, ↑pr2 at this]; exact this,
by rewrite [map_id at this]; exact this
theorem mem_product {a : A} {b : B} : ∀ {l₁ l₂}, a ∈ l₁ → b ∈ l₂ → (a, b) ∈ product l₁ l₂
@ -439,10 +439,10 @@ theorem mem_product {a : A} {b : B} : ∀ {l₁ l₂}, a ∈ l₁ → b ∈ l₂
| (x::l₁) l₂ h₁ h₂ :=
or.elim (eq_or_mem_of_mem_cons h₁)
(assume aeqx : a = x,
assert (a, b) ∈ map (λ b, (a, b)) l₂, from mem_map _ h₂,
have (a, b) ∈ map (λ b, (a, b)) l₂, from mem_map _ h₂,
begin rewrite [-aeqx, product_cons], exact mem_append_left _ this end)
(assume ainl₁ : a ∈ l₁,
assert (a, b) ∈ product l₁ l₂, from mem_product ainl₁ h₂,
have (a, b) ∈ product l₁ l₂, from mem_product ainl₁ h₂,
begin rewrite [product_cons], exact mem_append_right _ this end)
theorem mem_of_mem_product_left {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ product l₁ l₂ → a ∈ l₁
@ -450,7 +450,7 @@ theorem mem_of_mem_product_left {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ pr
| (x::l₁) l₂ h :=
or.elim (mem_or_mem_of_mem_append h)
(suppose (a, b) ∈ map (λ b, (x, b)) l₂,
assert a = x, from eq_of_mem_map_pair₁ this,
have a = x, from eq_of_mem_map_pair₁ this,
by rewrite this; exact !mem_cons)
(suppose (a, b) ∈ product l₁ l₂,
have a ∈ l₁, from mem_of_mem_product_left this,
@ -468,7 +468,7 @@ theorem mem_of_mem_product_right {a : A} {b : B} : ∀ {l₁ l₂}, (a, b) ∈ p
theorem length_product : ∀ (l₁ : list A) (l₂ : list B), length (product l₁ l₂) = length l₁ * length l₂
| [] l₂ := by rewrite [length_nil, zero_mul]
| (x::l₁) l₂ :=
assert length (product l₁ l₂) = length l₁ * length l₂, from length_product l₁ l₂,
have length (product l₁ l₂) = length l₁ * length l₂, from length_product l₁ l₂,
by rewrite [product_cons, length_append, length_cons,
length_map, this, right_distrib, one_mul, add.comm]
end product
@ -521,14 +521,14 @@ lemma exists_of_mem_dmap : ∀ {l : list A} {b : B}, b ∈ dmap p f l → ∃ a
rewrite [dmap_cons_of_pos Pa, mem_cons_iff],
intro Pb, cases Pb with Peq Pin,
exact exists.intro a (exists.intro Pa (and.intro !mem_cons Peq)),
assert Pex : ∃ (a : A) (P : p a), a ∈ l ∧ b = f a P, exact exists_of_mem_dmap Pin,
have Pex : ∃ (a : A) (P : p a), a ∈ l ∧ b = f a P, from exists_of_mem_dmap Pin,
cases Pex with a' Pex', cases Pex' with Pa' P',
exact exists.intro a' (exists.intro Pa' (and.intro (mem_cons_of_mem a (and.left P')) (and.right P')))
end)
(assume nPa, begin
rewrite [dmap_cons_of_neg nPa],
intro Pin,
assert Pex : ∃ (a : A) (P : p a), a ∈ l ∧ b = f a P, exact exists_of_mem_dmap Pin,
have Pex : ∃ (a : A) (P : p a), a ∈ l ∧ b = f a P, from exists_of_mem_dmap Pin,
cases Pex with a' Pex', cases Pex' with Pa' P',
exact exists.intro a' (exists.intro Pa' (and.intro (mem_cons_of_mem a (and.left P')) (and.right P')))
end)
@ -537,8 +537,8 @@ lemma map_dmap_of_inv_of_pos {g : B → A} (Pinv : ∀ a (Pa : p a), g (f a Pa)
∀ {l : list A}, (∀ ⦃a⦄, a ∈ l → p a) → map g (dmap p f l) = l
| [] := assume Pl, by rewrite [dmap_nil, map_nil]
| (a::l) := assume Pal,
assert Pa : p a, from Pal a !mem_cons,
assert Pl : ∀ a, a ∈ l → p a,
have Pa : p a, from Pal a !mem_cons,
have Pl : ∀ a, a ∈ l → p a,
from take x Pxin, Pal x (mem_cons_of_mem a Pxin),
by rewrite [dmap_cons_of_pos Pa, map_cons, Pinv, map_dmap_of_inv_of_pos Pl]

88
library/data/list/perm.lean
View file

@ -239,22 +239,22 @@ include Ha
definition decidable_perm_aux : ∀ (n : nat) (l₁ l₂ : list A), length l₁ = n → length l₂ = n → decidable (l₁ ~ l₂)
| 0 l₁ l₂ H₁ H₂ :=
assert l₁n : l₁ = [], from eq_nil_of_length_eq_zero H₁,
assert l₂n : l₂ = [], from eq_nil_of_length_eq_zero H₂,
have l₁n : l₁ = [], from eq_nil_of_length_eq_zero H₁,
have l₂n : l₂ = [], from eq_nil_of_length_eq_zero H₂,
by rewrite [l₁n, l₂n]; exact (inl perm.nil)
| (n+1) (x::t₁) l₂ H₁ H₂ :=
by_cases
(assume xinl₂ : x ∈ l₂,
let t₂ : list A := erase x l₂ in
have len_t₁ : length t₁ = n, begin injection H₁ with e, exact e end,
assert length t₂ = pred (length l₂), from length_erase_of_mem xinl₂,
assert length t₂ = n, by rewrite [this, H₂],
have length t₂ = pred (length l₂), from length_erase_of_mem xinl₂,
have length t₂ = n, by rewrite [this, H₂],
match decidable_perm_aux n t₁ t₂ len_t₁ this with
| inl p := inl (calc
x::t₁ ~ x::(erase x l₂) : skip x p
... ~ l₂ : perm_erase xinl₂)
| inr np := inr (λ p : x::t₁ ~ l₂,
assert erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p,
have erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p,
have t₁ ~ erase x l₂, by rewrite [erase_cons_head at this]; exact this,
absurd this np)
end)
@ -325,7 +325,7 @@ perm_induction_on p'
obtain (s₂₁ s₂₂ : list A) (C₂₁ : s₂ = s₂₁ ++ s₂₂) (C₂₂ : x::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂,
discr C₁₂
(λ (s₁₁_eq : s₁₁ = []) (x_eq_a : x = a) (t₁_eq : t₁ = s₁₂),
assert s₁_p : s₁ ~ t₂, from calc
have s₁_p : s₁ ~ t₂, from calc
s₁ = s₁₁ ++ s₁₂ : C₁₁
... = t₁ : by rewrite [-t₁_eq, s₁₁_eq, append_nil_left]
... ~ t₂ : p,
@ -345,8 +345,8 @@ perm_induction_on p'
... = s₂ : by rewrite C₂₁
qed))
(λ (ts₁₁ : list A) (s₁₁_eq : s₁₁ = x::ts₁₁) (t₁_eq : t₁ = ts₁₁++(a::s₁₂)),
assert t₁_qeq : t₁ ≈ a|(ts₁₁++s₁₂), by rewrite t₁_eq; exact !qeq_app,
assert s₁_eq : s₁ = x::(ts₁₁++s₁₂), from calc
have t₁_qeq : t₁ ≈ a|(ts₁₁++s₁₂), by rewrite t₁_eq; exact !qeq_app,
have s₁_eq : s₁ = x::(ts₁₁++s₁₂), from calc
s₁ = s₁₁ ++ s₁₂ : C₁₁
... = x::(ts₁₁++ s₁₂) : by rewrite s₁₁_eq,
discr C₂₂
@ -359,7 +359,7 @@ perm_induction_on p'
... = s₂ : by rewrite [t₂_eq, C₂₁, s₂₁_eq, append_nil_left]
qed)
(λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
assert t₂_qeq : t₂ ≈ a|(ts₂₁++s₂₂), by rewrite t₂_eq; exact !qeq_app,
have t₂_qeq : t₂ ≈ a|(ts₂₁++s₂₂), by rewrite t₂_eq; exact !qeq_app,
proof calc
s₁ = x::(ts₁₁++s₁₂) : s₁_eq
... ~ x::(ts₂₁++s₂₂) : skip x (r t₁_qeq t₂_qeq)
@ -370,7 +370,7 @@ perm_induction_on p'
obtain (s₂₁ s₂₂ : list A) (C₂₁ : s₂ = s₂₁ ++ s₂₂) (C₂₂ : x::y::t₂ = s₂₁++(a::s₂₂)), from qeq_split e₂,
discr₂ C₁₂
(λ (s₁₁_eq : s₁₁ = []) (s₁₂_eq : s₁₂ = x::t₁) (y_eq_a : y = a),
assert s₁_p : s₁ ~ x::t₂, from calc
have s₁_p : s₁ ~ x::t₂, from calc
s₁ = s₁₁ ++ s₁₂ : C₁₁
... = x::t₁ : by rewrite [s₁₂_eq, s₁₁_eq, append_nil_left]
... ~ x::t₂ : skip x p,
@ -396,7 +396,7 @@ perm_induction_on p'
... = s₂ : by rewrite C₂₁
qed))
(λ (s₁₁_eq : s₁₁ = [y]) (x_eq_a : x = a) (t₁_eq : t₁ = s₁₂),
assert s₁_p : s₁ ~ y::t₂, from calc
have s₁_p : s₁ ~ y::t₂, from calc
s₁ = y::t₁ : by rewrite [C₁₁, s₁₁_eq, t₁_eq]
... ~ y::t₂ : skip y p,
discr₂ C₂₂
@ -422,7 +422,7 @@ perm_induction_on p'
... = s₂ : by rewrite C₂₁
qed))
(λ (ts₁₁ : list A) (s₁₁_eq : s₁₁ = y::x::ts₁₁) (t₁_eq : t₁ = ts₁₁++(a::s₁₂)),
assert s₁_eq : s₁ = y::x::(ts₁₁++s₁₂), by rewrite [C₁₁, s₁₁_eq],
have s₁_eq : s₁ = y::x::(ts₁₁++s₁₂), by rewrite [C₁₁, s₁₁_eq],
discr₂ C₂₂
(λ (s₂₁_eq : s₂₁ = []) (s₂₂_eq : s₂₂ = y::t₂) (x_eq_a : x = a),
proof calc
@ -445,9 +445,9 @@ perm_induction_on p'
... = s₂ : by rewrite C₂₁
qed)
(λ (ts₂₁ : list A) (s₂₁_eq : s₂₁ = x::y::ts₂₁) (t₂_eq : t₂ = ts₂₁++(a::s₂₂)),
assert t₁_qeq : t₁ ≈ a|(ts₁₁++s₁₂), by rewrite t₁_eq; exact !qeq_app,
assert t₂_qeq : t₂ ≈ a|(ts₂₁++s₂₂), by rewrite t₂_eq; exact !qeq_app,
assert p_aux : ts₁₁++s₁₂ ~ ts₂₁++s₂₂, from r t₁_qeq t₂_qeq,
have t₁_qeq : t₁ ≈ a|(ts₁₁++s₁₂), by rewrite t₁_eq; exact !qeq_app,
have t₂_qeq : t₂ ≈ a|(ts₂₁++s₂₂), by rewrite t₂_eq; exact !qeq_app,
have p_aux : ts₁₁++s₁₂ ~ ts₂₁++s₂₂, from r t₁_qeq t₂_qeq,
proof calc
s₁ = y::x::(ts₁₁++s₁₂) : by rewrite s₁_eq
... ~ y::x::(ts₂₁++s₂₂) : skip y (skip x p_aux)
@ -521,39 +521,39 @@ assume p, perm_induction_on p
nil
(λ x t₁ t₂ p r, by_cases
(λ xint₁ : x ∈ t₁,
assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)),
have xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)),
by rewrite [erase_dup_cons_of_mem xint₁, erase_dup_cons_of_mem xint₂]; exact r)
(λ nxint₁ : x ∉ t₁,
assert nxint₂ : x ∉ t₂, from
have nxint₂ : x ∉ t₂, from
assume xint₂ : x ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (perm.symm r) (mem_erase_dup xint₂))) nxint₁,
by rewrite [erase_dup_cons_of_not_mem nxint₂, erase_dup_cons_of_not_mem nxint₁]; exact (skip x r)))
(λ y x t₁ t₂ p r, by_cases
(λ xinyt₁ : x ∈ y::t₁, by_cases
(λ yint₁ : y ∈ t₁,
assert yint₂ : y ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁)),
assert yinxt₂ : y ∈ x::t₂, from or.inr (yint₂),
have yint₂ : y ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁)),
have yinxt₂ : y ∈ x::t₂, from or.inr (yint₂),
or.elim (eq_or_mem_of_mem_cons xinyt₁)
(λ xeqy : x = y,
assert xint₂ : x ∈ t₂, by rewrite [-xeqy at yint₂]; exact yint₂,
have xint₂ : x ∈ t₂, by rewrite [-xeqy at yint₂]; exact yint₂,
begin
rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂,
erase_dup_cons_of_mem yint₁, erase_dup_cons_of_mem xint₂],
exact r
end)
(λ xint₁ : x ∈ t₁,
assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)),
have xint₂ : x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup xint₁)),
begin
rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂,
erase_dup_cons_of_mem yint₁, erase_dup_cons_of_mem xint₂],
exact r
end))
(λ nyint₁ : y ∉ t₁,
assert nyint₂ : y ∉ t₂, from
have nyint₂ : y ∉ t₂, from
assume yint₂ : y ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (perm.symm r) (mem_erase_dup yint₂))) nyint₁,
by_cases
(λ xeqy : x = y,
assert nxint₂ : x ∉ t₂, by rewrite [-xeqy at nyint₂]; exact nyint₂,
assert yinxt₂ : y ∈ x::t₂, by rewrite [xeqy]; exact !mem_cons,
have nxint₂ : x ∉ t₂, by rewrite [-xeqy at nyint₂]; exact nyint₂,
have yinxt₂ : y ∈ x::t₂, by rewrite [xeqy]; exact !mem_cons,
begin
rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂,
erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂, xeqy],
@ -561,8 +561,8 @@ assume p, perm_induction_on p
end)
(λ xney : x ≠ y,
have x ∈ t₁, from or_resolve_right xinyt₁ xney,
assert x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup this)),
assert y ∉ x::t₂, from
have x ∈ t₂, from mem_of_mem_erase_dup (mem_perm r (mem_erase_dup this)),
have y ∉ x::t₂, from
suppose y ∈ x::t₂, or.elim (eq_or_mem_of_mem_cons this)
(λ h, absurd h (ne.symm xney))
(λ h, absurd h nyint₂),
@ -572,20 +572,20 @@ assume p, perm_induction_on p
exact skip y r
end)))
(λ nxinyt₁ : x ∉ y::t₁,
have xney : x ≠ y, from ne_of_not_mem_cons nxinyt₁,
have nxint₁ : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁,
assert nxint₂ : x ∉ t₂, from
have xney : x ≠ y, from ne_of_not_mem_cons nxinyt₁,
have nxint₁ : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁,
have nxint₂ : x ∉ t₂, from
assume xint₂ : x ∈ t₂, absurd (mem_of_mem_erase_dup (mem_perm (perm.symm r) (mem_erase_dup xint₂))) nxint₁,
by_cases
(λ yint₁ : y ∈ t₁,
assert yinxt₂ : y ∈ x::t₂, from or.inr (mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁))),
have yinxt₂ : y ∈ x::t₂, from or.inr (mem_of_mem_erase_dup (mem_perm r (mem_erase_dup yint₁))),
begin
rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_mem yinxt₂,
erase_dup_cons_of_mem yint₁, erase_dup_cons_of_not_mem nxint₂],
exact skip x r
end)
(λ nyint₁ : y ∉ t₁,
assert nyinxt₂ : y ∉ x::t₂, from
have nyinxt₂ : y ∉ x::t₂, from
assume yinxt₂ : y ∈ x::t₂, or.elim (eq_or_mem_of_mem_cons yinxt₂)
(λ h, absurd h (ne.symm xney))
(λ h, absurd (mem_of_mem_erase_dup (mem_perm (perm.symm r) (mem_erase_dup h))) nyint₁),
@ -624,10 +624,10 @@ list.induction_on l
(λ p, by rewrite [*union_nil]; exact p)
(λ x xs r p, by_cases
(λ xint₁ : x ∈ t₁,
assert xint₂ : x ∈ t₂, from mem_perm p xint₁,
have xint₂ : x ∈ t₂, from mem_perm p xint₁,
by rewrite [union_cons_of_mem _ xint₁, union_cons_of_mem _ xint₂]; exact (r p))
(λ nxint₁ : x ∉ t₁,
assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
have nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
by rewrite [union_cons_of_not_mem _ nxint₁, union_cons_of_not_mem _ nxint₂]; exact (skip _ (r p))))
theorem perm_union [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (union l₁ t₁) ~ (union l₂ t₂) :=
@ -641,10 +641,10 @@ include H
theorem perm_insert [congr] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → (insert a l₁) ~ (insert a l₂) :=
assume p, by_cases
(λ ainl₁ : a ∈ l₁,
assert ainl₂ : a ∈ l₂, from mem_perm p ainl₁,
have ainl₂ : a ∈ l₂, from mem_perm p ainl₁,
by rewrite [insert_eq_of_mem ainl₁, insert_eq_of_mem ainl₂]; exact p)
(λ nainl₁ : a ∉ l₁,
assert nainl₂ : a ∉ l₂, from not_mem_perm p nainl₁,
have nainl₂ : a ∉ l₂, from not_mem_perm p nainl₁,
by rewrite [insert_eq_of_not_mem nainl₁, insert_eq_of_not_mem nainl₂]; exact (skip _ p))
end perm_insert
@ -678,10 +678,10 @@ list.induction_on l
(λ p, by rewrite [*inter_nil])
(λ x xs r p, by_cases
(λ xint₁ : x ∈ t₁,
assert xint₂ : x ∈ t₂, from mem_perm p xint₁,
have xint₂ : x ∈ t₂, from mem_perm p xint₁,
by rewrite [inter_cons_of_mem _ xint₁, inter_cons_of_mem _ xint₂]; exact (skip _ (r p)))
(λ nxint₁ : x ∉ t₁,
assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
have nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
by rewrite [inter_cons_of_not_mem _ nxint₁, inter_cons_of_not_mem _ nxint₂]; exact (r p)))
theorem perm_inter [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (inter l₁ t₁) ~ (inter l₂ t₂) :=
@ -704,13 +704,13 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
have eqv : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from
take a, iff.intro
(suppose a ∈ t₁,
assert a ∈ a₂::t₂, from iff.mp (e a) (mem_cons_of_mem _ this),
have a ∈ s₁++(a₁::s₂), by rewrite [t₂_eq at this]; exact this,
have a ∈ a₂::t₂, from iff.mp (e a) (mem_cons_of_mem _ this),
have a ∈ s₁++(a₁::s₂), by rewrite [t₂_eq at this]; exact this,
or.elim (mem_or_mem_of_mem_append this)
(suppose a ∈ s₁, mem_append_left s₂ this)
(suppose a ∈ a₁::s₂, or.elim (eq_or_mem_of_mem_cons this)
(suppose a = a₁,
assert a₁ ∉ t₁, from not_mem_of_nodup_cons d₁,
have a₁ ∉ t₁, from not_mem_of_nodup_cons d₁,
by subst a; contradiction)
(suppose a ∈ s₂, mem_append_right s₁ this)))
(suppose a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append this)
@ -719,8 +719,8 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
have a ∈ a₁::t₁, from iff.mpr (e a) this,
or.elim (eq_or_mem_of_mem_cons this)
(suppose a = a₁,
have a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
assert a₁ ∉ s₁, from not_mem_of_not_mem_append_left this,
have a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
have a₁ ∉ s₁, from not_mem_of_not_mem_append_left this,
by subst a; contradiction)
(suppose a ∈ t₁, this))
(suppose a ∈ s₂,
@ -728,8 +728,8 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
have a ∈ a₁::t₁, from iff.mpr (e a) this,
or.elim (eq_or_mem_of_mem_cons this)
(suppose a = a₁,
have a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
assert a₁ ∉ s₂, from not_mem_of_not_mem_append_right this,
have a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
have a₁ ∉ s₂, from not_mem_of_not_mem_append_right this,
by subst a; contradiction)
(suppose a ∈ t₁, this))),
have ds₁s₂ : nodup (s₁++s₂), from nodup_of_nodup_cons dt₂',

96
library/data/list/set.lean
View file

@ -41,14 +41,14 @@ lemma length_erase_of_mem {a : A} : ∀ {l}, a ∈ l → length (erase a l) = pr
by_cases
(suppose a = x, by rewrite [this, erase_cons_head])
(suppose a ≠ x,
assert ainyxs : a ∈ y::xs, from or_resolve_right h this,
have ainyxs : a ∈ y::xs, from or_resolve_right h this,
by rewrite [erase_cons_tail _ this, *length_cons, length_erase_of_mem ainyxs])
lemma length_erase_of_not_mem {a : A} : ∀ {l}, a ∉ l → length (erase a l) = length l
| [] h := rfl
| (x::xs) h :=
assert anex : a ≠ x, from λ aeqx : a = x, absurd (or.inl aeqx) h,
assert aninxs : a ∉ xs, from λ ainxs : a ∈ xs, absurd (or.inr ainxs) h,
have anex : a ≠ x, from λ aeqx : a = x, absurd (or.inl aeqx) h,
have aninxs : a ∉ xs, from λ ainxs : a ∈ xs, absurd (or.inr ainxs) h,
by rewrite [erase_cons_tail _ anex, length_cons, length_erase_of_not_mem aninxs]
lemma erase_append_left {a : A} : ∀ {l₁} (l₂), a ∈ l₁ → erase a (l₁++l₂) = erase a l₁ ++ l₂
@ -57,7 +57,7 @@ lemma erase_append_left {a : A} : ∀ {l₁} (l₂), a ∈ l₁ → erase a (l
by_cases
(λ aeqx : a = x, by rewrite [aeqx, append_cons, *erase_cons_head])
(λ anex : a ≠ x,
assert ainxs : a ∈ xs, from mem_of_ne_of_mem anex h,
have ainxs : a ∈ xs, from mem_of_ne_of_mem anex h,
by rewrite [append_cons, *erase_cons_tail _ anex, erase_append_left l₂ ainxs])
lemma erase_append_right {a : A} : ∀ {l₁} (l₂), a ∉ l₁ → erase a (l₁++l₂) = l₁ ++ erase a l₂
@ -66,7 +66,7 @@ lemma erase_append_right {a : A} : ∀ {l₁} (l₂), a ∉ l₁ → erase a (l
by_cases
(λ aeqx : a = x, by rewrite aeqx at h; exact (absurd !mem_cons h))
(λ anex : a ≠ x,
assert nainxs : a ∉ xs, from not_mem_of_not_mem_cons h,
have nainxs : a ∉ xs, from not_mem_of_not_mem_cons h,
by rewrite [append_cons, *erase_cons_tail _ anex, erase_append_right l₂ nainxs])
lemma erase_sub (a : A) : ∀ l, erase a l ⊆ l
@ -75,31 +75,31 @@ lemma erase_sub (a : A) : ∀ l, erase a l ⊆ l
by_cases
(λ aeqx : a = x, by rewrite [aeqx at xine, erase_cons_head at xine]; exact (or.inr xine))
(λ anex : a ≠ x,
assert yinxe : y ∈ x :: erase a xs, by rewrite [erase_cons_tail _ anex at xine]; exact xine,
assert subxs : erase a xs ⊆ xs, from erase_sub xs,
have yinxe : y ∈ x :: erase a xs, by rewrite [erase_cons_tail _ anex at xine]; exact xine,
have subxs : erase a xs ⊆ xs, from erase_sub xs,
by_cases
(λ yeqx : y = x, by rewrite yeqx; apply mem_cons)
(λ ynex : y ≠ x,
assert yine : y ∈ erase a xs, from mem_of_ne_of_mem ynex yinxe,
assert yinxs : y ∈ xs, from subxs yine,
have yine : y ∈ erase a xs, from mem_of_ne_of_mem ynex yinxe,
have yinxs : y ∈ xs, from subxs yine,
or.inr yinxs))
theorem mem_erase_of_ne_of_mem {a b : A} : ∀ {l : list A}, a ≠ b → a ∈ l → a ∈ erase b l
| [] n i := absurd i !not_mem_nil
| (c::l) n i := by_cases
(λ beqc : b = c,
assert ainl : a ∈ l, from or.elim (eq_or_mem_of_mem_cons i)
have ainl : a ∈ l, from or.elim (eq_or_mem_of_mem_cons i)
(λ aeqc : a = c, absurd aeqc (beqc ▸ n))
(λ ainl : a ∈ l, ainl),
by rewrite [beqc, erase_cons_head]; exact ainl)
(λ bnec : b ≠ c, by_cases
(λ aeqc : a = c,
assert aux : a ∈ c :: erase b l, by rewrite [aeqc]; exact !mem_cons,
have aux : a ∈ c :: erase b l, by rewrite [aeqc]; exact !mem_cons,
by rewrite [erase_cons_tail _ bnec]; exact aux)
(λ anec : a ≠ c,
have ainl : a ∈ l, from mem_of_ne_of_mem anec i,
have ainel : a ∈ erase b l, from mem_erase_of_ne_of_mem n ainl,
assert aux : a ∈ c :: erase b l, from mem_cons_of_mem _ ainel,
have aux : a ∈ c :: erase b l, from mem_cons_of_mem _ ainel,
by rewrite [erase_cons_tail _ bnec]; exact aux)) --
theorem mem_of_mem_erase {a b : A} : ∀ {l}, a ∈ erase b l → a ∈ l
@ -117,10 +117,10 @@ theorem mem_of_mem_erase {a b : A} : ∀ {l}, a ∈ erase b l → a ∈ l
theorem all_erase_of_all {p : A → Prop} (a : A) : ∀ {l}, all l p → all (erase a l) p
| [] h := by rewrite [erase_nil]; exact h
| (b::l) h :=
assert h₁ : all l p, from all_of_all_cons h,
have h₁ : all l p, from all_of_all_cons h,
have h₂ : all (erase a l) p, from all_erase_of_all h₁,
have pb : p b, from of_all_cons h,
assert h₃ : all (b :: erase a l) p, from all_cons_of_all pb h₂,
have h₃ : all (b :: erase a l) p, from all_cons_of_all pb h₂,
by_cases
(λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact h₁)
(λ aneb : a ≠ b, by rewrite [erase_cons_tail _ aneb]; exact h₃)
@ -280,13 +280,13 @@ nodup_append_of_nodup_of_nodup_of_disjoint d₂ d₄ disj₂
theorem nodup_map {f : A → B} (inj : injective f) : ∀ {l : list A}, nodup l → nodup (map f l)
| [] n := begin rewrite [map_nil], apply nodup_nil end
| (x::xs) n :=
assert nxinxs : x ∉ xs, from not_mem_of_nodup_cons n,
assert ndxs : nodup xs, from nodup_of_nodup_cons n,
assert ndmfxs : nodup (map f xs), from nodup_map ndxs,
assert nfxinm : f x ∉ map f xs, from
have nxinxs : x ∉ xs, from not_mem_of_nodup_cons n,
have ndxs : nodup xs, from nodup_of_nodup_cons n,
have ndmfxs : nodup (map f xs), from nodup_map ndxs,
have nfxinm : f x ∉ map f xs, from
λ ab : f x ∈ map f xs,
obtain (y : A) (yinxs : y ∈ xs) (fyfx : f y = f x), from exists_of_mem_map ab,
assert yeqx : y = x, from inj fyfx,
have yeqx : y = x, from inj fyfx,
by subst y; contradiction,
nodup_cons nfxinm ndmfxs
@ -299,7 +299,7 @@ theorem nodup_erase_of_nodup [decidable_eq A] (a : A) : ∀ {l}, nodup l → nod
have ndl : nodup l, from nodup_of_nodup_cons n,
have ndeal : nodup (erase a l), from nodup_erase_of_nodup ndl,
have nbineal : b ∉ erase a l, from λ i, absurd (erase_sub _ _ i) nbinl,
assert aux : nodup (b :: erase a l), from nodup_cons nbineal ndeal,
have aux : nodup (b :: erase a l), from nodup_cons nbineal ndeal,
by rewrite [erase_cons_tail _ aneb]; exact aux)
theorem mem_erase_of_nodup [decidable_eq A] (a : A) : ∀ {l}, nodup l → a ∉ erase a l
@ -307,11 +307,11 @@ theorem mem_erase_of_nodup [decidable_eq A] (a : A) : ∀ {l}, nodup l → a ∉
| (b::l) n :=
have ndl : nodup l, from nodup_of_nodup_cons n,
have naineal : a ∉ erase a l, from mem_erase_of_nodup ndl,
assert nbinl : b ∉ l, from not_mem_of_nodup_cons n,
have nbinl : b ∉ l, from not_mem_of_nodup_cons n,
by_cases
(λ aeqb : a = b, by rewrite [aeqb, erase_cons_head]; exact nbinl)
(λ aneb : a ≠ b,
assert aux : a ∉ b :: erase a l, from
have aux : a ∉ b :: erase a l, from
assume ainbeal : a ∈ b :: erase a l, or.elim (eq_or_mem_of_mem_cons ainbeal)
(λ aeqb : a = b, absurd aeqb aneb)
(λ aineal : a ∈ erase a l, absurd aineal naineal),
@ -366,16 +366,16 @@ theorem nodup_erase_dup [decidable_eq A] : ∀ l : list A, nodup (erase_dup l)
| (a::l) := by_cases
(λ ainl : a ∈ l, by rewrite [erase_dup_cons_of_mem ainl]; exact (nodup_erase_dup l))
(λ nainl : a ∉ l,
assert r : nodup (erase_dup l), from nodup_erase_dup l,
assert nin : a ∉ erase_dup l, from
have r : nodup (erase_dup l), from nodup_erase_dup l,
have nin : a ∉ erase_dup l, from
assume ab : a ∈ erase_dup l, absurd (mem_of_mem_erase_dup ab) nainl,
by rewrite [erase_dup_cons_of_not_mem nainl]; exact (nodup_cons nin r))
theorem erase_dup_eq_of_nodup [decidable_eq A] : ∀ {l : list A}, nodup l → erase_dup l = l
| [] d := rfl
| (a::l) d :=
assert nainl : a ∉ l, from not_mem_of_nodup_cons d,
assert dl : nodup l, from nodup_of_nodup_cons d,
have nainl : a ∉ l, from not_mem_of_nodup_cons d,
have dl : nodup l, from nodup_of_nodup_cons d,
by rewrite [erase_dup_cons_of_not_mem nainl, erase_dup_eq_of_nodup dl]
definition decidable_nodup [instance] [decidable_eq A] : ∀ (l : list A), decidable (nodup l)
@ -421,8 +421,8 @@ theorem nodup_filter (p : A → Prop) [decidable_pred p] : ∀ {l : list A}, nod
| (a::l) nd :=
have nainl : a ∉ l, from not_mem_of_nodup_cons nd,
have ndl : nodup l, from nodup_of_nodup_cons nd,
assert ndf : nodup (filter p l), from nodup_filter ndl,
assert nainf : a ∉ filter p l, from
have ndf : nodup (filter p l), from nodup_filter ndl,
have nainf : a ∉ filter p l, from
assume ainf, absurd (mem_of_mem_filter ainf) nainl,
by_cases
(λ pa : p a, by rewrite [filter_cons_of_pos _ pa]; exact (nodup_cons nainf ndf))
@ -575,14 +575,14 @@ by_cases
theorem nodup_union_of_nodup_of_nodup : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → nodup (union l₁ l₂)
| [] l₂ n₁ nl₂ := by rewrite nil_union; exact nl₂
| (a::l₁) l₂ nal₁ nl₂ :=
assert nl₁ : nodup l₁, from nodup_of_nodup_cons nal₁,
assert nl₁l₂ : nodup (union l₁ l₂), from nodup_union_of_nodup_of_nodup nl₁ nl₂,
have nl₁ : nodup l₁, from nodup_of_nodup_cons nal₁,
have nl₁l₂ : nodup (union l₁ l₂), from nodup_union_of_nodup_of_nodup nl₁ nl₂,
by_cases
(λ ainl₂ : a ∈ l₂,
by rewrite [union_cons_of_mem l₁ ainl₂]; exact nl₁l₂)
(λ nainl₂ : a ∉ l₂,
have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons nal₁,
assert nainl₁l₂ : a ∉ union l₁ l₂, from
have nainl₁l₂ : a ∉ union l₁ l₂, from
assume ainl₁l₂ : a ∈ union l₁ l₂, or.elim (mem_or_mem_of_mem_union ainl₁l₂)
(λ ainl₁, absurd ainl₁ nainl₁)
(λ ainl₂, absurd ainl₂ nainl₂),
@ -591,8 +591,8 @@ theorem nodup_union_of_nodup_of_nodup : ∀ {l₁ l₂ : list A}, nodup l₁ →
theorem union_eq_append : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → union l₁ l₂ = append l₁ l₂
| [] l₂ d := rfl
| (a::l₁) l₂ d :=
assert nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons,
assert d₁ : disjoint l₁ l₂, from disjoint_of_disjoint_cons_left d,
have nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons,
have d₁ : disjoint l₁ l₂, from disjoint_of_disjoint_cons_left d,
by rewrite [union_cons_of_not_mem _ nainl₂, append_cons, union_eq_append d₁]
theorem all_union {p : A → Prop} : ∀ {l₁ l₂ : list A}, all l₁ p → all l₂ p → all (union l₁ l₂) p
@ -600,8 +600,8 @@ theorem all_union {p : A → Prop} : ∀ {l₁ l₂ : list A}, all l₁ p → al
| (a::l₁) l₂ h₁ h₂ :=
have h₁' : all l₁ p, from all_of_all_cons h₁,
have pa : p a, from of_all_cons h₁,
assert au : all (union l₁ l₂) p, from all_union h₁' h₂,
assert au' : all (a :: union l₁ l₂) p, from all_cons_of_all pa au,
have au : all (union l₁ l₂) p, from all_union h₁' h₂,
have au' : all (a :: union l₁ l₂) p, from all_cons_of_all pa au,
by_cases
(λ ainl₂ : a ∈ l₂, by rewrite [union_cons_of_mem _ ainl₂]; exact au)
(λ nainl₂ : a ∉ l₂, by rewrite [union_cons_of_not_mem _ nainl₂]; exact au')
@ -757,10 +757,10 @@ theorem mem_inter_of_mem_of_mem : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈
theorem nodup_inter_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (inter l₁ l₂)
| [] l₂ d := nodup_nil
| (a::l₁) l₂ d :=
have d₁ : nodup l₁, from nodup_of_nodup_cons d,
assert d₂ : nodup (inter l₁ l₂), from nodup_inter_of_nodup _ d₁,
have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons d,
assert naini : a ∉ inter l₁ l₂, from λ i, absurd (mem_of_mem_inter_left i) nainl₁,
have d₁ : nodup l₁, from nodup_of_nodup_cons d,
have d₂ : nodup (inter l₁ l₂), from nodup_inter_of_nodup _ d₁,
have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons d,
have naini : a ∉ inter l₁ l₂, from λ i, absurd (mem_of_mem_inter_left i) nainl₁,
by_cases
(λ ainl₂ : a ∈ l₂, by rewrite [inter_cons_of_mem _ ainl₂]; exact (nodup_cons naini d₂))
(λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact d₂)
@ -768,17 +768,17 @@ theorem nodup_inter_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup
theorem inter_eq_nil_of_disjoint : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → inter l₁ l₂ = []
| [] l₂ d := rfl
| (a::l₁) l₂ d :=
assert aux_eq : inter l₁ l₂ = [], from inter_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d),
assert nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons,
have aux_eq : inter l₁ l₂ = [], from inter_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d),
have nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons,
by rewrite [inter_cons_of_not_mem _ nainl₂, aux_eq]
theorem all_inter_of_all_left {p : A → Prop} : ∀ {l₁} (l₂), all l₁ p → all (inter l₁ l₂) p
| [] l₂ h := trivial
| (a::l₁) l₂ h :=
have h₁ : all l₁ p, from all_of_all_cons h,
assert h₂ : all (inter l₁ l₂) p, from all_inter_of_all_left _ h₁,
have pa : p a, from of_all_cons h,
assert h₃ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₂,
have h₁ : all l₁ p, from all_of_all_cons h,
have h₂ : all (inter l₁ l₂) p, from all_inter_of_all_left _ h₁,
have pa : p a, from of_all_cons h,
have h₃ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₂,
by_cases
(λ ainl₂ : a ∈ l₂, by rewrite [inter_cons_of_mem _ ainl₂]; exact h₃)
(λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact h₂)
@ -786,11 +786,11 @@ theorem all_inter_of_all_left {p : A → Prop} : ∀ {l₁} (l₂), all l₁ p
theorem all_inter_of_all_right {p : A → Prop} : ∀ (l₁) {l₂}, all l₂ p → all (inter l₁ l₂) p
| [] l₂ h := trivial
| (a::l₁) l₂ h :=
assert h₁ : all (inter l₁ l₂) p, from all_inter_of_all_right _ h,
have h₁ : all (inter l₁ l₂) p, from all_inter_of_all_right _ h,
by_cases
(λ ainl₂ : a ∈ l₂,
have pa : p a, from of_mem_of_all ainl₂ h,
assert h₂ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₁,
have pa : p a, from of_mem_of_all ainl₂ h,
have h₂ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₁,
by rewrite [inter_cons_of_mem _ ainl₂]; exact h₂)
(λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact h₁)

36
library/data/list/sort.lean
View file

@ -33,34 +33,34 @@ lemma min_core_lemma : ∀ {b l} a, b ∈ l ∨ b = a → R (min_core R l a) b
| b [] a h := or.elim h
(suppose b ∈ [], absurd this !not_mem_nil)
(suppose b = a,
assert R a a, from rf a,
have R a a, from rf a,
begin subst b, unfold min_core, assumption end)
| b (c::l) a h := or.elim h
(suppose b ∈ c :: l, or.elim (eq_or_mem_of_mem_cons this)
(suppose b = c,
or.elim (em (R c a))
(suppose R c a,
assert R (min_core R l b) b, from min_core_lemma _ (or.inr rfl),
have R (min_core R l b) b, from min_core_lemma _ (or.inr rfl),
begin unfold min_core, rewrite [if_pos `R c a`], subst c, assumption end)
(suppose ¬ R c a,
assert R a c, from or_resolve_right (to c a) this,
assert R (min_core R l a) a, from min_core_lemma _ (or.inr rfl),
assert R (min_core R l a) c, from tr this `R a c`,
have R a c, from or_resolve_right (to c a) this,
have R (min_core R l a) a, from min_core_lemma _ (or.inr rfl),
have R (min_core R l a) c, from tr this `R a c`,
begin unfold min_core, rewrite [if_neg `¬ R c a`], subst b, exact `R (min_core R l a) c` end))
(suppose b ∈ l,
or.elim (em (R c a))
(suppose R c a,
assert R (min_core R l c) b, from min_core_lemma _ (or.inl `b ∈ l`),
have R (min_core R l c) b, from min_core_lemma _ (or.inl `b ∈ l`),
begin unfold min_core, rewrite [if_pos `R c a`], assumption end)
(suppose ¬ R c a,
assert R (min_core R l a) b, from min_core_lemma _ (or.inl `b ∈ l`),
have R (min_core R l a) b, from min_core_lemma _ (or.inl `b ∈ l`),
begin unfold min_core, rewrite [if_neg `¬ R c a`], assumption end)))
(suppose b = a,
assert R (min_core R l a) b, from min_core_lemma _ (or.inr this),
have R (min_core R l a) b, from min_core_lemma _ (or.inr this),
or.elim (em (R c a))
(suppose R c a,
assert R (min_core R l c) c, from min_core_lemma _ (or.inr rfl),
assert R (min_core R l c) a, from tr this `R c a`,
have R (min_core R l c) c, from min_core_lemma _ (or.inr rfl),
have R (min_core R l c) a, from tr this `R c a`,
begin unfold min_core, rewrite [if_pos `R c a`], subst b, exact `R (min_core R l c) a` end)
(suppose ¬ R c a, begin unfold min_core, rewrite [if_neg `¬ R c a`], assumption end))
@ -76,10 +76,10 @@ lemma min_lemma : ∀ {l} (h : l ≠ nil), all l (R (min R l h))
all_of_forall (take x, suppose x ∈ b::l,
or.elim (eq_or_mem_of_mem_cons this)
(suppose x = b,
assert R (min_core R l b) b, from min_core_le to tr rf b,
have R (min_core R l b) b, from min_core_le to tr rf b,
begin subst x, unfold min, assumption end)
(suppose x ∈ l,
assert R (min_core R l b) x, from min_core_le_of_mem to tr rf _ this,
have R (min_core R l b) x, from min_core_le_of_mem to tr rf _ this,
begin unfold min, assumption end))
variable (R)
@ -135,7 +135,7 @@ assume h₁ h₂, by rewrite h₂ at h₁; contradiction
include decR
lemma sort_aux_lemma {l n} (h : length l = succ n) : length (erase (min R l (ne_nil h)) l) = n :=
have min R l _ ∈ l, from min_mem R l (ne_nil h),
assert length (erase (min R l _) l) = pred (length l), from length_erase_of_mem this,
have length (erase (min R l _) l) = pred (length l), from length_erase_of_mem this,
by rewrite h at this; exact this
definition sort_aux : Π (n : nat) (l : list A), length l = n → list A
@ -154,7 +154,7 @@ lemma sort_aux_perm : ∀ {n : nat} {l : list A} (h : length l = n), sort_aux R
| 0 l h := by rewrite [↑sort_aux, eq_nil_of_length_eq_zero h]
| (succ n) l h :=
let m := min R l (ne_nil h) in
assert leq : length (erase m l) = n, from sort_aux_lemma R h,
have leq : length (erase m l) = n, from sort_aux_lemma R h,
calc m :: sort_aux R n (erase m l) leq
~ m :: erase m l : perm.skip m (sort_aux_perm leq)
... ~ l : perm_erase (min_mem _ _ _)
@ -166,10 +166,10 @@ lemma strongly_sorted_sort_aux : ∀ {n : nat} {l : list A} (h : length l = n),
| 0 l h := !strongly_sorted.base
| (succ n) l h :=
let m := min R l (ne_nil h) in
assert leq : length (erase m l) = n, from sort_aux_lemma R h,
assert ss : strongly_sorted R (sort_aux R n (erase m l) leq), from strongly_sorted_sort_aux leq,
assert all l (R m), from min_lemma to tr rf (ne_nil h),
assert hall : all (sort_aux R n (erase m l) leq) (R m), from
have leq : length (erase m l) = n, from sort_aux_lemma R h,
have ss : strongly_sorted R (sort_aux R n (erase m l) leq), from strongly_sorted_sort_aux leq,
have all l (R m), from min_lemma to tr rf (ne_nil h),
have hall : all (sort_aux R n (erase m l) leq) (R m), from
all_of_forall (take x,
suppose x ∈ sort_aux R n (erase m l) leq,
have x ∈ erase m l, from mem_perm (sort_aux_perm R leq) this,

12
library/data/list/sorted.lean
View file

@ -104,10 +104,10 @@ lemma eq_of_sorted_of_perm (tr : transitive R) (anti : anti_symmetric R) : ∀ {
| (a::l₁) l₂ h₁ h₂ h₃ :=
have aux : ∀ {t}, l₂ = a::t → a::l₁ = l₂, from
take t, suppose l₂ = a::t,
have l₁ ~ t, by rewrite [this at h₁]; apply perm_cons_inv h₁,
have sorted R l₁, from and.right (sorted_inv h₂),
have sorted R t, by rewrite [`l₂ = a::t` at h₃]; exact and.right (sorted_inv h₃),
assert l₁ = t, from eq_of_sorted_of_perm `l₁ ~ t` `sorted R l₁` `sorted R t`,
have l₁ ~ t, by rewrite [this at h₁]; apply perm_cons_inv h₁,
have sorted R l₁, from and.right (sorted_inv h₂),
have sorted R t, by rewrite [`l₂ = a::t` at h₃]; exact and.right (sorted_inv h₃),
have l₁ = t, from eq_of_sorted_of_perm `l₁ ~ t` `sorted R l₁` `sorted R t`,
show a :: l₁ = l₂, by rewrite [`l₂ = a::t`, this],
have a ∈ l₂, from mem_perm h₁ !mem_cons,
obtain s t (e₁ : l₂ = s ++ (a::t)), from mem_split this,
@ -125,8 +125,8 @@ lemma eq_of_sorted_of_perm (tr : transitive R) (anti : anti_symmetric R) : ∀ {
apply or.elim (eq_or_mem_of_mem_cons `b ∈ a::l₁`),
suppose b = a, by rewrite this at e₁; exact aux e₁,
suppose b ∈ l₁,
have R a b, from of_mem_of_all this hall₁,
assert b = a, from anti `R b a` `R a b`,
have R a b, from of_mem_of_all this hall₁,
have b = a, from anti `R b a` `R a b`,
by rewrite this at e₁; exact aux e₁ }
end
end list

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

@ -148,7 +148,7 @@ nat.induction_on n
(by simp)
(take a iH,
-- TODO(Leo): replace with forward reasoning after we add strategies for it.
assert succ (a + m) = succ (a + k) → a + m = a + k, from !succ.inj,
have succ (a + m) = succ (a + k) → a + m = a + k, from !succ.inj,
by inst_simp)
protected theorem add_right_cancel {n m k : ℕ} (H : n + m = k + m) : n = k :=

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

@ -165,15 +165,15 @@ begin
intro x IH,
show succ x = succ x / y * y + succ x % y, from
if H1 : succ x < y then
assert H2 : succ x / y = 0, from div_eq_zero_of_lt H1,
assert H3 : succ x % y = succ x, from mod_eq_of_lt H1,
have H2 : succ x / y = 0, from div_eq_zero_of_lt H1,
have H3 : succ x % y = succ x, from mod_eq_of_lt H1,
begin rewrite [H2, H3, zero_mul, zero_add] end
else
have H2 : y ≤ succ x, from le_of_not_gt H1,
assert H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2,
assert H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2,
have H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2,
have H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2,
have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
assert H6 : succ x - y ≤ x, from le_of_lt_succ H5,
have H6 : succ x - y ≤ x, from le_of_lt_succ H5,
(calc
succ x / y * y + succ x % y =
succ ((succ x - y) / y) * y + succ x % y : by rewrite H3
@ -210,7 +210,7 @@ by_cases_zero_pos n
assume npos : n > 0,
assume H1 : (m + i) % n = (k + i) % n,
have H2 : (m + i % n) % n = (k + i % n) % n, by rewrite [*add_mod_mod, H1],
assert H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n,
have H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n,
from add_mod_eq_add_mod_right _ H2,
begin
revert H3,
@ -298,11 +298,11 @@ theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) % k = (m * (n % k)) % k :
!mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod
protected theorem div_one (n : ℕ) : n / 1 = n :=
assert n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹,
have n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹,
begin rewrite [-this at {2}, mul_one, mod_one] end
protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 :=
assert (n * 1) / (n * 1) = 1 / 1, from !nat.mul_div_mul_left H,
have (n * 1) / (n * 1) = 1 / 1, from !nat.mul_div_mul_left H,
by rewrite [nat.div_one at this, -this, *mul_one]
theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m % n = 0) : m / n * n = m :=
@ -448,11 +448,11 @@ end
lemma le_of_dvd {m n : nat} : n > 0 → m ∣ n → m ≤ n :=
assume (h₁ : n > 0) (h₂ : m ∣ n),
assert h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂,
have h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂,
by_contradiction
(λ nle : ¬ m ≤ n,
have h₄ : m > n, from lt_of_not_ge nle,
assert h₅ : n % m = n, from mod_eq_of_lt h₄,
have h₅ : n % m = n, from mod_eq_of_lt h₄,
begin
rewrite h₃ at h₅, subst n,
exact absurd h₁ (lt.irrefl 0)
@ -513,7 +513,7 @@ lt_of_mul_lt_mul_right (calc
... < n * k : H)
protected theorem lt_mul_of_div_lt {m n k : ℕ} (H1 : k > 0) (H2 : m / k < n) : m < n * k :=
assert H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2),
have H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2),
have H4 : m / k * k + k ≤ n * k, by rewrite [succ_mul at H3]; apply H3,
calc
m = m / k * k + m % k : eq_div_mul_add_mod
@ -564,29 +564,29 @@ nat.strong_induction_on a
(λ a ih,
let k₁ := a / (b*c) in
let k₂ := a %(b*c) in
assert bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`,
assert k₂ < b * c, from mod_lt _ bc_pos,
assert k₂ ≤ a, from !mod_le,
have bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`,
have k₂ < b * c, from mod_lt _ bc_pos,
have k₂ ≤ a, from !mod_le,
or.elim (eq_or_lt_of_le this)
(suppose k₂ = a,
assert i₁ : a < b * c, by rewrite -this; assumption,
assert k₁ = 0, from div_eq_zero_of_lt i₁,
assert a / b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁,
have i₁ : a < b * c, by rewrite -this; assumption,
have k₁ = 0, from div_eq_zero_of_lt i₁,
have a / b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁,
begin
rewrite [`k₁ = 0`],
show (a / b) / c = 0, from div_eq_zero_of_lt `a / b < c`
end)
(suppose k₂ < a,
assert a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c),
assert a / b = k₁*c + k₂ / b, by
have a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c),
have a / b = k₁*c + k₂ / b, by
rewrite [this at {1}, mul.comm b c at {2}, -mul.assoc,
add.comm, add_mul_div_self `b > 0`, add.comm],
assert e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by
have e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by
rewrite [this, add.comm, add_mul_div_self `c > 0`, add.comm],
assert e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`,
assert e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`,
assert (k₂ / b) / c = 0, by rewrite [e₂, e₃],
show (a / b) / c = k₁, by rewrite [e₁, this]))
have e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`,
have e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`,
have (k₂ / b) / c = 0, by rewrite [e₂, e₃],
show (a / b) / c = k₁, by rewrite [e₁, this]))
protected lemma div_div_eq_div_mul (a b c : nat) : (a / b) / c = a / (b * c) :=
begin

4
library/data/nat/examples/partial_sum.lean
View file

@ -28,6 +28,6 @@ lemma two_mul_partial_sum_eq : ∀ n, 2 * partial_sum n = (succ n) * n
theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) / 2 :=
take n,
assert h₁ : (2 * partial_sum n) / 2 = ((succ n) * n) / 2, by rewrite two_mul_partial_sum_eq,
assert h₂ : (2:nat) > 0, from dec_trivial,
have h₁ : (2 * partial_sum n) / 2 = ((succ n) * n) / 2, by rewrite two_mul_partial_sum_eq,
have h₂ : (2:nat) > 0, from dec_trivial,
by rewrite [nat.mul_div_cancel_left _ h₂ at h₁]; exact h₁

2
library/data/nat/find.lean
View file

@ -58,7 +58,7 @@ acc.intro y (λ (z : nat) (l : z ≺ y),
private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gtb y
| 0 y a0 ylt0 := absurd ylt0 !not_lt_zero
| (succ x) y asx yltsx :=
assert acc gtb x, from acc_of_acc_succ asx,
have acc gtb x, from acc_of_acc_succ asx,
by_cases
(suppose y = x, by substvars; assumption)
(suppose y ≠ x, acc_of_acc_of_lt `acc gtb x` (lt_of_le_of_ne (le_of_lt_succ yltsx) this))

2
library/data/nat/gcd.lean
View file

@ -306,7 +306,7 @@ calc
theorem not_coprime_of_dvd_of_dvd {m n d : ℕ} (dgt1 : d > 1) (Hm : d ∣ m) (Hn : d ∣ n) :
¬ coprime m n :=
assume co : coprime m n,
assert d ∣ gcd m n, from dvd_gcd Hm Hn,
have d ∣ gcd m n, from dvd_gcd Hm Hn,
have d ∣ 1, by rewrite [↑coprime at co, co at this]; apply this,
have d ≤ 1, from le_of_dvd dec_trivial this,
show false, from not_lt_of_ge `d ≤ 1` `d > 1`

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

@ -275,7 +275,7 @@ exists_eq_succ_of_lt H
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 :=
pos_of_ne_zero
(suppose m = 0,
assert n = 0, from eq_zero_of_zero_dvd (this ▸ H1),
have n = 0, from eq_zero_of_zero_dvd (this ▸ H1),
ne_of_lt H2 (by subst n))
/- multiplication -/
@ -367,11 +367,11 @@ or.elim !lt_or_ge
protected theorem min_add_add_left (a b c : ℕ) : min (a + b) (a + c) = a + min b c :=
decidable.by_cases
(suppose b ≤ c,
assert a + b ≤ a + c, from add_le_add_left this _,
have a + b ≤ a + c, from add_le_add_left this _,
by rewrite [min_eq_left `b ≤ c`, min_eq_left this])
(suppose ¬ b ≤ c,
assert c ≤ b, from le_of_lt (lt_of_not_ge this),
assert a + c ≤ a + b, from add_le_add_left this _,
have c ≤ b, from le_of_lt (lt_of_not_ge this),
have a + c ≤ a + b, from add_le_add_left this _,
by rewrite [min_eq_right `c ≤ b`, min_eq_right this])
protected theorem min_add_add_right (a b c : ℕ) : min (a + c) (b + c) = min a b + c :=
@ -380,11 +380,11 @@ by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply nat.min_add_add_lef
protected theorem max_add_add_left (a b c : ℕ) : max (a + b) (a + c) = a + max b c :=
decidable.by_cases
(suppose b ≤ c,
assert a + b ≤ a + c, from add_le_add_left this _,
have a + b ≤ a + c, from add_le_add_left this _,
by rewrite [max_eq_right `b ≤ c`, max_eq_right this])
(suppose ¬ b ≤ c,
assert c ≤ b, from le_of_lt (lt_of_not_ge this),
assert a + c ≤ a + b, from add_le_add_left this _,
have c ≤ b, from le_of_lt (lt_of_not_ge this),
have a + c ≤ a + b, from add_le_add_left this _,
by rewrite [max_eq_left `c ≤ b`, max_eq_left this])
protected theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c :=

24
library/data/nat/pairing.lean
View file

@ -27,19 +27,19 @@ by_cases
rewrite [if_pos this, add_sub_of_le (sqrt_lower n)]
end)
(suppose h₁ : ¬ n - s*s < s,
have s ≤ n - s*s, from le_of_not_gt h₁,
assert s + s*s ≤ n - s*s + s*s, from add_le_add_right this (s*s),
assert s*s + s ≤ n, by rewrite [nat.sub_add_cancel (sqrt_lower n) at this,
have s ≤ n - s*s, from le_of_not_gt h₁,
have s + s*s ≤ n - s*s + s*s, from add_le_add_right this (s*s),
have s*s + s ≤ n, by rewrite [nat.sub_add_cancel (sqrt_lower n) at this,
add.comm at this]; assumption,
have n ≤ s*s + s + s, from sqrt_upper n,
have n - s*s ≤ s + s, from calc
have n ≤ s*s + s + s, from sqrt_upper n,
have n - s*s ≤ s + s, from calc
n - s*s ≤ (s*s + s + s) - s*s : nat.sub_le_sub_right this (s*s)
... = (s*s + (s+s)) - s*s : by rewrite add.assoc
... = s + s : by rewrite nat.add_sub_cancel_left,
have n - s*s - s ≤ s, from calc
n - s*s - s ≤ (s + s) - s : nat.sub_le_sub_right this s
... = s : by rewrite nat.add_sub_cancel_left,
assert h₂ : ¬ s < n - s*s - s, from not_lt_of_ge this,
have h₂ : ¬ s < n - s*s - s, from not_lt_of_ge this,
begin
esimp [unpair],
rewrite [if_neg h₁], esimp,
@ -50,7 +50,7 @@ by_cases
theorem unpair_mkpair (a b : nat) : unpair (mkpair a b) = (a, b) :=
by_cases
(suppose a < b,
assert a ≤ b + b, from calc
have a ≤ b + b, from calc
a ≤ b : le_of_lt this
... ≤ b+b : !le_add_right,
begin
@ -61,9 +61,9 @@ by_cases
end)
(suppose ¬ a < b,
have b ≤ a, from le_of_not_gt this,
assert a + b ≤ a + a, from add_le_add_left this a,
have a + b ≤ a + a, from add_le_add_left this a,
have a + b ≥ a, from !le_add_right,
assert ¬ a + b < a, from not_lt_of_ge this,
have ¬ a + b < a, from not_lt_of_ge this,
begin
esimp [mkpair],
rewrite [if_neg `¬ a < b`],
@ -82,9 +82,9 @@ or.elim (eq_or_lt_of_le this)
let s := sqrt n in
by_cases
(suppose h : n - s*s < s,
assert n > 0, from lt_of_succ_lt `n > 1`,
assert sqrt n > 0, from sqrt_pos_of_pos this,
assert sqrt n * sqrt n > 0, from mul_pos this this,
have n > 0, from lt_of_succ_lt `n > 1`,
have sqrt n > 0, from sqrt_pos_of_pos this,
have sqrt n * sqrt n > 0, from mul_pos this this,
begin unfold unpair, rewrite [if_pos h], esimp, exact sub_lt `n > 0` `sqrt n * sqrt n > 0` end)
(suppose ¬ n - s*s < s, begin unfold unpair, rewrite [if_neg this], esimp, apply sqrt_lt `n > 1` end))

26
library/data/nat/parity.lean
View file

@ -68,7 +68,7 @@ have h : n+1 ≡ 1 [mod 2], from this,
by_contradiction (suppose ¬ odd (succ n),
have n+1 ≡ 0 [mod 2], from even_of_not_odd this,
have 1 ≡ 0 [mod 2], from eq.trans (eq.symm h) this,
assert 1 = 0, from this,
have 1 = 0, from this,
by contradiction)
lemma eq_1_of_ne_0_lt_2 : ∀ {n : nat}, n ≠ 0 → n < 2 → n = 1
@ -85,13 +85,13 @@ suppose odd n,
lemma odd_of_mod_eq {n} : n % 2 = 1 → odd n :=
suppose n % 2 = 1,
by_contradiction (suppose ¬ odd n,
assert n % 2 = 0, from even_of_not_odd this,
have n % 2 = 0, from even_of_not_odd this,
by rewrite this at *; contradiction)
lemma even_succ_of_odd {n} : odd n → even (succ n) :=
suppose odd n,
assert n % 2 = 1 % 2, from mod_eq_of_odd this,
assert (n+1) % 2 = 2 % 2, from add_mod_eq_add_mod_right 1 this,
have n % 2 = 1 % 2, from mod_eq_of_odd this,
have (n+1) % 2 = 2 % 2, from add_mod_eq_add_mod_right 1 this,
by rewrite mod_self at this; exact this
lemma odd_succ_succ_of_odd {n} : odd n → odd (succ (succ n)) :=
@ -174,7 +174,7 @@ assume h, by_contradiction (λ hn,
have ∃ k, n = 2 * k, from exists_of_even this,
obtain k₁ (hk₁ : n = 2 * k₁ + 1), from h,
obtain k₂ (hk₂ : n = 2 * k₂), from this,
assert (2 * k₁ + 1) % 2 = (2 * k₂) % 2, by rewrite [-hk₁, -hk₂],
have (2 * k₁ + 1) % 2 = (2 * k₂) % 2, by rewrite [-hk₁, -hk₂],
begin
rewrite [mul_mod_right at this, add.comm at this, add_mul_mod_self_left at this],
contradiction
@ -188,19 +188,19 @@ even_of_exists (exists.intro (k₁+k₂) (by rewrite [hk₁, hk₂, left_distrib
lemma even_add_of_odd_of_odd {n m} : odd n → odd m → even (n+m) :=
suppose odd n, suppose odd m,
assert even (succ n + succ m),
have even (succ n + succ m),
from even_add_of_even_of_even (even_succ_of_odd `odd n`) (even_succ_of_odd `odd m`),
have even(succ (succ (n + m))), by rewrite [add_succ at this, succ_add at this]; exact this,
even_of_even_succ_succ this
lemma odd_add_of_even_of_odd {n m} : even n → odd m → odd (n+m) :=
suppose even n, suppose odd m,
assert even (n + succ m), from even_add_of_even_of_even `even n` (even_succ_of_odd `odd m`),
have even (n + succ m), from even_add_of_even_of_even `even n` (even_succ_of_odd `odd m`),
odd_of_even_succ this
lemma odd_add_of_odd_of_even {n m} : odd n → even m → odd (n+m) :=
suppose odd n, suppose even m,
assert odd (m+n), from odd_add_of_even_of_odd `even m` `odd n`,
have odd (m+n), from odd_add_of_even_of_odd `even m` `odd n`,
by rewrite add.comm at this; exact this
lemma even_mul_of_even_left {n} (m) : even n → even (n*m) :=
@ -210,15 +210,15 @@ even_of_exists (exists.intro (k*m) (by rewrite [hk, mul.assoc]))
lemma even_mul_of_even_right {n} (m) : even n → even (m*n) :=
suppose even n,
assert even (n*m), from even_mul_of_even_left _ this,
have even (n*m), from even_mul_of_even_left _ this,
by rewrite mul.comm at this; exact this
lemma odd_mul_of_odd_of_odd {n m} : odd n → odd m → odd (n*m) :=
suppose odd n, suppose odd m,
assert even (n * succ m), from even_mul_of_even_right _ (even_succ_of_odd `odd m`),
assert even (n * m + n), by rewrite mul_succ at this; exact this,
have even (n * succ m), from even_mul_of_even_right _ (even_succ_of_odd `odd m`),
have even (n * m + n), by rewrite mul_succ at this; exact this,
by_contradiction (suppose ¬ odd (n*m),
assert even (n*m), from even_of_not_odd this,
have even (n*m), from even_of_not_odd this,
absurd `even (n * m + n)` (not_even_of_odd (odd_add_of_even_of_odd this `odd n`)))
lemma even_of_even_mul_self {n} : even (n * n) → even n :=
@ -274,7 +274,7 @@ assume h₁ h₂,
(suppose odd n, or.elim (em (even m))
(suppose even m, absurd `odd n` (not_odd_of_even (iff.mpr h₂ `even m`)))
(suppose odd m,
assert d : 1 / 2 = (0:nat), from dec_trivial,
have d : 1 / 2 = (0:nat), from dec_trivial,
obtain w₁ (hw₁ : n = 2*w₁ + 1), from exists_of_odd `odd n`,
obtain w₂ (hw₂ : m = 2*w₂ + 1), from exists_of_odd `odd m`,
begin

14
library/data/nat/power.lean
View file

@ -58,16 +58,16 @@ by krewrite [*pow_succ, *pow_zero, mul_one]
theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a ^ b = a ^ c → b = c
| a 0 0 h₁ h₂ := rfl
| a (succ b) 0 h₁ h₂ :=
assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
assert (1:nat) < 1, by rewrite [this at h₁]; exact h₁,
have a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
have (1:nat) < 1, by rewrite [this at h₁]; exact h₁,
absurd `1 <[nat] 1` !lt.irrefl
| a 0 (succ c) h₁ h₂ :=
assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
assert (1:nat) < 1, by rewrite [this at h₁]; exact h₁,
have a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
have (1:nat) < 1, by rewrite [this at h₁]; exact h₁,
absurd `1 <[nat] 1` !lt.irrefl
| a (succ b) (succ c) h₁ h₂ :=
assert a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
assert a^b = a^c, by rewrite [*pow_succ at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
have a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
have a^b = a^c, by rewrite [*pow_succ at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
by rewrite [pow_cancel_left h₁ this]
theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → (a ^ succ b) / a = a ^ b
@ -87,7 +87,7 @@ iff.mp !dvd_iff_mod_eq_zero (dvd_pow i h)
lemma pow_dvd_of_pow_succ_dvd {p i n : nat} : p^(succ i) ∣ n → p^i ∣ n :=
suppose p^(succ i) ∣ n,
assert p^i ∣ p^(succ i),
have p^i ∣ p^(succ i),
by rewrite [pow_succ']; apply nat.dvd_of_eq_mul; apply rfl,
dvd.trans `p^i ∣ p^(succ i)` `p^(succ i) ∣ n`

38
library/data/nat/sqrt.lean
View file

@ -31,7 +31,7 @@ theorem sqrt_aux_le : ∀ (s n), sqrt_aux s n ≤ s
| (succ s) n := or.elim (em ((succ s)*(succ s) ≤ n))
(λ h, begin unfold sqrt_aux, rewrite [if_pos h] end)
(λ h,
assert sqrt_aux s n ≤ succ s, from le.step (sqrt_aux_le s n),
have sqrt_aux s n ≤ succ s, from le.step (sqrt_aux_le s n),
begin unfold sqrt_aux, rewrite [if_neg h], assumption end)
definition sqrt (n : nat) : nat :=
@ -42,7 +42,7 @@ theorem sqrt_aux_lower : ∀ {s n : nat}, s ≤ n → sqrt_aux s n * sqrt_aux s
| (succ s) n h := by_cases
(λ h₁ : (succ s)*(succ s) ≤ n, by rewrite [sqrt_aux_succ_of_pos h₁]; exact h₁)
(λ h₂ : ¬ (succ s)*(succ s) ≤ n,
assert aux : s ≤ n, from le_of_succ_le h,
have aux : s ≤ n, from le_of_succ_le h,
by rewrite [sqrt_aux_succ_of_neg h₂]; exact (sqrt_aux_lower aux))
theorem sqrt_lower (n : nat) : sqrt n * sqrt n ≤ n :=
@ -54,8 +54,8 @@ theorem sqrt_aux_upper : ∀ {s n : nat}, n ≤ s*s + s + s → n ≤ sqrt_aux s
(λ h₁ : (succ s)*(succ s) ≤ n,
by rewrite [sqrt_aux_succ_of_pos h₁]; exact h)
(λ h₂ : ¬ (succ s)*(succ s) ≤ n,
assert h₃ : n < (succ s) * (succ s), from lt_of_not_ge h₂,
assert h₄ : n ≤ s * s + s + s, by rewrite [succ_mul_succ_eq at h₃]; exact le_of_lt_succ h₃,
have h₃ : n < (succ s) * (succ s), from lt_of_not_ge h₂,
have h₄ : n ≤ s * s + s + s, by rewrite [succ_mul_succ_eq at h₃]; exact le_of_lt_succ h₃,
by rewrite [sqrt_aux_succ_of_neg h₂]; exact (sqrt_aux_upper h₄))
theorem sqrt_upper (n : nat) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n :=
@ -65,8 +65,8 @@ sqrt_aux_upper aux
private theorem le_squared : ∀ (n : nat), n ≤ n*n
| 0 := !le.refl
| (succ n) :=
have aux₁ : 1 ≤ succ n, from succ_le_succ !zero_le,
assert aux₂ : 1 * succ n ≤ succ n * succ n, from nat.mul_le_mul aux₁ !le.refl,
have aux₁ : 1 ≤ succ n, from succ_le_succ !zero_le,
have aux₂ : 1 * succ n ≤ succ n * succ n, from nat.mul_le_mul aux₁ !le.refl,
by rewrite [one_mul at aux₂]; exact aux₂
private theorem lt_squared : ∀ {n : nat}, n > 1 → n < n * n
@ -74,7 +74,7 @@ private theorem lt_squared : ∀ {n : nat}, n > 1 → n < n * n
| 1 h := absurd h dec_trivial
| (succ (succ n)) h :=
have 1 < succ (succ n), from dec_trivial,
assert succ (succ n) * 1 < succ (succ n) * succ (succ n), from mul_lt_mul_of_pos_left this dec_trivial,
have succ (succ n) * 1 < succ (succ n) * succ (succ n), from mul_lt_mul_of_pos_left this dec_trivial,
by rewrite [mul_one at this]; exact this
theorem sqrt_le (n : nat) : sqrt n ≤ n :=
@ -83,13 +83,13 @@ calc sqrt n ≤ sqrt n * sqrt n : le_squared
theorem eq_zero_of_sqrt_eq_zero {n : nat} : sqrt n = 0 → n = 0 :=
suppose sqrt n = 0,
assert n ≤ sqrt n * sqrt n + sqrt n + sqrt n, from !sqrt_upper,
have n ≤ 0, by rewrite [*`sqrt n = 0` at this]; exact this,
have n ≤ sqrt n * sqrt n + sqrt n + sqrt n, from !sqrt_upper,
have n ≤ 0, by rewrite [*`sqrt n = 0` at this]; exact this,
eq_zero_of_le_zero this
theorem le_three_of_sqrt_eq_one {n : nat} : sqrt n = 1 → n ≤ 3 :=
suppose sqrt n = 1,
assert n ≤ sqrt n * sqrt n + sqrt n + sqrt n, from !sqrt_upper,
have n ≤ sqrt n * sqrt n + sqrt n + sqrt n, from !sqrt_upper,
show n ≤ 3, by rewrite [*`sqrt n = 1` at this]; exact this
theorem sqrt_lt : ∀ {n : nat}, n > 1 → sqrt n < n
@ -116,21 +116,21 @@ theorem sqrt_pos_of_pos {n : nat} : n > 0 → sqrt n > 0 :=
suppose n > 0,
have sqrt n ≠ 0, from
suppose sqrt n = 0,
assert n = 0, from eq_zero_of_sqrt_eq_zero this,
have n = 0, from eq_zero_of_sqrt_eq_zero this,
by subst n; exact absurd `0 > 0` !lt.irrefl,
pos_of_ne_zero this
theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n → sqrt_aux s (n*n + k) = n
| 0 h₂ :=
assert neqz : n = 0, from eq_zero_of_le_zero h₂,
have neqz : n = 0, from eq_zero_of_le_zero h₂,
by rewrite neqz
| (succ s) h₂ := by_cases
(λ hl : (succ s)*(succ s) ≤ n*n + k,
have l₁ : n*n + k ≤ n*n + n + n, from by rewrite [add.assoc]; exact (add_le_add_left h₁ (n*n)),
assert l₂ : n*n + k < n*n + n + n + 1, from lt_succ_of_le l₁,
have l₃ : n*n + k < (succ n)*(succ n), by rewrite [-succ_mul_succ_eq at l₂]; exact l₂,
assert l₄ : (succ s)*(succ s) < (succ n)*(succ n), from lt_of_le_of_lt hl l₃,
have ng : ¬ succ s > (succ n), from
have l₁ : n*n + k ≤ n*n + n + n, from by rewrite [add.assoc]; exact (add_le_add_left h₁ (n*n)),
have l₂ : n*n + k < n*n + n + n + 1, from lt_succ_of_le l₁,
have l₃ : n*n + k < (succ n)*(succ n), by rewrite [-succ_mul_succ_eq at l₂]; exact l₂,
have l₄ : (succ s)*(succ s) < (succ n)*(succ n), from lt_of_le_of_lt hl l₃,
have ng : ¬ succ s > (succ n), from
assume g : succ s > succ n,
have g₁ : (succ s)*(succ s) > (succ n)*(succ n), from mul_lt_mul_of_le_of_le g g,
absurd (lt.trans g₁ l₄) !lt.irrefl,
@ -139,7 +139,7 @@ theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n
assume sseqsn : succ s = succ n,
by rewrite [sseqsn at l₄]; exact (absurd l₄ !lt.irrefl),
have sslen : s < n, from lt_of_succ_lt_succ (lt_of_le_of_ne sslesn ssnesn),
assert sseqn : succ s = n, from le.antisymm sslen h₂,
have sseqn : succ s = n, from le.antisymm sslen h₂,
by rewrite [sqrt_aux_succ_of_pos hl]; exact sseqn)
(λ hg : ¬ (succ s)*(succ s) ≤ n*n + k,
or.elim (eq_or_lt_of_le h₂)
@ -160,6 +160,6 @@ sqrt_offset_eq !zero_le
theorem mul_square_cancel {a b : nat} : a*a = b*b → a = b :=
assume h,
assert aux : sqrt (a*a) = sqrt (b*b), by rewrite h,
have aux : sqrt (a*a) = sqrt (b*b), by rewrite h,
by rewrite [*sqrt_eq at aux]; exact aux
end nat

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

@ -212,8 +212,8 @@ sub.cases
le.intro (add.right_cancel H4))
protected theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 :=
assert H1 : n = n - m + m, from (nat.sub_add_cancel (le_of_lt H))⁻¹,
have H2 : 0 + m < n - m + m, begin rewrite [zero_add, -H1], exact H end,
have H1 : n = n - m + m, from (nat.sub_add_cancel (le_of_lt H))⁻¹,
have H2 : 0 + m < n - m + m, begin rewrite [zero_add, -H1], exact H end,
!lt_of_add_lt_add_right H2
protected theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n :=
@ -242,7 +242,7 @@ sub.cases
sub.cases
(assume H : m ≤ k,
have H2 : n - k ≤ n - m, from nat.sub_le_sub_left H n,
assert H3 : n - k ≤ mn, from nat.sub_eq_of_add_eq Hmn ▸ H2,
have H3 : n - k ≤ mn, from nat.sub_eq_of_add_eq Hmn ▸ H2,
show n - k ≤ mn + 0, begin rewrite add_zero, assumption end)
(take km : ℕ,
assume Hkm : k + km = m,
@ -364,12 +364,12 @@ have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k
this ▸ add_le_add !nat.sub_lt_sub_add_sub !nat.sub_lt_sub_add_sub
theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
assert H : dist (n + m) (k + m) + dist (k + 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,
by rewrite [dist_add_add_left, dist_add_add_right],
by rewrite -H; apply dist.triangle_inequality
theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k :=
assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl,
have ∀ n m, dist n m = n - m + (m - n), from take n m, rfl,
by rewrite [this, this n m, right_distrib, *nat.mul_sub_right_distrib]
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=

6
library/data/pnat.lean
View file

@ -308,7 +308,7 @@ begin
end
theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_pnat n) = m⁻¹ :=
assert hsimp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c,
have hsimp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c,
begin
intro a b c,
rewrite[-*rat.mul_assoc],
@ -322,7 +322,7 @@ theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) (Ha : a > 0) : n
le.trans (inv_ge_of_le H) (one_div_le_one_div_of_le Ha (ubound_ge a))
theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a :=
assert (pceil (a / b))⁻¹ ≤ 1 / (1 / (b / a)),
have (pceil (a / b))⁻¹ ≤ 1 / (1 / (b / a)),
begin
apply one_div_le_one_div_of_le,
show 0 < 1 / (b / a), from
@ -387,7 +387,7 @@ begin
end
theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ :=
assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
have T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
by rewrite[*pnat.inv_mul_eq_mul_inv,-*right_distrib,T,rat.one_mul]
theorem rat_power_two_le (k : ℕ+) : rat_of_pnat k ≤ 2^k~ :=

2
library/data/prod.lean
View file

@ -37,6 +37,6 @@ namespace prod
theorem eq_of_swap_eq {A : Type} : ∀ p₁ p₂ : A × A, swap p₁ = swap p₂ → p₁ = p₂ :=
take p₁ p₂, assume seqs,
assert swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs,
have swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs,
by rewrite *swap_swap at this; exact this
end prod

10
library/data/rat/basic.lean
View file

@ -39,8 +39,8 @@ have num b * denom a > 0, from H ▸ this,
show num b > 0, from pos_of_mul_pos_right this (le_of_lt (denom_pos a))
theorem num_neg_of_equiv {a b : prerat} (H : a ≡ b) (na_neg : num a < 0) : num b < 0 :=
assert H₁ : num a * denom b = num b * denom a, from H,
assert num a * denom b < 0, from mul_neg_of_neg_of_pos na_neg (denom_pos b),
have H₁ : num a * denom b = num b * denom a, from H,
have num a * denom b < 0, from mul_neg_of_neg_of_pos na_neg (denom_pos b),
have -(-num b * denom a) < 0, begin rewrite [neg_mul_eq_neg_mul, neg_neg, -H₁], exact this end,
have -num b > 0, from pos_of_mul_pos_right (pos_of_neg_neg this) (le_of_lt (denom_pos a)),
neg_of_neg_pos this
@ -314,11 +314,11 @@ theorem reduce_eq_reduce : ∀ {a b : prerat}, a ≡ b → reduce a = reduce b
decidable.by_cases
(assume anz : an = 0,
have H' : bn * ad = 0, by rewrite [-H, anz, zero_mul],
assert bnz : bn = 0,
have bnz : bn = 0,
from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos),
by rewrite [↑reduce, if_pos anz, if_pos bnz])
(assume annz : an ≠ 0,
assert bnnz : bn ≠ 0, from
have bnnz : bn ≠ 0, from
assume bnz,
have H' : an * bd = 0, by rewrite [H, bnz, zero_mul],
have anz : an = 0,
@ -541,7 +541,7 @@ decidable.by_cases
(suppose a = 0, by substvars)
(quot.induction_on a
(take u H,
assert H' : prerat.num u ≠ 0, from take H'', H (quot.sound (prerat.equiv_zero_of_num_eq_zero H'')),
have H' : prerat.num u ≠ 0, from take H'', H (quot.sound (prerat.equiv_zero_of_num_eq_zero H'')),
begin
cases u with un ud udpos,
rewrite [▸*, ↑num, ↑denom, ↑reduce, ↑prerat.reduce, if_neg H', ▸*],

10
library/data/rat/order.lean
View file

@ -205,7 +205,7 @@ protected theorem le_refl (a : ℚ) : a ≤ a :=
by rewrite [rat.le_def, sub_self]; apply nonneg_zero
protected theorem le_trans (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
assert H3 : nonneg (c - b + (b - a)), from nonneg_add H2 H1,
have H3 : nonneg (c - b + (b - a)), from nonneg_add H2 H1,
begin
revert H3,
rewrite [rat.sub.def, add.assoc, sub_eq_add_neg, neg_add_cancel_left],
@ -256,14 +256,14 @@ have c + b - (c + a) = b - a,
show nonneg (c + b - (c + a)), from this⁻¹ ▸ H
protected theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
assert nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
have nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
begin rewrite -sub_zero at this, exact this end
private theorem to_pos : a > 0 → pos a :=
by intros; rewrite -sub_zero; eassumption
protected theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
assert pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
have pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
begin rewrite -sub_zero at this, exact this end
definition decidable_lt [instance] : decidable_rel rat.lt :=
@ -322,7 +322,7 @@ protected definition discrete_linear_ordered_field [trans_instance] :
add_lt_add_left := @rat.add_lt_add_left⦄
theorem of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
assert ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
have ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
int.induction_on a
(take b, abs_of_nonneg !of_nat_nonneg)
(take b, by rewrite [this, abs_neg, abs_of_nonneg !of_nat_nonneg])
@ -407,7 +407,7 @@ definition ubound : ℚ → ℕ := λ a : ℚ, nat.succ (int.nat_abs (num a))
theorem ubound_ge (a : ℚ) : of_nat (ubound a) ≥ a :=
have h : abs a * abs (of_int (denom a)) = abs (of_int (num a)), from
!abs_mul ▸ !mul_denom ▸ rfl,
assert of_int (denom a) > 0, from of_int_lt_of_int_of_lt !denom_pos,
have of_int (denom a) > 0, from of_int_lt_of_int_of_lt !denom_pos,
have 1 ≤ abs (of_int (denom a)), begin
rewrite (abs_of_pos this),
apply of_int_le_of_int_of_le,

12
library/data/real/basic.lean
View file

@ -102,7 +102,7 @@ end
private theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹)
(H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) :
(rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ :=
assert H3 : (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹ = (2 * k)⁻¹ * (m⁻¹ + n⁻¹),
have H3 : (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹ = (2 * k)⁻¹ * (m⁻¹ + n⁻¹),
begin
rewrite [left_distrib, *pnat.inv_mul_eq_mul_inv],
rewrite (mul.comm k⁻¹)
@ -304,15 +304,15 @@ definition K₂ (s t : seq) := max (K s) (K t)
private theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
if H : K s < K t then
(assert H1 : K₂ s t = K t, from pnat.max_eq_right H,
assert H2 : K₂ t s = K t, from pnat.max_eq_left (pnat.not_lt_of_ge (pnat.le_of_lt H)),
(have H1 : K₂ s t = K t, from pnat.max_eq_right H,
have H2 : K₂ t s = K t, from pnat.max_eq_left (pnat.not_lt_of_ge (pnat.le_of_lt H)),
by rewrite [H1, -H2])
else
(assert H1 : K₂ s t = K s, from pnat.max_eq_left H,
(have H1 : K₂ s t = K s, from pnat.max_eq_left H,
if J : K t < K s then
(assert H2 : K₂ t s = K s, from pnat.max_eq_right J, by rewrite [H1, -H2])
(have H2 : K₂ t s = K s, from pnat.max_eq_right J, by rewrite [H1, -H2])
else
(assert Heq : K t = K s, from
(have Heq : K t = K s, from
pnat.eq_of_le_of_ge (pnat.le_of_not_gt H) (pnat.le_of_not_gt J),
by rewrite [↑K₂, Heq]))

2
library/data/real/complete.lean
View file

@ -558,7 +558,7 @@ open nat
theorem archimedean_small {ε : ℝ} (H : ε > 0) : ∃ (n : ℕ), 1 / succ n < ε :=
let n := int.nat_abs (ceil (2 / ε)) in
assert int.of_nat n ≥ ceil (2 / ε),
have int.of_nat n ≥ ceil (2 / ε),
by rewrite of_nat_nat_abs; apply le_abs_self,
have int.of_nat (succ n) ≥ ceil (2 / ε),
begin apply le.trans, exact this, apply int.of_nat_le_of_nat_of_le, apply le_succ end,

10
library/data/real/division.lean
View file

@ -422,10 +422,10 @@ theorem inv_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s
apply one_is_reg
end)
else
(assert H : s_inv Hs = zero, from funext (λ n, dif_neg Hsep),
(have H : s_inv Hs = zero, from funext (λ n, dif_neg Hsep),
have Hsept : ¬ sep t zero, from
assume H', Hsep (sep_of_equiv_sep Ht Hs (equiv.symm _ _ Heq) H'),
assert H' : s_inv Ht = zero, from funext (λ n, dif_neg Hsept),
have H' : s_inv Ht = zero, from funext (λ n, dif_neg Hsept),
by rewrite [H', H]; apply equiv.refl)
theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
@ -545,7 +545,7 @@ theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (
noncomputable definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s))
(if H : sep (reg_seq.sq s) zero then reg_inv_reg (reg_seq.is_reg s) H else
assert Hz : s_inv (reg_seq.is_reg s) = zero, from funext (λ n, dif_neg H),
have Hz : s_inv (reg_seq.is_reg s) = zero, from funext (λ n, dif_neg H),
by rewrite Hz; apply zero_is_reg)
theorem r_inv_zero : requiv (r_inv r_zero) r_zero :=
@ -680,8 +680,8 @@ theorem eq_zero_of_nonneg_of_forall_le {x : ℝ} (xnonneg : x ≥ 0) (H : ∀ ε
x = 0 :=
have ∀ ε : ℝ, ε > 0 → x < ε, from
take ε, suppose ε > 0,
assert e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos,
assert ε / 2 < ε, from div_two_lt_of_pos `ε > 0`,
have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos,
have ε / 2 < ε, from div_two_lt_of_pos `ε > 0`,
begin apply lt_of_le_of_lt, apply H _ e2pos, apply this end,
eq_zero_of_nonneg_of_forall_lt xnonneg this

4
library/data/set/card.lean
View file

@ -27,7 +27,7 @@ theorem card_insert_of_mem {a : A} {s : set A} (H : a ∈ s) : card (insert a s)
if fins : finite s then
(by rewrite [↑card, to_finset_insert, -mem_to_finset_eq at H, finset.card_insert_of_mem H])
else
(assert ¬ finite (insert a s), from suppose _, absurd (!finite_of_finite_insert this) fins,
(have ¬ finite (insert a s), from suppose _, absurd (!finite_of_finite_insert this) fins,
by rewrite [card_of_not_finite fins, card_of_not_finite this])
theorem card_insert_of_not_mem {a : A} {s : set A} [finite s] (H : a ∉ s) :
@ -142,7 +142,7 @@ begin
end
theorem exists_two_of_card_gt_one {s : set A} (H : 1 < card s) : ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
assert fins : finite s, from
have fins : finite s, from
by_contradiction
(assume nfins, by rewrite [card_of_not_finite nfins at H]; apply !not_succ_le_zero H),
by rewrite [-to_set_to_finset s]; apply finset.exists_two_of_card_gt_one H

2
library/data/set/filter.lean
View file

@ -201,7 +201,7 @@ namespace complete_lattice
λ a b Ha Hb,
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha,
obtain b₁ [b₁F₁ [b₂ [b₂F₂ (Hb' : b ⊇ b₁ ∩ b₂)]]], from Hb,
assert a₁ ∩ b₁ ∩ (a₂ ∩ b₂) = a₁ ∩ a₂ ∩ (b₁ ∩ b₂),
have a₁ ∩ b₁ ∩ (a₂ ∩ b₂) = a₁ ∩ a₂ ∩ (b₁ ∩ b₂),
by rewrite [*inter_assoc, inter_left_comm b₁],
have a ∩ b ⊇ a₁ ∩ b₁ ∩ (a₂ ∩ b₂),
begin

10
library/data/set/finite.lean
View file

@ -168,14 +168,14 @@ theorem finite_iff_finite_of_bij_on {B : Type} {f : A → B} {s : set A} {t : se
iff.intro (assume fs, finite_of_bij_on bijf) (assume ft, finite_of_bij_on' bijf)
theorem finite_powerset (s : set A) [finite s] : finite 𝒫 s :=
assert H : 𝒫 s = finset.to_set ' (finset.to_set (#finset 𝒫 (to_finset s))),
have H : 𝒫 s = finset.to_set ' (finset.to_set (#finset 𝒫 (to_finset s))),
from ext (take t, iff.intro
(suppose t ∈ 𝒫 s,
assert t ⊆ s, from this,
assert finite t, from finite_subset this,
assert (#finset to_finset t ∈ 𝒫 (to_finset s)),
have t ⊆ s, from this,
have finite t, from finite_subset this,
have (#finset to_finset t ∈ 𝒫 (to_finset s)),
by rewrite [finset.mem_powerset_iff_subset, to_finset_subset_to_finset_eq]; apply `t ⊆ s`,
assert to_finset t ∈ (finset.to_set (finset.powerset (to_finset s))), from this,
have to_finset t ∈ (finset.to_set (finset.powerset (to_finset s))), from this,
mem_image this (by rewrite to_set_to_finset))
(assume H',
obtain t' [(tmem : (#finset t' ∈ 𝒫 (to_finset s))) (teq : finset.to_set t' = t)],

4
library/data/stream.lean
View file

@ -634,7 +634,7 @@ obtain (i₁ : nat) hlt₁ he₁, from h₁,
obtain (i₂ : nat) hlt₂ he₂, from h₂,
lt.by_cases
(λ i₁lti₂ : i₁ < i₂,
assert aux : nth i₁ s₂ = nth i₁ s₃, from he₂ _ i₁lti₂,
have aux : nth i₁ s₂ = nth i₁ s₃, from he₂ _ i₁lti₂,
begin
existsi i₁, split,
{rewrite -aux, exact hlt₁},
@ -650,7 +650,7 @@ lt.by_cases
exact !he₂ jlti₁
end)
(λ i₂lti₁ : i₂ < i₁,
assert nth i₂ s₁ = nth i₂ s₂, from he₁ _ i₂lti₁,
have nth i₂ s₁ = nth i₂ s₂, from he₁ _ i₂lti₁,
begin
existsi i₂, split,
{rewrite this, exact hlt₂},

4
library/init/simplifier.lean
View file

@ -75,12 +75,12 @@ iff.intro (assume H, and.intro (assume a, implies_of_if_pos H a)
(assume H, and.rec_on H
(assume Hab Hnac, decidable.rec_on A_dec
(assume a,
assert rw : @decidable.inl A a = A_dec, from
have rw : @decidable.inl A a = A_dec, from
subsingleton.rec_on (subsingleton_decidable A)
(assume H, H (@decidable.inl A a) A_dec),
by rewrite [rw, if_pos a] ; exact Hab a)
(assume na,
assert rw : @decidable.inr A na = A_dec, from
have rw : @decidable.inr A na = A_dec, from
subsingleton.rec_on (subsingleton_decidable A)
(assume H, H (@decidable.inr A na) A_dec),
by rewrite [rw, if_neg na] ; exact Hnac na)))

8
library/logic/examples/colog88.lean
View file

@ -42,7 +42,7 @@ lemma betaA (p : Phi A) : matchA (introA p) = p :=
-- As in all inductive datatypes, we would be able to prove that constructors are injective.
lemma introA_injective : ∀ {p p' : Phi A}, introA p = introA p' → p = p' :=
λ p p' h,
assert aux : matchA (introA p) = matchA (introA p'), by rewrite h,
have aux : matchA (introA p) = matchA (introA p'), by rewrite h,
by rewrite [*betaA at aux]; exact aux
-- For any type T, there is an injection from T to (T → Prop)
@ -80,9 +80,9 @@ rfl
lemma not_P0_x0 : ¬ P0 x0 :=
λ h : P0 x0,
obtain (P : A → Prop) (hp : f P = x0 ∧ ¬ P x0), from h,
have fp_eq : f P = f P0, from and.elim_left hp,
assert p_eq : P = P0, from f_injective fp_eq,
have nh : ¬ P0 x0, by rewrite [p_eq at hp]; exact (and.elim_right hp),
have fp_eq : f P = f P0, from and.elim_left hp,
have p_eq : P = P0, from f_injective fp_eq,
have nh : ¬ P0 x0, by rewrite [p_eq at hp]; exact (and.elim_right hp),
absurd h nh
lemma P0_x0 : P0 x0 :=

10
library/logic/examples/cont.lean
View file

@ -58,12 +58,12 @@ lemma β0_eq (β : nat → nat) : ∀ α, zω =[f β] α → β 0 = β (α m) :=
lemma not_all_continuous : false :=
let β := znkω (M f + 1) 1 in
let α := znkω m (M f + 1) in
assert βeq₁ : zω =[M f + 1] β, from
have βeq₁ : zω =[M f + 1] β, from
λ (a : nat) (h : a < M f + 1), begin unfold zω, unfold znkω, rewrite [if_pos h] end,
assert βeq₂ : zω =[M f] β, from pred_beq βeq₁,
assert m_eq_fβ : m = f β, from M_spec f β βeq₂,
assert aux : ∀ α, zω =[m] α → β 0 = β (α m), by rewrite m_eq_fβ at {1}; exact (β0_eq β),
assert zero_eq_one : 0 = 1, from calc
have βeq₂ : zω =[M f] β, from pred_beq βeq₁,
have m_eq_fβ : m = f β, from M_spec f β βeq₂,
have aux : ∀ α, zω =[m] α → β 0 = β (α m), by rewrite m_eq_fβ at {1}; exact (β0_eq β),
have zero_eq_one : 0 = 1, from calc
0 = β 0 : by rewrite znkω_succ
... = β (α m) : aux α (zω_eq_znkω m (M f + 1))
... = β (M f + 1) : by rewrite znkω_bound

4
library/logic/examples/leftinv_of_inj.lean
View file

@ -20,8 +20,8 @@ assume inj : ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂,
let finv : B → A := mk_left_inv f in
have linv : left_inverse finv f, from
λ a,
assert ex : ∃ a₁ : A, f a₁ = f a, from exists.intro a rfl,
assert h₁ : f (some ex) = f a, from !some_spec,
have ex : ∃ a₁ : A, f a₁ = f a, from exists.intro a rfl,
have h₁ : f (some ex) = f a, from !some_spec,
begin
esimp [mk_left_inv, compose, id],
rewrite [dif_pos ex],

8
library/logic/examples/propositional/soundness.lean
View file

@ -123,13 +123,13 @@ namespace PropF
have aux : bnot (TrueQ v A) = tt, by rewrite (eq_ff_of_ne_tt f),
bor_inl aux))
(λ Γ A B H₁ H₂ r₁ r₂ v s,
assert aux₁ : bnot (TrueQ v A) || TrueQ v B = tt, from r₁ v s,
assert aux₂ : TrueQ v A = tt, from r₂ v s,
have aux₁ : bnot (TrueQ v A) || TrueQ v B = tt, from r₁ v s,
have aux₂ : TrueQ v A = tt, from r₂ v s,
by rewrite [aux₂ at aux₁, bnot_true at aux₁, ff_bor at aux₁]; exact aux₁)
(λ Γ A H r v s, by_contradiction
(λ n : TrueQ v A ≠ tt,
assert aux₁ : TrueQ v A = ff, from eq_ff_of_ne_tt n,
assert aux₂ : TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), rewrite aux₁ end,
have aux₁ : TrueQ v A = ff, from eq_ff_of_ne_tt n,
have aux₂ : TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), rewrite aux₁ end,
have aux₃ : Satisfies v ((~A)::Γ), from Satisfies_cons s aux₂,
have aux₄ : TrueQ v ⊥ = tt, from r v aux₃,
absurd aux₄ ff_ne_tt))

8
library/logic/examples/propositional/soundness_type.lean
View file

@ -129,13 +129,13 @@ namespace PropF
have aux : bnot (TrueQ v A) = tt, by rewrite (eq_ff_of_ne_tt f),
bor_inl aux)
| ⌞B⌟ Γ (ImpE Γ A B H₁ H₂) s :=
assert aux₁ : bnot (TrueQ v A) || TrueQ v B = tt, from Soundness_general H₁ s,
assert aux₂ : TrueQ v A = tt, from Soundness_general H₂ s,
have aux₁ : bnot (TrueQ v A) || TrueQ v B = tt, from Soundness_general H₁ s,
have aux₂ : TrueQ v A = tt, from Soundness_general H₂ s,
by rewrite [aux₂ at aux₁, bnot_true at aux₁, ff_bor at aux₁]; exact aux₁
| ⌞A⌟ Γ (BotC Γ A H) s := by_contradiction
(λ n : TrueQ v A ≠ tt,
assert aux₁ : TrueQ v A = ff, from eq_ff_of_ne_tt n,
assert aux₂ : TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), rewrite aux₁ end,
have aux₁ : TrueQ v A = ff, from eq_ff_of_ne_tt n,
have aux₂ : TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), rewrite aux₁ end,
have aux₃ : Satisfies v ((~A)::Γ), from Satisfies_cons s aux₂,
have aux₄ : TrueQ v ⊥ = tt, from Soundness_general H aux₃,
absurd aux₄ ff_ne_tt)

4
library/logic/weak_fan.lean
View file

@ -53,7 +53,7 @@ private lemma Y_unique : ∀ {P l₁ l₂}, length l₁ = length l₂ → Y P l
have n₁ : length l₁ = length l₂, by rewrite [*length_cons at h₁]; apply nat.add_right_cancel h₁,
have n₂ : Y P l₁, from and.elim_left h₂,
have n₃ : Y P l₂, from and.elim_left h₃,
assert ih : l₁ = l₂, from Y_unique n₁ n₂ n₃,
have ih : l₁ = l₂, from Y_unique n₁ n₂ n₃,
begin
clear Y_unique, subst l₂, congruence,
show a₁ = a₂,
@ -94,7 +94,7 @@ private lemma Y_approx : ∀ {P l}, approx (X P) l → Y P l
theorem weak_fan : ∀ {P}, barred P → inductively_barred P [] :=
λ P Hbar,
obtain l Hd HP, from Hbar (X P),
assert ib : inductively_barred P l, from inductively_barred.base l HP,
have ib : inductively_barred P l, from inductively_barred.base l HP,
begin
clear Hbar HP,
induction l with a l ih,

4
library/theories/analysis/inner_product.lean
View file

@ -212,8 +212,8 @@ theorem cauchy_schwartz' (u v : V) : ⟨u, v⟩ ≤ ∥ u ∥ * ∥ v ∥ := ip_
theorem eq_proj_on_cauchy_schwartz {u v : V} (H : v ≠ 0) (H₁ : abs ⟨u, v⟩ = ∥ u ∥ * ∥ v ∥) :
u = proj_on u H :=
assert ∥ v ∥ ≠ 0, from assume H', H (eq_zero_of_norm_eq_zero H'),
assert ∥ u ∥ = ∥ proj_on u H ∥, by rewrite [norm_proj_on_eq, H₁, mul_div_cancel _ this],
have ∥ v ∥ ≠ 0, from assume H', H (eq_zero_of_norm_eq_zero H'),
have ∥ u ∥ = ∥ proj_on u H ∥, by rewrite [norm_proj_on_eq, H₁, mul_div_cancel _ this],
have ∥ u - proj_on u H ∥^2 + ∥ u ∥^2 = 0 + ∥ u ∥^2,
by rewrite [zero_add, norm_squared_pythagorean u H at {2}, this],
have ∥ u - proj_on u H ∥^2 = 0, from eq_of_add_eq_add_right this,

8
library/theories/analysis/real_limit.lean
View file

@ -529,16 +529,16 @@ let aX := (λ n, (abs x)^n),
have noninc_aX : nonincreasing aX, from
nonincreasing_of_forall_succ_le
(take i,
assert (abs x) * (abs x)^i ≤ 1 * (abs x)^i,
have (abs x) * (abs x)^i ≤ 1 * (abs x)^i,
from mul_le_mul_of_nonneg_right (le_of_lt H) (!pow_nonneg_of_nonneg !abs_nonneg),
assert (abs x) * (abs x)^i ≤ (abs x)^i, by krewrite one_mul at this; exact this,
have (abs x) * (abs x)^i ≤ (abs x)^i, by krewrite one_mul at this; exact this,
show (abs x) ^ (succ i) ≤ (abs x)^i, by rewrite pow_succ; apply this),
have bdd_aX : ∀ i, 0 ≤ aX i, from take i, !pow_nonneg_of_nonneg !abs_nonneg,
assert aXconv : aX ⟶ iaX in ℕ, proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed,
have aXconv : aX ⟶ iaX in ℕ, proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed,
have asXconv : asX ⟶ iaX in ℕ, from converges_to_seq_offset_succ aXconv,
have asXconv' : asX ⟶ (abs x) * iaX in ℕ, from mul_left_converges_to_seq (abs x) aXconv,
have iaX = (abs x) * iaX, from converges_to_seq_unique asXconv asXconv',
assert iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this),
have iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this),
show aX ⟶ 0 in ℕ, begin rewrite -this, exact aXconv end --from this ▸ aXconv
end xn

26
library/theories/combinatorics/choose.lean
View file

@ -36,7 +36,7 @@ nat.induction_on n
take k,
suppose succ n' < k,
obtain k' (keq : k = succ k'), from exists_eq_succ_of_lt this,
assert n' < k', by rewrite keq at this; apply lt_of_succ_lt_succ this,
have n' < k', by rewrite keq at this; apply lt_of_succ_lt_succ this,
by rewrite [keq, choose_succ_succ, IH _ this, IH _ (lt.trans this !lt_succ_self)])
theorem choose_self (n : ℕ) : choose n n = 1 :=
@ -71,7 +71,7 @@ begin
cases k with k,
{intros, rewrite [choose_zero_right], apply zero_lt_one},
suppose succ k ≤ succ n,
assert k ≤ n, from le_of_succ_le_succ this,
have k ≤ n, from le_of_succ_le_succ this,
by rewrite [choose_succ_succ]; apply add_pos_right (ih this)
end
@ -129,16 +129,16 @@ include deceqA
private theorem aux₀ (s : finset A) : {t ∈ powerset s | card t = 0} = '{∅} :=
ext (take t, iff.intro
(assume H,
assert t = ∅, from eq_empty_of_card_eq_zero (of_mem_sep H),
have t = ∅, from eq_empty_of_card_eq_zero (of_mem_sep H),
show t ∈ '{ ∅ }, by rewrite [this, mem_singleton_iff])
(assume H,
assert t = ∅, by rewrite mem_singleton_iff at H; assumption,
have t = ∅, by rewrite mem_singleton_iff at H; assumption,
by substvars; exact mem_sep_of_mem !empty_mem_powerset rfl))
private theorem aux₁ (k : ℕ) : {t ∈ powerset (∅ : finset A) | card t = succ k} = ∅ :=
eq_empty_of_forall_not_mem (take t, assume H,
assert t ∈ powerset ∅, from mem_of_mem_sep H,
assert t = ∅, by rewrite [powerset_empty at this, mem_singleton_iff at this]; assumption,
have t ∈ powerset ∅, from mem_of_mem_sep H,
have t = ∅, by rewrite [powerset_empty at this, mem_singleton_iff at this]; assumption,
have card (∅ : finset A) = succ k, by rewrite -this; apply of_mem_sep H,
nat.no_confusion this)
@ -154,18 +154,18 @@ iff.intro
(assume H,
obtain H' cardt, from H,
obtain t' [(t'pows : t' ∈ powerset s) (teq : insert a t' = t)], from exists_of_mem_image H',
assert aint : a ∈ t, by rewrite -teq; apply mem_insert,
assert anint' : a ∉ t', from
have aint : a ∈ t, by rewrite -teq; apply mem_insert,
have anint' : a ∉ t', from
(assume aint',
have a ∈ s, from mem_of_subset_of_mem (subset_of_mem_powerset t'pows) aint',
anins this),
assert t' = erase a t, by rewrite [-teq, erase_insert (aux₂ anins t'pows)],
have t' = erase a t, by rewrite [-teq, erase_insert (aux₂ anins t'pows)],
have card t' = k, by rewrite [this, card_erase_of_mem aint, cardt],
mem_image (mem_sep_of_mem t'pows this) teq)
(assume H,
obtain t' [Ht' (teq : insert a t' = t)], from exists_of_mem_image H,
assert t'pows : t' ∈ powerset s, from mem_of_mem_sep Ht',
assert cardt' : card t' = k, from of_mem_sep Ht',
have t'pows : t' ∈ powerset s, from mem_of_mem_sep Ht',
have cardt' : card t' = k, from of_mem_sep Ht',
and.intro
(show t ∈ (insert a) ' (powerset s), from mem_image t'pows teq)
(show card t = succ k,
@ -196,9 +196,9 @@ have set.inj_on (insert a) (ts {t ∈ powerset s| card t = k}), from
take t₁ t₂, assume Ht₁ Ht₂,
assume Heq : insert a t₁ = insert a t₂,
have t₁ ∈ powerset s, from mem_of_mem_sep Ht₁,
assert anint₁ : a ∉ t₁, from aux₂ anins this,
have anint₁ : a ∉ t₁, from aux₂ anins this,
have t₂ ∈ powerset s, from mem_of_mem_sep Ht₂,
assert anint₂ : a ∉ t₂, from aux₂ anins this,
have anint₂ : a ∉ t₂, from aux₂ anins this,
calc
t₁ = erase a (insert a t₁) : by rewrite (erase_insert anint₁)
... = erase a (insert a t₂) : Heq

50
library/theories/group_theory/action.lean
View file

@ -51,7 +51,7 @@ lemma exists_of_orbit {b : S} : b ∈ orbit hom H a → ∃ h, h ∈ H ∧ hom h
assume Pb,
obtain p (Pp₁ : p ∈ image hom H) (Pp₂ : move_by a p = b), from exists_of_mem_image Pb,
obtain h (Ph₁ : h ∈ H) (Ph₂ : hom h = p), from exists_of_mem_image Pp₁,
assert Phab : hom h a = b, from calc
have Phab : hom h a = b, from calc
hom h a = p a : Ph₂
... = b : Pp₂,
exists.intro h (and.intro Ph₁ Phab)
@ -111,7 +111,7 @@ rfl
lemma stab_lmul {f g : G} : g ∈ stab hom H a → hom (f*g) a = hom f a :=
assume Pgstab,
assert hom g a = a, from of_mem_sep Pgstab, calc
have hom g a = a, from of_mem_sep Pgstab, calc
hom (f*g) a = perm.f ((hom f) * (hom g)) a : is_hom hom
... = ((hom f) ∘ (hom g)) a : by rewrite perm_f_mul
... = (hom f) a : by unfold compose; rewrite this
@ -123,7 +123,7 @@ lemma stab_subset : stab hom H a ⊆ H :=
lemma reverse_move {h g : G} : g ∈ moverset hom H a (hom h a) → hom (h⁻¹*g) a = a :=
assume Pg,
assert hom g a = hom h a, from of_mem_sep Pg, calc
have hom g a = hom h a, from of_mem_sep Pg, calc
hom (h⁻¹*g) a = perm.f ((hom h⁻¹) * (hom g)) a : by rewrite (is_hom hom)
... = ((hom h⁻¹) ∘ hom g) a : by rewrite perm_f_mul
... = perm.f ((hom h)⁻¹ * hom h) a : by unfold compose; rewrite [this, perm_f_mul, hom_map_inv hom h]
@ -133,7 +133,7 @@ assert hom g a = hom h a, from of_mem_sep Pg, calc
lemma moverset_inj_on_orbit : set.inj_on (moverset hom H a) (ts (orbit hom H a)) :=
take b1 b2,
assume Pb1, obtain h1 Ph1₁ Ph1₂, from exists_of_orbit Pb1,
assert Ph1b1 : h1 ∈ moverset hom H a b1,
have Ph1b1 : h1 ∈ moverset hom H a b1,
from mem_sep_of_mem Ph1₁ Ph1₂,
assume Psetb2 Pmeq, begin
subst b1,
@ -147,7 +147,7 @@ include finsubgH
lemma subg_stab_of_move {h g : G} :
h ∈ H → g ∈ moverset hom H a (hom h a) → h⁻¹*g ∈ stab hom H a :=
assume Ph Pg,
assert Phinvg : h⁻¹*g ∈ H, from begin
have Phinvg : h⁻¹*g ∈ H, from begin
apply finsubg_mul_closed H,
apply finsubg_has_inv H, assumption,
apply mem_of_mem_sep Pg
@ -155,31 +155,31 @@ lemma subg_stab_of_move {h g : G} :
mem_sep_of_mem Phinvg (reverse_move Pg)
lemma subg_stab_closed : finset_mul_closed_on (stab hom H a) :=
take f g, assume Pfstab, assert Pf : hom f a = a, from of_mem_sep Pfstab,
take f g, assume Pfstab, have Pf : hom f a = a, from of_mem_sep Pfstab,
assume Pgstab,
assert Pfg : hom (f*g) a = a, from calc
have Pfg : hom (f*g) a = a, from calc
hom (f*g) a = (hom f) a : stab_lmul Pgstab
... = a : Pf,
assert PfginH : (f*g) ∈ H,
have PfginH : (f*g) ∈ H,
from finsubg_mul_closed H (mem_of_mem_sep Pfstab) (mem_of_mem_sep Pgstab),
mem_sep_of_mem PfginH Pfg
lemma subg_stab_has_one : 1 ∈ stab hom H a :=
assert P : hom 1 a = a, from calc
have P : hom 1 a = a, from calc
hom 1 a = perm.f (1 : perm S) a : {hom_map_one hom}
... = a : rfl,
assert PoneinH : 1 ∈ H, from finsubg_has_one H,
have PoneinH : 1 ∈ H, from finsubg_has_one H,
mem_sep_of_mem PoneinH P
lemma subg_stab_has_inv : finset_has_inv (stab hom H a) :=
take f, assume Pfstab, assert Pf : hom f a = a, from of_mem_sep Pfstab,
assert Pfinv : hom f⁻¹ a = a, from calc
take f, assume Pfstab, have Pf : hom f a = a, from of_mem_sep Pfstab,
have Pfinv : hom f⁻¹ a = a, from calc
hom f⁻¹ a = hom f⁻¹ ((hom f) a) : by rewrite Pf
... = perm.f ((hom f⁻¹) * (hom f)) a : by rewrite perm_f_mul
... = hom (f⁻¹ * f) a : by rewrite (is_hom hom)
... = hom 1 a : by rewrite mul.left_inv
... = perm.f (1 : perm S) a : by rewrite (hom_map_one hom),
assert PfinvinH : f⁻¹ ∈ H, from finsubg_has_inv H (mem_of_mem_sep Pfstab),
have PfinvinH : f⁻¹ ∈ H, from finsubg_has_inv H (mem_of_mem_sep Pfstab),
mem_sep_of_mem PfinvinH Pfinv
definition subg_stab_is_finsubg [instance] :
@ -190,14 +190,14 @@ lemma subg_lcoset_eq_moverset {h : G} :
h ∈ H → fin_lcoset (stab hom H a) h = moverset hom H a (hom h a) :=
assume Ph, ext (take g, iff.intro
(assume Pl, obtain f (Pf₁ : f ∈ stab hom H a) (Pf₂ : h*f = g), from exists_of_mem_image Pl,
assert Pfstab : hom f a = a, from of_mem_sep Pf₁,
assert PginH : g ∈ H, begin
have Pfstab : hom f a = a, from of_mem_sep Pf₁,
have PginH : g ∈ H, begin
subst Pf₂,
apply finsubg_mul_closed H,
assumption,
apply mem_of_mem_sep Pf₁
end,
assert Pga : hom g a = hom h a, from calc
have Pga : hom g a = hom h a, from calc
hom g a = hom (h*f) a : by subst g
... = hom h a : stab_lmul Pf₁,
mem_sep_of_mem PginH Pga)
@ -214,7 +214,7 @@ lemma subg_moverset_of_orbit_is_lcoset_of_stab (b : S) :
assume Porb,
obtain p (Pp₁ : p ∈ image hom H) (Pp₂ : move_by a p = b), from exists_of_mem_image Porb,
obtain h (Ph₁ : h ∈ H) (Ph₂ : hom h = p), from exists_of_mem_image Pp₁,
assert Phab : hom h a = b, from by subst p; assumption,
have Phab : hom h a = b, from by subst p; assumption,
exists.intro h (and.intro Ph₁ (Phab ▸ subg_lcoset_eq_moverset Ph₁))
lemma subg_lcoset_of_stab_is_moverset_of_orbit (h : G) :
@ -270,8 +270,8 @@ orbit_of_exists (exists.intro (h*g) (and.intro
lemma in_orbit_symm {a b : S} : a ∈ orbit hom H b → b ∈ orbit hom H a :=
assume Painb, obtain h PhinH Phba, from exists_of_orbit Painb,
assert perm.f (hom h)⁻¹ a = b, by rewrite [-Phba, -perm_f_mul, mul.left_inv],
assert (hom h⁻¹) a = b, by rewrite [hom_map_inv, this],
have perm.f (hom h)⁻¹ a = b, by rewrite [-Phba, -perm_f_mul, mul.left_inv],
have (hom h⁻¹) a = b, by rewrite [hom_map_inv, this],
orbit_of_exists (exists.intro h⁻¹ (and.intro (finsubg_has_inv H PhinH) this))
lemma orbit_is_partition : is_partition (orbit hom H) :=
@ -422,7 +422,7 @@ lemma aol_fixed_point_subset_normalizer (J : lcoset_type univ H) :
is_fixed_point (action_on_lcoset H) H J → elt_of J ⊆ normalizer H :=
obtain j Pjin Pj, from exists_of_lcoset_type J,
assume Pfp,
assert PH : ∀ {h}, h ∈ H → fin_lcoset (fin_lcoset H j) h = fin_lcoset H j,
have PH : ∀ {h}, h ∈ H → fin_lcoset (fin_lcoset H j) h = fin_lcoset H j,
from take h, assume Ph, by rewrite [Pj, -action_on_lcoset_eq, Pfp h Ph],
subset_of_forall take g, begin
rewrite [-Pj, fin_lcoset_same, -inv_inv at {2}],
@ -431,7 +431,7 @@ subset_of_forall take g, begin
apply finsubg_has_inv,
apply mem_sep_of_mem !mem_univ,
intro h Ph,
assert Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, exact PH Ph,
have Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, exact PH Ph,
revert Phg,
rewrite [↑conj_by, inv_inv, mul.assoc, fin_lcoset_compose, -fin_lcoset_same, ↑fin_lcoset, mem_image_iff, ↑lmul_by],
intro Pex, cases Pex with k Pand, cases Pand with Pkin Pk,
@ -494,8 +494,8 @@ lemma lift_lower_eq : ∀ {p : perm (fin (succ n))} (P : p maxi = maxi),
| (perm.mk pf Pinj) := assume Pmax, begin
rewrite [↑lift_perm], congruence,
apply funext, intro i,
assert Pfmax : pf maxi = maxi, apply Pmax,
assert Pd : decidable (i = maxi),
have Pfmax : pf maxi = maxi, apply Pmax,
have Pd : decidable (i = maxi),
exact _,
cases Pd with Pe Pne,
rewrite [Pe, Pfmax], apply lift_fun_max,
@ -513,13 +513,13 @@ eq.symm to_set_univ ▸ iff.elim_left set.injective_iff_inj_on_univ lift_perm_in
lemma lift_to_stab : image (@lift_perm n) univ = stab id univ maxi :=
ext (take (pp : perm (fin (succ n))), iff.intro
(assume Pimg, obtain p P_ Pp, from exists_of_mem_image Pimg,
assert Ppp : pp maxi = maxi, from calc
have Ppp : pp maxi = maxi, from calc
pp maxi = lift_perm p maxi : {eq.symm Pp}
... = lift_fun p maxi : rfl
... = maxi : lift_fun_max,
mem_sep_of_mem !mem_univ Ppp)
(assume Pstab,
assert Ppp : pp maxi = maxi, from of_mem_sep Pstab,
have Ppp : pp maxi = maxi, from of_mem_sep Pstab,
mem_image !mem_univ (lift_lower_eq Ppp)))
definition move_from_max_to (i : fin (succ n)) : perm (fin (succ n)) :=

20
library/theories/group_theory/cyclic.lean
View file

@ -22,7 +22,7 @@ include ambG
lemma pow_mod {a : A} {n m : nat} : a ^ m = 1 → a ^ n = a ^ (n % m) :=
assume Pid,
assert a ^ (n / m * m) = 1, from calc
have a ^ (n / m * m) = 1, from calc
a ^ (n / m * m) = a ^ (m * (n / m)) : by rewrite (mul.comm (n / m) m)
... = (a ^ m) ^ (n / m) : by rewrite pow_mul
... = 1 ^ (n / m) : by rewrite Pid
@ -64,13 +64,13 @@ include deceqA
lemma exists_pow_eq_one (a : A) : ∃ n, n < card A ∧ a ^ (succ n) = 1 :=
let f := (λ i : fin (succ (card A)), a ^ i) in
assert Pninj : ¬(injective f), from assume Pinj,
have Pninj : ¬(injective f), from assume Pinj,
absurd (card_le_of_inj _ _ (exists.intro f Pinj))
(begin rewrite [card_fin], apply not_succ_le_self end),
obtain i₁ P₁, from exists_not_of_not_forall Pninj,
obtain i₂ P₂, from exists_not_of_not_forall P₁,
obtain Pfe Pne, from and_not_of_not_implies P₂,
assert Pvne : val i₁ ≠ val i₂, from assume Pveq, absurd (eq_of_veq Pveq) Pne,
have Pvne : val i₁ ≠ val i₂, from assume Pveq, absurd (eq_of_veq Pveq) Pne,
exists.intro (pred (dist i₁ i₂)) (begin
rewrite [succ_pred_of_pos (dist_pos_of_ne Pvne)], apply and.intro,
apply lt_of_succ_lt_succ,
@ -123,7 +123,7 @@ take g, assume Pgin,
obtain n Plt Pe, from exists_pow_eq_one a,
obtain i Pilt Pig, from of_mem_sep Pgin,
let ni := -(mk_mod n i) in
assert Pinv : g*a^ni = 1, by
have Pinv : g*a^ni = 1, by
rewrite [-Pig, mk_pow_mod Pe, -(pow_madd Pe), add.right_inv],
begin
rewrite [inv_eq_of_mul_eq_one Pinv],
@ -144,7 +144,7 @@ lemma mem_cyc (a : A) : ∀ {n : nat}, a^n ∈ cyc a
lemma order_le {a : A} {n : nat} : a^(succ n) = 1 → order a ≤ succ n :=
assume Pe, let s := image (pow_nat a) (upto (succ n)) in
assert Psub: cyc a ⊆ s, from subset_of_forall
have Psub: cyc a ⊆ s, from subset_of_forall
(take g, assume Pgin, obtain i Pilt Pig, from of_mem_sep Pgin, begin
rewrite [-Pig, pow_mod Pe],
apply mem_image,
@ -170,7 +170,7 @@ have dist i j = 0, from
eq_of_veq (eq_of_dist_eq_zero this)
lemma cyc_eq_cyc (a : A) (n : nat) : cyc_pow_fin a n = cyc a :=
assert Psub : cyc_pow_fin a n ⊆ cyc a, from subset_of_forall
have Psub : cyc_pow_fin a n ⊆ cyc a, from subset_of_forall
(take g, assume Pgin,
obtain i Pin Pig, from exists_of_mem_image Pgin, by rewrite [-Pig]; apply mem_cyc),
eq_of_card_eq_of_subset (begin apply eq.trans,
@ -193,14 +193,14 @@ lemma order_of_min_pow {a : A} {n : nat}
(Pone : a^(succ n) = 1) (Pmin : ∀ i, i < n → a^(succ i) ≠ 1) : order a = succ n :=
or.elim (eq_or_lt_of_le (order_le Pone)) (λ P, P)
(λ P : order a < succ n, begin
assert Pn : a^(order a) ≠ 1,
have Pn : a^(order a) ≠ 1,
rewrite [-(succ_pred_of_pos (order_pos a))],
apply Pmin, apply nat.lt_of_succ_lt_succ,
rewrite [succ_pred_of_pos !order_pos], assumption,
exact absurd (pow_order a) Pn end)
lemma order_dvd_of_pow_eq_one {a : A} {n : nat} (Pone : a^n = 1) : order a ∣ n :=
assert Pe : a^(n % order a) = 1, from
have Pe : a^(n % order a) = 1, from
begin
revert Pone,
rewrite [eq_div_mul_add_mod n (order a) at {1}, pow_add, mul.comm _ (order a), pow_mul, pow_order, one_pow, one_mul],
@ -243,7 +243,7 @@ local attribute group_of_add_group [instance]
lemma pow_eq_mul {n : nat} {i : fin (succ n)} : ∀ {k : nat}, i^k = mk_mod n (i*k)
| 0 := by rewrite [pow_zero]
| (succ k) := begin
assert Psucc : i^(succ k) = madd (i^k) i, apply pow_succ',
have Psucc : i^(succ k) = madd (i^k) i, apply pow_succ',
rewrite [Psucc, pow_eq_mul],
apply eq_of_veq,
rewrite [mul_succ, val_madd, ↑mk_mod, mod_add_mod]
@ -268,7 +268,7 @@ lemma rotl_zero : ∀ {n : nat}, @rotl n 0 = id
lemma rotl_id : ∀ {n : nat}, @rotl n n = id
| 0 := funext take i, elim0 i
| (nat.succ n) :=
assert P : mk_mod n (n * succ n) = mk_mod n 0,
have P : mk_mod n (n * succ n) = mk_mod n 0,
from eq_of_veq (by rewrite [↑mk_mod, mul_mod_left]),
begin rewrite [rotl_succ', P], apply rotl_zero end

22
library/theories/group_theory/finsubg.lean
View file

@ -120,12 +120,12 @@ lemma fin_lcoset_same (x a : A) : x ∈ (fin_lcoset H a) = (fin_lcoset H x = fin
end
lemma fin_mem_lcoset (g : A) : g ∈ fin_lcoset H g :=
have P : g ∈ g ∘> ts H, from and.left (subg_in_coset_refl g),
assert P1 : g ∈ ts (fin_lcoset H g), from eq.symm (fin_lcoset_eq g) ▸ P,
have P1 : g ∈ ts (fin_lcoset H g), from eq.symm (fin_lcoset_eq g) ▸ P,
eq.symm (mem_eq_mem_to_set _ g) ▸ P1
lemma fin_lcoset_subset {S : finset A} (Psub : S ⊆ H) : ∀ x, x ∈ H → fin_lcoset S x ⊆ H :=
assert Psubs : set.subset (ts S) (ts H), from subset_eq_to_set_subset S H ▸ Psub,
have Psubs : set.subset (ts S) (ts H), from subset_eq_to_set_subset S H ▸ Psub,
take x, assume Pxs : x ∈ ts H,
assert Pcoset : set.subset (x ∘> ts S) (ts H), from subg_lcoset_subset_subg Psubs x Pxs,
have Pcoset : set.subset (x ∘> ts S) (ts H), from subg_lcoset_subset_subg Psubs x Pxs,
by rewrite [subset_eq_to_set_subset, fin_lcoset_eq x]; exact Pcoset
lemma finsubg_lcoset_id {a : A} : a ∈ H → fin_lcoset H a = H :=
@ -261,7 +261,7 @@ ext (take S, iff.intro
lemma length_all_lcosets : length (all_lcosets G H) = card (fin_lcosets H G) :=
eq.trans
(show length (all_lcosets G H) = length (list_lcosets G H), from
assert Pmap : map elt_of (all_lcosets G H) = list_lcosets G H, from
have Pmap : map elt_of (all_lcosets G H) = list_lcosets G H, from
map_dmap_of_inv_of_pos (λ S P, rfl) (λ S, is_lcoset_of_mem_list_lcosets),
by rewrite[-Pmap, length_map])
(by rewrite fin_lcosets_eq)
@ -409,9 +409,11 @@ obtain j Pjin Pj, from has_property J,
obtain k Pkin Pk, from has_property K,
Union_const (lcoset_not_empty J) begin
rewrite [-Pk], intro h Phin,
assert Phinn : h ∈ normalizer H,
apply mem_of_subset_of_mem (lcoset_subset_normalizer_of_mem Pjin),
rewrite Pj, assumption,
have Phinn : h ∈ normalizer H,
begin
apply mem_of_subset_of_mem (lcoset_subset_normalizer_of_mem Pjin),
rewrite Pj, assumption
end,
revert Phin Pgin,
rewrite [-Pj, *fin_lcoset_same],
intro Pheq Pgeq,
@ -454,7 +456,7 @@ lemma fin_coset_mul_assoc (J K L : lcoset_type (normalizer H) H) :
J ^ K ^ L = J ^ (K ^ L) :=
obtain j Pjin Pj, from exists_of_lcoset_type J,
obtain k Pkin Pk, from exists_of_lcoset_type K,
assert Pjk : j*k ∈ elt_of (J ^ K), from mul_mem_lcoset_mul J K Pjin Pkin,
have Pjk : j*k ∈ elt_of (J ^ K), from mul_mem_lcoset_mul J K Pjin Pkin,
obtain l Plin Pl, from has_property L,
subtype.eq (begin
rewrite [fin_coset_mul_eq_lcoset (J ^ K) _ Pjk,
@ -479,7 +481,7 @@ end
lemma fin_coset_left_inv (J : lcoset_type (normalizer H) H) :
(fin_coset_inv J) ^ J = fin_coset_one :=
obtain j Pjin Pj, from exists_of_lcoset_type J,
assert Pjinv : j⁻¹ ∈ elt_of (fin_coset_inv J), from inv_mem_fin_inv Pjin,
have Pjinv : j⁻¹ ∈ elt_of (fin_coset_inv J), from inv_mem_fin_inv Pjin,
subtype.eq begin
rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ Pjinv, -Pj, fin_lcoset_inv]
end
@ -514,7 +516,7 @@ lemma fcU_mul_closed : finset_mul_closed_on (fin_coset_Union Hc) :=
take j k, assume Pjin Pkin,
obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
obtain K PK PkK, from iff.elim_left !mem_Union_iff Pkin,
assert Pjk : j*k ∈ elt_of (J*K), from mul_mem_lcoset_mul J K PjJ PkK,
have Pjk : j*k ∈ elt_of (J*K), from mul_mem_lcoset_mul J K PjJ PkK,
iff.elim_right !mem_Union_iff
(exists.intro (J*K) (and.intro (finsubg_mul_closed Hc PJ PK) Pjk))

24
library/theories/group_theory/hom.lean
View file

@ -69,10 +69,10 @@ theorem hom_map_one : f 1 = 1 :=
eq.symm (mul.right_inv (f 1) ▸ (mul_inv_eq_of_eq_mul P))
theorem hom_map_inv (a : A) : f a⁻¹ = (f a)⁻¹ :=
assert P : f 1 = 1, from hom_map_one f,
assert P1 : f (a⁻¹ * a) = 1, from (eq.symm (mul.left_inv a)) ▸ P,
assert P2 : (f a⁻¹) * (f a) = 1, from (is_hom f a⁻¹ a) ▸ P1,
assert P3 : (f a⁻¹) * (f a) = (f a)⁻¹ * (f a), from eq.symm (mul.left_inv (f a)) ▸ P2,
have P : f 1 = 1, from hom_map_one f,
have P1 : f (a⁻¹ * a) = 1, from (eq.symm (mul.left_inv a)) ▸ P,
have P2 : (f a⁻¹) * (f a) = 1, from (is_hom f a⁻¹ a) ▸ P1,
have P3 : (f a⁻¹) * (f a) = (f a)⁻¹ * (f a), from eq.symm (mul.left_inv (f a)) ▸ P2,
mul_right_cancel P3
theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f ' H) :=
@ -80,8 +80,8 @@ theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f '
assume Pb1 : b1 ∈ f ' H, assume Pb2 : b2 ∈ f ' H,
obtain a1 (Pa1 : a1 ∈ H ∧ f a1 = b1), from Pb1,
obtain a2 (Pa2 : a2 ∈ H ∧ f a2 = b2), from Pb2,
assert Pa1a2 : a1 * a2 ∈ H, from Pclosed a1 a2 (and.left Pa1) (and.left Pa2),
assert Pb1b2 : f (a1 * a2) = b1 * b2, from calc
have Pa1a2 : a1 * a2 ∈ H, from Pclosed a1 a2 (and.left Pa1) (and.left Pa2),
have Pb1b2 : f (a1 * a2) = b1 * b2, from calc
f (a1 * a2) = f a1 * f a2 : is_hom f a1 a2
... = b1 * f a2 : {and.right Pa1}
... = b1 * b2 : {and.right Pa2},
@ -118,11 +118,11 @@ include is_subgH
theorem hom_map_subgroup : is_subgroup (f ' H) :=
have Pone : 1 ∈ f ' H, from mem_image (@subg_has_one _ _ H _) (hom_map_one f),
have Pclosed : mul_closed_on (f ' H), from hom_map_mul_closed f H subg_mul_closed,
assert Pinv : ∀ b, b ∈ f ' H → b⁻¹ ∈ f ' H, from
have Pinv : ∀ b, b ∈ f ' H → b⁻¹ ∈ f ' H, from
assume b, assume Pimg,
obtain a (Pa : a ∈ H ∧ f a = b), from Pimg,
assert Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa),
assert Pfainv : (f a)⁻¹ ∈ f ' H, from mem_image Painv (hom_map_inv f a),
have Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa),
have Pfainv : (f a)⁻¹ ∈ f ' H, from mem_image Painv (hom_map_inv f a),
and.right Pa ▸ Pfainv,
is_subgroup.mk Pone Pclosed Pinv
end
@ -149,8 +149,8 @@ definition quot_over_ker [instance] : group (coset_of (ker f)) := mk_quotient_gr
example (a x : A) : (x ∈ a ∘> ker f) = (f (a⁻¹*x) = 1) := rfl
lemma ker_coset_same_val (a b : A): same_lcoset (ker f) a b → f a = f b :=
assume Psame,
assert Pin : f (b⁻¹*a) = 1, from subg_same_lcoset_in_lcoset a b Psame,
assert P : (f b)⁻¹ * (f a) = 1, from calc
have Pin : f (b⁻¹*a) = 1, from subg_same_lcoset_in_lcoset a b Psame,
have P : (f b)⁻¹ * (f a) = 1, from calc
(f b)⁻¹ * (f a) = (f b⁻¹) * (f a) : (hom_map_inv f)
... = f (b⁻¹*a) : by rewrite [is_hom f]
... = 1 : by rewrite Pin,
@ -173,7 +173,7 @@ lemma ker_map_is_hom : homomorphic (ker_natural_map : coset_of (ker f) → B) :=
lemma ker_coset_inj (a b : A) : (ker_natural_map ⟦a⟧ = ker_natural_map ⟦b⟧) → ⟦a⟧ = ⟦b⟧ :=
assume Pfeq : f a = f b,
assert Painb : a ∈ b ∘> ker f, from calc
have Painb : a ∈ b ∘> ker f, from calc
f (b⁻¹*a) = (f b⁻¹) * (f a) : by rewrite [is_hom f]
... = (f b)⁻¹ * (f a) : by rewrite (hom_map_inv f)
... = (f a)⁻¹ * (f a) : by rewrite Pfeq

2
library/theories/group_theory/perm.lean
View file

@ -76,7 +76,7 @@ lemma nodup_all_perms : nodup (@all_perms A _ _) :=
lemma all_perms_complete : ∀ p : perm A, p ∈ all_perms :=
take p, perm.destruct p (take f Pinj,
assert Pin : f ∈ all_injs A, from all_injs_complete Pinj,
have Pin : f ∈ all_injs A, from all_injs_complete Pinj,
mem_dmap Pinj Pin)
definition perm_is_fintype [instance] : fintype (perm A) :=

40
library/theories/group_theory/pgroup.lean
View file

@ -43,10 +43,12 @@ lemma card_mod_eq_of_action_by_psubg {p : nat} :
cases Pa with Pain Porb,
substvars,
cases Ppsubg with Pprime PcardH,
assert Pdvd : card (orbit hom H a) ∣ p ^ (succ m),
rewrite -PcardH,
apply dvd_of_eq_mul (finset.card (stab hom H a)),
apply orbit_stabilizer_theorem,
have Pdvd : card (orbit hom H a) ∣ p ^ (succ m),
begin
rewrite -PcardH,
apply dvd_of_eq_mul (finset.card (stab hom H a)),
apply orbit_stabilizer_theorem
end,
apply or.elim (eq_one_or_dvd_of_dvd_prime_pow Pprime Pdvd),
intro Pcardeq, contradiction,
intro Ppdvd, exact Ppdvd
@ -131,7 +133,7 @@ Prodl_map
lemma prodseq_eq_pow_of_constseq {n : nat} (s : seq A (succ n)) :
constseq s → prodseq s = (s !zero) ^ succ n :=
assume Pc, assert Pcl : ∀ i, i ∈ upto (succ n) → s i = s !zero,
assume Pc, have Pcl : ∀ i, i ∈ upto (succ n) → s i = s !zero,
from take i, assume Pin, Pc i,
by rewrite [↑prodseq, Prodl_eq_pow_of_const _ Pcl, fin.length_upto]
@ -142,7 +144,7 @@ assume Pc₁ Pc₂ Peq, funext take i, by rewrite [Pc₁ i, Pc₂ i, Peq]
lemma peo_const_one : ∀ {n : nat}, peo (λ i : fin n, (1 : A))
| 0 := rfl
| (succ n) := let s := λ i : fin (succ n), (1 : A) in
assert Pconst : constseq s, from take i, rfl,
have Pconst : constseq s, from take i, rfl,
calc prodseq s = (s !zero) ^ succ n : prodseq_eq_pow_of_constseq s Pconst
... = (1 : A) ^ succ n : rfl
... = 1 : one_pow
@ -174,13 +176,13 @@ by rewrite [prodseq_eq, Peq, list_to_fun_to_list, prodl_eq_one_of_mem_all_prodl_
lemma all_prodseq_eq_one_complete {n : nat} {s : seq A (succ n)} :
prodseq s = 1 → s ∈ all_prodseq_eq_one A n :=
assume Peq,
assert Plin : map s (elems (fin (succ n))) ∈ all_prodl_eq_one A n,
have Plin : map s (elems (fin (succ n))) ∈ all_prodl_eq_one A n,
from begin
apply all_prodl_eq_one_complete,
rewrite [length_map], exact length_upto (succ n),
rewrite prodseq_eq at Peq, exact Peq
end,
assert Psin : list_to_fun (map s (elems (fin (succ n)))) (length_map_of_fintype s) ∈ all_prodseq_eq_one A n,
have Psin : list_to_fun (map s (elems (fin (succ n)))) (length_map_of_fintype s) ∈ all_prodseq_eq_one A n,
from mem_dmap _ Plin,
by rewrite [fun_eq_list_to_fun_map s (length_map_of_fintype s)]; apply Psin
@ -196,7 +198,7 @@ local attribute perm.f [coercion]
lemma rotl_perm_peo_of_peo {n : nat} : ∀ {m} {s : seq A n}, peo s → peo (rotl_perm A n m s)
| 0 := begin rewrite [↑rotl_perm, rotl_seq_zero], intros, assumption end
| (succ m) := take s,
assert Pmul : rotl_perm A n (m + 1) s = rotl_fun 1 (rotl_perm A n m s), from
have Pmul : rotl_perm A n (m + 1) s = rotl_fun 1 (rotl_perm A n m s), from
calc s ∘ (rotl (m + 1)) = s ∘ ((rotl m) ∘ (rotl 1)) : rotl_compose
... = s ∘ (rotl m) ∘ (rotl 1) : compose.assoc,
begin
@ -211,18 +213,18 @@ dmap_nodup_of_dinj (dinj_tag peo) nodup_all_prodseq_eq_one
lemma all_peo_seqs_complete {n : nat} : ∀ s : peo_seq A n, s ∈ all_peo_seqs A n :=
take ps, subtype.destruct ps (take s, assume Ps,
assert Pin : s ∈ all_prodseq_eq_one A n, from all_prodseq_eq_one_complete Ps,
have Pin : s ∈ all_prodseq_eq_one A n, from all_prodseq_eq_one_complete Ps,
mem_dmap Ps Pin)
lemma length_all_peo_seqs {n : nat} : length (all_peo_seqs A n) = (card A)^n :=
eq.trans (eq.trans
(show length (all_peo_seqs A n) = length (all_prodseq_eq_one A n), from
assert Pmap : map elt_of (all_peo_seqs A n) = all_prodseq_eq_one A n,
have Pmap : map elt_of (all_peo_seqs A n) = all_prodseq_eq_one A n,
from map_dmap_of_inv_of_pos (λ s P, rfl)
(λ s, prodseq_eq_one_of_mem_all_prodseq_eq_one),
by rewrite [-Pmap, length_map])
(show length (all_prodseq_eq_one A n) = length (all_prodl_eq_one A n), from
assert Pmap : map fun_to_list (all_prodseq_eq_one A n) = all_prodl_eq_one A n,
have Pmap : map fun_to_list (all_prodseq_eq_one A n) = all_prodl_eq_one A n,
from map_dmap_of_inv_of_pos list_to_fun_to_list
(λ l Pin, by rewrite [length_of_mem_all_prodl_eq_one Pin, card_fin]),
by rewrite [-Pmap, length_map]))
@ -319,8 +321,8 @@ lemma generator_of_prime_of_dvd_order {p : nat}
: prime p → p ∣ card A → ∃ g : A, g ≠ 1 ∧ g^p = 1 :=
assume Pprime Pdvd,
let pp := nat.pred p, spp := nat.succ pp in
assert Peq : spp = p, from succ_pred_prime Pprime,
assert Ppsubg : psubg (@univ (fin spp) _) spp 1,
have Peq : spp = p, from succ_pred_prime Pprime,
have Ppsubg : psubg (@univ (fin spp) _) spp 1,
from and.intro (eq.symm Peq ▸ Pprime) (by rewrite [Peq, card_fin, pow_one]),
have (pow_nat (card A) pp) % spp = (card (fixed_points (rotl_perm_ps A pp) univ)) % spp,
by rewrite -card_peo_seq; apply card_mod_eq_of_action_by_psubg Ppsubg,
@ -335,7 +337,7 @@ have Pfpcardgt1 : card (fixed_points (rotl_perm_ps A pp) univ) > 1,
obtain s₁ s₂ Pin₁ Pin₂ Psnes, from exists_two_of_card_gt_one Pfpcardgt1,
decidable.by_cases
(λ Pe₁ : elt_of s₁ !zero = 1,
assert Pne₂ : elt_of s₂ !zero ≠ 1,
have Pne₂ : elt_of s₂ !zero ≠ 1,
from assume Pe₂,
absurd
(subtype.eq (seq_eq_of_constseq_of_eq
@ -352,7 +354,7 @@ end
theorem cauchy_theorem {p : nat} : prime p → p ∣ card A → ∃ g : A, order g = p :=
assume Pprime Pdvd,
obtain g Pne Pgpow, from generator_of_prime_of_dvd_order Pprime Pdvd,
assert Porder : order g ∣ p, from order_dvd_of_pow_eq_one Pgpow,
have Porder : order g ∣ p, from order_dvd_of_pow_eq_one Pgpow,
or.elim (eq_one_or_eq_self_of_prime_of_dvd Pprime Porder)
(λ Pe, absurd (eq_one_of_order_eq_one Pe) Pne)
(λ Porderp, exists.intro g Porderp)
@ -375,10 +377,10 @@ theorem first_sylow_theorem {p : nat} (Pp : prime p) :
(by rewrite [pow_zero]))
| (succ n) := assume Pdvd,
obtain H PfinsubgH PcardH, from first_sylow_theorem n (pow_dvd_of_pow_succ_dvd Pdvd),
assert Ppsubg : psubg H p n, from and.intro Pp PcardH,
assert Ppowsucc : p^(succ n) ∣ (card (lcoset_type univ H) * p^n),
have Ppsubg : psubg H p n, from and.intro Pp PcardH,
have Ppowsucc : p^(succ n) ∣ (card (lcoset_type univ H) * p^n),
by rewrite [-PcardH, -(lagrange_theorem' !subset_univ)]; exact Pdvd,
assert Ppdvd : p ∣ card (lcoset_type (normalizer H) H), from
have Ppdvd : p ∣ card (lcoset_type (normalizer H) H), from
dvd_of_mod_eq_zero
(by rewrite [-(card_psubg_cosets_mod_eq Ppsubg), -dvd_iff_mod_eq_zero];
exact dvd_of_pow_succ_dvd_mul_pow (pos_of_prime Pp) Ppowsucc),

22
library/theories/group_theory/subgroup.lean
View file

@ -112,7 +112,7 @@ lemma grcoset_eq_rcoset a (H : set A) : H <∘ a = coset.r a H :=
end
lemma glcoset_sub a (S H : set A) : S ⊆ H → (a ∘> S) ⊆ (a ∘> H) :=
assume Psub,
assert P : _, from coset.l_sub a S H Psub,
have P : _, from coset.l_sub a S H Psub,
eq.symm (glcoset_eq_lcoset a S) ▸ eq.symm (glcoset_eq_lcoset a H) ▸ P
lemma glcoset_compose (a b : A) (H : set A) : a ∘> b ∘> H = a*b ∘> H :=
begin
@ -174,8 +174,8 @@ lemma closed_rcontract a (H : set A) : mul_closed_on H → a ∈ H → H <∘ a
end
lemma closed_lcontract_set a (H G : set A) : mul_closed_on G → H ⊆ G → a∈G → a∘>H ⊆ G :=
assume Pclosed, assume PHsubG, assume PainG,
assert PaGsubG : a ∘> G ⊆ G, from closed_lcontract a G Pclosed PainG,
assert PaHsubaG : a ∘> H ⊆ a ∘> G, from
have PaGsubG : a ∘> G ⊆ G, from closed_lcontract a G Pclosed PainG,
have PaHsubaG : a ∘> H ⊆ a ∘> G, from
eq.symm (glcoset_eq_lcoset a H) ▸ eq.symm (glcoset_eq_lcoset a G) ▸ (coset.l_sub a H G PHsubG),
subset.trans PaHsubaG PaGsubG
definition subgroup.has_inv H := ∀ (a : A), a ∈ H → a⁻¹ ∈ H
@ -207,9 +207,9 @@ lemma subg_mul_closed : mul_closed_on H := @is_subgroup.mul_closed A s H is_subg
lemma subg_has_inv : subgroup.has_inv H := @is_subgroup.has_inv A s H is_subg
lemma subgroup_coset_id : ∀ a, a ∈ H → (a ∘> H = H ∧ H <∘ a = H) :=
take a, assume PHa : H a,
assert Pl : a ∘> H ⊆ H, from closed_lcontract a H subg_mul_closed PHa,
assert Pr : H <∘ a ⊆ H, from closed_rcontract a H subg_mul_closed PHa,
assert PHainv : H a⁻¹, from subg_has_inv a PHa,
have Pl : a ∘> H ⊆ H, from closed_lcontract a H subg_mul_closed PHa,
have Pr : H <∘ a ⊆ H, from closed_rcontract a H subg_mul_closed PHa,
have PHainv : H a⁻¹, from subg_has_inv a PHa,
and.intro
(ext (assume x,
begin
@ -232,9 +232,9 @@ lemma subgroup_rcoset_id : ∀ a, a ∈ H → H <∘ a = H :=
take a, assume PHa : H a,
and.right (subgroup_coset_id a PHa)
lemma subg_in_coset_refl (a : A) : a ∈ a ∘> H ∧ a ∈ H <∘ a :=
assert PH1 : H 1, from subg_has_one,
assert PHinvaa : H (a⁻¹*a), from (eq.symm (mul.left_inv a)) ▸ PH1,
assert PHainva : H (a*a⁻¹), from (eq.symm (mul.right_inv a)) ▸ PH1,
have PH1 : H 1, from subg_has_one,
have PHinvaa : H (a⁻¹*a), from (eq.symm (mul.left_inv a)) ▸ PH1,
have PHainva : H (a*a⁻¹), from (eq.symm (mul.right_inv a)) ▸ PH1,
and.intro PHinvaa PHainva
end set_reducible
lemma subg_in_lcoset_same_lcoset (a b : A) : in_lcoset H a b → same_lcoset H a b :=
@ -245,7 +245,7 @@ lemma subg_in_lcoset_same_lcoset (a b : A) : in_lcoset H a b → same_lcoset H a
mul_inv_cancel_left b a ▸ Pbbinva
lemma subg_same_lcoset_in_lcoset (a b : A) : same_lcoset H a b → in_lcoset H a b :=
assume Psame : a∘>H = b∘>H,
assert Pa : a ∈ a∘>H, from and.left (subg_in_coset_refl a),
have Pa : a ∈ a∘>H, from and.left (subg_in_coset_refl a),
by exact (Psame ▸ Pa)
lemma subg_lcoset_same (a b : A) : in_lcoset H a b = (a∘>H = b∘>H) :=
propext(iff.intro (subg_in_lcoset_same_lcoset a b) (subg_same_lcoset_in_lcoset a b))
@ -257,7 +257,7 @@ lemma subg_rcoset_same (a b : A) : in_rcoset H a b = (H<∘a = H<∘b) :=
have Pabinvb : H <∘ a*b⁻¹*b = H <∘ b, from grcoset_compose (a*b⁻¹) b H ▸ Pabinv_b,
inv_mul_cancel_right a b ▸ Pabinvb)
(assume Psame,
assert Pa : a ∈ H<∘a, from and.right (subg_in_coset_refl a),
have Pa : a ∈ H<∘a, from and.right (subg_in_coset_refl a),
by exact (Psame ▸ Pa)))
lemma subg_same_lcoset.refl (a : A) : same_lcoset H a a := rfl
lemma subg_same_rcoset.refl (a : A) : same_rcoset H a a := rfl

2
library/theories/number_theory/bezout.lean
View file

@ -97,7 +97,7 @@ decidable.by_cases
(suppose ¬ p ∣ x,
have cpx : coprime p x, from coprime_of_prime_of_not_dvd pp this,
obtain (a b : ℤ) (Hab : a * p + b * x = gcd p x), from Bezout_aux p x,
assert a * p * y + b * x * y = y,
have a * p * y + b * x * y = y,
by krewrite [-right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul],
have p ∣ y,
begin

10
library/theories/number_theory/irrational_roots.lean
View file

@ -29,7 +29,7 @@ section
from even_of_exists (exists.intro _ (eq.symm this)),
have even b,
from even_of_even_pow this,
assert 2 ∣ gcd a b,
have 2 ∣ gcd a b,
from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
have (2:nat) ∣ 1,
begin rewrite [gcd_eq_one_of_coprime co at this], exact this end,
@ -51,7 +51,7 @@ section
(suppose b = 0,
have a^n = 0,
by rewrite [H, this, zero_pow npos],
assert a = 0,
have a = 0,
from eq_zero_of_pow_eq_zero this,
show false,
from ne_of_lt `0 < a` this⁻¹),
@ -59,7 +59,7 @@ section
take p,
suppose prime p,
suppose p ∣ b,
assert p ∣ b^n,
have p ∣ b^n,
from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`,
have p ∣ a^n,
by rewrite H; apply dvd_mul_of_dvd_right this,
@ -156,7 +156,7 @@ section
(suppose p = 0,
show false,
by note H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H),
assert agtz : a > 0, from pos_of_ne_zero
have agtz : a > 0, from pos_of_ne_zero
(suppose a = 0,
show false, by revert peq; rewrite [this, zero_pow npos]; exact pnez),
have n * mult p a = 1, from calc
@ -197,7 +197,7 @@ section
example {a b c : ℤ} (co : coprime a b) (apos : a > 0) (bpos : b > 0)
(H : a * a = c * (b * b)) :
b = 1 :=
assert H₁ : gcd (c * b) a = gcd c a,
have H₁ : gcd (c * b) a = gcd c a,
from gcd_mul_right_cancel_of_coprime _ (coprime_swap co),
have a * a = c * b * b,
by rewrite -mul.assoc at H; apply H,

36
library/theories/number_theory/prime_factorization.lean
View file

@ -93,8 +93,8 @@ begin
(take n',
suppose n = p * n',
have p > 0, from lt.trans zero_lt_one pgt1,
assert n / p = n', from !nat.div_eq_of_eq_mul_right this `n = p * n'`,
assert n' < n,
have n / p = n', from !nat.div_eq_of_eq_mul_right this `n = p * n'`,
have n' < n,
by rewrite -this; apply mult_rec_decreasing pgt1 npos,
begin
rewrite [mult_rec pgt1 npos pdvdn, `n / p = n'`, pow_succ], subst n,
@ -104,14 +104,14 @@ begin
end
theorem mult_one_right (p : ℕ) : mult p 1 = 0:=
assert H : p^(mult p 1) = 1, from eq_one_of_dvd_one !pow_mult_dvd,
have H : p^(mult p 1) = 1, from eq_one_of_dvd_one !pow_mult_dvd,
or.elim (le_or_gt p 1)
(suppose p ≤ 1, by rewrite [!mult_eq_zero_of_le_one this])
(suppose p > 1,
by_contradiction
(suppose mult p 1 ≠ 0,
have mult p 1 > 0, from pos_of_ne_zero this,
assert p^(mult p 1) > 1, from pow_gt_one `p > 1` this,
have p^(mult p 1) > 1, from pow_gt_one `p > 1` this,
show false, by rewrite H at this; apply !lt.irrefl this))
private theorem mult_pow_mul {p n : ℕ} (i : ℕ) (pgt1 : p > 1) (npos : n > 0) :
@ -136,13 +136,13 @@ theorem le_mult {p i n : ℕ} (pgt1 : p > 1) (npos : n > 0) (pidvd : p^i ∣ n)
dvd.elim pidvd
(take m,
suppose n = p^i * m,
assert m > 0, from pos_of_mul_pos_left (this ▸ npos),
have m > 0, from pos_of_mul_pos_left (this ▸ npos),
by subst n; rewrite [mult_pow_mul i pgt1 this]; apply le_add_right)
theorem not_dvd_div_pow_mult {p n : ℕ} (pgt1 : p > 1) (npos : n > 0) : ¬ p ∣ n / p^(mult p n) :=
assume pdvd : p ∣ n / p^(mult p n),
obtain m (H : n / p^(mult p n) = p * m), from exists_eq_mul_right_of_dvd pdvd,
assert n = p^(succ (mult p n)) * m, from
have n = p^(succ (mult p n)) * m, from
calc
n = p^mult p n * (n / p^mult p n) : by rewrite (nat.mul_div_cancel' !pow_mult_dvd)
... = p^(succ (mult p n)) * m : by rewrite [H, pow_succ', mul.assoc],
@ -153,16 +153,16 @@ show false, from !not_succ_le_self this
theorem mult_mul {p m n : ℕ} (primep : prime p) (mpos : m > 0) (npos : n > 0) :
mult p (m * n) = mult p m + mult p n :=
let m' := m / p^mult p m, n' := n / p^mult p n in
assert p > 1, from gt_one_of_prime primep,
assert meq : m = p^mult p m * m', by rewrite (nat.mul_div_cancel' !pow_mult_dvd),
assert neq : n = p^mult p n * n', by rewrite (nat.mul_div_cancel' !pow_mult_dvd),
have p > 1, from gt_one_of_prime primep,
have meq : m = p^mult p m * m', by rewrite (nat.mul_div_cancel' !pow_mult_dvd),
have neq : n = p^mult p n * n', by rewrite (nat.mul_div_cancel' !pow_mult_dvd),
have m'pos : m' > 0, from pos_of_mul_pos_left (meq ▸ mpos),
have n'pos : n' > 0, from pos_of_mul_pos_left (neq ▸ npos),
have npdvdm' : ¬ p ∣ m', from !not_dvd_div_pow_mult `p > 1` mpos,
have npdvdn' : ¬ p ∣ n', from !not_dvd_div_pow_mult `p > 1` npos,
assert npdvdm'n' : ¬ p ∣ m' * n', from not_dvd_mul_of_prime primep npdvdm' npdvdn',
assert m'n'pos : m' * n' > 0, from mul_pos m'pos n'pos,
assert multm'n' : mult p (m' * n') = 0, from mult_eq_zero_of_not_dvd npdvdm'n',
have npdvdm'n' : ¬ p ∣ m' * n', from not_dvd_mul_of_prime primep npdvdm' npdvdn',
have m'n'pos : m' * n' > 0, from mul_pos m'pos n'pos,
have multm'n' : mult p (m' * n') = 0, from mult_eq_zero_of_not_dvd npdvdm'n',
calc
mult p (m * n) = mult p (p^(mult p m + mult p n) * (m' * n')) :
by rewrite [pow_add, mul.right_comm, -mul.assoc, -meq, mul.assoc,
@ -196,8 +196,8 @@ begin
{intros; rewrite nz; apply dvd_zero},
assume H : ∀ {p : ℕ}, prime p → mult p m ≤ mult p n,
obtain m' (meq : m = p * m'), from exists_eq_mul_right_of_dvd pdvdm,
assert pgt1 : p > 1, from gt_one_of_prime primep,
assert m'pos : m' > 0, from pos_of_ne_zero
have pgt1 : p > 1, from gt_one_of_prime primep,
have m'pos : m' > 0, from pos_of_ne_zero
(assume m'z, by revert mpos; rewrite [meq, m'z, mul_zero]; apply not_lt_zero),
have m'ltm : m' < m,
by rewrite [meq, -one_mul m' at {1}]; apply mul_lt_mul_of_lt_of_le m'pos pgt1 !le.refl,
@ -205,7 +205,7 @@ begin
have multpn : mult p n ≥ 1, from le.trans multpm (H primep),
obtain n' (neq : n = p * n'),
from exists_eq_mul_right_of_dvd (dvd_of_mult_pos (lt_of_succ_le multpn)),
assert n'pos : n' > 0, from pos_of_ne_zero
have n'pos : n' > 0, from pos_of_ne_zero
(assume n'z, by revert npos; rewrite [neq, n'z, mul_zero]; apply not_lt_zero),
have ∀q, prime q → mult q m' ≤ mult q n', from
(take q,
@ -215,7 +215,7 @@ begin
have multqn : mult q n = mult q p + mult q n',
by rewrite [neq, mult_mul primeq (pos_of_prime primep) n'pos],
show mult q m' ≤ mult q n', from le_of_add_le_add_left (multqm ▸ multqn ▸ H primeq)),
assert m'dvdn' : m' ∣ n', from ih m' m'ltm m'pos n' this,
have m'dvdn' : m' ∣ n', from ih m' m'ltm m'pos n' this,
show m ∣ n, by rewrite [meq, neq]; apply mul_dvd_mul !dvd.refl m'dvdn'
end
@ -293,7 +293,7 @@ end
theorem eq_prime_factorization {n : ℕ} (npos : n > 0) :
n = (∏ p ∈ prime_factors n, p^(mult p n)) :=
let nprod := ∏ p ∈ prime_factors n, p^(mult p n) in
assert primefactors : ∀ p, p ∈ prime_factors n → prime p,
have primefactors : ∀ p, p ∈ prime_factors n → prime p,
from take p, @prime_of_mem_prime_factors p n,
have prodpos : (∏ q ∈ prime_factors n, q^(mult q n)) > 0,
from Prod_pos (take q, assume qpf,
@ -306,6 +306,6 @@ eq_of_forall_prime_mult_eq npos prodpos
eq.symm (mult_prod_pow_of_mem primep primefactors (λ p, mult p n) pprimefactors))
(assume pnprimefactors : p ∉ prime_factors n,
have ¬ p ∣ n, from assume H, pnprimefactors (mem_prime_factors npos primep H),
assert mult p n = 0, from mult_eq_zero_of_not_dvd this,
have mult p n = 0, from mult_eq_zero_of_not_dvd this,
by rewrite [this, mult_prod_pow_of_not_mem primep primefactors _ pnprimefactors]))
end nat

14
library/theories/number_theory/primes.lean
View file

@ -90,7 +90,7 @@ definition sub_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → {m | m
assume h₁ h₂,
have n ≠ 0, from assume h, begin subst n, exact absurd h₁ dec_trivial end,
obtain m m_dvd_n m_ne_1 m_ne_n, from sub_dvd_of_not_prime h₁ h₂,
assert m_ne_0 : m ≠ 0, from assume h, begin subst m, exact absurd (eq_zero_of_zero_dvd m_dvd_n) `n ≠ 0` end,
have m_ne_0 : m ≠ 0, from assume h, begin subst m, exact absurd (eq_zero_of_zero_dvd m_dvd_n) `n ≠ 0` end,
begin
existsi m, split, assumption,
split,
@ -145,7 +145,7 @@ lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=
λ pp p_gt_2, by_contradiction (λ hn,
have even p, from even_of_not_odd hn,
obtain k `p = 2*k`, from exists_of_even this,
assert 2 ∣ p, by rewrite [`p = 2*k`]; apply dvd_mul_right,
have 2 ∣ p, by rewrite [`p = 2*k`]; apply dvd_mul_right,
or.elim (eq_one_or_eq_self_of_prime_of_dvd pp this)
(suppose 2 = 1, absurd this dec_trivial)
(suppose 2 = p, by subst this; exact absurd p_gt_2 !lt.irrefl))
@ -190,8 +190,8 @@ lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n →
lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m
| 0 hp hd :=
assert p = 1, from eq_one_of_dvd_one hd,
have (1:nat) ≥ 2, begin rewrite -this at {1}, apply ge_two_of_prime hp end,
have p = 1, from eq_one_of_dvd_one hd,
have (1:nat) ≥ 2, begin rewrite -this at {1}, apply ge_two_of_prime hp end,
absurd this dec_trivial
| (succ n) hp hd :=
have p ∣ (m^n)*m, by rewrite [pow_succ' at hd]; exact hd,
@ -204,12 +204,12 @@ lemma coprime_pow_of_prime_of_not_dvd {p m a : nat} : prime p → ¬ p ∣ a →
lemma coprime_primes {p q : nat} : prime p → prime q → p ≠ q → coprime p q :=
λ hp hq hn,
assert gcd p q ∣ p, from !gcd_dvd_left,
have gcd p q ∣ p, from !gcd_dvd_left,
or.elim (eq_one_or_eq_self_of_prime_of_dvd hp this)
(suppose gcd p q = 1, this)
(assume h : gcd p q = p,
assert gcd p q ∣ q, from !gcd_dvd_right,
have p ∣ q, by rewrite -h; exact this,
have gcd p q ∣ q, from !gcd_dvd_right,
have p ∣ q, by rewrite -h; exact this,
or.elim (eq_one_or_eq_self_of_prime_of_dvd hq this)
(suppose p = 1, by subst p; exact absurd hp not_prime_one)
(suppose p = q, by contradiction))