1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/cprop_connectives.ma".
17 record powerset (A: Type) : Type ≝ { char: A → CProp }.
19 interpretation "powerset" 'powerset A = (powerset A).
21 interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
23 definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
25 interpretation "mem" 'mem a S = (mem _ S a).
27 definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
29 interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
31 definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
33 interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
35 definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
37 interpretation "intersects" 'intersects U V = (intersects _ U V).
39 definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
41 interpretation "union" 'union U V = (union _ U V).
43 record ssigma (A:Type) (S: powerset A) : Type ≝
50 record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝
51 { satisfy:2> U → V → CProp }.
53 (*notation < "hvbox (x (\circ term 19 r \frac \nbsp \circ) y)" with precedence 45 for @{'satisfy $r $x $y}.*)
54 notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}.
55 notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
56 interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y).
58 definition composition:
59 ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C.
60 binary_relation ?? U1 U2 → binary_relation ?? U2 U3 →
61 binary_relation ?? U1 U3.
62 intros (A B C U1 U2 U3 R12 R23);
65 apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
68 interpretation "binary relation composition" 'compose x y = (composition ______ x y).
70 definition equal_relations ≝
71 λA,B,U,V.λr,r': binary_relation A B U V.
74 interpretation "equal relation" 'eq x y = (equal_relations ____ x y).
76 lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V).
77 intros 5; intros 2; split; intro; assumption.
80 lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V).
81 intros 7; intros 2; split; intro;
82 [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
85 lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V).
86 intros 9; intros 2; split; intro;
87 [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
88 [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
93 ∀A,B,U,V.∀r1,r1',r2,r2':binary_relation A B U V.
94 r1' = r1 → r2 = r2' → r1 = r2 → r1' = r2'.
97 [ apply (if ?? (H1 ??));
98 apply (if ?? (H2 ??));
101 | apply (fi ?? (H ??));
102 apply (fi ?? (H2 ??));
103 apply (fi ?? (H1 ??));
108 lemma associative_composition:
109 ∀A,B,C,D.∀U1,U2,U3,U4.
110 ∀r1:binary_relation A B U1 U2.
111 ∀r2:binary_relation B C U2 U3.
112 ∀r3:binary_relation C D U3 U4.
113 (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
116 cases H; clear H; cases H1; clear H1;
117 [cases H; clear H | cases H2; clear H2]
119 exists; try assumption;
120 split; try assumption;
121 exists; try assumption;
125 lemma composition_morphism:
127 ∀r1,r1':binary_relation A B U1 U2.
128 ∀r2,r2':binary_relation B C U2 U3.
129 r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
130 intros 14; split; intro;
131 cases H2; clear H2; cases H3; clear H3;
132 [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
133 [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
134 exists; try assumption;
138 include "logic/equality.ma".
140 definition singleton ≝ λA:Type.λa:A.{b | a=b}.
142 interpretation "singleton" 'singl a = (singleton _ a).