From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 17 Dec 2008 17:35:00 +0000 (+0000)
Subject: foo overlap
X-Git-Tag: make_still_working~4376
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62e9e8296d172d6497f9ad29bad402fbad2014c3;p=helm.git

foo overlap
---

diff --git a/helm/software/matita/contribs/formal_topology/o-algebra.ma b/helm/software/matita/contribs/formal_topology/o-algebra.ma
deleted file mode 100644
index b1ef232ff..000000000
--- a/helm/software/matita/contribs/formal_topology/o-algebra.ma
+++ /dev/null
@@ -1,170 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-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 : 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_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.∀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 (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
-}.
-
-(*
-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 = (fun1 ___ (oa_overlap _) a b).
-
-notation > "hovbox(a ∧ b)" left associative with precedence 50
-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
-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_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
-for @{ 'oa_join $f }.
-notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
-for @{ 'oa_join (λ${ident i}:$I.$p) }.
-notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
-for @{ 'oa_join (λ${ident i}.($p $_)) }.
-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. 
-
-
-
diff --git a/helm/software/matita/contribs/formal_topology/overlap/Makefile b/helm/software/matita/contribs/formal_topology/overlap/Makefile
new file mode 100644
index 000000000..92a16d1f0
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/Makefile
@@ -0,0 +1,16 @@
+include ../../Makefile.defs
+
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+	$(BIN)../matitac
+$(DIR).opt opt all.opt:
+	$(BIN)../matitac.opt
+clean:
+	$(BIN)../matitaclean
+clean.opt:
+	$(BIN)../matitaclean.opt
+depend:
+	$(BIN)../matitadep -dot && rm depends.dot
+depend.opt:
+	$(BIN)../matitadep.opt -dot && rm depends.dot
diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends
new file mode 100644
index 000000000..039a5df4e
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/depends
@@ -0,0 +1,7 @@
+o-basic_pairs.ma datatypes/categories.ma o-algebra.ma
+o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
+o-saturations.ma o-algebra.ma
+o-algebra.ma datatypes/bool.ma datatypes/categories.ma logic/cprop_connectives.ma
+datatypes/bool.ma 
+datatypes/categories.ma 
+logic/cprop_connectives.ma 
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
new file mode 100644
index 000000000..f04b0a70c
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -0,0 +1,171 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+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 : 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_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.∀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 (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
+}.
+
+(*
+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 = (fun1 ___ (oa_overlap _) a b).
+
+notation > "hovbox(a ∧ b)" left associative with precedence 50
+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
+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_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
+for @{ 'oa_join $f }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" non associative with precedence 49
+for @{ 'oa_join (λ${ident i}:$I.$p) }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
+for @{ 'oa_join (λ${ident i}.($p $_)) }.
+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_star : P → Q;
+  or_f_star : Q → P;
+  or_f_minus : 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 p >< q ⇔ p >< or_f_minus q
+}.
+
+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. 
+
+
+
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
new file mode 100644
index 000000000..9bd76ebeb
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -0,0 +1,187 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "o-algebra.ma".
+include "datatypes/categories.ma".
+
+record basic_pair: Type ≝
+ { concr: OA;
+   form: OA;
+   rel: arrows1 ? concr form
+ }.
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation < "x (⊩  \below c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation < "⊩ \sub c" with precedence 60 for @{'Vdash $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+
+interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y).
+interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
+
+alias symbol "eq" = "setoid1 eq".
+alias symbol "compose" = "category1 composition".
+record relation_pair (BP1,BP2: basic_pair): Type ≝
+ { concr_rel: arrows1 ? (concr BP1) (concr BP2);
+   form_rel: arrows1 ? (form BP1) (form BP2);
+   commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
+ }.
+
+notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
+notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
+
+interpretation "concrete relation" 'concr_rel r = (concr_rel __ r). 
+interpretation "formal relation" 'form_rel r = (form_rel __ r). 
+
+definition relation_pair_equality:
+ ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
+ intros;
+ constructor 1;
+  [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
+  | simplify;
+    intros;
+    apply refl1;
+  | simplify;
+    intros 2;
+    apply sym1;
+  | simplify;
+    intros 3;
+    apply trans1;
+  ]      
+qed.
+
+definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
+ intros;
+ constructor 1;
+  [ apply (relation_pair b b1)
+  | apply relation_pair_equality
+  ]
+qed.
+
+lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+ intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c);
+ apply (.= (commute ?? r \sup -1));
+ apply (.= H);
+ apply (.= (commute ?? r'));
+ apply refl1;
+qed.
+
+
+definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
+ intro;
+ constructor 1;
+  [1,2: apply id1;
+  | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
+    lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
+    apply (.= H);
+    apply (H1 \sup -1);]
+qed.
+
+definition relation_pair_composition:
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ intros;
+ constructor 1;
+  [ intros (r r1);
+    constructor 1;
+     [ apply (r1 \sub\c ∘ r \sub\c) 
+     | apply (r1 \sub\f ∘ r \sub\f)
+     | lapply (commute ?? r) as H;
+       lapply (commute ?? r1) as H1;
+       apply (.= ASSOC1);
+       apply (.= #‡H1);
+       apply (.= ASSOC1\sup -1);
+       apply (.= H‡#);
+       apply ASSOC1]
+  | intros;
+    change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));  
+    change in H with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
+    change in H1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
+    apply (.= ASSOC1);
+    apply (.= #‡H1);
+    apply (.= #‡(commute ?? b'));
+    apply (.= ASSOC1 \sup -1);
+    apply (.= H‡#);
+    apply (.= ASSOC1);
+    apply (.= #‡(commute ?? b')\sup -1);
+    apply (ASSOC1 \sup -1)]
+qed.
+    
+definition BP: category1.
+ constructor 1;
+  [ apply basic_pair
+  | apply relation_pair_setoid
+  | apply id_relation_pair
+  | apply relation_pair_composition
+  | intros;
+    change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
+                 ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
+    apply (ASSOC1‡#);
+  | intros;
+    change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
+    apply ((id_neutral_right1 ????)‡#);
+  | intros;
+    change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
+    apply ((id_neutral_left1 ????)‡#);]
+qed.
+
+
+(*
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
+ intros; constructor 1;
+  [ apply (ext ? ? (rel o));
+  | intros;
+    apply (.= #‡H);
+    apply refl1]
+qed.
+
+definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
+ λo.extS ?? (rel o).
+*)
+
+(*
+definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
+ intros (o); constructor 1;
+  [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
+    intros; simplify; apply (.= (†H)‡#); apply refl1
+  | intros; split; simplify; intros;
+     [ apply (. #‡((†H)‡(†H1))); assumption
+     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
+
+definition fintersectsS:
+ ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
+ intros (o); constructor 1;
+  [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
+    intros; simplify; apply (.= (†H)‡#); apply refl1
+  | intros; split; simplify; intros;
+     [ apply (. #‡((†H)‡(†H1))); assumption
+     | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
+*)
+
+(*
+definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+ intros (o); constructor 1;
+  [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
+  | intros; split; intros; cases H2; exists [1,3: apply w]
+     [ apply (. (#‡H1)‡(H‡#)); assumption
+     | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
+qed.
+
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
+*)
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
new file mode 100644
index 000000000..135dae3c9
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -0,0 +1,131 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "o-basic_pairs.ma".
+include "o-saturations.ma".
+
+lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed.
+coercion xxx.
+
+record concrete_space : Type ≝
+ { bp:> BP;
+   downarrow: form bp → oa_P (form bp);
+   downarrow_is_sat: is_saturation ? downarrow;
+   converges: ∀q1,q2:form bp.
+     or_f_minus ?? (⊩) q1 ∧ or_f_minus ?? (⊩) q2 = 
+     or_f_minus ?? (⊩) ((downarrow q1) ∧ (downarrow q2));
+   all_covered: (*⨍^-_bp*) or_f_minus ?? (⊩) (oa_one (form bp)) = oa_one (concr bp);
+   il2: ∀I:setoid.∀p:ums I (oa_P (form bp)).
+     downarrow (oa_join ? I (mk_unary_morphism ?? (λi:I. downarrow (p i)) ?)) =
+     oa_join ? I (mk_unary_morphism ?? (λi:I. downarrow (p i)) ?)
+ }.
+
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
+
+coercion bp'.
+
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+ { rp:> arrows1 ? CS1 CS2;
+   respects_converges:
+    ∀b,c.
+     extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+     BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+   respects_all_covered:
+    extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
+ }.
+
+definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
+ λCS1,CS2,c. rp CS1 CS2 c.
+ 
+coercion rp'.
+
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
+ intros;
+ constructor 1;
+  [ apply (convergent_relation_pair c c1)
+  | constructor 1;
+     [ intros;
+       apply (relation_pair_equality c c1 c2 c3);
+     | intros 1; apply refl1;
+     | intros 2; apply sym1; 
+     | intros 3; apply trans1]]
+qed.
+
+definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
+ λCS1,CS2,c.rp ?? c.
+
+coercion rp''.
+
+definition convergent_relation_space_composition:
+ ∀o1,o2,o3: concrete_space.
+  binary_morphism1
+   (convergent_relation_space_setoid o1 o2)
+   (convergent_relation_space_setoid o2 o3)
+   (convergent_relation_space_setoid o1 o3).
+ intros; constructor 1;
+     [ intros; whd in c c1 ⊢ %;
+       constructor 1;
+        [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+        | intros;
+          change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+            with (c1 \sub \f ∘ c \sub \f);
+          change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+            with (c1 \sub \f ∘ c \sub \f);
+          apply (.= (extS_com ??????));
+          apply (.= (†(respects_converges ?????)));
+          apply (.= (respects_converges ?????));
+          apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
+          apply refl1;
+        | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+          apply (.= (extS_com ??????));
+          apply (.= (†(respects_all_covered ???)));
+          apply (.= respects_all_covered ???);
+          apply refl1]
+     | intros;
+       change with (b ∘ a = b' ∘ a');
+       change in H with (rp'' ?? a = rp'' ?? a');
+       change in H1 with (rp'' ?? b = rp ?? b');
+       apply (.= (H‡H1));
+       apply refl1]
+qed.
+
+definition CSPA: category1.
+ constructor 1;
+  [ apply concrete_space
+  | apply convergent_relation_space_setoid
+  | intro; constructor 1;
+     [ apply id1
+     | intros;
+       unfold id; simplify;
+       apply (.= (equalset_extS_id_X_X ??));
+       apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
+                    (equalset_extS_id_X_X ??)\sup -1)));
+       apply refl1;
+     | apply (.= (equalset_extS_id_X_X ??));
+       apply refl1]
+  | apply convergent_relation_space_composition
+  | intros; simplify;
+    change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
+    apply (.= ASSOC1);
+    apply refl1
+  | intros; simplify;
+    change with (a ∘ id1 ? o1 = a);
+    apply (.= id_neutral_right1 ????);
+    apply refl1
+  | intros; simplify;
+    change with (id1 ? o2 ∘ a = a);
+    apply (.= id_neutral_left1 ????);
+    apply refl1]
+qed.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma
new file mode 100644
index 000000000..9b68972b4
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-saturations.ma
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "o-algebra.ma".
+
+definition hint1: OA → Type ≝ λc:OA.carr (oa_P c).
+coercion hint1.
+
+definition hint2: ∀C.hint1 C → carr1 ((λx.x) (setoid1_of_setoid (oa_P C))).
+intros; assumption;
+qed.
+coercion hint2. 
+
+alias symbol "eq" = "setoid1 eq".
+definition is_saturation ≝
+ λC:OA.λA:C → C.
+  ∀U,V. (U ≤ A V) = (A U ≤ A V).
+
+definition is_reduction ≝
+ λC:OA.λJ:C → C.
+    ∀U,V. (J U ≤ V) = (J U ≤ J V).
+
+theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ≤ A U.
+ intros; apply (fi ?? (H ??)); apply (oa_leq_refl C).
+qed.
+
+theorem saturation_monotone:
+ ∀C,A. is_saturation C A →
+  ∀U,V:C. U ≤ V → A U ≤ A V.
+ intros; apply (if ?? (H ??)); apply (oa_leq_trans C);
+  [apply V|3: apply saturation_expansive ]
+ assumption.
+qed.
+
+theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. 
+ eq (oa_P C) (A (A U)) (A U).
+ intros; apply (oa_leq_antisym C);
+  [ apply (if ?? (H (A U) U)); apply (oa_leq_refl C).
+  | apply saturation_expansive; assumption]
+qed.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/root b/helm/software/matita/contribs/formal_topology/overlap/root
new file mode 100644
index 000000000..d57275734
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/formal_topology