helm/software/matita/contribs/formal_topology/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 "datatypes/bool.ma".
  17 include "logic/cprop_connectives.ma".
  18
  19 record OAlgebra : Type := {
  20   oa_P :> setoid;
  21   oa_leq : oa_P → oa_P → CProp;
  22   oa_overlap: oa_P → oa_P → CProp;
  23   oa_meet: ∀I:Type.(I → oa_P) → oa_P;
  24   oa_join: ∀I:Type.(I → oa_P) → oa_P;
  25   oa_one: oa_P;
  26   oa_zero: oa_P;
  27   oa_leq_refl: ∀a:oa_P.oa_leq a a;
  28   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
  29   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
  30   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
  31   oa_meet_inf: ∀I:Type.∀p_i.∀p:oa_P.oa_leq p (oa_meet I p_i) → ∀i:I.oa_leq p (p_i i);
  32   oa_join_sup: ∀I:Type.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
  33   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
  34   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
  35   oa_overlap_preservers_meet:
  36     ∀p,q.oa_overlap p q → oa_overlap p (oa_meet bool (λx.match x with [ true ⇒ p | false ⇒ q ]));
  37   oa_join_split:
  38     ∀I.∀p,q.oa_overlap p (oa_join I q) ↔ ∃i:I.oa_overlap p (q i);
  39   oa_density:
  40     ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
  41 }.
  42
  43 interpretation "o-algebra leq" 'leq a b = (oa_leq _ a b).
  44
  45 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
  46 for @{ 'overlap $a $b}.
  47 interpretation "o-algebra overlap" 'overlap a b = (oa_overlap _ a b).
  48
  49 notation > "hovbox(a ∧ b)" left associative with precedence 50
  50 for @{ 'oa_meet (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
  51 notation > "hovbox(∧ f)" non associative with precedence 60
  52 for @{ 'oa_meet $f }.
  53 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" non associative with precedence 50
  54 for @{ 'oa_meet (λ${ident i}:$I.$p) }.
  55 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
  56 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
  57 notation < "hovbox(a ∧ b)" left associative with precedence 50
  58 for @{ 'oa_meet (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
  59
  60 interpretation "o-algebra meet" 'oa_meet \eta.f = (oa_meet _ _ f).
  61
  62 notation > "hovbox(a ∨ b)" left associative with precedence 49
  63 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
  64 notation > "hovbox(∨ f)" non associative with precedence 59
  65 for @{ 'oa_join $f }.
  66 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
  67 for @{ 'oa_join (λ${ident i}:$I.$p) }.
  68 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
  69 for @{ 'oa_join (λ${ident i}.($p $_)) }.
  70 notation < "hovbox(a ∨ b)" left associative with precedence 49
  71 for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
  72
  73 interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
  74
  75
  76 include "nat/plus.ma".
  77
  78 lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A.
  79    x ≤ y →
  80    (x ∧ y >< x ∨ y ∧ x) →
  81    x = ∧ (λi:ℕ.x ∧ f i) ∧ ∨ (λi:ℕ.∧ (λx.f (x+i))) → x = y.
  82 intros;
  83