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

style(library/data/real): clean up proofs in basic.lean

Browse source
This commit is contained in:
Rob Lewis 2015-08-05 12:44:13 -04:00 • committed by Leonardo de Moura
parent 5568085ab9
commit 11bb342819
1 changed files with 6 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,20 +49,17 @@ theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻
begin begin
apply rat.le_of_not_gt, apply rat.le_of_not_gt,
intro Hb, intro Hb,
apply (exists.elim (find_midpoint Hb)), cases find_midpoint Hb with [c, Hc],
intro c Hc, cases find_thirds b c (and.right Hc) with [j, Hbj],
apply (exists.elim (find_thirds b c (and.right Hc))),
intro j Hbj,
have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj (and.left Hc), have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj (and.left Hc),
exact absurd !H (not_le_of_gt Ha) apply (not_le_of_gt Ha) !H
end end
theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b := theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b :=
begin begin
apply rat.le_of_not_gt, apply rat.le_of_not_gt,
intro Hb, intro Hb,
apply (exists.elim (find_midpoint Hb)), cases find_midpoint Hb with [c, Hc],
intro c Hc,
let Hc' := H c (and.right Hc), let Hc' := H c (and.right Hc),
apply (rat.not_le_of_gt (and.left Hc)) (iff.mpr !le_add_iff_sub_right_le Hc') apply (rat.not_le_of_gt (and.left Hc)) (iff.mpr !le_add_iff_sub_right_le Hc')
end end
@ -145,7 +142,7 @@ theorem bdd_of_eq {s t : seq} (H : s ≡ t) :
begin begin
intros [j, n, Hn], intros [j, n, Hn],
apply rat.le.trans, apply rat.le.trans,
apply H n, apply H,
rewrite -(add_halves j), rewrite -(add_halves j),
apply rat.add_le_add, apply rat.add_le_add,
apply inv_ge_of_le Hn, apply inv_ge_of_le Hn,
@ -199,7 +196,7 @@ theorem eq_of_bdd_var {s t : seq} (Hs : regular s) (Ht : regular t)
apply eq_of_bdd, apply eq_of_bdd,
repeat assumption, repeat assumption,
intros, intros,
apply H j⁻¹, apply H,
apply inv_pos apply inv_pos
end end
@ -472,8 +469,6 @@ theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu
apply Hs, apply Hs,
apply abs_nonneg, apply abs_nonneg,
apply rat.mul_nonneg, apply rat.mul_nonneg,
repeat (apply Kq_bound_nonneg | assumption),
repeat apply rat.mul_le_mul,
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg | repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg), apply abs_nonneg),
apply Hu, apply Hu,