merged commits, the same proof is missing :-(

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 9e8b473b6e8ff85d753ed67da84af87aefa9b208..12b348cc35f40afeb151ce36669e0a1f9d9c1d4a 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -17,11 +17,7 @@ include "logic/cprop_connectives.ma".
 
 inductive bool : Type := true : bool | false : bool.
 
-<<<<<<< .mine
-lemma BOOL : setoid.
-=======
 lemma BOOL : objs1 SET.
->>>>>>> .r9407
 constructor 1; [apply bool] constructor 1;
 [ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]);
 | whd; simplify; intros; cases x; apply I;
@@ -42,17 +38,8 @@ lemma IF_THEN_ELSE_p :
 intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H;
 qed. 
 
-<<<<<<< .mine
-interpretation "unary morphism comprehension with no proof" 'comprehension T P = 
-=======
-lemma if_then_else : ∀T:SET. ∀a,b:T. arrows1 SET BOOL T.
-intros; constructor 1; intros; 
-[ apply (match c with [ true ⇒ t | false ⇒ t1 ]);
-| apply (IF_THEN_ELSE_p T t t1 a a' H);]
-qed.
 
-interpretation "mk " 'comprehension T P = 
->>>>>>> .r9407
+interpretation "unary morphism comprehension with no proof" 'comprehension T P = 
   (mk_unary_morphism T _ P _).
 
 notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
@@ -63,24 +50,13 @@ for @{ 'comprehension_by $s (λ${ident i}:$_. $p) $by}.
 interpretation "unary morphism comprehension with proof" 'comprehension_by s \eta.f p = 
   (mk_unary_morphism s _ f p).
 
-<<<<<<< .mine
-=======
-definition A : ∀S:SET.∀a,b:S.arrows1 SET BOOL S.
-apply (λS,a,b.{ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b] | IF_THEN_ELSE_p S a b}).
-qed.
 
->>>>>>> .r9407
 record OAlgebra : Type := {
   oa_P :> SET;
   oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
-<<<<<<< .mine
-  oa_meet: ∀I:setoid.unary_morphism (unary_morphism_setoid I oa_P) oa_P;
-  oa_join: ∀I:setoid.unary_morphism (unary_morphism_setoid I oa_P) oa_P;
-=======
   oa_meet: ∀I:SET.unary_morphism (arrows1 SET I oa_P) oa_P;
   oa_join: ∀I:SET.unary_morphism (arrows1 SET I oa_P) oa_P;
->>>>>>> .r9407
   oa_one: oa_P;
   oa_zero: oa_P;
   oa_leq_refl: ∀a:oa_P. oa_leq a a; 
@@ -94,17 +70,10 @@ record OAlgebra : Type := {
   oa_overlap_preservers_meet: 
       ∀p,q.oa_overlap p q → oa_overlap p 
        (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
-<<<<<<< .mine
-  oa_join_split:
-      ∀I:setoid.∀p.∀q:I ⇒  oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
-  (*
-  oa_base : setoid;
-=======
      (*(oa_meet BOOL (if_then_else oa_P p q));*)
   oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *)
       ∀I:SET.∀p.∀q:arrows1 SET I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
   (*oa_base : setoid;
->>>>>>> .r9407
   oa_enum : ums oa_base oa_P;
   oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q
   *)
@@ -181,16 +150,8 @@ intros (P Q);
 constructor 1;
 [ apply (ORelation P Q);
 | constructor 1;
-<<<<<<< .mine
-   [ alias symbol "and" = "constructive and".
-     apply (λp,q. And4 (∀a.p⎻* a = q⎻* a) (∀a.p⎻ a  = q⎻ a)
-                       (∀a.p a   = q a)   (∀a.p* a  = q* a)); 
-   | whd; simplify; intros; repeat split; intros; apply refl;
-=======
-   [ apply (λp,q. eq1 ? p⎻* q⎻* ∧ eq1 ? p⎻ q⎻ ∧ eq1 ? p q ∧ eq1 ? p* q* ); 
+   [ apply (λp,q. And4 (eq1 ? p⎻* q⎻* ) (eq1 ? p⎻ q⎻) (eq1 ? p q) (eq1 ? p* q* )); 
    | whd; simplify; intros; repeat split; intros; apply refl1;
->>>>>>> .r9407
-<<<<<<< .mine
    | whd; simplify; intros; cases H; clear H; split; 
      intro a; apply sym; generalize in match a;assumption;
    | whd; simplify; intros; cases H; cases H1; clear H H1; split; intro a;
@@ -199,24 +160,7 @@ constructor 1;
      | apply (.= (H4 a)); apply H8;
      | apply (.= (H5 a)); apply H9;]]]
 qed.  
-=======
-   | whd; simplify; intros; cases H; cases H1; cases H3; clear H H3 H1;
-     repeat split; intros; apply sym1; assumption;
-   | whd; simplify; intros; cases H; cases H1; cases H2; cases H4; cases H6; cases H8;
-     repeat split; intros; clear H H1 H2 H4 H6 H8; apply trans1;
-      [2: apply H10;
-      |5: apply H11;
-      |8: apply H7;
-      |11: apply H3;
-      |1,4,7,10: skip
-      |*: assumption
-      ]]]
-qed.
->>>>>>> .r9407
 
-<<<<<<< .mine
-definition ORelation_composition : ∀P,Q,R. 
-=======
 lemma hint1 : ∀P,Q. ORelation_setoid P Q → arrows1 SET P Q. intros; apply (or_f ?? c);qed.
 coercion hint1.
 
@@ -226,35 +170,12 @@ coercion hint3.
 lemma hint2: OAlgebra → setoid. intros; apply (oa_P o). qed.
 coercion hint2.
 
-definition composition : ∀P,Q,R. 
->>>>>>> .r9407
+definition ORelation_composition : ∀P,Q,R. 
   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
 intros;
 constructor 1;
 [ intros (F G);
   constructor 1;
-<<<<<<< .mine
-    [ apply {x ∈ P | G (F x)}; intros; simplify; apply (†(†H));
-    | apply {x ∈ P | G⎻* (F⎻* x)}; intros; simplify; apply (†(†H));
-    | apply {x ∈ R | F* (G* x)}; intros; simplify; apply (†(†H));
-    | apply {x ∈ R | F⎻ (G⎻ x)}; intros; simplify; apply (†(†H));
-    | intros; simplify; 
-      lapply (or_prop1 ?? G (F p) q) as H1; lapply (or_prop1 ?? F p (G* q)) as H2;
-      split; intro H; 
-        [ apply (if1 ?? H2); apply (if1 ?? H1); apply H;
-        | apply (fi1 ?? H1); apply (fi1 ?? H2); apply H;] 
-    | intros; simplify;
-      lapply (or_prop2 ?? G p (F⎻* q)) as H1; lapply (or_prop2 ?? F (G⎻ p) q) as H2;
-      split; intro H;
-        [ apply (if1 ?? H1); apply (if1 ?? H2); apply H;   
-        | apply (fi1 ?? H2); apply (fi1 ?? H1); apply H;]
-    | intros; simplify;
-      lapply (or_prop3 ?? F p (G⎻ q)) as H1; lapply (or_prop3 ?? G (F p) q) as H2;
-      split; intro H;
-        [ apply (if1 ?? H1); apply (if1 ?? H2); apply H;   
-        | apply (fi1 ?? H2); apply (fi1 ?? H1); apply H;]]
-| intros; simplify; split; simplify; intros; elim DAEMON;]
-=======
   [ apply (G ∘ F);
   | apply (G⎻* ∘ F⎻* );
   | apply (F* ∘ G* );
@@ -279,7 +200,6 @@ constructor 1;
      lapply (.= ((†H1)‡#)); [8: apply Hletin;
    [ apply trans1; [2: lapply (prop1); [apply Hletin;
 *)]
->>>>>>> .r9407
 qed.
 
 definition OA : category1.
@@ -287,21 +207,11 @@ split;
 [ apply (OAlgebra);
 | intros; apply (ORelation_setoid o o1);
 | intro O; split;
-<<<<<<< .mine
-  [1,2,3,4: constructor 1; [1,3,5,7:apply (λx.x);|*:intros;assumption]
-  |5,6,7:intros;split;intros; assumption;] 
-|4: apply ORelation_composition;
-|*: elim DAEMON;]
-qed. 
-
-
-
-=======
   [1,2,3,4: apply id1;
   |5,6,7:intros; apply refl1;] 
-| apply composition;
-| intros; repeat split; unfold composition; simplify;
-  [1,3: apply (comp_assoc1); | 2,4: apply ((comp_assoc1 ????????) \sup -1);]
-| intros; repeat split; unfold composition; simplify; apply id_neutral_left1;
-| intros; repeat split; unfold composition; simplify; apply id_neutral_right1;]
-qed.>>>>>>> .r9407
+| apply ORelation_composition;
+| intros; repeat split; unfold ORelation_composition; simplify;
+  [1,3: apply (comp_assoc1); | 2,4: apply ((comp_assoc1 :?) ^ -1);]
+| intros; repeat split; unfold ORelation_composition; simplify; apply id_neutral_left1;
+| intros; repeat split; unfold ORelation_composition; simplify; apply id_neutral_right1;]
+qed.