1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "cprop_connectives.ma".
18 record ordered_set: Type ≝ {
20 os_excess: os_carr → os_carr → CProp;
21 os_coreflexive: coreflexive ? os_excess;
22 os_cotransitive: cotransitive ? os_excess
25 interpretation "Ordered set excess" 'nleq a b = (os_excess _ a b).
27 (* Definition 2.2 (3) *)
28 definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b).
30 interpretation "Ordered set greater or equal than" 'geq a b = (le _ b a).
32 interpretation "Ordered set less or equal than" 'leq a b = (le _ a b).
34 lemma le_reflexive: ∀E.reflexive ? (le E).
35 unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H);
38 lemma le_transitive: ∀E.transitive ? (le E).
39 unfold transitive; intros 7 (E x y z H1 H2 H3); cases (os_cotransitive ??? y H3) (H4 H4);
40 [cases (H1 H4)|cases (H2 H4)]
44 lemma exc_le_variance:
45 ∀O:ordered_set.∀a,b,a',b':O.a ≰ b → a ≤ a' → b' ≤ b → a' ≰ b'.
46 intros (O a b a1 b1 Eab Laa1 Lb1b);
47 cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
48 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]