helm/software/matita/contribs/dama/dama/bishop_set_rewrite.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.ma".
  16
  17 coercion cic:/matita/dama/bishop_set/eq_sym.con.
  18
  19 lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
  20   λE,x,y,z.eq_trans_ E x z y.
  21
  22 notation > "'Eq'≈" non associative with precedence 50
  23   for @{'eqrewrite}.
  24
  25 interpretation "eq_rew" 'eqrewrite =
  26   (cic:/matita/dama/bishop_set/eq_trans.con _ _ _).
  27
  28 lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
  29 intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
  30 intro Xyz; apply Exy; right; assumption;
  31 qed.
  32
  33 lemma le_rewr: ∀E:ordered_set.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
  34 intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
  35 intro Xyz; apply Exy; left; assumption;
  36 qed.
  37
  38 notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
  39 interpretation "le_rewl" 'lerewritel = (cic:/matita/dama/bishop_set_rewrite/le_rewl.con _ _ _).
  40 notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
  41 interpretation "le_rewr" 'lerewriter = (cic:/matita/dama/bishop_set_rewrite/le_rewr.con _ _ _).
  42
  43 lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
  44 intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
  45 cases (eq_sym ??? Exy H);
  46 qed.
  47
  48 lemma ap_rewr: ∀A:bishop_set.∀x,z,y:A. x ≈ y → z # y → z # x.
  49 intros (A x z y Exy Azy); apply bs_symmetric; apply (ap_rewl ???? Exy);
  50 apply bs_symmetric; assumption;
  51 qed.
  52
  53 notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
  54 interpretation "ap_rewl" 'aprewritel = (cic:/matita/dama/bishop_set_rewrite/ap_rewl.con _ _ _).
  55 notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
  56 interpretation "ap_rewr" 'aprewriter = (cic:/matita/dama/bishop_set_rewrite/ap_rewr.con _ _ _).
  57
  58 lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
  59 intros (A x z y Exy Ayz); cases (os_cotransitive ??? x Ayz); [2:assumption]
  60 cases Exy; right; assumption;
  61 qed.
  62
  63 lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
  64 intros (A x z y Exy Azy); cases (os_cotransitive ???x Azy); [assumption]
  65 cases (Exy); left; assumption;
  66 qed.
  67
  68 notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
  69 interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_rewrite/exc_rewl.con _ _ _).
  70 notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
  71 interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _).
  72
  73
  74 lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
  75 intros (A x y z E H); split; cases H;
  76 [apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
  77 qed.
  78
  79 lemma lt_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y < z → x < z.
  80 intros (A x y z E H); split; cases H;
  81 [apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
  82 qed.
  83
  84 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
  85 interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/bishop_set_rewrite/lt_rewl.con _ _ _).
  86 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
  87 interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/bishop_set_rewrite/lt_rewr.con _ _ _).
  88