helm/software/matita/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 set "baseuri" "cic:/matita/sandwich/".
  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 "sequence.ma".
  30 include "metric_lattice.ma".
  31
  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;
  37 intro H3;
  38 cut (0<w1) as H4; [2:
  39   apply (ltpow_lt ??? 2); apply (lt_rewr ???? H2);
  40   apply (lt_rewl ???? (powzero ? 3)); assumption]
  41 cut (0<w) as H5; [2:
  42   apply (ltpow_lt ??? 3); apply (lt_rewr ???? H1);
  43   apply (lt_rewl ???? (powzero ? 4)); assumption]
  44 cut (w<w1) as H6; [2:
  45   apply (poweqplus_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;
  55 qed.
  56
  57 definition d2s ≝
  58   λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
  59
  60 notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
  61
  62 interpretation "tends to" 'tends s x =
  63   (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
  64
  65 alias symbol "and" = "constructive and".
  66 theorem sandwich:
  67   ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
  68     (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
  69     an ⇝ x →
  70     bn ⇝ x →
  71     xn ⇝ x.
  72 intros (R ml an bn xn x H Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %.
  73 intros (e He);
  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;
  81 (* the main step *)
  82 cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2:
  83   apply (le_transitive ???? (mtineq ???? (an n3)));
  84   lapply (le_mtri ????? H7 H8);
  85   lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin);
  86   cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [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 Hletin1;
  92   apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[
  93     apply feq_plusr; apply msymmetric;]
  94   apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[
  95     apply feq_plusr; assumption;]
  96   clear Hcut Hletin Dym Dxm H8 H7 H6 H5 H4 H3;
  97   apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x));[
  98     apply feq_plusr; apply plus_comm;]
  99   apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
 100   apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
 101   apply lew_opp; [apply mpositive] apply fle_plusr;
 102   apply (le_rewr ???? (plus_comm ???));
 103   apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
 104   apply mtineq;]
 105 split; [
 106   apply (lt_le_transitive ????? (mpositive ????));
 107   split; elim He; [apply  le_zero_x_to_le_opp_x_zero; assumption;]
 108   cases t1; [
 109     left; apply exc_zero_opp_x_to_exc_x_zero;
 110     apply (Ex≫ ? (eq_opp_opp_x_x ??));assumption;]
 111   right;  apply exc_opp_x_zero_to_exc_zero_x;
 112   apply (Ex≪ ? (eq_opp_opp_x_x ??)); assumption;]
 113 clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2;
 114 apply (le_lt_transitive ???? ? (sandwich_ineq ?? He));
 115 apply (le_transitive ???? Hcut);
 116 apply (le_transitive ??  (e/3+ δ(an n3) x+ δ(an n3) x)); [
 117   repeat apply fle_plusr; cases H6; assumption;]
 118 apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x)); [
 119   apply fle_plusr; apply fle_plusl; cases H4; assumption;]
 120 apply (le_transitive ??  (e/3+ e/2 + e/2)); [
 121   apply fle_plusl; cases H4; assumption;]
 122 apply le_reflexive;
 123 qed.