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
  14 (********** predicates *********)
  15
  16 definition predicate: Type[0] → Type[0]
  17 ≝ λA.A→Prop.
  18
  19 (********** relations **********)
  20 definition relation : Type[0] → Type[0]
  21 ≝ λA.A→A→Prop.
  22
  23 definition relation2 : Type[0] → Type[0] → Type[0]
  24 ≝ λA,B.A→B→Prop.
  25
  26 definition reflexive: ∀A.∀R :relation A.Prop
  27 ≝ λA.λR.∀x:A.R x x.
  28
  29 definition symmetric: ∀A.∀R: relation A.Prop
  30 ≝ λA.λR.∀x,y:A.R x y → R y x.
  31
  32 definition transitive: ∀A.∀R:relation A.Prop
  33 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
  34
  35 definition irreflexive: ∀A.∀R:relation A.Prop
  36 ≝ λA.λR.∀x:A.¬(R x x).
  37
  38 definition cotransitive: ∀A.∀R:relation A.Prop
  39 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
  40
  41 definition tight_apart: ∀A.∀eq,ap:relation A.Prop
  42 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
  43 (eq x y → ¬(ap x y)).
  44
  45 definition antisymmetric: ∀A.∀R:relation A.Prop
  46 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
  47
  48 (********** operations **********)
  49 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
  50   ∃am.R1 a1 am ∧ R2 am a2.
  51 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
  52
  53 definition Runion ≝ λA.λR1,R2:relation A.λa,b. R1 a b ∨ R2 a b.
  54 interpretation "union of relations" 'union R1 R2 = (Runion ? R1 R2).
  55
  56 definition Rintersection ≝ λA.λR1,R2:relation A.λa,b.R1 a b ∧ R2 a b.
  57 interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? R1 R2).
  58
  59 definition inv ≝ λA.λR:relation A.λa,b.R b a.
  60
  61 (*********** sub relation ***********)
  62 definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
  63 interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
  64
  65 lemma sub_reflexive :
  66   ∀T.∀R:relation T.R ⊆ R.
  67 #T #R #x //
  68 qed.
  69
  70 lemma sub_comp_l:  ∀A.∀R,R1,R2:relation A.
  71   R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
  72 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
  73 qed.
  74
  75 lemma sub_comp_r:  ∀A.∀R,R1,R2:relation A.
  76   R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2.
  77 #A #R #R1 #R2 #Hsub #a #b * #c * /4/
  78 qed.
  79
  80 lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A.
  81   R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3.
  82 #A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/
  83 qed.
  84
  85 lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A.
  86   (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3).
  87 #A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/
  88 qed.
  89
  90 (************* functions ************)
  91
  92 definition compose ≝
  93   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
  94
  95 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
  96
  97 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
  98 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
  99
 100 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
 101 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
 102
 103 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
 104 ≝ λA.λf.∀x,y.f x y = f y x.
 105
 106 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
 107 ≝ λA,B.λf.∀x,y.f x y = f y x.
 108
 109 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
 110 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
 111
 112 (* functions and relations *)
 113 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
 114 ∀f:A→A.Prop ≝
 115 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
 116
 117 (* functions and functions *)
 118 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
 119 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
 120
 121 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
 122 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
 123
 124 lemma injective_compose : ∀A,B,C,f,g.
 125 injective A B f → injective B C g → injective A C (λx.g (f x)).
 126 /3/; qed-.
 127
 128 (* extensional equality *)
 129
 130 (* moved inside sets.ma
 131 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
 132 λA.λP,Q.∀a.iff (P a) (Q a). *)
 133
 134 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 135 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
 136
 137 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
 138 λA,B.λf,g.∀a.f a = g a.
 139
 140 (*
 141 notation " x \eqP y " non associative with precedence 45
 142 for @{'eqP A $x $y}.
 143
 144 interpretation "functional extentional equality"
 145 'eqP A x y = (exteqP A x y). *)
 146
 147 notation "x \eqR y" non associative with precedence 45
 148 for @{'eqR ? ? x y}.
 149
 150 interpretation "functional extentional equality"
 151 'eqR A B R S = (exteqR A B R S).
 152
 153 notation " f \eqF g " non associative with precedence 45
 154 for @{'eqF ? ? f g}.
 155
 156 interpretation "functional extentional equality"
 157 'eqF A B f g = (exteqF A B f g).
 158