matita/matita/re_complete/basics/relations.ma

   1 include "basics/logic.ma".
   2
   3 (********** relations **********)
   4 definition relation : Type[0] → Type[0]
   5 ≝ λA.A→A→Prop.
   6
   7 definition reflexive: ∀A.∀R :relation A.Prop
   8 ≝ λA.λR.∀x:A.R x x.
   9
  10 definition symmetric: ∀A.∀R: relation A.Prop
  11 ≝ λA.λR.∀x,y:A.R x y → R y x.
  12
  13 definition transitive: ∀A.∀R:relation A.Prop
  14 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
  15
  16 definition irreflexive: ∀A.∀R:relation A.Prop
  17 ≝ λA.λR.∀x:A.¬(R x x).
  18
  19 definition cotransitive: ∀A.∀R:relation A.Prop
  20 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
  21
  22 definition tight_apart: ∀A.∀eq,ap:relation A.Prop
  23 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
  24 (eq x y → ¬(ap x y)).
  25
  26 definition antisymmetric: ∀A.∀R:relation A.Prop
  27 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
  28
  29 (********** functions **********)
  30
  31 definition compose ≝
  32   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
  33
  34 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
  35
  36 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
  37 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
  38
  39 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
  40 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
  41
  42 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
  43 ≝ λA.λf.∀x,y.f x y = f y x.
  44
  45 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
  46 ≝ λA,B.λf.∀x,y.f x y = f y x.
  47
  48 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
  49 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
  50
  51 (* functions and relations *)
  52 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
  53 ∀f:A→A.Prop ≝
  54 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
  55
  56 (* functions and functions *)
  57 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
  58 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
  59
  60 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
  61 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
  62
  63 (* extensional equality *)
  64
  65 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
  66 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
  67
  68 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
  69 λA,B.λf,g.∀a.f a = g a.
  70
  71 notation "x \eqR y" non associative with precedence 45
  72 for @{'eqR ? ? x y}.
  73
  74 interpretation "functional extentional equality"
  75 'eqR A B R S = (exteqR A B R S).
  76
  77 notation " f \eqF g " non associative with precedence 45
  78 for @{'eqF ? ? f g}.
  79
  80 interpretation "functional extentional equality"
  81 'eqF A B f g = (exteqF A B f g).
  82