binary_meet is back again, with some effort

[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 5f99153ba85d6a477b05b7280a888d112678afcb..a84fc24770ac859b40040b56a3ecdaf826d5c8ca 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -60,7 +60,6 @@ coercion hint2.
 (* 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 *)
 (*alias symbol "comprehension_by" = "unary morphism comprehension with proof".*)
 record OAlgebra : Type2 := {
   oa_P :> SET1;
@@ -118,22 +117,35 @@ 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 = 
-  (fun11 __ (oa_meet __) f).
+  (fun12 __ (oa_meet __) f).
 interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = 
-  (fun11 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
+  (fun12 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
+
+definition hint3: OAlgebra → setoid1.
+ intro; apply (oa_P o);
+qed.
+coercion hint3.
+
+definition hint4: ∀A. setoid2_OF_OAlgebra A → hint3 A.
+ intros; apply t;
+qed.
+coercion hint4.
 
 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;]
+| intros; lapply (prop12 ? O (oa_meet O BOOL));
+   [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
+   |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
+   | apply Hletin;]
+  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).
+  (fun21 ___ (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);
@@ -315,4 +327,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.
+qed.
\ No newline at end of file