2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
14 (********** predicates *********)
16 definition predicate: Type[0] → Type[0]
19 (********** relations **********)
20 definition relation : Type[0] → Type[0]
23 definition relation2 : Type[0] → Type[0] → Type[0]
26 definition relation3 : Type[0] → Type[0] → Type[0] → Type[0]
29 definition reflexive: ∀A.∀R :relation A.Prop
32 definition symmetric: ∀A.∀R: relation A.Prop
33 ≝ λA.λR.∀x,y:A.R x y → R y x.
35 definition transitive: ∀A.∀R:relation A.Prop
36 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
38 definition irreflexive: ∀A.∀R:relation A.Prop
39 ≝ λA.λR.∀x:A.¬(R x x).
41 definition cotransitive: ∀A.∀R:relation A.Prop
42 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
44 definition tight_apart: ∀A.∀eq,ap:relation A.Prop
45 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
48 definition antisymmetric: ∀A.∀R:relation A.Prop
49 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
51 (* Reflexive closure ************)
53 definition RC: ∀A:Type[0]. relation A → relation A ≝
54 λA,R,x,y. R … x y ∨ x = y.
56 lemma RC_reflexive: ∀A,R. reflexive A (RC … R).
59 (********** operations **********)
60 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
61 ∃am.R1 a1 am ∧ R2 am a2.
62 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
64 definition Runion ≝ λA.λR1,R2:relation A.λa,b. R1 a b ∨ R2 a b.
65 interpretation "union of relations" 'union R1 R2 = (Runion ? R1 R2).
67 definition Rintersection ≝ λA.λR1,R2:relation A.λa,b.R1 a b ∧ R2 a b.
68 interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? R1 R2).
70 definition inv ≝ λA.λR:relation A.λa,b.R b a.
72 (*********** sub relation ***********)
73 definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
74 interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
77 ∀T.∀R:relation T.R ⊆ R.
81 lemma sub_comp_l: ∀A.∀R,R1,R2:relation A.
82 R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
83 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
86 lemma sub_comp_r: ∀A.∀R,R1,R2:relation A.
87 R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2.
88 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
91 lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A.
92 R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3.
93 #A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/
96 lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A.
97 (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3).
98 #A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/
101 (************* functions ************)
104 λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
106 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
108 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
109 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
111 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
112 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
114 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
115 ≝ λA.λf.∀x,y.f x y = f y x.
117 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
118 ≝ λA,B.λf.∀x,y.f x y = f y x.
120 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
121 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
123 (* functions and relations *)
124 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
126 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
128 (* functions and functions *)
129 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
130 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
132 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
133 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
135 lemma injective_compose : ∀A,B,C,f,g.
136 injective A B f → injective B C g → injective A C (λx.g (f x)).
139 (* extensional equality *)
141 (* moved inside sets.ma
142 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
143 λA.λP,Q.∀a.iff (P a) (Q a). *)
145 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
146 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
148 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
149 λA,B.λf,g.∀a.f a = g a.
152 notation " x \eqP y " non associative with precedence 45
155 interpretation "functional extentional equality"
156 'eqP A x y = (exteqP A x y). *)
158 notation "x \eqR y" non associative with precedence 45
161 interpretation "functional extentional equality"
162 'eqR A B R S = (exteqR A B R S).
164 notation " f \eqF g " non associative with precedence 45
167 interpretation "functional extentional equality"
168 'eqF A B f g = (exteqF A B f g).
170 (********** relations on unboxed pairs **********)
172 definition bi_relation: Type[0] → Type[0] → Type[0]
175 definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
176 ≝ λA,B,R. ∀x,y. R x y x y.
178 definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
179 ∀a1,a2,b1,b2. R a2 b2 a1 b1 → R a1 b1 a2 b2.
181 definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
182 ∀a1,a,b1,b. R a1 b1 a b →
183 ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.