From aaa4f7b476bbde454c49990652199dfaf931ac7b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 17 Dec 2008 15:20:44 +0000
Subject: [PATCH] ....

---
 .../contribs/formal_topology/o-algebra.ma     | 137 ++++++++++++++----
 1 file changed, 112 insertions(+), 25 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/o-algebra.ma b/helm/software/matita/contribs/formal_topology/o-algebra.ma
index dadca0e4c..b1ef232ff 100644
--- a/helm/software/matita/contribs/formal_topology/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/o-algebra.ma
@@ -12,42 +12,84 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "datatypes/categories.ma".
 include "datatypes/bool.ma".
+include "datatypes/categories.ma".
 include "logic/cprop_connectives.ma". 
 
+lemma ums : setoid → setoid → setoid.
+intros (S T);
+constructor 1;
+[ apply (unary_morphism S T);
+| constructor 1;
+  [ intros (f1 f2); apply (∀a,b:S.eq1 ? a b → eq1 ? (f1 a) (f2 b));
+  | whd; simplify; intros; apply (.= (†H)); apply refl1;
+  | whd; simplify; intros; apply (.= (†H1)); apply sym1; apply H; apply refl1;
+  | whd; simplify; intros; apply (.= (†H2)); apply (.= (H ?? #)); apply (.= (H1 ?? #)); apply rule #;]] 
+qed.
+
+lemma BOOL : setoid.
+constructor 1; [apply bool] constructor 1;
+[ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]);
+| whd; simplify; intros; cases x; apply I;
+| whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption;
+| whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros; try assumption; apply I]
+qed.
+
+lemma IF_THEN_ELSE_p :
+  ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → 
+  let f ≝ λm.match m with [ true ⇒ a | false ⇒ b ] in f x = f y.
+intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H;
+qed. 
+
+lemma if_then_else : ∀T:setoid. ∀a,b:T. ums BOOL T.
+intros; constructor 1; intros; 
+[ apply (match c2 with [ true ⇒ c | false ⇒ c1 ]);
+| apply (IF_THEN_ELSE_p T c c1 a a' H);]
+qed.
+
 record OAlgebra : Type := {
   oa_P :> setoid;
-  oa_leq : oa_P → oa_P → CProp;
-  oa_overlap: oa_P → oa_P → CProp;
-  oa_meet: ∀I:Type.(I → oa_P) → oa_P;
-  oa_join: ∀I:Type.(I → oa_P) → oa_P;
+  oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1 *)
+  oa_overlap: binary_morphism1 oa_P oa_P CPROP;
+  oa_meet: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
+  oa_join: ∀I:setoid.unary_morphism (ums I oa_P) oa_P;
   oa_one: oa_P;
   oa_zero: oa_P;
-  oa_leq_refl: ∀a:oa_P.oa_leq a a;
+  oa_leq_refl: ∀a:oa_P. oa_leq a a; 
   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
-  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);
-  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;
+  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);
+  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;
   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
   oa_overlap_preservers_meet: 
-    ∀p,q.oa_overlap p q → oa_overlap p (oa_meet bool (λx.match x with [ true ⇒ p | false ⇒ q ]));
-  oa_join_split: 
-    ∀I.∀p,q.oa_overlap p (oa_join I q) ↔ ∃i:I.oa_overlap p (q i);
+      ∀p,q.oa_overlap p q → oa_overlap p 
+     (oa_meet BOOL (if_then_else oa_P p q));
+  oa_join_split: (* ha I → oa_P da castare a funX (ums A oa_P) *)
+      ∀I:setoid.∀p.∀q:ums I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
+  (*oa_base : setoid;
+  oa_enum : ums oa_base oa_P;
+  oa_density: ∀p,q.(∀i.oa_overlap p (oa_enum i) → oa_overlap q (oa_enum i)) → oa_leq p q*)
   oa_density: 
-    ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q    
+      ∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
 }.
 
-interpretation "o-algebra leq" 'leq a b = (oa_leq _ a b).
+(*
+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 = (oa_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_meet (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
+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
@@ -55,10 +97,11 @@ for @{ 'oa_meet (λ${ident i}:$I.$p) }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" non associative with precedence 50
 for @{ 'oa_meet (λ${ident i}.($p $_)) }.
 notation < "hovbox(a ∧ b)" left associative with precedence 50
-for @{ 'oa_meet (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
-
-interpretation "o-algebra meet" 'oa_meet \eta.f = (oa_meet _ _ f).
+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)).
+(*
 notation > "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
 notation > "hovbox(∨ f)" non associative with precedence 59
@@ -71,13 +114,57 @@ notation < "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 
 interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).
+*)
+
+record ORelation (P,Q : OAlgebra) : Type ≝ {
+  or_f : P → Q;
+  or_f_minus : P → Q;
+  or_f_star : Q → P;
+  or_f_minus_star : 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_minus q >< p ⇔ q >< or_f_minus p
+}.
+
+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).
+
+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]]]
+qed.  
+
+axiom DAEMON: False.
+
+definition composition : ∀P,Q,R. 
+  binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
+intros;
+constructor 1;
+[ intros (F G);
+  constructor 1;
+  [ apply (λx.⨍_G (⨍_F x));
+  |2,3,4,5,6,7: cases DAEMON;]
+| intros; cases DAEMON;]
+qed.
+
+definition OA : category1. (* category2 *)
+split;
+[ apply (OAlgebra);
+| intros; apply (ORelation_setoid o o1);
+| intro O; split;
+  [1,2,3,4: apply (λx.x);
+  |*:intros;split;intros; assumption;  
+|*: elim DAEMON;]
+qed. 
 
 
-include "nat/plus.ma".
 
-lemma x : ∀A:OAlgebra.∀x,y:A.∀f:ℕ→A.
-   x ≤ y → 
-   (x ∧ y >< x ∨ y ∧ x) → 
-   x = ∧ (λi:ℕ.x ∧ f i) ∧ ∨ (λi:ℕ.∧ (λx.f (x+i))) → x = y.
-intros;  
-  
-- 
2.39.2