helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "datatypes/categories.ma".
  16 include "logic/cprop_connectives.ma".
  17
  18 inductive bool : Type := true : bool | false : bool.
  19
  20 lemma ums : setoid → setoid → setoid.
  21 intros (S T);
  22 constructor 1;
  23 [ apply (unary_morphism S T);
  24 | constructor 1;
  25   [ intros (f1 f2); apply (∀a,b:S.eq1 ? a b → eq1 ? (f1 a) (f2 b));
  26   | whd; simplify; intros; apply (.= (†H)); apply refl1;
  27   | whd; simplify; intros; apply (.= (†H1)); apply sym1; apply H; apply refl1;
  28   | whd; simplify; intros; apply (.= (†H2)); apply (.= (H ?? #)); apply (.= (H1 ?? #)); apply rule #;]]
  29 qed.
  30
  31 lemma BOOL : setoid.
  32 constructor 1; [apply bool] constructor 1;
  33 [ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]);
  34 | whd; simplify; intros; cases x; apply I;
  35 | whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption;
  36 | whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros; try assumption; apply I]
  37 qed.
  38
  39 lemma IF_THEN_ELSE_p :
  40   ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y →
  41   let f ≝ λm.match m with [ true ⇒ a | false ⇒ b ] in f x = f y.
  42 intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H;
  43 qed.
  44
  45 lemma if_then_else : ∀T:setoid. ∀a,b:T. ums BOOL T.
  46 intros; constructor 1; intros;
  47 [ apply (match c2 with [ true ⇒ c | false ⇒ c1 ]);
  48 | apply (IF_THEN_ELSE_p T c c1 a a' H);]
  49 qed.
  50
  51 interpretation "mk " 'comprehension T P =
  52   (mk_unary_morphism T _ P _).
  53
  54 notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
  55 for @{ 'comprehension_by $s (\lambda ${ident i}. $p) $by}.
  56
  57 interpretation "unary morphism comprehension with proof" 'comprehension_by s f p =
  58   (mk_unary_morphism s _ f p).
  59
  60 definition A : ∀S:setoid.∀a,b:S.ums BOOL S.
  61 apply (λS,a,b.{ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b] | IF_THEN_ELSE_p S a b}).
  62 qed.
  63
  64 record OAlgebra : Type := {
  65   oa_P :> setoid;
  66   oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
  67   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
  68   oa_meet: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
  69   oa_join: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
  70   oa_one: oa_P;
  71   oa_zero: oa_P;
  72   oa_leq_refl: ∀a:oa_P. oa_leq a a;
  73   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
  74   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
  75   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
  76   oa_meet_inf: ∀I.∀p_i.∀p:oa_P.oa_leq p (oa_meet I p_i) → ∀i:I.oa_leq p (p_i i);
  77   oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
  78   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
  79   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
  80   oa_overlap_preservers_meet:
  81       ∀p,q.oa_overlap p q → oa_overlap p
  82        (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
  83      (*(oa_meet BOOL (if_then_else oa_P p q));*)
  84   oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *)
  85       ∀I:setoid.∀p.∀q:ums I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
  86   (*oa_base : setoid;
  87   oa_enum : ums oa_base oa_P;
  88   oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q*)
  89   oa_density:
  90       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
  91 }.
  92
  93 interpretation "o-algebra leq" 'leq a b = (fun1 ___ (oa_leq _) a b).
  94
  95 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
  96 for @{ 'overlap $a $b}.
  97 interpretation "o-algebra overlap" 'overlap a b = (fun1 ___ (oa_overlap _) a b).
  98
  99 notation > "hovbox(∧ f)" non associative with precedence 60
 100 for @{ 'oa_meet $f }.
 101 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50
 102 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
 103 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
 104 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
 105 notation < "hovbox(a ∧ b)" left associative with precedence 50
 106 for @{ 'oa_meet
 107   ($foo $bar $baz
 108     (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ])
 109     $res) }.
 110
 111 interpretation "o-algebra meet" 'oa_meet f = (fun_1 __ (oa_meet __) f).
 112 (*interpretation "o-algebra binary meet" 'and x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)).*)
 113
 114 (*
 115 notation > "hovbox(a ∨ b)" left associative with precedence 49
 116 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
 117 notation > "hovbox(∨ f)" non associative with precedence 59
 118 for @{ 'oa_join $f }.
 119 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
 120 for @{ 'oa_join (λ${ident i}:$I.$p) }.
 121 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
 122 for @{ 'oa_join (λ${ident i}.($p $_)) }.
 123 notation < "hovbox(a ∨ b)" left associative with precedence 49
 124 for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 125
 126 interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
 127 *)
 128
 129 record ORelation (P,Q : OAlgebra) : Type ≝ {
 130   or_f :> P ⇒ Q;
 131   or_f_minus_star : P ⇒ Q;
 132   or_f_star : Q ⇒ P;
 133   or_f_minus : Q ⇒ P;
 134   or_prop1 : ∀p,q. or_f p ≤ q ⇔ p ≤ or_f_star q;
 135   or_prop2 : ∀p,q. or_f_minus p ≤ q ⇔ p ≤ or_f_minus_star q;
 136   or_prop3 : ∀p,q. or_f p >< q ⇔ p >< or_f_minus q
 137 }.
 138
 139 notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
 140 notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
 141 interpretation "o-relation f*" 'OR_f_star r = (or_f_star _ _ r).
 142
 143 notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
 144 notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
 145 interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star _ _ r).
 146
 147 notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 148 notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 149 interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r).
 150
 151 axiom DAEMON: False.
 152
 153 definition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
 154 intros (P Q);
 155 constructor 1;
 156 [ apply (ORelation P Q);
 157 | constructor 1;
 158    [
 159      alias symbol "and" = "constructive and".
 160      apply (λp,q.
 161             (∀a.p⎻* a = q⎻* a) ∧
 162             (∀a.p⎻ a  = q⎻ a) ∧
 163             (∀a.p a   = q a) ∧
 164             (∀a.p* a  = q* a));
 165    | whd; simplify; intros; repeat split; intros; apply refl;
 166    | whd; simplify; intros; cases H; cases H1; cases H3; clear H H3 H1;
 167      repeat split; intros; apply sym; generalize in match a;assumption;
 168    | whd; simplify; intros; elim DAEMON;]]
 169 qed.
 170
 171 lemma hint : ∀P,Q. ORelation_setoid P Q → P ⇒ Q. intros; apply (or_f ?? c);qed.
 172 coercion hint.
 173
 174 definition composition : ∀P,Q,R.
 175   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
 176 intros;
 177 constructor 1;
 178 [ intros (F G);
 179   constructor 1;
 180   [ constructor 1; [apply (λx. G (F x)); | intros; apply (†(†H));]
 181   |2,3,4,5,6,7: cases DAEMON;]
 182 | intros; cases DAEMON;]
 183 qed.
 184
 185 definition OA : category1. (* category2 *)
 186 split;
 187 [ apply (OAlgebra);
 188 | intros; apply (ORelation_setoid o o1);
 189 | intro O; split;
 190   [1,2,3,4: constructor 1; [1,3,5,7:apply (λx.x);|*:intros;assumption]
 191   |5,6,7:intros;split;intros; assumption; ]
 192 |4: apply composition;
 193 |*: elim DAEMON;]
 194 qed.
 195
 196
 197