From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 16:23:15 +0000 (+0000)
Subject: go notation go!
X-Git-Tag: make_still_working~4351
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4dfb1305a9c4a7c292f4b1957de1454d46c1ab8a;p=helm.git

go notation go!
---

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 }.