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