helm/software/matita/contribs/dama/dama/extra.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "bishop_set_rewrite.ma".
  16
  17 definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x # y.
  18
  19
  20
  21 definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
  22
  23 interpretation "ordered sets less than" 'lt a b = (lt _ a b).
  24
  25 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
  26 intros 2 (E x); intro H; cases H (_ ABS);
  27 apply (ap_coreflexive ? x ABS);
  28 qed.
  29
  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)]]
  36 qed.
  37
  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 *)
  41 qed.
  42
  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;
  46 qed.
  47
  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;
  51 qed.
  52
  53 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
  54 interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
  55 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
  56 interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
  57
  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)]
  62 right; assumption;
  63 qed.
  64
  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]
  69 cases LE; assumption;
  70 qed.
  71
  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;
  74 qed.
  75
  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.
  79 qed.
  80
  81 lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a.
  82 intros; split; assumption;
  83 qed.
  84
  85 definition total_order_property : ∀E:excess. Type ≝
  86   λE:excess. ∀a,b:E. a ≰ b → b < a.
  87