(* *)
(**************************************************************************)
-include "datatypes/bool.ma".
include "datatypes/categories.ma".
include "logic/cprop_connectives.ma".
+inductive bool : Type := true : bool | false : bool.
+
lemma ums : setoid → setoid → setoid.
intros (S T);
constructor 1;
∀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_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)).
+interpretation "o-algebra binary meet" 'and 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 ]) }.
*)
record ORelation (P,Q : OAlgebra) : Type ≝ {
- or_f : P â\86\92 Q;
- or_f_minus_star : P â\86\92 Q;
- or_f_star : Q â\86\92 P;
- or_f_minus : Q â\86\92 P;
+ or_f :> P â\87\92 Q;
+ or_f_minus_star : P â\87\92 Q;
+ or_f_star : Q â\87\92 P;
+ or_f_minus : Q â\87\92 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).
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+interpretation "o-relation f*" 'OR_f_star r = (or_f_star _ _ r).
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+interpretation "o-relation f⎻*" 'OR_f_minus_star r = (or_f_minus_star _ _ r).
+notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+interpretation "o-relation f⎻" 'OR_f_minus r = (or_f_minus _ _ r).
+
+axiom DAEMON: False.
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]]]
+ [
+ alias symbol "and" = "constructive and".
+ apply (λp,q.
+ (∀a.p⎻* a = q⎻* a) ∧
+ (∀a.p⎻ a = q⎻ a) ∧
+ (∀a.p a = q a) ∧
+ (∀a.p* a = q* a));
+ | whd; simplify; intros; repeat split; intros; apply refl;
+ | whd; simplify; intros; cases H; cases H1; cases H3; clear H H3 H1;
+ repeat split; intros; apply sym; generalize in match a;assumption;
+ | whd; simplify; intros; elim DAEMON;]]
qed.
-axiom DAEMON: False.
+lemma hint : ∀P,Q. ORelation_setoid P Q → P ⇒ Q. intros; apply (or_f ?? c);qed.
+coercion hint.
definition composition : ∀P,Q,R.
binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
constructor 1;
[ intros (F G);
constructor 1;
- [ apply (λx.⨍_G (⨍_F x));
+ [ constructor 1; [apply (λx. G (F x)); | intros; apply (†(†H));]
|2,3,4,5,6,7: cases DAEMON;]
| intros; cases DAEMON;]
qed.
[ apply (OAlgebra);
| intros; apply (ORelation_setoid o o1);
| intro O; split;
- [1,2,3,4: apply (λx.x);
- |*:intros;split;intros; assumption; ]
+ [1,2,3,4: constructor 1; [1,3,5,7:apply (λx.x);|*:intros;assumption]
+ |5,6,7:intros;split;intros; assumption; ]
+|4: apply composition;
|*: elim DAEMON;]
qed.
include "o-basic_pairs.ma".
include "o-saturations.ma".
+notation "□ \sub b" non associative with precedence 90 for @{'box $b}.
+notation > "□_term 90 b" non associative with precedence 90 for @{'box $b}.
+interpretation "Universal image ⊩⎻*" 'box x = (or_f_minus_star _ _ (rel x)).
+
+notation "◊ \sub b" non associative with precedence 90 for @{'diamond $b}.
+notation > "◊_term 90 b" non associative with precedence 90 for @{'diamond $b}.
+interpretation "Existential image ⊩" 'diamond x = (or_f _ _ (rel x)).
+
+notation "'Rest' \sub b" non associative with precedence 90 for @{'rest $b}.
+notation > "'Rest'⎽term 90 b" non associative with precedence 90 for @{'rest $b}.
+interpretation "Universal pre-image ⊩*" 'rest x = (or_f_star _ _ (rel x)).
+
+notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
+notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
+interpretation "Existential pre-image ⊩⎻" 'ext x = (or_f_minus _ _ (rel x)).
+
+definition A : ∀b:BP. unary_morphism (oa_P (form b)) (oa_P (form b)).
+intros; constructor 1; [ apply (λx.□_b (Ext⎽b x)); | intros; apply (†(†H));] qed.
+
lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed.
coercion xxx.
+definition d_p_i :
+ ∀S:setoid.∀I:setoid.∀d:unary_morphism S S.∀p:ums I S.ums I S.
+intros; constructor 1; [ apply (λi:I. u (c i));| intros; apply (†(†H));].
+qed.
+
+alias symbol "eq" = "setoid eq".
+alias symbol "and" = "o-algebra binary meet".
record concrete_space : Type ≝
{ bp:> BP;
+ (*distr : is_distributive (form bp);*)
downarrow: unary_morphism (oa_P (form bp)) (oa_P (form bp));
downarrow_is_sat: is_saturation ? downarrow;
converges: ∀q1,q2.
- 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);
+ (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2)));
+ all_covered: Ext⎽bp (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)) ?)
+ downarrow (oa_join ? I (d_p_i ?? downarrow p)) =
+ oa_join ? I (d_p_i ?? downarrow p);
+ il1: ∀q.downarrow (A ? q) = A ? q
}.
-definition bp': concrete_space → basic_pair ≝ λc.bp c.
+interpretation "o-concrete space downarrow" 'downarrow x = (fun_1 __ (downarrow _) x).
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
coercion bp'.
record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
projects / helm.git / commitdiff