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

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 0b464aeec..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.
@@ -245,11 +253,6 @@ apply (subst_dual_excess e_);
   |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.
@@ -315,10 +318,12 @@ 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);
+rewrite < (tech2 e eb );
 reflexivity;
 qed.
-   
+ 
+ 
+ 
 alias symbol "nleq" = "Excess base excess".
 lemma subst_excess_base_in_semi_lattice: 
   ∀sl:semi_lattice.
@@ -334,225 +339,37 @@ 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;
-  |
-  unfold apartness_OF_semi_lattice;
-   letin xxx \def subst_excess_preserves_aprtness; clearbody xxx;
-  
-  
-  clear H3 H4; unfold apartness_OF_semi_lattice;
-   generalize in match (sl_exc sl);
-   intro; whd in \vdash (? ? ? %); unfold in ⊢ (? ? ? (? ? match ? (? %) return ? with [_⇒?] ? ? ?));
+  |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); 
    
    
-  
-  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;
-  |
-  |
+   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: latt_jcarr_ = subst latt_jcarr (exc_dual_dual latt_mcarr)*) 
-(*  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.