freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
index 557cdfbb11097ad22ef1cdc3b61ea4b45df2b76e..40aaf0b4e839de31e1872e318f71f8a012ac6012 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
@@ -68,7 +68,7 @@ nqed.
 
 nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
  #T; #l1;
- napply (list_ind ???? l1);
+ nelim l1;
  ##[ ##1: #l2; ncases l2; nnormalize;
           ##[ ##1: #H; napply (refl_eq ??)
           ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
@@ -86,7 +86,7 @@ nlemma symmetric_foldrightlist2_aux
   (∀x,y,z.f x y z = f y x z) →
   fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
  #T1; #T2; #f; #acc; #l1;
- napply (list_ind ???? l1);
+ nelim l1;
  ##[ ##1: #l2; ncases l2;
           ##[ ##1: nnormalize; #H1; #H2; #H3; napply (refl_eq ??)
           ##| ##2: #h; #l; #H1; #H2; #H3;
@@ -117,9 +117,72 @@ nlemma symmetric_foldrightlist2
  napply (refl_eq ??).
 nqed.
 
+nlemma symmetric_bfoldrightlist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+  (∀x,y.f x y = f y x) →
+  bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; nnormalize; napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; nnormalize; napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H1; nnormalize;
+                   nrewrite > (H ll2 H1);
+                   nrewrite > (H1 hh1 hh2);
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma bfoldrightlist2_to_eq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+   (∀x,y.(f x y = true → x = y)) →
+   (bfold_right_list2 T1 f l1 l2 = true → l1 = l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; #H1; napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct ??? H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2;
+                   nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
+                   nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2));
+                   nrewrite > (H ll2 H1 (andb_true_true_r ?? H2));
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma eq_to_bfoldrightlist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+   (∀x,y.(x = y → f x y = true)) →
+   (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; #H1; nnormalize; napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
+                   nrewrite > (list_destruct_1 ????? H2);
+                   nrewrite > (H1 hh2 hh2 (refl_eq ??));
+                   nnormalize;
+                   nrewrite > (H ll2 H1 (list_destruct_2 ????? H2));
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
 nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
  #T; #l1;
- napply (ne_list_ind ???? l1);
+ nelim l1;
  ##[ ##1: #h; #l2; ncases l2; nnormalize;
           ##[ ##1: #H; #H1; napply (refl_eq ??)
           ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??)
@@ -137,7 +200,7 @@ nlemma symmetric_foldrightnelist2_aux
   (∀x,y,z.f x y z = f y x z) →
   fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
  #T1; #T2; #f; #acc; #l1;
- napply (ne_list_ind ???? l1);
+ nelim l1;
  ##[ ##1: #h; #l2; ncases l2;
           ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??)
           ##| ##2: #h1; #l; ncases l;
@@ -179,6 +242,71 @@ nlemma symmetric_foldrightnelist2
  napply (refl_eq ??).
 nqed.
 
+nlemma symmetric_bfoldrightnelist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+  (∀x,y.f x y = f y x) →
+  bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; nnormalize; napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H1; nnormalize;
+                   nrewrite > (H ll2 H1);
+                   nrewrite > (H1 hh1 hh2);
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma bfoldrightnelist2_to_eq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+   (∀x,y.(f x y = true → x = y)) →
+   (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct ??? H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2;
+                   nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
+                   nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2));
+                   nrewrite > (H ll2 H1 (andb_true_true_r ?? H2));
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma eq_to_bfoldrightnelist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+   (∀x,y.(x = y → f x y = true)) →
+   (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; #H1; nnormalize;
+                   nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil ??? H1));
+                   napply (refl_eq ??)
+          ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
+          ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
+                   nrewrite > (nelist_destruct_cons_cons_1 ????? H2);
+                   nrewrite > (H1 hh2 hh2 (refl_eq ??));
+                   nnormalize;
+                   nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 ????? H2));
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
  #T; #l;
  ncases l;