X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=78046c688ead8c5561ad629785fce67f98ea52c1;hb=8da8820a77f2104dd1bf17c01fa77f75ee31c8fb;hp=79bc27ee194ab8091b26acc3a805094b005e0261;hpb=2de5506abeebb60e552d68b828d8c481ee7be742;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 79bc27ee1..78046c688 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -180,6 +180,14 @@ lemma subst_excess_: ∀e:excess. ∀e1: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.
@@ -199,8 +207,8 @@ lemma subst_excess:
    |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 H1;
-   |7: clear H1; apply H2;]]
+   |6: clear H2; apply hole; apply H1;
+   |7: clear H1; apply hole; apply H2;]]
 qed.
 
 lemma excess_of_excess_base: excess_base → excess.
@@ -212,251 +220,156 @@ 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.
+
+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.
-  
-  mancano le 4 proprietà riscritte con p
-    
+  (∀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.
-intros (l eb H); apply (subst_excess l);
-  [apply (subst_excess_ l);
-    [apply (subst_dual_excess l);
-      [apply (subst_excess_base l eb);
-      |apply H;]
-    | change in \vdash (% -> % -> ?) with (exc_carr eb);
-    letin xxx \def (ap2exc l); clearbody xxx;
-    change in xxx:(%→%→?) with (Type_OF_semi_lattice l);
-    whd in ⊢ (?→?→? (? %) ? ?→?); 
-    unfold exc_ap;
-    simplify in ⊢ (?→?→%→?);
-
-intros 2;
-generalize in ⊢ (% -> ?); intro P;
-generalize in match x in ⊢ % as x;
-generalize in match y in ⊢ % as y; clear x y;
-
-    
-cases H; simplify;
-
-
-cut (Πy:exc_carr eb
-.Πx:exc_carr eb
- .match 
-  (match H
-   in eq
-   return 
-  λright_1:Type
-  .(λmatched:eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1
-    .eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1)
-   with 
-  [refl_eq⇒refl_eq Type (Type_OF_excess_ (excess__OF_semi_lattice l))])
-   in eq
-   return 
-  λright_1:Type
-  .(λmatched:eq Type (ap_carr (exc_ap (excess__OF_semi_lattice l))) right_1
-    .right_1→right_1→Type)
-   with 
-  [refl_eq⇒ap_apart (exc_ap (excess__OF_semi_lattice l))] y x);[2:
-  
-
-    change in ⊢ (?→?→? % ? ?→?) with (exc_ap_ (excess__OF_semi_lattice l));
-    generalize in match H in \vdash (? -> %); cases H;  
-    cases H;
-    
-    
-normalize in ⊢ (?→?→?→? (? (? (? ? (% ? ?) ?)) ? ?) ?);
-whd in ⊢ (?→?→? % ? ?→?); change in ⊢ (?→?→? (? % ? ? ? ?) ? ?→?) with (exc_carr eb);
-cases H;
-      change in ⊢ (?→?→? % ? ?→?) with (exc_ap l);
-(subst_dual_excess (excess__OF_semi_lattice l)
- (subst_excess_base (excess_dual_OF_semi_lattice l) eb) H)
-      
-      
-       unfold subst_excess_base;
-        unfold mk_excess_dual_smart;
-        unfold excess__OF_semi_lattice;
-        unfold excess_dual_OF_semi_lattice;
-        unfold excess_dual_OF_semi_lattice;
-        
-      reflexivity]
-*)
+[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_with1:   (subst_excess_
-                  (subst_dual_excess
-                    (subst_excess_base 
-                      (excess_dual_OF_excess (sl_exc latt_jcarr_))
-                      (excess_base_OF_excess (sl_exc latt_mcarr))))) =
-                sl_exc latt_jcarr_;   
-  
-*)  
-  latt_with1: excess_base_OF_excess1 (sl_exc latt_jcarr_) =  excess_base_OF_excess (sl_exc latt_mcarr);
-  latt_with2: excess_base_OF_excess (sl_exc latt_jcarr_) =  excess_base_OF_excess1 (sl_exc latt_mcarr);
-  latt_with3: apartness_OF_excess (sl_exc latt_jcarr_) = apartness_OF_excess (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   
 }.
 
-axiom FALSE: False.
-
 lemma latt_jcarr : lattice_ → semi_lattice.
-intro l;
-apply mk_semi_lattice;
-  [apply mk_excess;
-    [apply mk_excess_;
-      [apply (mk_excess_dual_smart l);
-      |apply (exc_ap l);
-      |reflexivity]
-    |unfold mk_excess_dual_smart; simplify;
-     intros (x y H); cases (ap2exc ??? H); [right|left]  assumption;
-    |unfold mk_excess_dual_smart; simplify;
-     intros (x y H);cases H; apply exc2ap;[right|left] assumption;]] 
-unfold mk_excess_dual_smart; simplify;
-[1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l);
-    simplify; unfold apartness_OF_lattice_; 
-    cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l)); 
-|2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify;
-    unfold apartness_OF_lattice_;
-    cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l));
-|3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
-    cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l));
-|4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
-    cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l));
-|5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
-    cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l));
-|7: 
-(*
-unfold excess_base_OF_lattice_; 
-    change in ⊢ (?→?→? ? (% ? ?) ?)
-    with (match latt_with3 l
- in eq
- return 
-λright_1:apartness
-.(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1
-  .ap_carr right_1→ap_carr right_1→ap_carr right_1)
- with 
-[refl_eq⇒sl_meet (latt_jcarr_ l)]
- : ?
-);
-  change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?)
-  with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l)));
-  unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
-  simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
-change in ⊢ (?→?→? ? (% ? ?) ?) with
-  (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq
-   return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R)
-   with [refl_eq⇒ 
-     (match latt_with3 l in eq
-     return 
-       (λright:apartness
-        .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
-          .ap_carr right→ap_carr right→ap_carr right))
-     with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
-     :
-     exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
-      →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
-       →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
-     )
-   ]);
-   generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
-   unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?);
-   cases (latt_with1 l);
-  change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?)
-  with ((λx.ap_carr x) (latt_mcarr l));
-  simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?);
-  cases (latt_with3 l);
-   
-   change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
-   simplify in ⊢ (% → ?);
-   change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
-     with ((λx.ap_carr x) (apartness_OF_lattice_ l));
-   unfold apartness_OF_lattice_;  
-   cases (latt_with3 l); simplify;
-   change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
-   unfold excess_base_OF_lattice_;
-   cases (latt_with1 l); simplify;
-   change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
-   change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
-     with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
-   simplify;
-   intro H;
-   unfold excess_base_OF_semi_lattice1;
-   unfold excess_base_OF_excess1;
-   unfold excess_base_OF_excess_1;
-   change 
-*)
-
-change in ⊢ (?→?→? ? (% ? ?) ?) with
-  (match refl_eq ? (Type_OF_lattice_ l) in eq
-   return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R)
-   with [refl_eq⇒ 
-     match latt_with3 l in eq
-     return 
-       (λright:apartness
-        .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
-          .ap_carr right→ap_carr right→ap_carr right))
-     with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
-   ]);
-   generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
-   change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
-   simplify in ⊢ (% → ?);
-   change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
-     with ((λx.ap_carr x) (apartness_OF_lattice_ l));
-   unfold apartness_OF_lattice_;  
-   cases (latt_with3 l); simplify;
-   change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
-   unfold excess_base_OF_lattice_;
-   cases (latt_with1 l); simplify;
-   change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
-   change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
-     with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
-   simplify;
-   intro H;
-   change in ⊢ (?→?→%) with (le (mk_excess_base 
-          ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
-          ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
-          ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
-          ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
-        ) (match H
- in eq
- return 
-λR:Type
-.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R
-  .R→R→R)
- with 
-[refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y); 
- simplify in ⊢ (?→?→? (? % ???) ? ?); 
- change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
- with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
- simplify in  ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?);
- lapply (match H in eq return 
-        λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right.
-       
-∀x:right
-.∀y:right
- .le
-  (mk_excess_base right ???)
-  (match e
-    in eq
-    return 
-   λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R)
-    with 
-   [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y
-        with [refl_eq ⇒ ?]) as XX;
-  [cases e; apply (exc_excess (latt_jcarr_ l)); 
-  |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l)); 
-  |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l)); 
-  ||apply XX|
-  |apply XX;
-        
-         simplify; apply (sl_lem);
-|elim FALSE]
+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.