matitaB/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 (********** relations **********)
  15 definition relation : Type[0] → Type[0]
  16 ≝ λA.A→A→Prop.
  17
  18 definition reflexive: ∀A.∀R :relation A.Prop
  19 ≝ λA.λR.∀x:A.R x x.
  20
  21 definition symmetric: ∀A.∀R: relation A.Prop
  22 ≝ λA.λR.∀x,y:A.R x y → R y x.
  23
  24 definition transitive: ∀A.∀R:relation A.Prop
  25 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
  26
  27 definition irreflexive: ∀A.∀R:relation A.Prop
  28 ≝ λA.λR.∀x:A.¬(R x x).
  29
  30 definition cotransitive: ∀A.∀R:relation A.Prop
  31 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
  32
  33 definition tight_apart: ∀A.∀eq,ap:relation A.Prop
  34 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
  35 (eq x y → ¬(ap x y)).
  36
  37 definition antisymmetric: ∀A.∀R:relation A.Prop
  38 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
  39
  40 (********** functions **********)
  41
  42 definition compose ≝
  43   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
  44
  45 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
  46
  47 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
  48 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
  49
  50 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
  51 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
  52
  53 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
  54 ≝ λA.λf.∀x,y.f x y = f y x.
  55
  56 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
  57 ≝ λA,B.λf.∀x,y.f x y = f y x.
  58
  59 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
  60 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
  61
  62 (* functions and relations *)
  63 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
  64 ∀f:A→A.Prop ≝
  65 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
  66
  67 (* functions and functions *)
  68 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
  69 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
  70
  71 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
  72 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
  73
  74 lemma injective_compose : ∀A,B,C,f,g.
  75 injective A B f → injective B C g → injective A C (λx.g (f x)).
  76 /3/; qed.
  77
  78 (* extensional equality *)
  79
  80 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
  81 λA.λP,Q.∀a.iff (P a) (Q a).
  82
  83 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
  84 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
  85
  86 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
  87 λA,B.λf,g.∀a.f a = g a.
  88
  89 notation " x \eqP y " non associative with precedence 45
  90 for @{'eqP A $x $y}.
  91
  92 interpretation "functional extentional equality"
  93 'eqP A x y = (exteqP A x y).
  94
  95 notation "x \eqR y" non associative with precedence 45
  96 for @{'eqR ? ? x y}.
  97
  98 interpretation "functional extentional equality"
  99 'eqR A B R S = (exteqR A B R S).
 100
 101 notation " f \eqF g " non associative with precedence 45
 102 for @{'eqF ? ? f g}.
 103
 104 interpretation "functional extentional equality"
 105 'eqF A B f g = (exteqF A B f g).
 106