freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
index 7429ab70b3dfa8ddb30c019c7993bad7eb452707..170581a672a50ba1cc72f83e07bc734464094800 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma
@@ -22,6 +22,9 @@
 
 include "common/string.ma".
 include "common/ascii_lemmas2.ma".
+include "common/ascii_lemmas3.ma".
+include "common/ascii_lemmas4.ma".
+include "common/ascii_lemmas5.ma".
 include "common/list_utility_lemmas.ma".
 
 (* ************************ *)
@@ -43,6 +46,25 @@ nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
  napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii).
 nqed.
 
+nlemma decidable_str : ∀x,y:list ascii.decidable (x = y).
+ napply (decidable_list ascii …);
+ napply decidable_ascii. 
+nqed.
+
+nlemma neqstr_to_neq : ∀s,s'.eq_str s s' = false → s ≠ s'.
+ #s1; #s2;
+ napply (nbfoldrightlist2_to_neq ascii eq_ascii s1 s2 …);
+ napply neqascii_to_neq.
+nqed.
+
+nlemma neq_to_neqstr : ∀s,s'.s ≠ s' → eq_str s s' = false.
+ #s1; #s2;
+ napply (neq_to_nbfoldrightlist2 ascii eq_ascii s1 s2 …);
+ ##[ ##1: napply decidable_ascii
+ ##| ##2: napply neq_to_neqascii
+ ##]
+nqed.
+
 (* ************ *)
 (* STRINGA + ID *)
 (* ************ *)
@@ -99,3 +121,66 @@ nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
  nnormalize;
  napply refl_eq.
 nqed.
+
+nlemma decidable_strid_aux1 : ∀s1,n1,s2,n2.s1 ≠ s2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
+ #s1; #n1; #s2; #n2;
+ nnormalize; #H; #H1;
+ napply (H (strid_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_strid_aux2 : ∀s1,n1,s2,n2.n1 ≠ n2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
+ #s1; #n1; #s2; #n2;
+ nnormalize; #H; #H1;
+ napply (H (strid_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_strid : ∀x,y:strId.decidable (x = y).
+ #x; nelim x; #s1; #n1;
+ #y; nelim y; #s2; #n2;
+ nnormalize;
+ napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_strid_aux1 … H))
+ ##| ##1: #H; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
+          ##[ ##2: #H1; napply (or2_intro2 … (decidable_strid_aux2 … H1))
+          ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+                        napply (or2_intro1 … (refl_eq ? (mk_strId s2 n2)))
+          ##]
+ ##]
+nqed.
+
+nlemma neqstrid_to_neq : ∀sid1,sid2:strId.(eq_strId sid1 sid2 = false) → (sid1 ≠ sid2).
+ #sid1; nelim sid1; #s1; #n1;
+ #sid2; nelim sid2; #s2; #n2;
+ nchange with ((((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_str s1 s2) = false) ((eq_nat n1 n2) = false) ? (andb_false … H) …);
+ ##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1))
+ ##]
+nqed.
+
+nlemma strid_destruct : ∀s1,s2,n1,n2.(mk_strId s1 n1) ≠ (mk_strId s2 n2) → s1 ≠ s2 ∨ n1 ≠ n2.
+ #s1; #s2; #n1; #n2;
+ nnormalize; #H;
+ napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
+          ##[ ##2: #H2; napply (or2_intro2 … H2)
+          ##| ##1: #H2; nrewrite > H1 in H:(%);
+                   nrewrite > H2;
+                   #H; nelim (H (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqstrid : ∀sid1,sid2.sid1 ≠ sid2 → eq_strId sid1 sid2 = false.
+ #sid1; nelim sid1; #s1; #n1;
+ #sid2; nelim sid2; #s2; #n2;
+ #H; nchange with (((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false);
+ napply (or2_elim (s1 ≠ s2) (n1 ≠ n2) ? (strid_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqstr … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqnat … H1);
+          nrewrite > (symmetric_andbool (eq_str s1 s2) false);
+          nnormalize; napply refl_eq
+ ##]
+nqed.