matita/matita/contribs/ng_assembly/num/comp_num_lemmas.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 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/comp_num.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* **** *)
  27 (* BYTE *)
  28 (* **** *)
  29
  30 nlemma cn_destruct_1 :
  31 ∀T.∀x1,x2,y1,y2:T.
  32  mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → x1 = x2.
  33  #T; #x1; #x2; #y1; #y2; #H;
  34  nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num a _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma cn_destruct_2 :
  41 ∀T.∀x1,x2,y1,y2:T.
  42  mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → y1 = y2.
  43  #T; #x1; #x2; #y1; #y2; #H;
  44  nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num _ b ⇒ y1 = b ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_eqcn :
  51 ∀T.∀feq:T → T → bool.
  52  (symmetricT T bool feq) →
  53  (symmetricT (comp_num T) bool (eq2_cn T feq)).
  54  #T; #feq; #H;
  55  #b1; nelim b1; #e1; #e2;
  56  #b2; nelim b2; #e3; #e4;
  57  nchange with (((feq e1 e3)⊗(feq e2 e4)) = ((feq e3 e1)⊗(feq e4 e2)));
  58  nrewrite > (H e1 e3);
  59  nrewrite > (H e2 e4);
  60  napply refl_eq.
  61 nqed.
  62
  63 nlemma eqcn_to_eq :
  64 ∀T.∀feq:T → T → bool.
  65  (∀x,y:T.(feq x y = true) → (x = y)) →
  66  (∀b1,b2:comp_num T.
  67   ((eq2_cn T feq b1 b2 = true) → (b1 = b2))).
  68  #T; #feq; #H; #b1; #b2;
  69  nelim b1; #e1; #e2;
  70  nelim b2; #e3; #e4;
  71  nchange in ⊢ (% → ?) with (((feq e1 e3)⊗(feq e2 e4)) = true);
  72  #H1;
  73  nrewrite < (H … (andb_true_true_l … H1));
  74  nrewrite < (H … (andb_true_true_r … H1));
  75  napply refl_eq.
  76 nqed.
  77
  78 nlemma eq_to_eqcn :
  79 ∀T.∀feq:T → T → bool.
  80  (∀x,y:T.(x = y) → (feq x y = true)) →
  81  (∀b1,b2:comp_num T.
  82   ((b1 = b2) → (eq2_cn T feq b1 b2 = true))).
  83  #T; #feq; #H; #b1; #b2;
  84  nelim b1; #e1; #e2;
  85  nelim b2; #e3; #e4;
  86  #H1;
  87  nrewrite < (cn_destruct_1 … H1);
  88  nrewrite < (cn_destruct_2 … H1);
  89  nchange with (((feq e1 e1)⊗(feq e2 e2)) = true);
  90  nrewrite > (H e1 e1 (refl_eq …));
  91  nrewrite > (H e2 e2 (refl_eq …));
  92  nnormalize;
  93  napply refl_eq.
  94 nqed.
  95
  96 nlemma decidable_cn_aux1 :
  97 ∀T.∀e1,e2,e3,e4:T.e1 ≠ e3 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
  98  #T; #e1; #e2; #e3; #e4;
  99  nnormalize; #H; #H1;
 100  napply (H (cn_destruct_1 … H1)).
 101 nqed.
 102
 103 nlemma decidable_cn_aux2 :
 104 ∀T.∀e1,e2,e3,e4:T.e2 ≠ e4 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
 105  #T; #e1; #e2; #e3; #e4;
 106  nnormalize; #H; #H1;
 107  napply (H (cn_destruct_2 … H1)).
 108 nqed.
 109
 110 nlemma decidable_cn :
 111 ∀T.(∀x,y:T.decidable (x = y)) →
 112    (∀b1,b2:comp_num T.
 113     (decidable (b1 = b2))).
 114  #T; #H;
 115  #b1; nelim b1; #e1; #e2;
 116  #b2; nelim b2; #e3; #e4;
 117  nnormalize;
 118  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
 119  ##[ ##2: #H1; napply (or2_intro2 … (decidable_cn_aux1 T e1 e2 e3 e4 H1))
 120  ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
 121           ##[ ##2: #H2; napply (or2_intro2 … (decidable_cn_aux2 T e1 e2 e3 e4 H2))
 122           ##| ##1: #H2; nrewrite > H1; nrewrite > H2;
 123                         napply (or2_intro1 … (refl_eq ? (mk_comp_num T e3 e4)))
 124           ##]
 125  ##]
 126 nqed.
 127
 128 nlemma neqcn_to_neq :
 129 ∀T.∀feq:T → T → bool.
 130  (∀x,y:T.(feq x y = false) → (x ≠ y)) →
 131  (∀b1,b2:comp_num T.
 132   ((eq2_cn T feq b1 b2 = false) → (b1 ≠ b2))).
 133  #T; #feq; #H; #b1; #b2;
 134  nelim b1; #e1; #e2;
 135  nelim b2; #e3; #e4;
 136  nchange with ((((feq e1 e3) ⊗ (feq e2 e4)) = false) → ?);
 137  #H1;
 138  napply (or2_elim ((feq e1 e3) = false) ((feq e2 e4) = false) ? (andb_false2 … H1) …);
 139  ##[ ##1: #H2; napply (decidable_cn_aux1 … (H … H2))
 140  ##| ##2: #H2; napply (decidable_cn_aux2 … (H … H2))
 141  ##]
 142 nqed.
 143
 144 nlemma cn_destruct :
 145 ∀T.(∀x,y:T.decidable (x = y)) →
 146    (∀e1,e2,e3,e4:T.
 147     ((mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4)) →
 148     ((e1 ≠ e3) ∨ (e2 ≠ e4))).
 149  #T; #H; #e1; #e2; #e3; #e4;
 150  nnormalize; #H1;
 151  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
 152  ##[ ##2: #H2; napply (or2_intro1 … H2)
 153  ##| ##1: #H2; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
 154           ##[ ##2: #H3; napply (or2_intro2 … H3)
 155           ##| ##1: #H3; nrewrite > H2 in H1:(%);
 156                    nrewrite > H3;
 157                    #H1; nelim (H1 (refl_eq …))
 158           ##]
 159  ##]
 160 nqed.
 161
 162 nlemma neq_to_neqcn :
 163 ∀T.∀feq:T → T → bool.
 164  (∀x,y:T.(x ≠ y) → (feq x y = false)) →
 165  (∀x,y:T.decidable (x = y)) →
 166  (∀b1,b2:comp_num T.
 167   ((b1 ≠ b2) → (eq2_cn T feq b1 b2 = false))).
 168  #T; #feq; #H; #H1; #b1; #b2;
 169  nelim b1; #e1; #e2;
 170  nelim b2; #e3; #e4;
 171  #H2; nchange with (((feq e1 e3) ⊗ (feq e2 e4)) = false);
 172  napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (cn_destruct T H1 e1 e2 e3 e4 … H2) …);
 173  ##[ ##1: #H3; nrewrite > (H … H3); nnormalize; napply refl_eq
 174  ##| ##2: #H3; nrewrite > (H … H3);
 175           nrewrite > (symmetric_andbool (feq e1 e3) false);
 176           nnormalize; napply refl_eq
 177  ##]
 178 nqed.