helm/software/matita/contribs/ng_assembly/utility/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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "utility/string.ma".
  24 include "utility/ascii_lemmas2.ma".
  25
  26 (* ************************ *)
  27 (* MANIPOLAZIONE DI STRINGA *)
  28 (* ************************ *)
  29
  30 nlemma symmetric_eqstr : symmetricT aux_str_type bool eq_str.
  31  #l1;
  32  napply (list_ind ascii ??? l1);
  33  ##[ ##1: #l2; ncases l2;
  34           ##[ ##1: nnormalize; napply (refl_eq ??)
  35           ##| ##2: #x; #y; nnormalize; napply (refl_eq ??)
  36           ##]
  37  ##| ##2: #x1; #x2; #H; #l2; ncases l2;
  38           ##[ ##1: nnormalize; napply (refl_eq ??)
  39           ##| ##2: #y1; #y2;
  40                    nchange with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = ((eq_ascii y1 x1)⊗(eq_str y2 x2)));
  41                    nrewrite > (symmetric_eqascii x1 y1);
  42                    nrewrite > (H y2);
  43                    napply (refl_eq ??)
  44           ##]
  45  ##]
  46 nqed.
  47
  48 nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'.
  49  #l1;
  50  napply (list_ind ascii ??? l1);
  51  ##[ ##1: #l2; ncases l2;
  52           ##[ ##1: nnormalize; #H; napply (refl_eq ??)
  53           ##| ##2: #x1; #x2; nnormalize; #H; napply (bool_destruct ??? H)
  54           ##]
  55  ##| ##2: #x1; #x2; #H; #l2; ncases l2;
  56           ##[ ##1: nnormalize; #H1; napply (bool_destruct ??? H1)
  57           ##| ##2: #y1; #y2; #H1;
  58                    nchange in H1:(%) with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = true);
  59                    nrewrite > (eqascii_to_eq x1 y1 (andb_true_true_l ?? H1));
  60                    nrewrite > (H y2 (andb_true_true_r ?? H1));
  61                    napply (refl_eq ??)
  62           ##]
  63  ##]
  64 nqed.
  65
  66 nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
  67  #l1;
  68  napply (list_ind ascii ??? l1);
  69  ##[ ##1: #l2; ncases l2;
  70           ##[ ##1: nnormalize; #H; napply (refl_eq ??)
  71           ##| ##2: #x1; #x2; nnormalize; #H; nelim (list_destruct_nil_cons ascii ?? H)
  72           ##]
  73  ##| ##2: #x1; #x2; #H; #l2; ncases l2;
  74           ##[ ##1: #H; nelim (list_destruct_cons_nil ascii ?? H)
  75           ##| ##2: #y1; #y2; #H1;
  76                    nrewrite > (list_destruct_1 ascii ???? H1);
  77                    nchange with (((eq_ascii y1 y1)⊗(eq_str x2 y2)) = true);
  78                    nrewrite > (H y2 (list_destruct_2 ascii ???? H1));
  79                    nrewrite > (eq_to_eqascii y1 y1 (refl_eq ??));
  80                    nnormalize;
  81                    napply (refl_eq ??)
  82           ##]
  83  ##]
  84 nqed.
  85
  86 (* ************ *)
  87 (* STRINGA + ID *)
  88 (* ************ *)
  89
  90 nlemma strid_destruct_1 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → x1 = x2.
  91  #x1; #x2; #y1; #y2; #H;
  92  nchange with (match STR_ID x2 y2 with [ STR_ID a _ ⇒ x1 = a ]);
  93  nrewrite < H;
  94  nnormalize;
  95  napply (refl_eq ??).
  96 nqed.
  97
  98 nlemma strid_destruct_2 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → y1 = y2.
  99  #x1; #x2; #y1; #y2; #H;
 100  nchange with (match STR_ID x2 y2 with [ STR_ID _ b ⇒ y1 = b ]);
 101  nrewrite < H;
 102  nnormalize;
 103  napply (refl_eq ??).
 104 nqed.
 105
 106 nlemma symmetric_eqstrid : symmetricT aux_strId_type bool eq_strId.
 107  #si1; #si2;
 108  ncases si1;
 109  #l1; #n1;
 110  ncases si2;
 111  #l2; #n2;
 112  nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = ((eq_str l2 l1)⊗(eq_nat n2 n1)));
 113  nrewrite > (symmetric_eqstr l1 l2);
 114  nrewrite > (symmetric_eqnat n1 n2);
 115  napply (refl_eq ??).
 116 nqed.
 117
 118 nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
 119   #si1; #si2;
 120  ncases si1;
 121  #l1; #n1;
 122  ncases si2;
 123  #l2; #n2; #H;
 124  nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
 125  nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l ?? H));
 126  nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r ?? H));
 127  napply (refl_eq ??).
 128 nqed.
 129
 130 nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
 131   #si1; #si2;
 132  ncases si1;
 133  #l1; #n1;
 134  ncases si2;
 135  #l2; #n2; #H;
 136  nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
 137  nrewrite > (strid_destruct_1 ???? H);
 138  nrewrite > (strid_destruct_2 ???? H);
 139  nrewrite > (eq_to_eqstr l2 l2 (refl_eq ??));
 140  nrewrite > (eq_to_eqnat n2 n2 (refl_eq ??));
 141  nnormalize;
 142  napply (refl_eq ??).
 143 nqed.