From 4dfb1305a9c4a7c292f4b1957de1454d46c1ab8a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 16:23:15 +0000 Subject: [PATCH] go notation go! --- .../formal_topology/overlap/o-algebra.ma | 65 +++++++++++-------- .../formal_topology/overlap/o-basic_pairs.ma | 2 +- .../overlap/o-concrete_spaces.ma | 40 ++++++++++-- helm/software/matita/core_notation.moo | 7 +- 4 files changed, 76 insertions(+), 38 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 f04b0a70c..b5410f7af 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -12,10 +12,11 @@ (* *) (**************************************************************************) -include "datatypes/bool.ma". include "datatypes/categories.ma". include "logic/cprop_connectives.ma". +inductive bool : Type := true : bool | false : bool. + lemma ums : setoid → setoid → setoid. intros (S T); constructor 1; @@ -75,21 +76,12 @@ record OAlgebra : Type := { ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q }. -(* -axiom Al : OAlgebra. -axiom x : carr (oa_P Al). -definition wwww := (oa_density Al x x). -definition X := ((λx:Type.λa:x.True) ? wwww). -*) - interpretation "o-algebra leq" 'leq a b = (fun1 ___ (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 = (fun1 ___ (oa_overlap _) a b). -notation > "hovbox(a ∧ b)" left associative with precedence 50 -for @{ 'oa_meet2 $a $b }. notation > "hovbox(∧ f)" non associative with precedence 60 for @{ 'oa_meet $f }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50 @@ -100,7 +92,8 @@ notation < "hovbox(a ∧ b)" left associative with precedence 50 for @{ 'oa_meet2 $a $b }. interpretation "o-algebra meet" 'oa_meet \eta.f = (fun_1 __ (oa_meet __) f). -interpretation "o-algebra binary meet" 'oa_meet2 x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)). +interpretation "o-algebra binary meet" 'and x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)). + (* notation > "hovbox(a ∨ b)" left associative with precedence 49 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }. @@ -117,34 +110,49 @@ interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f). *) record ORelation (P,Q : OAlgebra) : Type ≝ { - or_f : P → Q; - or_f_minus_star : P → Q; - or_f_star : Q → P; - or_f_minus : 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 }. -notation < "⨍ \sub (term 90 r)" non associative with precedence 90 for @{'OR_f $r}. -notation < "⨍ \sub (term 90 r) term 90 a" non associative with precedence 70 for @{'OR_f_app1 $r $a}. -notation > "⨍_(term 90 r)" non associative with precedence 90 for @{'OR_f $r}. -interpretation "o-relation f" 'OR_f r = (or_f _ _ r). -interpretation "o-relation f x" 'OR_f_app1 r a = (or_f _ _ r a). +notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}. +notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}. +interpretation "o-relation f*" 'OR_f_star r = (or_f_star _ _ r). + +notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}. +notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}. +interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star _ _ r). +notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. +notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. +interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r). + +axiom DAEMON: False. definition ORelation_setoid : OAlgebra → OAlgebra → setoid1. intros (P Q); constructor 1; [ apply (ORelation P Q); | constructor 1; - [ apply (λp,q. ∀a.⨍_p a = ⨍_q a (* ∧ f^-1 a = .... *)); - | whd; simplify; intros; apply refl; - | whd; simplify; intros; apply (H ? \sup -1); - | whd; simplify; intros; apply trans; [2: apply H;|3: apply H1]]] + [ + alias symbol "and" = "constructive and". + apply (λp,q. + (∀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; + | whd; simplify; intros; cases H; cases H1; cases H3; clear H H3 H1; + repeat split; intros; apply sym; generalize in match a;assumption; + | whd; simplify; intros; elim DAEMON;]] qed. -axiom DAEMON: False. +lemma hint : ∀P,Q. ORelation_setoid P Q → P ⇒ Q. intros; apply (or_f ?? c);qed. +coercion hint. definition composition : ∀P,Q,R. binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R). @@ -152,7 +160,7 @@ intros; constructor 1; [ intros (F G); constructor 1; - [ apply (λx.⨍_G (⨍_F x)); + [ constructor 1; [apply (λx. G (F x)); | intros; apply (†(†H));] |2,3,4,5,6,7: cases DAEMON;] | intros; cases DAEMON;] qed. @@ -162,8 +170,9 @@ split; [ apply (OAlgebra); | intros; apply (ORelation_setoid o o1); | intro O; split; - [1,2,3,4: apply (λx.x); - |*:intros;split;intros; assumption; ] + [1,2,3,4: constructor 1; [1,3,5,7:apply (λx.x);|*:intros;assumption] + |5,6,7:intros;split;intros; assumption; ] +|4: apply composition; |*: elim DAEMON;] qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 9bd76ebeb..01eac172c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -70,7 +70,7 @@ qed. lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩. intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c); - apply (.= (commute ?? r \sup -1)); + apply (.= ((commute ?? r) \sup -1)); apply (.= H); apply (.= (commute ?? r')); apply refl1; diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma index 7292b4ecb..4e989cb14 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -15,24 +15,52 @@ include "o-basic_pairs.ma". include "o-saturations.ma". +notation "□ \sub b" non associative with precedence 90 for @{'box $b}. +notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}. +interpretation "Universal image ⊩⎻*" 'box x = (or_f_minus_star _ _ (rel x)). + +notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}. +notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}. +interpretation "Existential image ⊩" 'diamond x = (or_f _ _ (rel x)). + +notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}. +notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}. +interpretation "Universal pre-image ⊩*" 'rest x = (or_f_star _ _ (rel x)). + +notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}. +notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}. +interpretation "Existential pre-image ⊩⎻" 'ext x = (or_f_minus _ _ (rel x)). + +definition A : ∀b:BP. unary_morphism (oa_P (form b)) (oa_P (form b)). +intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); | intros; apply (†(†H));] qed. + lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed. coercion xxx. +definition d_p_i : + ∀S:setoid.∀I:setoid.∀d:unary_morphism S S.∀p:ums I S.ums I S. +intros; constructor 1; [ apply (λi:I. u (c i));| intros; apply (†(†H));]. +qed. + +alias symbol "eq" = "setoid eq". +alias symbol "and" = "o-algebra binary meet". record concrete_space : Type ≝ { bp:> BP; + (*distr : is_distributive (form bp);*) downarrow: unary_morphism (oa_P (form bp)) (oa_P (form bp)); downarrow_is_sat: is_saturation ? downarrow; converges: ∀q1,q2. - or_f_minus ?? (⊩) q1 ∧ or_f_minus ?? (⊩) q2 = - or_f_minus ?? (⊩) ((downarrow q1) ∧ (downarrow q2)); - all_covered: (*⨍^-_bp*) or_f_minus ?? (⊩) (oa_one (form bp)) = oa_one (concr bp); + (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2))); + all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp); il2: ∀I:setoid.∀p:ums I (oa_P (form bp)). - downarrow (oa_join ? I (mk_unary_morphism ?? (λi:I. downarrow (p i)) ?)) = - oa_join ? I (mk_unary_morphism ?? (λi:I. downarrow (p i)) ?) + downarrow (oa_join ? I (d_p_i ?? downarrow p)) = + oa_join ? I (d_p_i ?? downarrow p); + il1: ∀q.downarrow (A ? q) = A ? q }. -definition bp': concrete_space → basic_pair ≝ λc.bp c. +interpretation "o-concrete space downarrow" 'downarrow x = (fun_1 __ (downarrow _) x). +definition bp': concrete_space → basic_pair ≝ λc.bp c. coercion bp'. record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 1c1e59cb3..98658726a 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -209,9 +209,10 @@ notation "↑a" with precedence 55 for @{ 'uparrow $a }. notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. -notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}. -notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }. -notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}. +notation "a \sup b" left associative with precedence 90 for @{ 'exp $a $b}. +notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }. +notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }. +notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}. notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }. -- 2.39.2