+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
-
-
-
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+baseuri=cic:/matita/formal_topology
projects / helm.git / commitdiff