helm/software/matita/contribs/ng_assembly2/common/string.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/ascii.ma".
  24 include "common/list.ma".
  25
  26 (* ******* *)
  27 (* STRINGA *)
  28 (* ******* *)
  29
  30 (* tipo pubblico *)
  31 ndefinition aux_str_type ≝ list ascii.
  32
  33 unification hint 0 ≔ ⊢ carr (list_is_comparable ascii_is_comparable) ≡ list ascii.
  34 unification hint 0 ≔ ⊢ carr (list_is_comparable ascii_is_comparable) ≡ aux_str_type.
  35
  36 (* ************ *)
  37 (* STRINGA + ID *)
  38 (* ************ *)
  39
  40 (* tipo pubblico *)
  41 nrecord strId : Type ≝
  42  {
  43  str_elem: aux_str_type;
  44  id_elem: nat
  45  }.
  46
  47 (* confronto *)
  48 ndefinition eq_strId ≝
  49 λsid,sid':strId.
  50  (eqc ? (str_elem sid) (str_elem sid'))⊗
  51  (eqc ? (id_elem sid) (id_elem sid')).
  52
  53 nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1 = x2.
  54  #x1; #x2; #y1; #y2; #H;
  55  nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]);
  56  nrewrite < H;
  57  nnormalize;
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2.
  62  #x1; #x2; #y1; #y2; #H;
  63  nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]);
  64  nrewrite < H;
  65  nnormalize;
  66  napply refl_eq.
  67 nqed.
  68
  69 nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
  70  #si1; #si2;
  71  nchange with (
  72   ((eqc ? (str_elem si1) (str_elem si2))⊗(eqc ? (id_elem si1) (id_elem si2))) =
  73   ((eqc ? (str_elem si2) (str_elem si1))⊗(eqc ? (id_elem si2) (id_elem si1))));
  74  nrewrite > (symmetric_eqc ? (str_elem si1) (str_elem si2));
  75  nrewrite > (symmetric_eqc ? (id_elem si1) (id_elem si2));
  76  napply refl_eq.
  77 nqed.
  78
  79 nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
  80  #si1; #si2;
  81  nelim si1;
  82  #l1; #n1;
  83  nelim si2;
  84  #l2; #n2; #H;
  85  nchange in H:(%) with (((eqc ? l1 l2)⊗(eqc ? n1 n2)) = true);
  86  nrewrite > (eqc_to_eq ? l1 l2 (andb_true_true_l … H));
  87  nrewrite > (eqc_to_eq ? n1 n2 (andb_true_true_r … H));
  88  napply refl_eq.
  89 nqed.
  90
  91 nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
  92  #si1; #si2;
  93  nelim si1;
  94  #l1; #n1;
  95  nelim si2;
  96  #l2; #n2; #H;
  97  nchange with (((eqc ? l1 l2)⊗(eqc ? n1 n2)) = true);
  98  nrewrite > (strid_destruct_1 … H);
  99  nrewrite > (strid_destruct_2 … H);
 100  nrewrite > (eq_to_eqc ? l2 l2 (refl_eq …));
 101  nrewrite > (eq_to_eqc ? n2 n2 (refl_eq …));
 102  nnormalize;
 103  napply refl_eq.
 104 nqed.
 105
 106 nlemma decidable_strid_aux1 : ∀s1,n1,s2,n2.s1 ≠ s2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
 107  #s1; #n1; #s2; #n2;
 108  nnormalize; #H; #H1;
 109  napply (H (strid_destruct_1 … H1)).
 110 nqed.
 111
 112 nlemma decidable_strid_aux2 : ∀s1,n1,s2,n2.n1 ≠ n2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
 113  #s1; #n1; #s2; #n2;
 114  nnormalize; #H; #H1;
 115  napply (H (strid_destruct_2 … H1)).
 116 nqed.
 117
 118 nlemma decidable_strid : ∀x,y:strId.decidable (x = y).
 119  #x; nelim x; #s1; #n1;
 120  #y; nelim y; #s2; #n2;
 121  nnormalize;
 122  napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_c ? s1 s2) …);
 123  ##[ ##2: #H; napply (or2_intro2 … (decidable_strid_aux1 … H))
 124  ##| ##1: #H; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_c ? n1 n2) …);
 125           ##[ ##2: #H1; napply (or2_intro2 … (decidable_strid_aux2 … H1))
 126           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
 127                         napply (or2_intro1 … (refl_eq ? (mk_strId s2 n2)))
 128           ##]
 129  ##]
 130 nqed.
 131
 132 nlemma neqstrid_to_neq : ∀sid1,sid2:strId.(eq_strId sid1 sid2 = false) → (sid1 ≠ sid2).
 133  #sid1; nelim sid1; #s1; #n1;
 134  #sid2; nelim sid2; #s2; #n2;
 135  nchange with ((((eqc ? s1 s2) ⊗ (eqc ? n1 n2)) = false) → ?);
 136  #H;
 137  napply (or2_elim ((eqc ? s1 s2) = false) ((eqc ? n1 n2) = false) ? (andb_false2 … H) …);
 138  ##[ ##1: #H1; napply (decidable_strid_aux1 … (neqc_to_neq … H1))
 139  ##| ##2: #H1; napply (decidable_strid_aux2 … (neqc_to_neq … H1))
 140  ##]
 141 nqed.
 142
 143 nlemma strid_destruct : ∀s1,s2,n1,n2.(mk_strId s1 n1) ≠ (mk_strId s2 n2) → s1 ≠ s2 ∨ n1 ≠ n2.
 144  #s1; #s2; #n1; #n2;
 145  nnormalize; #H;
 146  napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_c ? s1 s2) …);
 147  ##[ ##2: #H1; napply (or2_intro1 … H1)
 148  ##| ##1: #H1; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_c ? n1 n2) …);
 149           ##[ ##2: #H2; napply (or2_intro2 … H2)
 150           ##| ##1: #H2; nrewrite > H1 in H:(%);
 151                    nrewrite > H2;
 152                    #H; nelim (H (refl_eq …))
 153           ##]
 154  ##]
 155 nqed.
 156
 157 nlemma neq_to_neqstrid : ∀sid1,sid2.sid1 ≠ sid2 → eq_strId sid1 sid2 = false.
 158  #sid1; nelim sid1; #s1; #n1;
 159  #sid2; nelim sid2; #s2; #n2;
 160  #H; nchange with (((eqc ? s1 s2) ⊗ (eqc ? n1 n2)) = false);
 161  napply (or2_elim (s1 ≠ s2) (n1 ≠ n2) ? (strid_destruct … H) …);
 162  ##[ ##1: #H1; nrewrite > (neq_to_neqc … H1); nnormalize; napply refl_eq
 163  ##| ##2: #H1; nrewrite > (neq_to_neqc … H1);
 164           nrewrite > (symmetric_andbool (eqc ? s1 s2) false);
 165           nnormalize; napply refl_eq
 166  ##]
 167 nqed.
 168
 169 nlemma strid_is_comparable : comparable.
 170  napply (mk_comparable strId);
 171  ##[ napply (mk_strId (nil ?) O)
 172  ##| napply (λx.false)
 173  ##| napply eq_strId
 174  ##| napply eqstrid_to_eq
 175  ##| napply eq_to_eqstrid
 176  ##| napply neqstrid_to_neq
 177  ##| napply neq_to_neqstrid
 178  ##| napply decidable_strid
 179  ##| napply symmetric_eqstrid
 180  ##]
 181 nqed.
 182
 183 unification hint 0 ≔ ⊢ carr strid_is_comparable ≡ strId.