matita/matita/lib/basics/relations.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/logic.ma".
  13 include "basics/core_notation/compose_2.ma".
  14 include "basics/core_notation/subseteq_2.ma".
  15
  16 (********** predicates *********)
  17
  18 definition predicate: Type[0] → Type[0]
  19 ≝ λA.A→Prop.
  20
  21 (********** relations **********)
  22 definition relation : Type[0] → Type[0]
  23 ≝ λA.A→A→Prop.
  24
  25 definition relation2 : Type[0] → Type[0] → Type[0]
  26 ≝ λA,B.A→B→Prop.
  27
  28 definition relation3 : Type[0] → Type[0] → Type[0] → Type[0]
  29 ≝ λA,B,C.A→B→C→Prop.
  30
  31 definition relation4 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
  32 ≝ λA,B,C,D.A→B→C→D→Prop.
  33
  34 definition reflexive: ∀A.∀R :relation A.Prop
  35 ≝ λA.λR.∀x:A.R x x.
  36
  37 definition symmetric: ∀A.∀R: relation A.Prop
  38 ≝ λA.λR.∀x,y:A.R x y → R y x.
  39
  40 definition transitive: ∀A.∀R:relation A.Prop
  41 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
  42
  43 definition irreflexive: ∀A.∀R:relation A.Prop
  44 ≝ λA.λR.∀x:A.¬(R x x).
  45
  46 definition cotransitive: ∀A.∀R:relation A.Prop
  47 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
  48
  49 definition tight_apart: ∀A.∀eq,ap:relation A.Prop
  50 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
  51 (eq x y → ¬(ap x y)).
  52
  53 definition antisymmetric: ∀A.∀R:relation A.Prop
  54 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
  55
  56 definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
  57                          ∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
  58
  59 definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
  60                        ∀a1. R a0 a1 → ∀a2. R a0 a2 →
  61                        ∃∃a. R a1 a & R a2 a.
  62
  63 definition confluent: ∀A. predicate (relation A) ≝ λA,R.
  64                       ∀a0. confluent1 … R a0.
  65
  66 (* triangular confluence of two relations *)
  67 definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
  68                   ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b.
  69
  70 (* Reflexive closure ************)
  71
  72 definition RC: ∀A:Type[0]. relation A → relation A ≝
  73                λA,R,x,y. R … x y ∨ x = y.
  74
  75 lemma RC_reflexive: ∀A,R. reflexive A (RC … R).
  76 /2 width=1/ qed.
  77
  78 (********** operations **********)
  79 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
  80   ∃am.R1 a1 am ∧ R2 am a2.
  81 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
  82
  83 definition Runion ≝ λA.λR1,R2:relation A.λa,b. R1 a b ∨ R2 a b.
  84 interpretation "union of relations" 'union R1 R2 = (Runion ? R1 R2).
  85
  86 definition Rintersection ≝ λA.λR1,R2:relation A.λa,b.R1 a b ∧ R2 a b.
  87 interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? R1 R2).
  88
  89 definition inv ≝ λA.λR:relation A.λa,b.R b a.
  90
  91 (*********** sub relation ***********)
  92 definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
  93 interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
  94
  95 lemma sub_reflexive :
  96   ∀T.∀R:relation T.R ⊆ R.
  97 #T #R #x //
  98 qed.
  99
 100 lemma sub_comp_l:  ∀A.∀R,R1,R2:relation A.
 101   R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
 102 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
 103 qed.
 104
 105 lemma sub_comp_r:  ∀A.∀R,R1,R2:relation A.
 106   R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2.
 107 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
 108 qed.
 109
 110 lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A.
 111   R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3.
 112 #A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/
 113 qed.
 114
 115 lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A.
 116   (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3).
 117 #A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/
 118 qed.
 119
 120 (************* functions ************)
 121
 122 definition compose ≝
 123   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
 124
 125 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
 126
 127 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
 128 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
 129
 130 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
 131 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
 132
 133 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
 134 ≝ λA.λf.∀x,y.f x y = f y x.
 135
 136 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
 137 ≝ λA,B.λf.∀x,y.f x y = f y x.
 138
 139 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
 140 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
 141
 142 (* functions and relations *)
 143 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
 144 ∀f:A→A.Prop ≝
 145 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
 146
 147 (* functions and functions *)
 148 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
 149 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
 150
 151 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
 152 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
 153
 154 lemma injective_compose : ∀A,B,C,f,g.
 155 injective A B f → injective B C g → injective A C (λx.g (f x)).
 156 /3/; qed-.
 157
 158 (* extensional equality *)
 159
 160 (* moved inside sets.ma
 161 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
 162 λA.λP,Q.∀a.iff (P a) (Q a). *)
 163
 164 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 165 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
 166
 167 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
 168 λA,B.λf,g.∀a.f a = g a.
 169
 170 (*
 171 notation " x \eqP y " non associative with precedence 45
 172 for @{'eqP A $x $y}.
 173
 174 interpretation "functional extentional equality"
 175 'eqP A x y = (exteqP A x y). *)
 176
 177 notation "x \eqR y" non associative with precedence 45
 178 for @{'eqR ? ? x y}.
 179
 180 interpretation "functional extentional equality"
 181 'eqR A B R S = (exteqR A B R S).
 182
 183 notation " f \eqF g " non associative with precedence 45
 184 for @{'eqF ? ? f g}.
 185
 186 interpretation "functional extentional equality"
 187 'eqF A B f g = (exteqF A B f g).
 188
 189 (********** relations on unboxed pairs **********)
 190
 191 definition bi_relation: Type[0] → Type[0] → Type[0]
 192 ≝ λA,B.A→B→A→B→Prop.
 193
 194 definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
 195 ≝ λA,B,R. ∀a,b. R a b a b.
 196
 197 definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
 198                          ∀a1,a2,b1,b2. R a2 b2 a1 b1 → R a1 b1 a2 b2.
 199
 200 definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
 201                           ∀a1,a,b1,b. R a1 b1 a b →
 202                           ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.
 203
 204 definition bi_RC: ∀A,B:Type[0]. bi_relation A B → bi_relation A B ≝
 205                   λA,B,R,a1,b1,a2,b2. R … a1 b1 a2 b2 ∨ (a1 = a2 ∧ b1 = b2).
 206
 207 lemma bi_RC_reflexive: ∀A,B,R. bi_reflexive A B (bi_RC … R).
 208 /3 width=1/ qed.
 209
 210 (********** relations on unboxed triples **********)
 211
 212 definition tri_relation: Type[0] → Type[0] → Type[0] → Type[0]
 213 ≝ λA,B,C.A→B→C→A→B→C→Prop.
 214
 215 definition tri_reflexive: ∀A,B,C. ∀R:tri_relation A B C. Prop
 216 ≝ λA,B,C,R. ∀a,b,c. R a b c a b c.
 217
 218 definition tri_symmetric: ∀A,B,C. ∀R: tri_relation A B C. Prop ≝ λA,B,C,R.
 219                           ∀a1,a2,b1,b2,c1,c2.
 220                           R a2 b2 c2 a1 b1 c1 → R a1 b1 c1 a2 b2 c2.
 221
 222 definition tri_transitive: ∀A,B,C. ∀R: tri_relation A B C. Prop ≝ λA,B,C,R.
 223                            ∀a1,a,b1,b,c1,c. R a1 b1 c1 a b c →
 224                            ∀a2,b2,c2. R a b c a2 b2 c2 → R a1 b1 c1 a2 b2 c2.