From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 4 Feb 2008 10:57:45 +0000 (+0000)
Subject: snapshot
X-Git-Tag: make_still_working~5637
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=73fd8aa35ba65194053143eb51da0bbb090cfdc7;p=helm.git

snapshot
---

diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends
index 541721dbe..dcbfcc6f0 100644
--- a/helm/software/matita/dama/depends
+++ b/helm/software/matita/dama/depends
@@ -1,6 +1,6 @@
-metric_lattice.ma lattice.ma metric_space.ma
+metric_lattice.ma excess.ma lattice.ma metric_space.ma
 metric_space.ma ordered_divisible_group.ma
-sandwich.ma nat/orders.ma nat/plus.ma tend.ma
+sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma tend.ma
 premetric_lattice.ma lattice.ma metric_space.ma
 ordered_group.ma group.ma
 divisible_group.ma group.ma nat/orders.ma
@@ -12,7 +12,7 @@ prevalued_lattice.ma ordered_group.ma
 excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
 sandwich_corollary.ma sandwich.ma
 Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
-limit.ma excess.ma infsup.ma tend.ma
+limit.ma excess.ma infsup.ma metric_lattice.ma tend.ma
 lattice.ma excess.ma
 tend.ma metric_space.ma nat/orders.ma sequence.ma
 constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 96252c6ee..88db12061 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -212,38 +212,168 @@ apply mk_excess;
   |2,3: intros; assumption]
 qed. 
 
