refactor(library): use new 'suppose'-expression
This commit is contained in:
Leonardo de Moura
parent
c2fc612ec1
commit
48f8b8f18d
8 changed files with 157 additions and 159 deletions
|
|
@ -95,51 +95,51 @@ section division_ring
|
|||
|
||||
-- make "left" and "right" versions?
|
||||
theorem eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a :=
|
||||
have H2 : a ≠ 0, from
|
||||
(assume aeq0 : a = 0,
|
||||
have B : 0 = (1:A), by rewrite [-(zero_mul b), -aeq0, H],
|
||||
absurd B zero_ne_one),
|
||||
have a ≠ 0, from
|
||||
(suppose a = 0,
|
||||
have 0 = (1:A), by rewrite [-(zero_mul b), -this, H],
|
||||
absurd this zero_ne_one),
|
||||
show b = 1 / a, from symm (calc
|
||||
1 / a = (1 / a) * 1 : mul_one
|
||||
... = (1 / a) * (a * b) : H
|
||||
... = (1 / a) * a * b : mul.assoc
|
||||
... = 1 * b : one_div_mul_cancel H2
|
||||
... = 1 * b : one_div_mul_cancel this
|
||||
... = b : one_mul)
|
||||
|
||||
-- which one is left and which is right?
|
||||
theorem eq_one_div_of_mul_eq_one_left (H : b * a = 1) : b = 1 / a :=
|
||||
have H2 : a ≠ 0, from
|
||||
(assume A : a = 0,
|
||||
have B : 0 = 1, from symm (calc
|
||||
1 = b * a : symm H
|
||||
... = b * 0 : A
|
||||
... = 0 : mul_zero),
|
||||
absurd B zero_ne_one),
|
||||
have a ≠ 0, from
|
||||
(suppose a = 0,
|
||||
have 0 = 1, from symm (calc
|
||||
1 = b * a : symm H
|
||||
... = b * 0 : this
|
||||
... = 0 : mul_zero),
|
||||
absurd this zero_ne_one),
|
||||
show b = 1 / a, from symm (calc
|
||||
1 / a = 1 * (1 / a) : one_mul
|
||||
... = b * a * (1 / a) : H
|
||||
... = b * (a * (1 / a)) : mul.assoc
|
||||
... = b * 1 : mul_one_div_cancel H2
|
||||
... = b * 1 : mul_one_div_cancel this
|
||||
... = b : mul_one)
|
||||
|
||||
theorem one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) :=
|
||||
have H : (b * a) * ((1 / a) * (1 / b)) = 1, by
|
||||
have (b * a) * ((1 / a) * (1 / b)) = 1, by
|
||||
rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)],
|
||||
eq_one_div_of_mul_eq_one H
|
||||
eq_one_div_of_mul_eq_one this
|
||||
|
||||
theorem one_div_neg_one_eq_neg_one : (1:A) / (-1) = -1 :=
|
||||
have H : (-1) * (-1) = (1:A), by rewrite [-neg_eq_neg_one_mul, neg_neg],
|
||||
symm (eq_one_div_of_mul_eq_one H)
|
||||
have (-1) * (-1) = (1:A), by rewrite [-neg_eq_neg_one_mul, neg_neg],
|
||||
symm (eq_one_div_of_mul_eq_one this)
|
||||
|
||||
theorem one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) :=
|
||||
have H1 : -1 ≠ 0, from
|
||||
(assume H2 : -1 = 0, absurd (symm (calc
|
||||
have -1 ≠ 0, from
|
||||
(suppose -1 = 0, absurd (symm (calc
|
||||
1 = -(-1) : neg_neg
|
||||
... = -0 : H2
|
||||
... = -0 : this
|
||||
... = (0:A) : neg_zero)) zero_ne_one),
|
||||
calc
|
||||
1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul
|
||||
... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1
|
||||
... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H this
|
||||
... = (1 / a) * (-1) : one_div_neg_one_eq_neg_one
|
||||
... = - (1 / a) : mul_neg_one_eq_neg
|
||||
|
||||
|
|
@ -163,12 +163,11 @@ section division_ring
|
|||
by rewrite [-(div_div Ha), H, (div_div Hb)]
|
||||
|
||||
theorem mul_inv_eq (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ :=
|
||||
have H1 : b * a ≠ 0, from mul_ne_zero' Hb Ha,
|
||||
eq.symm (calc
|
||||
a⁻¹ * b⁻¹ = (1 / a) * b⁻¹ : inv_eq_one_div
|
||||
... = (1 / a) * (1 / b) : inv_eq_one_div
|
||||
... = (1 / (b * a)) : one_div_mul_one_div Ha Hb
|
||||
... = (b * a)⁻¹ : inv_eq_one_div)
|
||||
... = (1 / a) * (1 / b) : inv_eq_one_div
|
||||
... = (1 / (b * a)) : one_div_mul_one_div Ha Hb
|
||||
... = (b * a)⁻¹ : inv_eq_one_div)
|
||||
|
||||
theorem mul_div_cancel (Hb : b ≠ 0) : a * b / b = a :=
|
||||
by rewrite [↑divide, mul.assoc, (mul_inv_cancel Hb), mul_one]
|
||||
|
|
@ -190,22 +189,22 @@ section division_ring
|
|||
|
||||
theorem div_eq_one_iff_eq (Hb : b ≠ 0) : a / b = 1 ↔ a = b :=
|
||||
iff.intro
|
||||
(assume H1 : a / b = 1, symm (calc
|
||||
(suppose a / b = 1, symm (calc
|
||||
b = 1 * b : one_mul
|
||||
... = a / b * b : H1
|
||||
... = a / b * b : this
|
||||
... = a : div_mul_cancel Hb))
|
||||
(assume H2 : a = b, calc
|
||||
a / b = b / b : H2
|
||||
(suppose a = b, calc
|
||||
a / b = b / b : this
|
||||
... = 1 : div_self Hb)
|
||||
|
||||
theorem eq_div_iff_mul_eq (Hc : c ≠ 0) : a = b / c ↔ a * c = b :=
|
||||
iff.intro
|
||||
(assume H : a = b / c, by rewrite [H, (div_mul_cancel Hc)])
|
||||
(assume H : a * c = b, by rewrite [-(mul_div_cancel Hc), H])
|
||||
(suppose a = b / c, by rewrite [this, (div_mul_cancel Hc)])
|
||||
(suppose a * c = b, by rewrite [-(mul_div_cancel Hc), this])
|
||||
|
||||
theorem add_div_eq_mul_add_div (Hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
|
||||
have H : (a + b / c) * c = a * c + b, by rewrite [right_distrib, (div_mul_cancel Hc)],
|
||||
(iff.elim_right (eq_div_iff_mul_eq Hc)) H
|
||||
have (a + b / c) * c = a * c + b, by rewrite [right_distrib, (div_mul_cancel Hc)],
|
||||
(iff.elim_right (eq_div_iff_mul_eq Hc)) this
|
||||
|
||||
theorem mul_mul_div (Hc : c ≠ 0) : a = a * c * (1 / c) :=
|
||||
calc
|
||||
|
|
@ -229,13 +228,13 @@ section field
|
|||
by rewrite [(one_div_mul_one_div Ha Hb), mul.comm b]
|
||||
|
||||
theorem div_mul_right (Hb : b ≠ 0) (H : a * b ≠ 0) : a / (a * b) = 1 / b :=
|
||||
let Ha : a ≠ 0 := and.left (ne_zero_and_ne_zero_of_mul_ne_zero H) in
|
||||
have a ≠ 0, from and.left (ne_zero_and_ne_zero_of_mul_ne_zero H),
|
||||
symm (calc
|
||||
1 / b = 1 * (1 / b) : one_mul
|
||||
... = (a * a⁻¹) * (1 / b) : mul_inv_cancel Ha
|
||||
... = (a * a⁻¹) * (1 / b) : mul_inv_cancel this
|
||||
... = a * (a⁻¹ * (1 / b)) : mul.assoc
|
||||
... = a * ((1 / a) * (1 / b)) :inv_eq_one_div
|
||||
... = a * (1 / (b * a)) : one_div_mul_one_div Ha Hb
|
||||
... = a * (1 / (b * a)) : one_div_mul_one_div this Hb
|
||||
... = a * (1 / (a * b)) : mul.comm
|
||||
... = a * (a * b)⁻¹ : inv_eq_one_div)
|
||||
|
||||
|
|
@ -250,14 +249,13 @@ 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) :=
|
||||
have H [visible] : a * b ≠ 0, from (mul_ne_zero' Ha Hb),
|
||||
by rewrite [add.comm, -(div_mul_left Ha H), -(div_mul_right Hb H), ↑divide, -right_distrib]
|
||||
assert a * b ≠ 0, from (mul_ne_zero' Ha Hb),
|
||||
by rewrite [add.comm, -(div_mul_left Ha this), -(div_mul_right Hb this), ↑divide, -right_distrib]
|
||||
|
||||
theorem div_mul_div (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) :=
|
||||
by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)]
|
||||
|
||||
theorem mul_div_mul_left (Hb : b ≠ 0) (Hc : c ≠ 0) : (c * a) / (c * b) = a / b :=
|
||||
have H [visible] : c * b ≠ 0, from mul_ne_zero' Hc Hb,
|
||||
by rewrite [-(div_mul_div Hc Hb), (div_self Hc), one_mul]
|
||||
|
||||
theorem mul_div_mul_right (Hb : b ≠ 0) (Hc : c ≠ 0) : (a * c) / (b * c) = a / b :=
|
||||
|
|
@ -272,7 +270,6 @@ section field
|
|||
|
||||
theorem div_add_div (Hb : b ≠ 0) (Hd : d ≠ 0) :
|
||||
(a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
|
||||
have H [visible] : b * d ≠ 0, from mul_ne_zero' Hb Hd,
|
||||
by rewrite [-(mul_div_mul_right Hb Hd), -(mul_div_mul_left Hd Hb), div_add_div_same]
|
||||
|
||||
theorem div_sub_div (Hb : b ≠ 0) (Hd : d ≠ 0) :
|
||||
|
|
@ -285,11 +282,11 @@ section field
|
|||
-(div_mul_eq_mul_div_comm Hb), H, (div_mul_eq_mul_div), (div_mul_cancel Hd)]
|
||||
|
||||
theorem one_div_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / (a / b) = b / a :=
|
||||
have H : (a / b) * (b / a) = 1, from calc
|
||||
have (a / b) * (b / a) = 1, from calc
|
||||
(a / b) * (b / a) = (a * b) / (b * a) : div_mul_div Hb Ha
|
||||
... = (a * b) / (a * b) : mul.comm
|
||||
... = 1 : div_self (mul_ne_zero' Ha Hb),
|
||||
symm (eq_one_div_of_mul_eq_one H)
|
||||
symm (eq_one_div_of_mul_eq_one this)
|
||||
|
||||
theorem div_div_eq_mul_div (Hb : b ≠ 0) (Hc : c ≠ 0) : a / (b / c) = (a * c) / b :=
|
||||
by rewrite [div_eq_mul_one_div, (one_div_div Hb Hc), -mul_div_assoc]
|
||||
|
|
@ -322,9 +319,9 @@ section discrete_field
|
|||
theorem discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero
|
||||
(x y : A) (H : x * y = 0) : x = 0 ∨ y = 0 :=
|
||||
decidable.by_cases
|
||||
(assume H : x = 0, or.inl H)
|
||||
(assume H1 : x ≠ 0,
|
||||
or.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero]))
|
||||
(suppose x = 0, or.inl this)
|
||||
(suppose x ≠ 0,
|
||||
or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
|
||||
|
||||
definition discrete_field.to_integral_domain [trans-instance] [reducible] [coercion] :
|
||||
integral_domain A :=
|
||||
|
|
@ -352,18 +349,18 @@ section discrete_field
|
|||
-- the following could all go in "discrete_division_ring"
|
||||
theorem one_div_mul_one_div'' : (1 / a) * (1 / b) = 1 / (b * a) :=
|
||||
decidable.by_cases
|
||||
(assume Ha : a = 0,
|
||||
by rewrite [Ha, div_zero, zero_mul, -(@div_zero A s 1), mul_zero b])
|
||||
(suppose a = 0,
|
||||
by rewrite [this, div_zero, zero_mul, -(@div_zero A s 1), mul_zero b])
|
||||
(assume Ha : a ≠ 0,
|
||||
decidable.by_cases
|
||||
(assume Hb : b = 0,
|
||||
by rewrite [Hb, div_zero, mul_zero, -(@div_zero A s 1), zero_mul a])
|
||||
(assume Hb : b ≠ 0, one_div_mul_one_div Ha Hb))
|
||||
(suppose b = 0,
|
||||
by rewrite [this, div_zero, mul_zero, -(@div_zero A s 1), zero_mul a])
|
||||
(suppose b ≠ 0, one_div_mul_one_div Ha this))
|
||||
|
||||
theorem one_div_neg_eq_neg_one_div' : 1 / (- a) = - (1 / a) :=
|
||||
decidable.by_cases
|
||||
(assume Ha : a = 0, by rewrite [Ha, neg_zero, 2 div_zero, neg_zero])
|
||||
(assume Ha : a ≠ 0, one_div_neg_eq_neg_one_div Ha)
|
||||
(suppose a = 0, by rewrite [this, neg_zero, 2 div_zero, neg_zero])
|
||||
(suppose a ≠ 0, one_div_neg_eq_neg_one_div this)
|
||||
|
||||
theorem neg_div' : (-b) / a = - (b / a) :=
|
||||
decidable.by_cases
|
||||
|
|
|
|||
|
|
@ -16,11 +16,11 @@ open encodable
|
|||
|
||||
definition countable_of_encodable {A : Type} : encodable A → countable A :=
|
||||
assume e : encodable A,
|
||||
have inj_encode : injective encode, from
|
||||
have injective encode, from
|
||||
λ (a₁ a₂ : A) (h : encode a₁ = encode a₂),
|
||||
assert aux : decode A (encode a₁) = decode A (encode a₂), by rewrite h,
|
||||
by rewrite [*encodek at aux]; injection aux; assumption,
|
||||
exists.intro encode inj_encode
|
||||
assert decode A (encode a₁) = decode A (encode a₂), by rewrite h,
|
||||
by rewrite [*encodek at this]; injection this; assumption,
|
||||
exists.intro encode this
|
||||
|
||||
definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : encodable A :=
|
||||
encodable.mk
|
||||
|
|
@ -301,11 +301,11 @@ match decode A n with
|
|||
end (eq.refl (decode A n))
|
||||
|
||||
private definition find_a : (∃ x, p x) → {a : A | p a} :=
|
||||
assume ex : ∃ x, p x,
|
||||
have exn : ∃ x, pn x, from ex_pn_of_ex ex,
|
||||
let r : nat := @nat.choose pn decidable_pn exn in
|
||||
have pnr : pn r, from @nat.choose_spec pn decidable_pn exn,
|
||||
of_nat r pnr
|
||||
suppose ∃ x, p x,
|
||||
have ∃ x, pn x, from ex_pn_of_ex this,
|
||||
let r := @nat.choose pn decidable_pn this in
|
||||
have pn r, from @nat.choose_spec pn decidable_pn this,
|
||||
of_nat r this
|
||||
end find_a
|
||||
|
||||
namespace encodable
|
||||
|
|
@ -320,16 +320,16 @@ has_property (find_a ex)
|
|||
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} [c : Π a, encodable (B a)] [d : ∀ x y, decidable (R x y)]
|
||||
: (∀x, ∃y, R x y) → ∃f, ∀x, R x (f x) :=
|
||||
assume H,
|
||||
have H₁ : ∀x, R x (choose (H x)), from take x, choose_spec (H x),
|
||||
exists.intro _ H₁
|
||||
have ∀x, R x (choose (H x)), from take x, choose_spec (H x),
|
||||
exists.intro _ this
|
||||
|
||||
theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} [c : Π a, encodable (B a)] [d : ∀ x y, decidable (P x y)]
|
||||
: (∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
|
||||
iff.intro
|
||||
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
|
||||
(assume H : (∃f, (∀x, P x (f x))),
|
||||
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
|
||||
exists.intro (fw x) (Hw x))
|
||||
(suppose (∀ x, ∃y, P x y), axiom_of_choice this)
|
||||
(suppose (∃ f, (∀x, P x (f x))),
|
||||
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from this,
|
||||
exists.intro (fw x) (Hw x))
|
||||
end encodable
|
||||
|
||||
namespace quot
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ lemma eq_of_veq : ∀ {i j : fin n}, (val i) = j → i = j
|
|||
|
||||
lemma veq_of_eq : ∀ {i j : fin n}, i = j → (val i) = j
|
||||
| (mk iv ilt) (mk jv jlt) := assume Peq,
|
||||
have veq : iv = jv, from fin.no_confusion Peq (λ Pe Pqe, Pe), veq
|
||||
show iv = jv, from fin.no_confusion Peq (λ Pe Pqe, Pe)
|
||||
|
||||
lemma eq_iff_veq : ∀ {i j : fin n}, (val i) = j ↔ i = j :=
|
||||
take i j, iff.intro eq_of_veq veq_of_eq
|
||||
|
|
@ -57,8 +57,8 @@ 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 Pin : ival ∈ list.upto n, from mem_upto_of_lt Piltn,
|
||||
mem_dmap Piltn Pin)
|
||||
assert ival ∈ list.upto n, from mem_upto_of_lt Piltn,
|
||||
mem_dmap Piltn this)
|
||||
|
||||
lemma upto_zero : upto 0 = [] :=
|
||||
by rewrite [↑upto, list.upto_nil, dmap_nil]
|
||||
|
|
@ -132,13 +132,13 @@ 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 visn : val i < nat.succ n, from val_lt i,
|
||||
assert aux : val (@maxi n) = n, from rfl,
|
||||
assert vne : val i ≠ n, from
|
||||
assume he,
|
||||
have vivm : val i = val (@maxi n), from he ⬝ aux⁻¹,
|
||||
absurd (eq_of_veq vivm) hne,
|
||||
lt_of_le_of_ne (le_of_lt_succ visn) vne
|
||||
have val (@maxi n) = n, from rfl,
|
||||
have val i = val (@maxi n), from he ⬝ this⁻¹,
|
||||
absurd (eq_of_veq this) hne,
|
||||
have val i < nat.succ n, from val_lt i,
|
||||
lt_of_le_of_ne (le_of_lt_succ this) vne
|
||||
|
||||
lemma lift_succ_ne_max {i : fin n} : lift_succ i ≠ maxi :=
|
||||
begin
|
||||
|
|
@ -199,8 +199,8 @@ end
|
|||
|
||||
lemma lift_fun_inj : injective (@lift_fun n) :=
|
||||
take f₁ f₂ Peq, funext (λ i,
|
||||
assert Peqi : lift_fun f₁ (lift_succ i) = lift_fun f₂ (lift_succ i), from congr_fun Peq _,
|
||||
begin revert Peqi, rewrite [*lift_fun_eq], apply lift_succ_inj end)
|
||||
assert 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) :
|
||||
val (lower_inj f Pinj Pmax i) = val (f (lift_succ i)) :=
|
||||
|
|
@ -295,15 +295,15 @@ begin
|
|||
eq.symm (succ_pred_of_pos HT),
|
||||
assert pj : vj < n, from
|
||||
lt_of_succ_lt_succ (eq.subst HSv pk),
|
||||
have HS : succ (mk vj pj) = mk vk pk, from
|
||||
have succ (mk vj pj) = mk vk pk, from
|
||||
val_inj (eq.symm HSv),
|
||||
eq.rec_on HS (CS (mk vj pj)) },
|
||||
eq.rec_on this (CS (mk vj pj)) },
|
||||
{ show C (mk vk pk), from
|
||||
have HOv : vk = 0, from
|
||||
have vk = 0, from
|
||||
eq_zero_of_le_zero (le_of_not_gt HF),
|
||||
have HO : zero n = mk vk pk, from
|
||||
val_inj (eq.symm HOv),
|
||||
eq.rec_on HO CO }
|
||||
have zero n = mk vk pk, from
|
||||
val_inj (eq.symm this),
|
||||
eq.rec_on this CO }
|
||||
end
|
||||
|
||||
theorem choice {C : fin n → Type} :
|
||||
|
|
|
|||
|
|
@ -22,9 +22,9 @@ definition fintype_of_equiv {A B : Type} [h : fintype A] : A ≃ B → fintype B
|
|||
(map f (elements_of A))
|
||||
(nodup_map (injective_of_left_inverse l) !fintype.unique)
|
||||
(λ b,
|
||||
have h₁ : g b ∈ elements_of A, from fintype.complete (g b),
|
||||
assert h₂ : f (g b) ∈ map f (elements_of A), from mem_map f h₁,
|
||||
by rewrite r at h₂; exact h₂)
|
||||
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,
|
||||
by rewrite r at this; exact this)
|
||||
end
|
||||
|
||||
definition fintype_unit [instance] : fintype unit :=
|
||||
|
|
@ -66,23 +66,24 @@ assume eq, if_pos eq
|
|||
theorem ne_of_find_discr_eq_some {f g : A → B} {a : A} : ∀ {l}, find_discr f g l = some a → f a ≠ g a
|
||||
| [] e := by contradiction
|
||||
| (x::l) e := by_cases
|
||||
(λ h : f x = g x,
|
||||
have aux : find_discr f g l = some a, by rewrite [find_discr_cons_of_eq l h at e]; exact e,
|
||||
ne_of_find_discr_eq_some aux)
|
||||
(λ h : f x ≠ g x,
|
||||
have aux : some x = some a, by rewrite [find_discr_cons_of_ne l h at e]; exact e,
|
||||
option.no_confusion aux (λ xeqa : x = a, eq.rec_on xeqa h))
|
||||
(suppose f x = g x,
|
||||
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,
|
||||
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
|
||||
| [] e a i := absurd i !not_mem_nil
|
||||
| (x::l) e a i := by_cases
|
||||
(λ fx_eq_gx : f x = g x,
|
||||
have aux : find_discr f g l = none, by rewrite [find_discr_cons_of_eq l fx_eq_gx at e]; exact e,
|
||||
(assume fx_eq_gx : f x = g x,
|
||||
or.elim (eq_or_mem_of_mem_cons i)
|
||||
(λ aeqx : a = x, by rewrite [-aeqx at fx_eq_gx]; exact fx_eq_gx)
|
||||
(λ ainl : a ∈ l, all_eq_of_find_discr_eq_none aux a ainl))
|
||||
(λ fx_ne_gx : f x ≠ g x,
|
||||
by rewrite [find_discr_cons_of_ne l fx_ne_gx at e]; contradiction)
|
||||
(suppose a = x, by rewrite [-this at fx_eq_gx]; exact fx_eq_gx)
|
||||
(suppose a ∈ l,
|
||||
have aux : find_discr f g l = none, by rewrite [find_discr_cons_of_eq l fx_eq_gx at e]; exact e,
|
||||
all_eq_of_find_discr_eq_none aux a this))
|
||||
(suppose f x ≠ g x,
|
||||
by rewrite [find_discr_cons_of_ne l this at e]; contradiction)
|
||||
end find_discr
|
||||
|
||||
definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : decidable_eq B] : decidable_eq (A → B) :=
|
||||
|
|
|
|||
|
|
@ -281,10 +281,10 @@ nat.cases_on n
|
|||
(take m',
|
||||
assume H : succ n' * succ m' = 0,
|
||||
absurd
|
||||
((calc
|
||||
(calc
|
||||
0 = succ n' * succ m' : H
|
||||
... = succ n' * m' + succ n' : mul_succ
|
||||
... = succ (succ n' * m' + n') : add_succ)⁻¹)
|
||||
... = succ (succ n' * m' + n') : add_succ)⁻¹
|
||||
!succ_ne_zero))
|
||||
|
||||
section migrate_algebra
|
||||
|
|
|
|||
|
|
@ -60,8 +60,8 @@ private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gt
|
|||
| (succ x) y asx yltsx :=
|
||||
assert ax : acc gtb x, from acc_of_acc_succ asx,
|
||||
by_cases
|
||||
(λ yeqx : y = x, by substvars; assumption)
|
||||
(λ ynex : y ≠ x, acc_of_acc_of_lt ax (lt_of_le_and_ne (le_of_lt_succ yltsx) ynex))
|
||||
(suppose y = x, by substvars; assumption)
|
||||
(suppose y ≠ x, acc_of_acc_of_lt ax (lt_of_le_and_ne (le_of_lt_succ yltsx) this))
|
||||
|
||||
parameter (ex : ∃ a, p a)
|
||||
parameter [dp : decidable_pred p]
|
||||
|
|
@ -70,9 +70,9 @@ include dp
|
|||
private lemma acc_of_ex (x : nat) : acc gtb x :=
|
||||
obtain (w : nat) (pw : p w), from ex,
|
||||
lt.by_cases
|
||||
(λ xltw : x < w, acc_of_acc_of_lt (acc_of_px pw) xltw)
|
||||
(λ xeqw : x = w, by subst x; exact (acc_of_px pw))
|
||||
(λ xgtw : x > w, acc_of_px_of_gt pw xgtw)
|
||||
(suppose x < w, acc_of_acc_of_lt (acc_of_px pw) this)
|
||||
(suppose x = w, by subst x; exact (acc_of_px pw))
|
||||
(suppose x > w, acc_of_px_of_gt pw this)
|
||||
|
||||
private lemma wf_gtb : well_founded gtb :=
|
||||
well_founded.intro acc_of_ex
|
||||
|
|
@ -83,14 +83,14 @@ match x with
|
|||
(λ p0 : p 0, tag 0 p0)
|
||||
(λ np0 : ¬ p 0,
|
||||
have l₁ : lbp 1, from lbp_succ l0 np0,
|
||||
have g : 1 ≺ 0, from and.intro (lt.base 0) l₁,
|
||||
f 1 g l₁)
|
||||
have 1 ≺ 0, from and.intro (lt.base 0) l₁,
|
||||
f 1 this l₁)
|
||||
| (succ n) := λ f lsn, by_cases
|
||||
(λ psn : p (succ n), tag (succ n) psn)
|
||||
(λ npsn : ¬ p (succ n),
|
||||
have lss : lbp (succ (succ n)), from lbp_succ lsn npsn,
|
||||
have g : succ (succ n) ≺ succ n, from and.intro (lt.base (succ n)) lss,
|
||||
f (succ (succ n)) g lss)
|
||||
have succ (succ n) ≺ succ n, from and.intro (lt.base (succ n)) lss,
|
||||
f (succ (succ n)) this lss)
|
||||
end
|
||||
|
||||
private definition find_x : {x : nat | p x} :=
|
||||
|
|
|
|||
|
|
@ -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 h₁ : swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs,
|
||||
by rewrite *swap_swap at h₁; exact h₁
|
||||
assert swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs,
|
||||
by rewrite *swap_swap at this; exact this
|
||||
end prod
|
||||
|
|
|
|||
|
|
@ -55,8 +55,8 @@ equiv_zero_of_num_eq_zero H3
|
|||
|
||||
theorem nonneg_total (a : prerat) : nonneg a ∨ nonneg (neg a) :=
|
||||
or.elim (le.total 0 (num a))
|
||||
(assume H : 0 ≤ num a, or.inl H)
|
||||
(assume H : 0 ≥ num a, or.inr (neg_nonneg_of_nonpos H))
|
||||
(suppose 0 ≤ num a, or.inl this)
|
||||
(suppose 0 ≥ num a, or.inr (neg_nonneg_of_nonpos this))
|
||||
|
||||
theorem nonneg_of_pos (H : pos a) : nonneg a := le_of_lt H
|
||||
|
||||
|
|
@ -64,9 +64,8 @@ theorem ne_zero_of_pos (H : pos a) : ¬ a ≡ zero :=
|
|||
assume H', ne_of_gt H (num_eq_zero_of_equiv_zero H')
|
||||
|
||||
theorem pos_of_nonneg_of_ne_zero (H1 : nonneg a) (H2 : ¬ a ≡ zero) : pos a :=
|
||||
have H3 : num a ≠ 0,
|
||||
from assume H' : num a = 0, H2 (equiv_zero_of_num_eq_zero H'),
|
||||
lt_of_le_of_ne H1 (ne.symm H3)
|
||||
have num a ≠ 0, from suppose num a = 0, H2 (equiv_zero_of_num_eq_zero this),
|
||||
lt_of_le_of_ne H1 (ne.symm this)
|
||||
|
||||
theorem nonneg_mul (H1 : nonneg a) (H2 : nonneg b) : nonneg (mul a b) :=
|
||||
mul_nonneg H1 H2
|
||||
|
|
@ -125,10 +124,10 @@ quot.induction_on a (take u, assume H1 H2, prerat.ne_zero_of_pos H1 (quot.exact
|
|||
private theorem pos_of_nonneg_of_ne_zero : nonneg a → ¬ a = 0 → pos a :=
|
||||
quot.induction_on a
|
||||
(take u,
|
||||
assume H1 : nonneg ⟦u⟧,
|
||||
assume H2 : ⟦u⟧ ≠ (rat.of_num 0),
|
||||
have H3 : ¬ (prerat.equiv u prerat.zero), from assume H, H2 (quot.sound H),
|
||||
prerat.pos_of_nonneg_of_ne_zero H1 H3)
|
||||
assume h : nonneg ⟦u⟧,
|
||||
suppose ⟦u⟧ ≠ (rat.of_num 0),
|
||||
have ¬ (prerat.equiv u prerat.zero), from assume H, this (quot.sound H),
|
||||
prerat.pos_of_nonneg_of_ne_zero h this)
|
||||
|
||||
private theorem nonneg_mul : nonneg a → nonneg b → nonneg (a * b) :=
|
||||
quot.induction_on₂ a b @prerat.nonneg_mul
|
||||
|
|
@ -210,43 +209,43 @@ theorem le.by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a →
|
|||
theorem lt_iff_le_and_ne (a b : ℚ) : a < b ↔ a ≤ b ∧ a ≠ b :=
|
||||
iff.intro
|
||||
(assume H : a < b,
|
||||
have H1 : b - a ≠ 0, from ne_zero_of_pos H,
|
||||
have H2 : a ≠ b, from ne.symm (assume H', H1 (H' ▸ !sub_self)),
|
||||
and.intro (nonneg_of_pos H) H2)
|
||||
have b - a ≠ 0, from ne_zero_of_pos H,
|
||||
have a ≠ b, from ne.symm (assume H', this (H' ▸ !sub_self)),
|
||||
and.intro (nonneg_of_pos H) this)
|
||||
(assume H : a ≤ b ∧ a ≠ b,
|
||||
obtain aleb aneb, from H,
|
||||
have H1 : b - a ≠ 0, from (assume H', aneb (eq_of_sub_eq_zero H')⁻¹),
|
||||
pos_of_nonneg_of_ne_zero aleb H1)
|
||||
have b - a ≠ 0, from (assume H', aneb (eq_of_sub_eq_zero H')⁻¹),
|
||||
pos_of_nonneg_of_ne_zero aleb this)
|
||||
|
||||
theorem le_iff_lt_or_eq (a b : ℚ) : a ≤ b ↔ a < b ∨ a = b :=
|
||||
iff.intro
|
||||
(assume H : a ≤ b,
|
||||
(assume h : a ≤ b,
|
||||
decidable.by_cases
|
||||
(assume H1 : a = b, or.inr H1)
|
||||
(assume H1 : a ≠ b, or.inl (iff.mpr !lt_iff_le_and_ne (and.intro H H1))))
|
||||
(assume H : a < b ∨ a = b,
|
||||
or.elim H
|
||||
(assume H1 : a < b, and.left (iff.mp !lt_iff_le_and_ne H1))
|
||||
(assume H1 : a = b, H1 ▸ !le.refl))
|
||||
(suppose a = b, or.inr this)
|
||||
(suppose a ≠ b, or.inl (iff.mpr !lt_iff_le_and_ne (and.intro h this))))
|
||||
(suppose a < b ∨ a = b,
|
||||
or.elim this
|
||||
(suppose a < b, and.left (iff.mp !lt_iff_le_and_ne this))
|
||||
(suppose a = b, this ▸ !le.refl))
|
||||
|
||||
theorem to_nonneg : a ≥ 0 → nonneg a :=
|
||||
by intros; rewrite -sub_zero; eassumption
|
||||
|
||||
theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
|
||||
have H1 : c + b - (c + a) = b - a,
|
||||
have c + b - (c + a) = b - a,
|
||||
by rewrite [↑sub, neg_add, -add.assoc, add.comm c, add_neg_cancel_right],
|
||||
show nonneg (c + b - (c + a)), from H1⁻¹ ▸ H
|
||||
show nonneg (c + b - (c + a)), from this⁻¹ ▸ H
|
||||
|
||||
theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
|
||||
have H : nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
|
||||
!sub_zero⁻¹ ▸ H
|
||||
have nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
|
||||
!sub_zero⁻¹ ▸ this
|
||||
|
||||
theorem to_pos : a > 0 → pos a :=
|
||||
by intros; rewrite -sub_zero; eassumption
|
||||
|
||||
theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
|
||||
have H : pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
|
||||
!sub_zero⁻¹ ▸ H
|
||||
have pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
|
||||
!sub_zero⁻¹ ▸ this
|
||||
|
||||
definition decidable_lt [instance] : decidable_rel rat.lt :=
|
||||
take a b, decidable_pos (b - a)
|
||||
|
|
@ -254,24 +253,24 @@ take a b, decidable_pos (b - a)
|
|||
theorem le_of_lt (H : a < b) : a ≤ b := iff.mpr !le_iff_lt_or_eq (or.inl H)
|
||||
|
||||
theorem lt_irrefl (a : ℚ) : ¬ a < a :=
|
||||
take Ha,
|
||||
take Ha,
|
||||
let Hand := (iff.mp !lt_iff_le_and_ne) Ha in
|
||||
(and.right Hand) rfl
|
||||
|
||||
theorem not_le_of_gt (H : a < b) : ¬ b ≤ a :=
|
||||
assume Hba,
|
||||
assume Hba,
|
||||
let Heq := le.antisymm (le_of_lt H) Hba in
|
||||
!lt_irrefl (Heq ▸ H)
|
||||
|
||||
theorem lt_of_lt_of_le (Hab : a < b) (Hbc : b ≤ c) : a < c :=
|
||||
let Hab' := le_of_lt Hab in
|
||||
let Hac := le.trans Hab' Hbc in
|
||||
let Hab' := le_of_lt Hab in
|
||||
let Hac := le.trans Hab' Hbc in
|
||||
(iff.mpr !lt_iff_le_and_ne) (and.intro Hac
|
||||
(assume Heq, not_le_of_gt (Heq ▸ Hab) Hbc))
|
||||
|
||||
theorem lt_of_le_of_lt (Hab : a ≤ b) (Hbc : b < c) : a < c :=
|
||||
let Hbc' := le_of_lt Hbc in
|
||||
let Hac := le.trans Hab Hbc' in
|
||||
let Hbc' := le_of_lt Hbc in
|
||||
let Hac := le.trans Hab Hbc' in
|
||||
(iff.mpr !lt_iff_le_and_ne) (and.intro Hac
|
||||
(assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab))
|
||||
|
||||
|
|
@ -324,28 +323,29 @@ section migrate_algebra
|
|||
end migrate_algebra
|
||||
|
||||
theorem rat_of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
|
||||
have hsimp [visible] : ∀ 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 [hsimp, abs_neg, abs_of_nonneg (!of_nat_nonneg)])
|
||||
assert ∀ 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)])
|
||||
|
||||
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,
|
||||
have H'' : 1 ≤ abs (of_int (denom a)), begin
|
||||
have J : of_int (denom a) > 0, from (iff.mpr !of_int_pos) !denom_pos,
|
||||
rewrite (abs_of_pos J),
|
||||
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 (iff.mpr !of_int_pos) !denom_pos,
|
||||
have 1 ≤ abs (of_int (denom a)), begin
|
||||
rewrite (abs_of_pos this),
|
||||
apply iff.mpr !of_int_le_of_int,
|
||||
apply denom_pos
|
||||
end,
|
||||
have H' : abs a ≤ abs (of_int (num a)), from
|
||||
le_of_mul_le_of_ge_one (H ▸ !le.refl) !abs_nonneg H'',
|
||||
calc
|
||||
a ≤ abs a : le_abs_self
|
||||
... ≤ abs (of_int (num a)) : H'
|
||||
... ≤ abs (of_int (num a)) + 1 : rat.le_add_of_nonneg_right trivial
|
||||
... = of_nat (int.nat_abs (num a)) + 1 : rat_of_nat_abs
|
||||
have abs a ≤ abs (of_int (num a)), from
|
||||
le_of_mul_le_of_ge_one (h ▸ !le.refl) !abs_nonneg this,
|
||||
calc
|
||||
a ≤ abs a : le_abs_self
|
||||
... ≤ abs (of_int (num a)) : this
|
||||
... ≤ abs (of_int (num a)) + 1 : rat.le_add_of_nonneg_right trivial
|
||||
... = of_nat (int.nat_abs (num a)) + 1 : rat_of_nat_abs
|
||||
... = of_nat (nat.succ (int.nat_abs (num a))) : of_nat_add
|
||||
|
||||
theorem ubound_pos (a : ℚ) : nat.gt (ubound a) nat.zero := !nat.succ_pos
|
||||
|
|
|
|||
Loading…
Reference in a new issue