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 "bishop_set_rewrite.ma".
17 definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x # y.
21 definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
23 interpretation "ordered sets less than" 'lt a b = (cic:/matita/dama/excess/lt.con _ a b).
25 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
26 intros 2 (E x); intro H; cases H (_ ABS);
27 apply (ap_coreflexive ? x ABS);
30 lemma lt_transitive: ∀E.transitive ? (lt E).
31 intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
32 split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
33 cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
34 [1: cases (exc_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (exc_coreflexive ?? X)]
35 |2: cases (exc_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
38 theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
39 intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
40 fold normalize (b ≰ a); assumption; (* BUG *)
43 lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
44 intros (A x y z E H); split; cases H;
45 [apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
48 lemma lt_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y < z → x < z.
49 intros (A x y z E H); split; cases H;
50 [apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
53 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
54 interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/excess/lt_rewl.con _ _ _).
55 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
56 interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/excess/lt_rewr.con _ _ _).
58 lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
59 intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
60 cases APx (EXx EXx); [cases (LEx EXx)]
61 cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)]
65 lemma le_lt_transitive: ∀A:excess.∀x,y,z:A.x ≤ y → y < z → x < z.
66 intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)]
67 cases APx (EXx EXx); [cases (LEx EXx)]
68 cases (exc_cotransitive ??? x EXx) (EXz EXz); [right; assumption]
72 lemma le_le_eq: ∀E:excess.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
73 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
76 lemma eq_le_le: ∀E:excess.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a.
77 intros (E x y H); whd in H;
78 split; intro; apply H; [left|right] assumption.
81 lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a.
82 intros; split; assumption;
85 definition total_order_property : ∀E:excess. Type ≝
86 λE:excess. ∀a,b:E. a ≰ b → b < a.