(* *)
(**************************************************************************)
-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.