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