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".
33 λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
35 notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
37 interpretation "tends to" 'tends s x =
38 (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
40 alias symbol "and" = "constructive and".
42 ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
43 (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
44 an ⇝ x → bn ⇝ x → xn ⇝ x.
45 intros (R ml an bn xn x H Ha Hb);
46 unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
47 alias num (instance 0) = "natural number".
48 cases (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha;
49 cases (Hb (e/2) (divide_preserves_lt ??? He)) (n2 H2); clear Hb;
50 apply (ex_introT ?? (n1+n2)); intros (n3 Lt_n1n2_n3);
51 lapply (ltwr ??? Lt_n1n2_n3) as Lt_n1n3; lapply (ltwl ??? Lt_n1n2_n3) as Lt_n2n3;
52 cases (H1 ? Lt_n1n3) (c daxe); cases (H2 ? Lt_n2n3) (c dbxe);
53 cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2;
54 (* the main inequality *)
55 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
56 apply (le_transitive ???? (mtineq ???? (an n3)));
57 lapply (le_mtri ????? H7 H8) as H9; clear H7 H8;
58 lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
59 cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
60 apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
61 apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
62 apply (Eq≈ (δ(an n3) (xn n3) + (-δ(xn n3) (bn n3) + δ(xn n3) (bn n3))) ? (opp_inverse ??));
63 apply (Eq≈ (δ(an n3) (xn n3) + (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
64 apply (Eq≈ ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear H10;
65 apply (le_rewl ??? ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
66 apply (le_rewl ??? (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
67 apply (Le≪ (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3))));
68 apply (Le≪ (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
69 apply (Le≪ ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
70 apply lew_opp; [apply mpositive] apply fle_plusr;
71 apply (Le≫ ? (plus_comm ???));
72 apply (Le≫ ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
74 split; [ (* first the trivial case: -e< δ(xn n3) x *)
75 apply (lt_le_transitive ????? (mpositive ????));
76 apply lt_zero_x_to_lt_opp_x_zero; assumption;]
77 (* the main goal: δ(xn n3) x<e *)
78 apply (le_lt_transitive ???? main_ineq);
79 apply (Lt≫ (e/2+e/2+e/2)); [apply (divpow ?e 2)]
80 repeat (apply ltplus; try assumption);