+lemma subst_excess_preserves_aprtness:
+  ∀l:semi_lattice.
+  ∀e:excess.
+  ∀p,H1,H2. 
+  exc_ap l = exc_ap (subst_excess l e p H1 H2).
+intros; 
+unfold subst_excess;
+simplify; assumption;
+qed.
+
+
+lemma subst_excess__preserves_aprtness:
+  ∀l:excess.
+  ∀e:excess_base.
+  ∀p,H1,H2. 
+  exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2).
+intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify);
+(unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p);
+intros; cases p;
+reflexivity;
+qed.
+
+lemma subst_excess_base_in_excess_:
+  ∀d:excess_.
+  ∀eb:excess_base.
+  ∀p:exc_carr d = exc_carr eb.
+  excess_.
+intros (e_ eb);
+apply (subst_dual_excess e_);
+  [apply (subst_excess_base e_ eb);
+  |assumption]
+qed.
+
+definition hole ≝ λT:Type.λx:T.x.
+
+notation < "\ldots" non associative with precedence 50 for @{'hole}.
+interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _).
+
+lemma subst_excess_base_in_excess:
+  ∀d:excess.
+  ∀eb:excess_base.
+  ∀p:exc_carr d = exc_carr eb.
+  (∀y1,x1:eb. (?(ap_apart d)) y1  x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
+  (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 →  (?(ap_apart d)) y2 x2) →
+  excess.
+[1,3,4:apply Type|2,5:intro f; cases p; apply f]
+intros (d eb p H1 H2);
+apply (subst_excess_ d);
+  [apply (subst_excess_base_in_excess_ d eb p);
+  |apply hole; clear H2; 
+   change in ⊢ (%→%→?) with (exc_carr eb);      
+   change in ⊢ (?→?→?→? (? % ? ?) (? % ? ?)) with eb; intros (y x H3);
+   apply H1; generalize in match H3;
+   unfold ap_apart; unfold subst_excess_base_in_excess_;
+   unfold subst_dual_excess; simplify; 
+   generalize in match x;
+   generalize in match y;
+   cases p; simplify; intros; assumption;
+  |apply hole; clear H1; 
+   change in ⊢ (%→%→?) with (exc_carr eb);      
+   change in ⊢ (?→?→? (? % ? ?) (? % ? ?)→?) with eb; intros (y x H3);
+   unfold ap_apart; unfold subst_excess_base_in_excess_;
+   unfold subst_dual_excess; simplify; generalize in match (H2 ?? H3);
+   generalize in match x; generalize in match y; cases p;
+   intros; assumption;]
+qed.    
+
+lemma tech1: ∀e:excess.
+ ∀eb:excess_base.
+ ∀p,H1,H2.
+ exc_ap e = exc_ap_  (subst_excess_base_in_excess e eb p H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; simplify;
+unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; simplify; reflexivity;
+qed.
+
+lemma tech2: 
+ ∀e:excess_.∀eb.∀p.
+  exc_ap e = exc_ap (mk_excess_ (subst_excess_base e eb) (exc_ap e) p).
+intros (e eb p);unfold exc_ap; simplify; cases p; simplify; reflexivity;
+qed.
+  
+(*
+lemma eq_fap:
+ ∀a1,b1,a2,b2,a3,b3,a4,b4,a5,b5.
+ a1=b1 → a2=b2 → a3=b3 → a4=b4 → a5=b5 → mk_apartness a1 a2 a3 a4 a5 = mk_apartness b1 b2 b3 b4 b5.
+intros; cases H; cases H1; cases H2; cases H3; cases H4; reflexivity;
+qed.
+*)
+
+lemma subst_excess_base_in_excess_preserves_apartness:
+ ∀e:excess.
+ ∀eb:excess_base.
+ ∀H,H1,H2.
+ apartness_OF_excess e =
+ apartness_OF_excess (subst_excess_base_in_excess e eb H H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; unfold apartness_OF_excess;
+simplify in ⊢ (? ? ? (? %));
+rewrite < (tech2 e eb);
+reflexivity;
+qed.
+   
+alias symbol "nleq" = "Excess base excess".
 lemma subst_excess_base_in_semi_lattice: 
   ∀sl:semi_lattice.
   ∀eb:excess_base.
   ∀p:exc_carr sl = exc_carr eb.
   (∀y1,x1:eb. (?(ap_apart sl)) y1  x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
   (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 →  (?(ap_apart sl)) y2 x2) →
-  (∀x3,y3:eb.(le eb) x3 y3 → (?(ap_apart sl)) x3 ((?(sl_meet sl)) x3 y3)) →
+  (∀x3,y3:eb.(le eb) x3 y3 → (?(eq sl)) x3 ((?(sl_meet sl)) x3 y3)) →
   (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) → 
   semi_lattice.
-[2,3,7,9,10: apply Type|4:apply (exc_carr eb);
-|1,5,6,8,11: intro f; cases p; apply f;]
-intros (sl eb H H1 H2 H3 H4); apply (subst_excess sl);
-  [apply (subst_excess_ sl);
-    [apply (subst_dual_excess sl);
-      [apply (subst_excess_base sl eb);
-      |apply H;]
-    | (*clear H2 H3 H4;*) 
-      change in ⊢ (% -> % -> ?) with (exc_carr eb);
-      unfold subst_excess_base; unfold mk_excess_dual_smart;
-      unfold subst_dual_excess; simplify in ⊢ (?→?→?→%);
-      (unfold exc_ap; simplify in ⊢ (?→?→? % ? ?→?));
-      simplify; intros (x y H2); apply H1;
-      generalize in match H2;
-      generalize in match x as x;
-      generalize in match y as y; (*clear H1 H2 x y;*)
-      change in ⊢ (?→?→match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?→?)
-      with (Type_OF_semi_lattice sl); 
-      change in ⊢ (?→?→match match ? return λ_:?.(λ_:? ? % ?.? ? % ?) with [_⇒? ? %] return ? with [_⇒?] ??→?) with (Type_OF_semi_lattice sl);
-      cases H; intros; assumption; (* se faccio le clear... BuM! *)
-    | clear H1 H3 H4;
+[2:apply Prop|3,7,9,10:apply Type|4:apply (exc_carr eb)|1,5,6,8,11:intro f; cases p; apply f;]
+intros (sl eb H H1 H2 H3 H4); 
+apply (subst_excess sl);
+  [apply (subst_excess_base_in_excess sl eb H H1 H2);
+  |rewrite > (subst_excess_preserves_aprtness sl);
+  
+  
+  clear H3 H4; unfold apartness_OF_semi_lattice;
+   generalize in match (sl_exc sl);
+   intro; whd in \vdash (? ? ? %); unfold in ⊢ (? ? ? (? ? match ? (? %) return ? with [_⇒?] ? ? ?));
+   
+   
+  
+  apply (subst_excess__preserves_aprtness (sl_exc sl) eb H H1 H2); 
+  | (clear H4;change in ⊢ (%→%→?) with (exc_carr eb);change in ⊢ (?→?→? % ? ?→?) with eb; simplify);
+    intros 3 (x y LE);
+    (generalize in ⊢ (? (? (? ? ? % ?)) ? ?); intro P1);
+    (generalize in ⊢ (? (? (? ? ? ? %)) ? ?); intro P2);
+    generalize in match (H3 x y LE);
+    generalize in match x as x;
+    generalize in match y as y;
+    generalize in ⊢ (?→?→?→? (? (? ? ? % ?)) ? ?); intro P1; 
+    generalize in ⊢ (?→?→?→? (? (? ? ? ? %)) ? ?); intro P2;
+    change (%->?) with (ap_carr ());
+    
+    cases H;
     
-    ]
+    lapply (pippo sl eb H P1 P2);
+    rewrite > Hletin;
+    intros (x y H5); generalize in match (H3 x y H5); clear H4;  
+    generalize in ⊢ (?→? (? (? ? ? % ?)) ? ?); intro P;
+    generalize in ⊢ (?→? (? (? ? ? ? %)) ? ?); intro Q;
+    
+    
+    change in ⊢ (?→? (? (? ? (? % ? ?) ? ?)) ? ?) with ((λx.excess_carr x) sl); simplify;
+    change in ⊢ (?→? (? (? ? (? ? (? % ?) ?) ? ?)) ? ?) with ((λx.excess_dual_OF_excess x) sl);simplify;
+    
+    rewrite < (subst_excess__preserves_aprtness (sl_exc sl) eb H P Q); 
+    generalize in ⊢ (?→?→?→? ? ? (match ? ? ? ? % ? return ? with [_⇒?] ? ?)); intro A;
+    generalize in ⊢ (?→?→?→? ? ? (match ? ? ? ? ? % return ? with [_⇒?] ? ?)); intro B;
+    simplify;
+  |
+  |
+  ] 
+qed.
 
 record lattice_ : Type ≝ {
   latt_mcarr:> semi_lattice;