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 record OAlgebra : Type := {
  52   oa_P :> setoid;
  53   oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
  54   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
  55   oa_meet: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
  56   oa_join: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
  57   oa_one: oa_P;
  58   oa_zero: oa_P;
  59   oa_leq_refl: ∀a:oa_P. oa_leq a a;
  60   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
  61   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
  62   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
  63   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);
  64   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;
  65   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
  66   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
  67   oa_overlap_preservers_meet:
  68       ∀p,q.oa_overlap p q → oa_overlap p
  69      (oa_meet BOOL (if_then_else oa_P p q));
  70   oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *)
  71       ∀I:setoid.∀p.∀q:ums I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
  72   (*oa_base : setoid;
  73   oa_enum : ums oa_base oa_P;
  74   oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q*)
  75   oa_density:
  76       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
  77 }.
  78
  79 interpretation "o-algebra leq" 'leq a b = (fun1 ___ (oa_leq _) a b).
  80
  81 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
  82 for @{ 'overlap $a $b}.
  83 interpretation "o-algebra overlap" 'overlap a b = (fun1 ___ (oa_overlap _) a b).
  84
  85 notation > "hovbox(∧ f)" non associative with precedence 60
  86 for @{ 'oa_meet $f }.
  87 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50
  88 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
  89 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
  90 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
  91 notation < "hovbox(a ∧ b)" left associative with precedence 50
  92 for @{ 'oa_meet2 $a $b }.
  93
  94 interpretation "o-algebra meet" 'oa_meet \eta.f = (fun_1 __ (oa_meet __) f).
  95 interpretation "o-algebra binary meet" 'and x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)).
  96
  97 (*
  98 notation > "hovbox(a ∨ b)" left associative with precedence 49
  99 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
 100 notation > "hovbox(∨ f)" non associative with precedence 59
 101 for @{ 'oa_join $f }.
 102 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
 103 for @{ 'oa_join (λ${ident i}:$I.$p) }.
 104 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
 105 for @{ 'oa_join (λ${ident i}.($p $_)) }.
 106 notation < "hovbox(a ∨ b)" left associative with precedence 49
 107 for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 108
 109 interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
 110 *)
 111
 112 record ORelation (P,Q : OAlgebra) : Type ≝ {
 113   or_f :> P ⇒ Q;
 114   or_f_minus_star : P ⇒ Q;
 115   or_f_star : Q ⇒ P;
 116   or_f_minus : Q ⇒ P;
 117   or_prop1 : ∀p,q. or_f p ≤ q ⇔ p ≤ or_f_star q;
 118   or_prop2 : ∀p,q. or_f_minus p ≤ q ⇔ p ≤ or_f_minus_star q;
 119   or_prop3 : ∀p,q. or_f p >< q ⇔ p >< or_f_minus q
 120 }.
 121
 122 notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
 123 notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
 124 interpretation "o-relation f*" 'OR_f_star r = (or_f_star _ _ r).
 125
 126 notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
 127 notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
 128 interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star _ _ r).
 129
 130 notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 131 notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
 132 interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r).
 133
 134 axiom DAEMON: False.
 135
 136 definition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
 137 intros (P Q);
 138 constructor 1;
 139 [ apply (ORelation P Q);
 140 | constructor 1;
 141    [
 142      alias symbol "and" = "constructive and".
 143      apply (λp,q.
 144             (∀a.p⎻* a = q⎻* a) ∧
 145             (∀a.p⎻ a  = q⎻ a) ∧
 146             (∀a.p a   = q a) ∧
 147             (∀a.p* a  = q* a));
 148    | whd; simplify; intros; repeat split; intros; apply refl;
 149    | whd; simplify; intros; cases H; cases H1; cases H3; clear H H3 H1;
 150      repeat split; intros; apply sym; generalize in match a;assumption;
 151    | whd; simplify; intros; elim DAEMON;]]
 152 qed.
 153
 154 lemma hint : ∀P,Q. ORelation_setoid P Q → P ⇒ Q. intros; apply (or_f ?? c);qed.
 155 coercion hint.
 156
 157 definition composition : ∀P,Q,R.
 158   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
 159 intros;
 160 constructor 1;
 161 [ intros (F G);
 162   constructor 1;
 163   [ constructor 1; [apply (λx. G (F x)); | intros; apply (†(†H));]
 164   |2,3,4,5,6,7: cases DAEMON;]
 165 | intros; cases DAEMON;]
 166 qed.
 167
 168 definition OA : category1. (* category2 *)
 169 split;
 170 [ apply (OAlgebra);
 171 | intros; apply (ORelation_setoid o o1);
 172 | intro O; split;
 173   [1,2,3,4: constructor 1; [1,3,5,7:apply (λx.x);|*:intros;assumption]
 174   |5,6,7:intros;split;intros; assumption; ]
 175 |4: apply composition;
 176 |*: elim DAEMON;]
 177 qed.
 178
 179
 180