From 7048db496643fc440aebc6e85dd425886bcd2e56 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 28 Dec 2008 17:47:25 +0000 Subject: [PATCH] Some more painful work. --- .../formal_topology/overlap/o-algebra.ma | 45 ++++++++++--------- 1 file changed, 25 insertions(+), 20 deletions(-) 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 a84fc2477..063e5988f 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -99,7 +99,7 @@ interpretation "o-algebra leq" 'leq a b = (fun21 ___ (oa_leq _) a b). notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45 for @{ 'overlap $a $b}. -interpretation "o-algebra overlap" 'overlap a b = (fun22 ___ (oa_overlap _) a b). +interpretation "o-algebra overlap" 'overlap a b = (fun21 ___ (oa_overlap _) a b). notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50 for @{ 'oa_meet $p }. @@ -148,8 +148,8 @@ interpretation "o-algebra binary meet" 'oa_meet_bin 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); -lapply (prop1 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?); +intros; lapply (oa_overlap_preserves_meet_ O p q f); +lapply (prop21 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?); [3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1; qed. @@ -166,15 +166,20 @@ notation > "hovbox(a ∨ b)" left associative with precedence 49 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }. interpretation "o-algebra join" 'oa_join f = - (fun_1 __ (oa_join __) f). + (fun12 __ (oa_join __) f). interpretation "o-algebra join with explicit function" 'oa_join_mk f = - (fun_1 __ (oa_join __) (mk_unary_morphism _ _ f _)). + (fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)). + +definition hint5: OAlgebra → objs2 SET1. + intro; apply (oa_P o); +qed. +coercion hint5. record ORelation (P,Q : OAlgebra) : Type ≝ { - or_f_ : arrows1 SET P Q; - or_f_minus_star_ : arrows1 SET P Q; - or_f_star_ : arrows1 SET Q P; - or_f_minus_ : arrows1 SET Q P; + or_f_ : P ⇒ Q; + or_f_minus_star_ : P ⇒ Q; + or_f_star_ : Q ⇒ P; + or_f_minus_ : Q ⇒ P; or_prop1_ : ∀p,q. (or_f_ p ≤ q) = (p ≤ or_f_star_ q); or_prop2_ : ∀p,q. (or_f_minus_ p ≤ q) = (p ≤ or_f_minus_star_ q); or_prop3_ : ∀p,q. (or_f_ p >< q) = (p >< or_f_minus_ q) @@ -188,19 +193,19 @@ constructor 1; | 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)) - (eq1 ? (or_f_star_ ?? p) (or_f_star_ ?? q))); - | whd; simplify; intros; repeat split; intros; apply refl1; + [ apply (λp,q. And4 (eq2 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) + (eq2 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q)) + (eq2 ? (or_f_ ?? p) (or_f_ ?? q)) + (eq2 ? (or_f_star_ ?? p) (or_f_star_ ?? q))); + | whd; simplify; intros; repeat split; intros; apply refl2; | whd; simplify; intros; cases H; clear H; split; - intro a; apply sym; generalize in match a;assumption; + intro a; apply sym1; generalize in match a;assumption; | whd; simplify; intros; cases H; cases H1; clear H H1; split; intro a; - [ apply (.= (H2 a)); apply H6; - | apply (.= (H3 a)); apply H7; - | apply (.= (H4 a)); apply H8; - | apply (.= (H5 a)); apply H9;]]] -qed. + [ apply (.= (e a)); apply e4; + | apply (.= (e1 a)); apply e5; + | apply (.= (e2 a)); apply e6; + | apply (.= (e3 a)); apply e7;]]] +qed. definition or_f_minus_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q. intros; constructor 1; -- 2.39.2