From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 28 Dec 2008 17:23:10 +0000 (+0000)
Subject: binary_meet is back again, with some effort
X-Git-Tag: make_still_working~4313
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bd9161789ad35aae35b66e1f9bba660d8fde3c61;p=helm.git

binary_meet is back again, with some effort
---

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 bcd1aae1b..a84fc2477 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -117,24 +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);
@@ -316,5 +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.
-*)
\ No newline at end of file
+qed.
\ No newline at end of file