]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/dama/sandwich.ma
the is_structure is a bad idea if you don't have canonical structures.
[helm.git] / 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 (ltmul_lt ??? 2); apply (lt_rewr ???? H2);
40   apply (lt_rewl ???? (mulzero ? 3)); assumption]
41 cut (0<w) as H5; [2:
42   apply (ltmul_lt ??? 3); apply (lt_rewr ???? H1);
43   apply (lt_rewl ???? (mulzero ? 4)); assumption]
44 cut (w<w1) as H6; [2: 
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;
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) 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 ????));
101   apply mtineq;]
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;]
112 apply le_reflexive;
113 qed.