helm/software/matita/contribs/ng_assembly/common/string_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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/string.ma".
  24 include "common/ascii_lemmas2.ma".
  25 include "common/ascii_lemmas3.ma".
  26 include "common/ascii_lemmas4.ma".
  27 include "common/ascii_lemmas5.ma".
  28 include "common/list_utility_lemmas.ma".
  29
  30 (* ************************ *)
  31 (* MANIPOLAZIONE DI STRINGA *)
  32 (* ************************ *)
  33
  34 nlemma symmetric_eqstr : symmetricT (list ascii) bool eq_str.
  35  #s1; #s2;
  36  napply (symmetric_bfoldrightlist2 ascii eq_ascii s1 s2 symmetric_eqascii).
  37 nqed.
  38
  39 nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'.
  40  #s1; #s2;
  41  napply (bfoldrightlist2_to_eq ascii eq_ascii s1 s2 eqascii_to_eq).
  42 nqed.
  43
  44 nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
  45  #s1; #s2;
  46  napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii).
  47 nqed.
  48
  49 nlemma decidable_str : ∀x,y:list ascii.decidable (x = y).
  50  napply (decidable_list ascii …);
  51  napply decidable_ascii.
  52 nqed.
  53
  54 nlemma neqstr_to_neq : ∀s,s'.eq_str s s' = false → s ≠ s'.
  55  #s1; #s2;
  56  napply (nbfoldrightlist2_to_neq ascii eq_ascii s1 s2 …);
  57  napply neqascii_to_neq.
  58 nqed.
  59
  60 nlemma neq_to_neqstr : ∀s,s'.s ≠ s' → eq_str s s' = false.
  61  #s1; #s2;
  62  napply (neq_to_nbfoldrightlist2 ascii eq_ascii s1 s2 …);
  63  ##[ ##1: napply decidable_ascii
  64  ##| ##2: napply neq_to_neqascii
  65  ##]
  66 nqed.
  67
  68 (* ************ *)
  69 (* STRINGA + ID *)
  70 (* ************ *)
  71
  72 nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1 = x2.
  73  #x1; #x2; #y1; #y2; #H;
  74  nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]);
  75  nrewrite < H;
  76  nnormalize;
  77  napply refl_eq.
  78 nqed.
  79
  80 nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2.
  81  #x1; #x2; #y1; #y2; #H;
  82  nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]);
  83  nrewrite < H;
  84  nnormalize;
  85  napply refl_eq.
  86 nqed.
  87
  88 nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
  89  #si1; #si2;
  90  nchange with (
  91   ((eq_str (str_elem si1) (str_elem si2))⊗(eq_nat (id_elem si1) (id_elem si2))) =
  92   ((eq_str (str_elem si2) (str_elem si1))⊗(eq_nat (id_elem si2) (id_elem si1))));
  93  nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
  94  nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
  95  napply refl_eq.
  96 nqed.
  97
  98 nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
  99  #si1; #si2;
 100  nelim si1;
 101  #l1; #n1;
 102  nelim si2;
 103  #l2; #n2; #H;
 104  nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
 105  nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l … H));
 106  nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r … H));
 107  napply refl_eq.
 108 nqed.
 109
 110 nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
 111  #si1; #si2;
 112  nelim si1;
 113  #l1; #n1;
 114  nelim si2;
 115  #l2; #n2; #H;
 116  nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
 117  nrewrite > (strid_destruct_1 … H);
 118  nrewrite > (strid_destruct_2 … H);
 119  nrewrite > (eq_to_eqstr l2 l2 (refl_eq …));
 120  nrewrite > (eq_to_eqnat n2 n2 (refl_eq …));
 121  nnormalize;
 122  napply refl_eq.
 123 nqed.
 124
 125 nlemma decidable_strid_aux1 : ∀s1,n1,s2,n2.s1 ≠ s2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
 126  #s1; #n1; #s2; #n2;
 127  nnormalize; #H; #H1;
 128  napply (H (strid_destruct_1 … H1)).
 129 nqed.
 130
 131 nlemma decidable_strid_aux2 : ∀s1,n1,s2,n2.n1 ≠ n2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
 132  #s1; #n1; #s2; #n2;
 133  nnormalize; #H; #H1;
 134  napply (H (strid_destruct_2 … H1)).
 135 nqed.
 136
 137 nlemma decidable_strid : ∀x,y:strId.decidable (x = y).
 138  #x; nelim x; #s1; #n1;
 139  #y; nelim y; #s2; #n2;
 140  nnormalize;
 141  napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
 142  ##[ ##2: #H; napply (or2_intro2 … (decidable_strid_aux1 … H))
 143  ##| ##1: #H; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
 144           ##[ ##2: #H1; napply (or2_intro2 … (decidable_strid_aux2 … H1))
 145           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
 146                         napply (or2_intro1 … (refl_eq ? (mk_strId s2 n2)))
 147           ##]
 148  ##]
 149 nqed.
 150
 151 nlemma neqstrid_to_neq : ∀sid1,sid2:strId.(eq_strId sid1 sid2 = false) → (sid1 ≠ sid2).
 152  #sid1; nelim sid1; #s1; #n1;
 153  #sid2; nelim sid2; #s2; #n2;
 154  nchange with ((((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false) → ?);
 155  #H;
 156  napply (or2_elim ((eq_str s1 s2) = false) ((eq_nat n1 n2) = false) ? (andb_false2 … H) …);
 157  ##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1))
 158  ##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1))
 159  ##]
 160 nqed.
 161
 162 nlemma strid_destruct : ∀s1,s2,n1,n2.(mk_strId s1 n1) ≠ (mk_strId s2 n2) → s1 ≠ s2 ∨ n1 ≠ n2.
 163  #s1; #s2; #n1; #n2;
 164  nnormalize; #H;
 165  napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
 166  ##[ ##2: #H1; napply (or2_intro1 … H1)
 167  ##| ##1: #H1; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
 168           ##[ ##2: #H2; napply (or2_intro2 … H2)
 169           ##| ##1: #H2; nrewrite > H1 in H:(%);
 170                    nrewrite > H2;
 171                    #H; nelim (H (refl_eq …))
 172           ##]
 173  ##]
 174 nqed.
 175
 176 nlemma neq_to_neqstrid : ∀sid1,sid2.sid1 ≠ sid2 → eq_strId sid1 sid2 = false.
 177  #sid1; nelim sid1; #s1; #n1;
 178  #sid2; nelim sid2; #s2; #n2;
 179  #H; nchange with (((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false);
 180  napply (or2_elim (s1 ≠ s2) (n1 ≠ n2) ? (strid_destruct … H) …);
 181  ##[ ##1: #H1; nrewrite > (neq_to_neqstr … H1); nnormalize; napply refl_eq
 182  ##| ##2: #H1; nrewrite > (neq_to_neqnat … H1);
 183           nrewrite > (symmetric_andbool (eq_str s1 s2) false);
 184           nnormalize; napply refl_eq
 185  ##]
 186 nqed.