carabinieri almost done

[helm.git] / helm / software / matita / dama / metric_lattice.ma

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index a4ca3b4f4b6029d692b618aae05eee9438190230..0e92f0a89c42c8b18215b3459befa2e17c40c1e3 100644 (file)
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -100,6 +100,67 @@ apply (Eq≈ (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
 apply eq_reflexive;   
 qed.  
 
+include "sequence.ma".
+include "nat/plus.ma".
+
+definition d2s ≝ 
+  λR.λml:mlattice R.λs:sequence (pordered_set_of_excedence ml).λk.λn. δ (s n) k.
+(*
+notation "s ⇝ 'Zero'" non associative with precedence 50 for @{'tends0 $s }.
+  
+interpretation "tends to" 'tends s x = 
+  (cic:/matita/sequence/tends0.con _ s).    
+*)
+
+alias symbol "leq" = "ordered sets less or equal than".
+alias symbol "and" = "constructive and".
+alias symbol "exists" = "constructive exists (Type)".
+lemma carabinieri: (* non trova la coercion .... *)
+  ∀R.∀ml:mlattice R.∀an,bn,xn:sequence (pordered_set_of_excedence ml).
+    (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
+    ∀x:ml. tends0 ? (d2s ? ml an x) → tends0 ? (d2s ? ml bn x) →
+    tends0 ? (d2s ? ml xn x).
+intros (R ml an bn xn H x Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %.
+intros (e He);
+elim (Ha ? He) (n1 H1); clear Ha; elim (Hb e He) (n2 H2); clear Hb;
+constructor 1; [apply (n1 + n2);] intros (n3 Hn3);
+cut (n1<n3) [2: 
+  generalize in match Hn3; elim n2; [rewrite > sym_plus in H3; assumption]
+  apply H3; rewrite > sym_plus in H4; simplify in H4; apply lt_S_to_lt; 
+  rewrite > sym_plus in H4; assumption;]
+elim (H1 ? Hcut) (H3 H4); clear Hcut;
+cut (n2<n3) [2: 
+  generalize in match Hn3; elim n1; [assumption]
+  apply H5; simplify in H6; apply lt_S_to_lt; assumption] 
+elim (H2 ? Hcut) (H5 H6); clear Hcut;
+elim (H n3) (H7 H8); clear H H1 H2; 
+lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym;
+cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2:
+  apply (le_transitive ???? (mtineq ???? (an n3)));
+  lapply (le_mtri ????? H7 H8);
+  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin);
+  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [2:
+    apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
+    apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
+    apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??));
+    apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
+    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear Hletin1;
+  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[
+    apply feq_plusr; apply msymmetric;]
+  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[
+    apply feq_plusr; assumption;]
+  ]
+[2: split; [
+  apply (lt_le_transitive ????? (mpositive ????));
+  split; elim He; [apply  le_zero_x_to_le_opp_x_zero|
+  cases t1; 
+    [left; apply exc_zero_opp_x_to_exc_x_zero;
+     apply (Ex≫ ? (eq_opp_opp_x_x ??));
+    |right;  apply exc_opp_x_zero_to_exc_zero_x;
+     apply (Ex≪ ? (eq_opp_opp_x_x ??));]] assumption;]
+clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2;
+
+  
 (* 3.17 conclusione: δ x y ≈ 0 *)
 (* 3.20 conclusione: δ x y ≈ 0 *)
 (* 3.21 sup forte