O-Basic Topologies do form a category.

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-algebra.ma

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 78372e72fc6e2394234451fd10f8e30b5728cdb7..cb211341427ed8cc934f3e390d76b611af124f80 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -26,11 +26,6 @@ constructor 1; [apply bool] constructor 1;
   try assumption; apply I]
 qed.
 
-definition setoid_OF_SET: objs1 SET → setoid.
- intros; apply o; qed.
-
-coercion setoid_OF_SET.
-
 lemma IF_THEN_ELSE_p :
   ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → 
     (λm.match m with [ true ⇒ a | false ⇒ b ]) x =
@@ -50,9 +45,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).
 
+(* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
+   lattices, Definizione 0.9 *)
+(* USARE L'ESISTENZIALE DEBOLE *)
+(* Far salire SET usando setoidi1 *)
 record OAlgebra : Type := {
   oa_P :> SET;
-  oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
+  oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1, CPROP importante che sia small *)
   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
   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;
@@ -62,16 +61,21 @@ record OAlgebra : Type := {
   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
+  (* Errore: = in oa_meet_inf e oa_join_sup *)
   oa_meet_inf: ∀I.∀p_i.∀p:oa_P.oa_leq p (oa_meet I p_i) → ∀i:I.oa_leq p (p_i i);
   oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
-  oa_overlap_preservers_meet: 
+  (* preservers!! (typo) *)
+  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 });
+  (* ⇔ deve essere =, l'esiste debole *)
   oa_join_split:
       ∀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;
+  1) enum non e' il nome giusto perche' non e' suriettiva
+  2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
   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
   *)
@@ -89,19 +93,41 @@ notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\
 non associative with precedence 50 for @{ 'oa_meet $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+
+(*
 notation < "hovbox(a ∧ b)" left associative with precedence 35
 for @{ 'oa_meet_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
-
+*)
 notation > "hovbox(∧ f)" non associative with precedence 60
 for @{ 'oa_meet $f }.
+(*
 notation > "hovbox(a ∧ b)" left associative with precedence 50
 for @{ 'oa_meet (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
-
+*)
 interpretation "o-algebra meet" 'oa_meet f = 
   (fun_1 __ (oa_meet __) f).
 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = 
   (fun_1 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
 
+definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+intros; split;
+[ intros (p q); 
+  apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
+| intros; apply (prop_1 ?? (oa_meet O BOOL)); intro x; simplify;
+  cases x; simplify; assumption;]
+qed.
+
+notation "hovbox(a ∧ b)" left associative with precedence 35
+for @{ 'oa_meet_bin $a $b }.
+interpretation "o-algebra binary meet" 'oa_meet_bin a b = 
+  (fun1 ___ (binary_meet _) a b).
+
+lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
+intros;  lapply (oa_overlap_preservers_meet_ O p q f);
+lapply (prop1 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
+[3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
+qed.
+
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" 
 non associative with precedence 49 for @{ 'oa_join $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" 
@@ -135,6 +161,8 @@ intros (P Q);
 constructor 1;
 [ apply (ORelation P Q);
 | constructor 1;
+   (* tenere solo una uguaglianza e usare la proposizione 9.9 per
+      le altre (unicita' degli aggiunti e del simmetrico) *)
    [ apply (λp,q. And4 (eq1 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) 
              (eq1 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q)) 
              (eq1 ? (or_f_ ?? p) (or_f_ ?? q)) 
@@ -237,8 +265,7 @@ intros;
 constructor 1;
 [ intros (F G);
   constructor 1;
-  [ lapply (G ∘ F);
-    apply (G ∘ F);
+  [ apply (G ∘ F);
   | apply (G⎻* ∘ F⎻* );
   | apply (F* ∘ G* );
   | apply (F⎻ ∘ G⎻);
@@ -275,4 +302,4 @@ split;
    | apply ((comp_assoc1 ????? H* G* F* ));]
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1;
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;]
-qed.
\ No newline at end of file
+qed.