]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/common/string_lemmas.ma
update in delayed_updating
[helm.git] / matita / 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.