1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "Plogic/connectives.ma".
17 ndefinition relation : Type \to Type
20 nrecord relation (A:Type) : Type ≝
23 ndefinition reflexive: ∀A:Type.∀R :relation A.Prop
26 ndefinition symmetric: ∀A:Type.∀R: relation A.Prop
27 ≝ λA.λR.∀x,y:A.R x y → R y x.
29 ndefinition transitive: ∀A:Type.∀R:relation A.Prop
30 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
32 ndefinition irreflexive: ∀A:Type.∀R:relation A.Prop
33 ≝ λA.λR.∀x:A.¬(R x x).
35 ndefinition cotransitive: ∀A:Type.∀R:relation A.Prop
36 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
38 ndefinition tight_apart: ∀A:Type.∀eq,ap:relation A.Prop
39 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
42 ndefinition antisymmetric: ∀A:Type.∀R:relation A.Prop
43 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).