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/bool.ma".
  16 include "datatypes/categories.ma".
  17 include "logic/cprop_connectives.ma".
  18
  19 lemma ums : setoid → setoid → setoid.
  20 intros (S T);
  21 constructor 1;
  22 [ apply (unary_morphism S T);
  23 | constructor 1;
  24   [ intros (f1 f2); apply (∀a,b:S.eq1 ? a b → eq1 ? (f1 a) (f2 b));
  25   | whd; simplify; intros; apply (.= (†H)); apply refl1;
  26   | whd; simplify; intros; apply (.= (†H1)); apply sym1; apply H; apply refl1;
  27   | whd; simplify; intros; apply (.= (†H2)); apply (.= (H ?? #)); apply (.= (H1 ?? #)); apply rule #;]]
  28 qed.
  29
  30 lemma BOOL : setoid.
  31 constructor 1; [apply bool] constructor 1;
  32 [ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]);
  33 | whd; simplify; intros; cases x; apply I;
  34 | whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption;
  35 | whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros; try assumption; apply I]
  36 qed.
  37
  38 lemma IF_THEN_ELSE_p :
  39   ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y →
  40   let f ≝ λm.match m with [ true ⇒ a | false ⇒ b ] in f x = f y.
  41 intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H;
  42 qed.
  43
  44 lemma if_then_else : ∀T:setoid. ∀a,b:T. ums BOOL T.
  45 intros; constructor 1; intros;
  46 [ apply (match c2 with [ true ⇒ c | false ⇒ c1 ]);
  47 | apply (IF_THEN_ELSE_p T c c1 a a' H);]
  48 qed.
  49
  50 record OAlgebra : Type := {
  51   oa_P :> setoid;
  52   oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
  53   oa_overlap: binary_morphism1 oa_P oa_P CPROP;
  54   oa_meet: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
  55   oa_join: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
  56   oa_one: oa_P;
  57   oa_zero: oa_P;
  58   oa_leq_refl: ∀a:oa_P. oa_leq a a;
  59   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
  60   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
  61   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
  62   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);
  63   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;
  64   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
  65   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
  66   oa_overlap_preservers_meet:
  67       ∀p,q.oa_overlap p q → oa_overlap p
  68      (oa_meet BOOL (if_then_else oa_P p q));
  69   oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *)
  70       ∀I:setoid.∀p.∀q:ums I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
  71   (*oa_base : setoid;
  72   oa_enum : ums oa_base oa_P;
  73   oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q*)
  74   oa_density:
  75       ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
  76 }.
  77
  78 (*
  79 axiom Al : OAlgebra.
  80 axiom x : carr (oa_P Al).
  81 definition wwww := (oa_density Al x x).
  82 definition X := ((λx:Type.λa:x.True) ? wwww).
  83 *)
  84
  85 interpretation "o-algebra leq" 'leq a b = (fun1 ___ (oa_leq _) a b).
  86
  87 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
  88 for @{ 'overlap $a $b}.
  89 interpretation "o-algebra overlap" 'overlap a b = (fun1 ___ (oa_overlap _) a b).
  90
  91 notation > "hovbox(a ∧ b)" left associative with precedence 50
  92 for @{ 'oa_meet2 $a $b }.
  93 notation > "hovbox(∧ f)" non associative with precedence 60
  94 for @{ 'oa_meet $f }.
  95 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50
  96 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
  97 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
  98 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
  99 notation < "hovbox(a ∧ b)" left associative with precedence 50
 100 for @{ 'oa_meet2 $a $b }.
 101
 102 interpretation "o-algebra meet" 'oa_meet \eta.f = (fun_1 __ (oa_meet __) f).
 103 interpretation "o-algebra binary meet" 'oa_meet2 x y = (fun_1 __ (oa_meet _ BOOL) (if_then_else _ x y)).
 104 (*
 105 notation > "hovbox(a ∨ b)" left associative with precedence 49
 106 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
 107 notation > "hovbox(∨ f)" non associative with precedence 59
 108 for @{ 'oa_join $f }.
 109 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
 110 for @{ 'oa_join (λ${ident i}:$I.$p) }.
 111 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
 112 for @{ 'oa_join (λ${ident i}.($p $_)) }.
 113 notation < "hovbox(a ∨ b)" left associative with precedence 49
 114 for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 115
 116 interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
 117 *)
 118
 119 record ORelation (P,Q : OAlgebra) : Type ≝ {
 120   or_f : P → Q;
 121   or_f_minus_star : P → Q;
 122   or_f_star : Q → P;
 123   or_f_minus : Q → P;
 124   or_prop1 : ∀p,q. or_f p ≤ q ⇔ p ≤ or_f_star q;
 125   or_prop2 : ∀p,q. or_f_minus p ≤ q ⇔ p ≤ or_f_minus_star q;
 126   or_prop3 : ∀p,q. or_f p >< q ⇔ p >< or_f_minus q
 127 }.
 128
 129 notation < "⨍ \sub (term 90 r)" non associative with precedence 90 for @{'OR_f $r}.
 130 notation < "⨍ \sub (term 90 r) term 90 a" non associative with precedence 70 for @{'OR_f_app1 $r $a}.
 131 notation > "⨍_(term 90 r)" non associative with precedence 90 for @{'OR_f $r}.
 132 interpretation "o-relation f" 'OR_f r = (or_f _ _ r).
 133 interpretation "o-relation f x" 'OR_f_app1 r a = (or_f _ _ r a).
 134
 135
 136 definition ORelation_setoid : OAlgebra → OAlgebra → setoid1.
 137 intros (P Q);
 138 constructor 1;
 139 [ apply (ORelation P Q);
 140 | constructor 1;
 141    [ apply (λp,q. ∀a.⨍_p a = ⨍_q a (* ∧ f^-1 a = .... *));
 142    | whd; simplify; intros; apply refl;
 143    | whd; simplify; intros; apply (H ? \sup -1);
 144    | whd; simplify; intros; apply trans; [2: apply H;|3: apply H1]]]
 145 qed.
 146
 147 axiom DAEMON: False.
 148
 149 definition composition : ∀P,Q,R.
 150   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
 151 intros;
 152 constructor 1;
 153 [ intros (F G);
 154   constructor 1;
 155   [ apply (λx.⨍_G (⨍_F x));
 156   |2,3,4,5,6,7: cases DAEMON;]
 157 | intros; cases DAEMON;]
 158 qed.
 159
 160 definition OA : category1. (* category2 *)
 161 split;
 162 [ apply (OAlgebra);
 163 | intros; apply (ORelation_setoid o o1);
 164 | intro O; split;
 165   [1,2,3,4: apply (λx.x);
 166   |*:intros;split;intros; assumption; ]
 167 |*: elim DAEMON;]
 168 qed.
 169
 170
 171