X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Futility%2Futility_lemmas.ma;h=557cdfbb11097ad22ef1cdc3b61ea4b45df2b76e;hb=c39f5efd7ee59d07dd62ddef25d7cd09a1a3a704;hp=6ed8dea6c82004a4bc5faf9b3c258b9f41cafb72;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git

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 6ed8dea6c..557cdfbb1 100755
--- a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma
@@ -58,7 +58,7 @@ nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y
  napply I.
 nqed.
 
-nlemma list_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
+nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
  #T; #x1; #x2; #y2; #H;
  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
  nrewrite < H;
@@ -66,6 +66,119 @@ nlemma list_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne
  napply I.
 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);
+ ##[ ##1: #l2; ncases l2; nnormalize;
+          ##[ ##1: #H; napply (refl_eq ??)
+          ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
+          ##]
+ ##| ##2: #h; #l2; ncases l2; nnormalize;
+          ##[ ##1: #H; #l; #H1; nrewrite < H1; napply (refl_eq ??)
+          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightlist2_aux
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.
+   ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1.
+  (∀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);
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: nnormalize; #H1; #H2; #H3; napply (refl_eq ??)
+          ##| ##2: #h; #l; #H1; #H2; #H3;
+                   nchange in H1:(%) with (O = (S (len_list ? l)));
+                   nelim (nat_destruct_0_S ? H1)
+          ##]
+ ##| ##2: #h3; #l3; #H; #l2; ncases l2;
+          ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O);
+                   nelim (nat_destruct_S_0 ? H1)
+          ##| ##2: #h4; #l4; #H1; #H2; #H3;
+                   nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
+                   nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
+                   nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
+                                 (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
+                   nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3);
+                   nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightlist2
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
+  (∀x,y,z.f x y z = f y x z) →
+  fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_eqlenlist T1 l1 l2 H).
+ #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
+ nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlenlist T1 l1 l2 H) H1);
+ 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);
+ ##[ ##1: #h; #l2; ncases l2; nnormalize;
+          ##[ ##1: #H; #H1; napply (refl_eq ??)
+          ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??)
+          ##]
+ ##| ##2: #h; #l2; ncases l2; nnormalize;
+          ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply (refl_eq ??)
+          ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightnelist2_aux
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
+   ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
+  (∀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);
+ ##[ ##1: #h; #l2; ncases l2;
+          ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??)
+          ##| ##2: #h1; #l; ncases l;
+                   ##[ ##1: #h3; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S O) = (S (S O)));
+                            nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
+                   ##| ##2: #h3; #l3; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
+                            nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
+                   ##]                   
+          ##]
+ ##| ##2: #h3; #l3; #H; #l2; ncases l2;
+          ##[ ##1: #h4; ncases l3;
+                   ##[ ##1: #h5; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S (S O)) = (S O));
+                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
+                   ##| ##2: #h5; #l5; #H1; #H2; #H3;
+                            nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
+                            nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
+                   ##]
+          ##| ##2: #h4; #l4; #H1; #H2; #H3;
+                   nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
+                   nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
+                   nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
+                                 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
+                   nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
+                   nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.
+
+nlemma symmetric_foldrightnelist2
+ : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
+  (∀x,y,z.f x y z = f y x z) →
+  fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_eqlennelist T1 l1 l2 H).
+ #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
+ nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1);
+ 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;