freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / string_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma
index 3944d87ad9a5e194e2e4962d718378a771c60d74..d00d67bb9882197ac8645a679e7f4e50786f54b7 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma
@@ -23,104 +23,62 @@
 include "utility/string.ma".
 include "utility/ascii_lemmas2.ma".
 include "freescale/nat_lemmas.ma".
+include "utility/utility_lemmas.ma".
 
 (* ************************ *)
 (* MANIPOLAZIONE DI STRINGA *)
 (* ************************ *)
 
-nlemma symmetric_eqstr : symmetricT aux_str_type bool eq_str.
- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
-          ##[ ##1: nnormalize; napply (refl_eq ??)
-          ##| ##2: #x; #y; nnormalize; napply (refl_eq ??)
-          ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
-          ##[ ##1: nnormalize; napply (refl_eq ??)
-          ##| ##2: #y1; #y2;
-                   nchange with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = ((eq_ascii y1 x1)⊗(eq_str y2 x2)));
-                   nrewrite > (symmetric_eqascii x1 y1);
-                   nrewrite > (H y2);
-                   napply (refl_eq ??)
-          ##]
- ##]
+nlemma symmetric_eqstr : symmetricT (list ascii) bool eq_str.
+ #s1; #s2;
+ napply (symmetric_bfoldrightlist2 ascii eq_ascii s1 s2 symmetric_eqascii).
 nqed.
 
 nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'.
- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
-          ##[ ##1: nnormalize; #H; napply (refl_eq ??)
-          ##| ##2: #x1; #x2; nnormalize; #H; napply (bool_destruct ??? H)
-          ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
-          ##[ ##1: nnormalize; #H1; napply (bool_destruct ??? H1)
-          ##| ##2: #y1; #y2; #H1;
-                   nchange in H1:(%) with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = true);
-                   nrewrite > (eqascii_to_eq x1 y1 (andb_true_true_l ?? H1));
-                   nrewrite > (H y2 (andb_true_true_r ?? H1));
-                   napply (refl_eq ??)
-          ##]
- ##]
+ #s1; #s2;
+ napply (bfoldrightlist2_to_eq ascii eq_ascii s1 s2 eqascii_to_eq).
 nqed.
 
 nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
-          ##[ ##1: nnormalize; #H; napply (refl_eq ??)
-          ##| ##2: #x1; #x2; nnormalize; #H; nelim (list_destruct_nil_cons ascii ?? H)
-          ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
-          ##[ ##1: #H; nelim (list_destruct_cons_nil ascii ?? H)
-          ##| ##2: #y1; #y2; #H1;
-                   nrewrite > (list_destruct_1 ascii ???? H1);
-                   nchange with (((eq_ascii y1 y1)⊗(eq_str x2 y2)) = true);
-                   nrewrite > (H y2 (list_destruct_2 ascii ???? H1));
-                   nrewrite > (eq_to_eqascii y1 y1 (refl_eq ??));
-                   nnormalize;
-                   napply (refl_eq ??)
-          ##]
- ##]
+ #s1; #s2;
+ napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii).
 nqed.
 
 (* ************ *)
 (* STRINGA + ID *)
 (* ************ *)
 
-nlemma strid_destruct_1 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → x1 = x2.
+nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1 = x2.
  #x1; #x2; #y1; #y2; #H;
- nchange with (match STR_ID x2 y2 with [ STR_ID a _ ⇒ x1 = a ]);
+ nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
  napply (refl_eq ??).
 nqed.
 
-nlemma strid_destruct_2 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → y1 = y2.
+nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2.
  #x1; #x2; #y1; #y2; #H;
- nchange with (match STR_ID x2 y2 with [ STR_ID _ b ⇒ y1 = b ]);
+ nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
  napply (refl_eq ??).
 nqed.
 
-nlemma symmetric_eqstrid : symmetricT aux_strId_type bool eq_strId.
+nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
  #si1; #si2;
- ncases si1;
- #l1; #n1;
- ncases si2;
- #l2; #n2;
- nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = ((eq_str l2 l1)⊗(eq_nat n2 n1)));
- nrewrite > (symmetric_eqstr l1 l2);
- nrewrite > (symmetric_eqnat n1 n2);
+ nchange with (
+  ((eq_str (str_elem si1) (str_elem si2))⊗(eq_nat (id_elem si1) (id_elem si2))) =
+  ((eq_str (str_elem si2) (str_elem si1))⊗(eq_nat (id_elem si2) (id_elem si1))));
+ nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
+ nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
  napply (refl_eq ??).
-nqed.
+nqed. 
 
 nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
-  #si1; #si2;
- ncases si1;
+ #si1; #si2;
+ nelim si1;
  #l1; #n1;
- ncases si2;
+ nelim si2;
  #l2; #n2; #H;
  nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
  nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l ?? H));
@@ -129,10 +87,10 @@ nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
 nqed.
 
 nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
-  #si1; #si2;
- ncases si1;
+ #si1; #si2;
+ nelim si1;
  #l1; #n1;
- ncases si2;
+ nelim si2;
  #l2; #n2; #H;
  nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
  nrewrite > (strid_destruct_1 ???? H);