X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=78046c688ead8c5561ad629785fce67f98ea52c1;hb=5b83f526bc4c63424313df91173b844699eada96;hp=ef02134256330b43f7a4006fed38a7702a9546a6;hpb=9483f7e6c85ec11f88bdb219b2cebad2039b1a74;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index ef0213425..78046c688 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -30,8 +30,8 @@ lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
 intro l;
 apply mk_excess;
 [1: apply mk_excess_;
-    [1: 
-    
+    [1: apply mk_excess_dual_smart;
+         
   apply (mk_excess_base (sl_carr l));
     [1: apply (λa,b:sl_carr l.a # (a ✗ b));
     |2: unfold; intros 2 (x H); simplify in H;
@@ -161,22 +161,216 @@ unfold excl; simplify;
 qed.
 *)
 
+(* ED(≰,≱) → EB(≰') → ED(≰',≱') *)
+lemma subst_excess_base: excess_dual → excess_base → excess_dual.
+intros; apply (mk_excess_dual_smart e1);
+qed.
+
+(* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *)
+lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_.
+intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity;
+qed. 
+
+(* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *)
+alias symbol "nleq" = "Excess excess_".
+lemma subst_excess_: ∀e:excess. ∀e1:excess_. 
+  (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) →
+  (∀y,x:e1.y ≰ x ∨ x ≰ y →  y # x) →
+  excess.
+intros (e e1 H1 H2); apply (mk_excess e1 H1 H2); 
+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 _ _).
+
+
+axiom FALSE : False.
+
+(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
+lemma subst_excess: 
+  ∀l:semi_lattice.
+  ∀e:excess. 
+  ∀p:exc_ap l = exc_ap e.
+  (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) →
+  (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) → 
+  semi_lattice.
+[1,2:intro M;
+ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+ cases p; apply M;
+|intros (l e p H1 H2);
+ apply (mk_semi_lattice e);
+   [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+     cases p; simplify; apply (sl_meet l);
+   |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl;
+   |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm;
+   |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc;  
+   |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm;
+   |6: clear H2; apply hole; apply H1;
+   |7: clear H1; apply hole; apply H2;]]
+qed.
+
+lemma excess_of_excess_base: excess_base → excess.
+intro eb;
+apply mk_excess;
+  [apply (mk_excess_ (mk_excess_dual_smart eb));
+    [apply (apartness_of_excess_base eb);
+    |reflexivity]
+  |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.
+
+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 → (?(eq sl)) x3 ((?(sl_meet sl)) x3 y3)) →
+  (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) → 
+  semi_lattice.
+[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);
+  |apply subst_excess_base_in_excess_preserves_apartness;
+  |change in ⊢ (%→%→?) with ((λx.ap_carr x) (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)); simplify;
+   intros 3 (x y LE);
+   generalize in match (H3 ?? LE);
+   generalize in match H1 as H1;generalize in match H2 as H2; 
+   generalize in match x as x; generalize in match y as y;
+   cases FALSE;
+   (*
+   (reduce in H ⊢ %; cases H; simplify; intros; assumption); 
+   
+   
+   cases (subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2); simplify;
+   change in x:(%) with (exc_carr eb);
+   change in y:(%) with (exc_carr eb);
+   generalize in match OK; generalize in match x as x; generalize in match y as y;
+   cases H; simplify; (* funge, ma devo fare 2 rewrite in un colpo solo *)
+   *) 
+  |cases FALSE;
+  ] 
+qed.
 
 record lattice_ : Type ≝ {
   latt_mcarr:> semi_lattice;
   latt_jcarr_: semi_lattice;
-  latt_with:  sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr)
+  W1:?; W2:?; W3:?; W4:?; W5:?;
+  latt_with1: latt_jcarr_ = subst_excess_base_in_semi_lattice latt_jcarr_
+    (excess_base_OF_semi_lattice latt_mcarr) W1 W2 W3 W4 W5   
 }.
 
 lemma latt_jcarr : lattice_ → semi_lattice.
-intro l;
-apply (mk_semi_lattice (dual_exc l)); 
-unfold excess_OF_lattice_;
-cases (latt_with l); simplify;
-[apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc|
-apply sl_strong_extm| apply sl_le_to_eqm|apply sl_lem]
-qed. 
- 
+intro l; apply (subst_excess_base_in_semi_lattice (latt_jcarr_ l) (excess_base_OF_semi_lattice (latt_mcarr l)) (W1 l) (W2 l) (W3 l) (W4 l) (W5 l));
+qed.
+    
 coercion cic:/matita/lattice/latt_jcarr.con.
 
 interpretation "Lattice meet" 'and a b =