(no commit message)

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

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
index da7c6158ef983f247bc56986c55aa3ecc33c02fa..971b1060497ad19542f69c3cf6a72afa7b709bd8 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -32,7 +32,7 @@ nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 
  nelim l1;
  ##[ ##1: #l2; ncases l2; nnormalize;
           ##[ ##1: #H; napply refl_eq
-          ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
+          ##| ##2: #h; #t; #H; ndestruct (*nelim (nat_destruct_0_S ? H)*)
           ##]
  ##| ##2: #h; #l2; ncases l2; nnormalize;
           ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
@@ -52,11 +52,11 @@ nlemma symmetric_foldrightlist2_aux
           ##[ ##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)
+                   ndestruct (*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)
+                   ndestruct (*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)));
@@ -106,10 +106,12 @@ nlemma bfoldrightlist2_to_eq
  nelim l1;
  ##[ ##1: #l2; ncases l2;
           ##[ ##1: #H; #H1; napply refl_eq
-          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
+          ##[ ##1: #H1; nnormalize; #H2;
+                   ndestruct (*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));
@@ -127,10 +129,14 @@ nlemma eq_to_bfoldrightlist2
  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: #hh2; #ll2; #H; #H1;
+                   (* !!! ndestruct: assert false *)
+                   nelim (list_destruct_nil_cons ??? H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
+          ##[ ##1: #H1; #H2;
+                   (* !!! ndestruct: assert false *)
+                   nelim (list_destruct_cons_nil ??? H2)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
                    nrewrite > (list_destruct_1 … H2);
                    nrewrite > (H1 hh2 hh2 (refl_eq …));
@@ -147,10 +153,12 @@ nlemma bfoldrightlist2_to_lenlist
  nelim l1;
  ##[ ##1: #l2; ncases l2;
           ##[ ##1: nnormalize; #H; napply refl_eq
-          ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H)
+          ##| ##2: nnormalize; #hh; #tt; #H;
+                   ndestruct (*napply (bool_destruct … H)*)
           ##]
  ##| ##2: #hh; #tt; #H; #l2; ncases l2;
-          ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1)
+          ##[ ##1: nnormalize; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
           ##| ##2: #hh1; #tt1; #H1; nnormalize;
                    nrewrite > (H tt1 ?);
                    ##[ ##1: napply refl_eq
@@ -166,11 +174,15 @@ nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.deci
  ##[ ##1: #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H1; napply (list_destruct_nil_cons T … H1)
+                   nnormalize; #H1;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_nil_cons T … H1)
           ##]
  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H2; napply (list_destruct_cons_nil T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_cons_nil T … H2)
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
@@ -192,11 +204,16 @@ nlemma nbfoldrightlist2_to_neq
  #T; #f; #l1;
  nelim l1;
  ##[ ##1: #l2; ncases l2;
-          ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
-          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
+          ##[ ##1: #H; nnormalize; #H1;
+                   ndestruct (*napply (bool_destruct … H1)*)
+          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #H1; #H2; nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
+          ##[ ##1: #H1; #H2; nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
                    napply (H ll2 H1 ? (list_destruct_2 T … H3));
@@ -219,11 +236,15 @@ nlemma list_destruct
                    nnormalize; #H2; nrewrite > H2 in H1:(%);
                    nnormalize; #H1; napply (H1 (refl_eq …))
           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
-                   nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
           ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
-                   nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
+                   nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (list_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H2;     
                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
@@ -267,7 +288,7 @@ nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_emp
  ncases l;
  nnormalize;
  ##[ ##1: #H; napply I
- ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+ ##| ##2: #x; #l; #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
@@ -275,7 +296,7 @@ nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true 
  #T; #l;
  ncases l;
  nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
  ##| ##2: #x; #l; #H; napply I
  ##]
 nqed.
@@ -310,9 +331,11 @@ nlemma symmetric_foldrightnelist2_aux
           ##| ##2: #h1; #l; ncases l;
                    ##[ ##1: #h3; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S O) = (S (S O)));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             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))));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
                    ##]                   
           ##]
@@ -320,9 +343,11 @@ nlemma symmetric_foldrightnelist2_aux
           ##[ ##1: #h4; ncases l3;
                    ##[ ##1: #h5; #H1; #H2; #H3;
                             nchange in H1:(%) with ((S (S O)) = (S O));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             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));
+                            (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
                             nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
                    ##]
           ##| ##2: #h4; #l4; #H1; #H2; #H3;
@@ -374,10 +399,10 @@ nlemma bfoldrightnelist2_to_eq
  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: #hh2; #ll2; #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
+          ##[ ##1: #hh2; #H1; nnormalize; #H2; ndestruct (*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));
@@ -397,10 +422,14 @@ nlemma eq_to_bfoldrightnelist2
           ##[ ##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: #hh2; #ll2; #H; #H1;
+                   (* !!! ndestruct: assert false *)
+                   nelim (nelist_destruct_nil_cons ???? H1)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
+          ##[ ##1: #hh2; #H1; #H2;
+                   (* !!! ndestruct: assert false *)
+                   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 …));
@@ -417,10 +446,10 @@ nlemma bfoldrightnelist2_to_lennelist
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
           ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
-          ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H)
+          ##| ##2: nnormalize; #hh2; #tt2; #H; ndestruct (*napply (bool_destruct … H)*)
           ##]
  ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
-          ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1)
+          ##[ ##1: nnormalize; #hh2; #H1; ndestruct (*napply (bool_destruct … H1)*)
           ##| ##2: #hh2; #tt2; #H1; nnormalize;
                    nrewrite > (H tt2 ?);
                    ##[ ##1: napply refl_eq
@@ -440,11 +469,15 @@ nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T
                             #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
                    ##]
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H1; napply (nelist_destruct_nil_cons T … H1)
+                   nnormalize; #H1;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_nil_cons T … H1)
           ##]
  ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
           ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize; #H2; napply (nelist_destruct_cons_nil T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_cons_nil T … H2)
           ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
                    ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
                             nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
@@ -467,10 +500,14 @@ nlemma nbfoldrightnelist2_to_neq
  nelim l1;
  ##[ ##1: #hh1; #l2; ncases l2;
           ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
-          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
+          ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
-          ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
+          ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
                    napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
@@ -499,11 +536,15 @@ nlemma nelist_destruct
                             ##]
                    ##]
           ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
-                   nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
+                   nnormalize; #H2;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_nil_cons T … H2)
           ##]
  ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
           ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
-                   nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
+                   nnormalize; #H3;
+                   (* !!! ndestruct: assert false *)
+                   napply (nelist_destruct_cons_nil T … H3)
           ##| ##2: #hh2; #ll2; #H2;     
                    napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
                    ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)