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 ndefinition reflexive: ∀A:Type.∀R :relation A.Prop
23 ndefinition symmetric: ∀A:Type.∀R: relation A.Prop
24 ≝ λA.λR.∀x,y:A.R x y → R y x.
26 ndefinition transitive: ∀A:Type.∀R:relation A.Prop
27 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
29 ndefinition irreflexive: ∀A:Type.∀R:relation A.Prop
30 ≝ λA.λR.∀x:A.¬(R x x).
32 ndefinition cotransitive: ∀A:Type.∀R:relation A.Prop
33 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
35 ndefinition tight_apart: ∀A:Type.∀eq,ap:relation A.Prop
36 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
39 ndefinition antisymmetric: ∀A:Type.∀R:relation A.Prop
40 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).