From f86ba51fa84583b5963fca03687cd23b838a99f5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 Nov 2007 17:57:32 +0000
Subject: [PATCH] carabinieri almost done

---
 helm/software/matita/dama/excedence.ma      |  8 +++
 helm/software/matita/dama/metric_lattice.ma | 61 +++++++++++++++++++++
 helm/software/matita/dama/ordered_set.ma    |  2 +
 helm/software/matita/dama/sequence.ma       |  4 +-
 4 files changed, 73 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 42d53a5dc..ab7a53af0 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -199,6 +199,14 @@ whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)]
 cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)]
 right; assumption;
 qed.
+
+lemma le_lt_transitive: ∀A:excedence.∀x,y,z:A.x ≤ y → y < z → x < z.
+intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)]
+whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)]
+cases (exc_cotransitive ??? x EXx) (EXz EXz); [right; assumption]
+cases LE; assumption;
+qed.
+
     
 lemma le_le_eq: ∀E:excedence.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index a4ca3b4f4..0e92f0a89 100644
--- 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
diff --git a/helm/software/matita/dama/ordered_set.ma b/helm/software/matita/dama/ordered_set.ma
index 709126c14..7178bd9a7 100644
--- a/helm/software/matita/dama/ordered_set.ma
+++ b/helm/software/matita/dama/ordered_set.ma
@@ -32,6 +32,8 @@ intros (E); apply (mk_pordered_set E); apply (mk_is_porder_relation);
 [apply le_reflexive|apply le_transitive|apply le_antisymmetric]
 qed. 
 
+coercion cic:/matita/ordered_set/pordered_set_of_excedence.con.
+
 alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con".
 alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con".
 alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con".
diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma
index 52baef839..40e2f477a 100644
--- a/helm/software/matita/dama/sequence.ma
+++ b/helm/software/matita/dama/sequence.ma
@@ -61,10 +61,10 @@ qed.
 include "ordered_group.ma".
 include "nat/orders.ma".
 
-definition tends ≝ 
+definition tends0 ≝ 
   λO:ogroup.λs:sequence O.
     ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
-
+    
 definition increasing ≝ 
   λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
 
-- 
2.39.2