1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/sandwich/".
17 include "nat/plus.ma".
18 include "nat/orders.ma".
20 lemma ltwl: ∀a,b,c:nat. b + a < c → a < c.
21 intros 3 (x y z); elim y (H z IH H); [apply H]
22 apply IH; apply lt_S_to_lt; apply H;
25 lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
26 intros 3 (x y z); rewrite > sym_plus; apply ltwl;
29 include "sequence.ma".
30 include "metric_lattice.ma".
32 lemma sandwich_ineq: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
33 intro G; cases G; unfold divide; intro e;
34 alias num (instance 0) = "natural number".
35 cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
36 cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
39 apply (ltmul_lt ??? 2); apply (lt_rewr ???? H2);
40 apply (lt_rewl ???? (mulzero ? 3)); assumption]
42 apply (ltmul_lt ??? 3); apply (lt_rewr ???? H1);
43 apply (lt_rewl ???? (mulzero ? 4)); assumption]
45 apply (muleqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
46 apply (plus_cancr_lt ??? w1);
47 apply (lt_rewl ??? (w+e)); [
48 apply (Eq≈ (w+3*w1) ? H2);
49 apply (Eq≈ (w+w1+(w1+w1)) (plus_assoc ??w1 w1));
50 apply (Eq≈ (w+(w1+(w1+w1))) (plus_assoc ?w w1 ?));
51 simplify; repeat apply feq_plusl; apply eq_sym;
52 apply (Eq≈ ? (plus_comm ???)); apply zero_neutral;]
53 apply (lt_rewl ???? (plus_comm ???));
54 apply flt_plusl; assumption;
58 λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
60 notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
62 interpretation "tends to" 'tends s x =
63 (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
65 alias symbol "and" = "constructive and".
67 ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
68 (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
72 intros (R ml an bn xn x H Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %.
74 elim (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha;
75 elim (Hb (e/3) (divide_preserves_lt ??? He)) (n2 H2); clear Hb;
76 constructor 1; [apply (n1 + n2);] intros (n3 Hn3);
77 lapply (ltwr ??? Hn3) as Hn1n3; lapply (ltwl ??? Hn3) as Hn2n3;
78 elim (H1 ? Hn1n3) (H3 H4); elim (H2 ? Hn2n3) (H5 H6); clear Hn1n3 Hn2n3;
79 elim (H n3) (H7 H8); clear H H1 H2;
80 lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym;
82 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
83 apply (le_transitive ???? (mtineq ???? (an n3)));
84 lapply (le_mtri ????? H7 H8) as H9;
85 lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
86 cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
87 apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
88 apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
89 apply (Eq≈ (δ(an n3) (xn n3) + (-δ(xn n3) (bn n3) + δ(xn n3) (bn n3))) ? (opp_inverse ??));
90 apply (Eq≈ (δ(an n3) (xn n3) + (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
91 apply (Eq≈ ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear H10;
92 apply (le_rewl ??? ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
93 apply (le_rewl ??? (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
94 clear Dym Dxm H8 H7 H6 H5 H4 H3;
95 apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3))));
96 apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
97 apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
98 apply lew_opp; [apply mpositive] apply fle_plusr;
99 apply (le_rewr ???? (plus_comm ???));
100 apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
102 split; [ (* first the trivial case *)
103 apply (lt_le_transitive ????? (mpositive ????));
104 apply lt_zero_x_to_lt_opp_x_zero; assumption;]
105 clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2; cases H4 (H7 H8); clear H4;
106 apply (le_lt_transitive ???? ? (sandwich_ineq ?? He));
107 apply (le_transitive ???? main_ineq);
108 apply (le_transitive ?? (e/3+ δ(an n3) x+ δ(an n3) x)); [
109 repeat apply fle_plusr; cases H6; assumption;]
110 apply (le_transitive ?? (e/3+ e/2 + δ(an n3) x) ); [apply fle_plusr; apply fle_plusl; assumption]
111 apply (le_transitive ?? (e/3+ e/2 + e/2)); [apply fle_plusl; assumption;]