1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "utility/string.ma".
24 include "utility/ascii_lemmas2.ma".
25 include "freescale/nat_lemmas.ma".
27 (* ************************ *)
28 (* MANIPOLAZIONE DI STRINGA *)
29 (* ************************ *)
31 nlemma symmetric_eqstr : symmetricT aux_str_type bool eq_str.
33 napply (list_ind ascii ??? l1);
34 ##[ ##1: #l2; ncases l2;
35 ##[ ##1: nnormalize; napply (refl_eq ??)
36 ##| ##2: #x; #y; nnormalize; napply (refl_eq ??)
38 ##| ##2: #x1; #x2; #H; #l2; ncases l2;
39 ##[ ##1: nnormalize; napply (refl_eq ??)
41 nchange with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = ((eq_ascii y1 x1)⊗(eq_str y2 x2)));
42 nrewrite > (symmetric_eqascii x1 y1);
49 nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'.
51 napply (list_ind ascii ??? l1);
52 ##[ ##1: #l2; ncases l2;
53 ##[ ##1: nnormalize; #H; napply (refl_eq ??)
54 ##| ##2: #x1; #x2; nnormalize; #H; napply (bool_destruct ??? H)
56 ##| ##2: #x1; #x2; #H; #l2; ncases l2;
57 ##[ ##1: nnormalize; #H1; napply (bool_destruct ??? H1)
58 ##| ##2: #y1; #y2; #H1;
59 nchange in H1:(%) with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = true);
60 nrewrite > (eqascii_to_eq x1 y1 (andb_true_true_l ?? H1));
61 nrewrite > (H y2 (andb_true_true_r ?? H1));
67 nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
69 napply (list_ind ascii ??? l1);
70 ##[ ##1: #l2; ncases l2;
71 ##[ ##1: nnormalize; #H; napply (refl_eq ??)
72 ##| ##2: #x1; #x2; nnormalize; #H; nelim (list_destruct_nil_cons ascii ?? H)
74 ##| ##2: #x1; #x2; #H; #l2; ncases l2;
75 ##[ ##1: #H; nelim (list_destruct_cons_nil ascii ?? H)
76 ##| ##2: #y1; #y2; #H1;
77 nrewrite > (list_destruct_1 ascii ???? H1);
78 nchange with (((eq_ascii y1 y1)⊗(eq_str x2 y2)) = true);
79 nrewrite > (H y2 (list_destruct_2 ascii ???? H1));
80 nrewrite > (eq_to_eqascii y1 y1 (refl_eq ??));
91 nlemma strid_destruct_1 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → x1 = x2.
92 #x1; #x2; #y1; #y2; #H;
93 nchange with (match STR_ID x2 y2 with [ STR_ID a _ ⇒ x1 = a ]);
99 nlemma strid_destruct_2 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → y1 = y2.
100 #x1; #x2; #y1; #y2; #H;
101 nchange with (match STR_ID x2 y2 with [ STR_ID _ b ⇒ y1 = b ]);
107 nlemma symmetric_eqstrid : symmetricT aux_strId_type bool eq_strId.
113 nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = ((eq_str l2 l1)⊗(eq_nat n2 n1)));
114 nrewrite > (symmetric_eqstr l1 l2);
115 nrewrite > (symmetric_eqnat n1 n2);
119 nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
125 nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
126 nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l ?? H));
127 nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r ?? H));
131 nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
137 nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
138 nrewrite > (strid_destruct_1 ???? H);
139 nrewrite > (strid_destruct_2 ???? H);
140 nrewrite > (eq_to_eqstr l2 l2 (refl_eq ??));
141 nrewrite > (eq_to_eqnat n2 n2 (refl_eq ??));