matita/contribs/dama/dama/sandwich.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/plus.ma".
  18 include "nat/orders.ma".
  19
  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;
  23 qed.
  24
  25 lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
  26 intros 3 (x y z); rewrite > sym_plus; apply ltwl;
  27 qed.
  28
  29 include "tend.ma".
  30 include "metric_lattice.ma".
  31
  32 alias symbol "leq" = "ordered sets less or equal than".
  33 alias symbol "and" = "constructive and".
  34 theorem sandwich:
  35 let ugo ≝ excess_OF_lattice1 in
  36   ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
  37     (∀n. (xn n ≤ an n) ∧ (bn n ≤ xn n)) →
  38     an ⇝ x → bn ⇝ x → xn ⇝ x.
  39 intros (R ml an bn xn x H Ha Hb);
  40 unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He);
  41 alias num (instance 0) = "natural number".
  42 cases (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha;
  43 cases (Hb (e/2) (divide_preserves_lt ??? He)) (n2 H2); clear Hb;
  44 apply (ex_introT ?? (n1+n2)); intros (n3 Lt_n1n2_n3);
  45 lapply (ltwr ??? Lt_n1n2_n3) as Lt_n1n3; lapply (ltwl ??? Lt_n1n2_n3) as Lt_n2n3;
  46 cases (H1 ? Lt_n1n3) (c daxe); cases (H2 ? Lt_n2n3) (c dbxe);
  47 cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2;
  48 (* the main inequality *)
  49 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
  50   apply (le_transitive ???? (mtineq ???? (an n3)));
  51   cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
  52     lapply (le_mtri ?? ??? H8 H7) as H9; clear H7 H8;
  53     lapply (Eq≈ ? (msymmetric ????) H9) as H10; clear H9;
  54     lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H10) as H9; clear H10;
  55     apply (Eq≈ ? H9); clear H9;
  56     apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(xn n3) (bn n3)) (plus_comm ??( δ(xn n3) (an n3))));
  57     apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(bn n3) (xn n3)) (feq_opp ??? (msymmetric ????)));
  58     apply (Eq≈ ( δ(xn n3) (an n3)+ (δ(bn n3) (xn n3)+- δ(bn n3) (xn n3))) (plus_assoc ????));
  59     apply (Eq≈ (δ(xn n3) (an n3) + (- δ(bn n3) (xn n3) + δ(bn n3) (xn n3))) (plus_comm ??(δ(bn n3) (xn n3))));
  60     apply (Eq≈ (δ(xn n3) (an n3) + 0) (opp_inverse ??));
  61     apply (Eq≈ ? (plus_comm ???));
  62     apply (Eq≈ ? (zero_neutral ??));
  63     apply (Eq≈ ? (msymmetric ????));
  64     apply eq_reflexive;]
  65   apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
  66   apply (Le≪ (δ(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 ????));
  73   apply mtineq;]
  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);
  81 qed.