X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Flist_utility_lemmas.ma;h=da7c6158ef983f247bc56986c55aa3ecc33c02fa;hb=bf0cc84dcef9ae3d2145e79754bb39feb3985574;hp=9cc7f317d8b1589d589de2843e5c98b993479c69;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

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 9cc7f317d..da7c6158e 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
@@ -141,6 +141,145 @@ nlemma eq_to_bfoldrightlist2
  ##]
 nqed.
 
+nlemma bfoldrightlist2_to_lenlist
+ : ∀T.∀f:T → T → bool.∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: nnormalize; #H; napply refl_eq
+          ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H)
+          ##]
+ ##| ##2: #hh; #tt; #H; #l2; ncases l2;
+          ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1)
+          ##| ##2: #hh1; #tt1; #H1; nnormalize;
+                   nrewrite > (H tt1 ?);
+                   ##[ ##1: napply refl_eq
+                   ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
+                            napply (andb_true_true_r … H1)
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.decidable (x = y).
+ #T; #H; #x; nelim x;
+ ##[ ##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)
+          ##]
+ ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
+          ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                   nnormalize; #H2; 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))
+                   ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
+                            ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                                     nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
+                            ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+                                     nrewrite > H2; nrewrite > H3; napply refl_eq
+                            ##]
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma nbfoldrightlist2_to_neq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+   (∀x,y.(f x y = false → x ≠ y)) →
+   (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2).
+ #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)
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; #H2; nnormalize; #H3; 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));
+                   napply (or2_elim ??? (andb_false2 … H2) );
+                   ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
+                            ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
+                            ##| ##2: napply (H1 … H4)
+                            ##]
+                   ##| ##2: #H4; napply H4
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma list_destruct
+ : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:list T.(h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2.
+ #T; #H; #h1; #h2; #l1; nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
+                   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)
+          ##]
+ ##| ##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)
+          ##| ##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)
+                   ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
+                            nrewrite > H3 in H2:(%); #H2;
+                            nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
+                            nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
+                            napply (H2 (refl_eq …))
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_nbfoldrightlist2
+ : ∀T:Type.∀f:T → T → bool.∀l1,l2:list T.
+   (∀x,y:T.decidable (x = y)) →
+   (∀x,y.(x ≠ y → f x y = false)) →
+   (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+          ##[ ##1: #H; #H1; nnormalize; #H2; nelim (H2 (refl_eq …))
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #H1; #H2; nnormalize; #H3; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
+                   nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
+                   napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H1 … H3) …);
+                   ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
+                   ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
+                            nrewrite > (symmetric_andbool (f hh1 hh2) false);
+                            nnormalize; 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;
+ nnormalize;
+ ##[ ##1: #H; napply I
+ ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ #T; #l;
+ ncases l;
+ nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2: #x; #l; #H; napply I
+ ##]
+nqed.
+
 (* ************** *)
 (* NON-EMPTY LIST *)
 (* ************** *)
@@ -272,20 +411,134 @@ nlemma eq_to_bfoldrightnelist2
  ##]
 nqed.
 
-nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
- #T; #l;
- ncases l;
- nnormalize;
- ##[ ##1: #H; napply I
- ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+nlemma bfoldrightnelist2_to_lennelist
+ : ∀T.∀f:T → T → bool.∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
+          ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H)
+          ##]
+ ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
+          ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1)
+          ##| ##2: #hh2; #tt2; #H1; nnormalize;
+                   nrewrite > (H tt2 ?);
+                   ##[ ##1: napply refl_eq
+                   ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
+                            napply (andb_true_true_r … H1)
+                   ##]
+          ##]
  ##]
 nqed.
 
-nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
- #T; #l;
- ncases l;
- nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
- ##| ##2: #x; #l; #H; napply I
+nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T.decidable (x = y).
+ #T; #H; #x; nelim x;
+ ##[ ##1: #hh1; #y; ncases y;
+          ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
+                   ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+                   ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
+                            #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)
+          ##]
+ ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
+          ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                   nnormalize; #H2; 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))
+                   ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
+                            ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+                                     nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
+                            ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+                                     nrewrite > H2; nrewrite > H3; napply refl_eq
+                            ##]
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma nbfoldrightnelist2_to_neq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+   (∀x,y.(f x y = false → x ≠ y)) →
+   (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2).
+ #T; #f; #l1;
+ 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: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; 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));
+                   napply (or2_elim ??? (andb_false2 … H2) );
+                   ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
+                            ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
+                            ##| ##2: napply (H1 … H4)
+                            ##]
+                   ##| ##2: #H4; napply H4
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma nelist_destruct
+ : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:ne_list T.(h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2.
+ #T; #H; #h1; #h2; #l1; nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
+                   ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
+                   ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
+                            napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
+                            ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
+                                     nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
+                            ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
+                            ##]
+                   ##]
+          ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
+                   nnormalize; #H2; 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)
+          ##| ##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)
+                   ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
+                            nrewrite > H3 in H2:(%); #H2;
+                            nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
+                            nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
+                            napply (H2 (refl_eq …))
+                   ##]
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_nbfoldrightnelist2
+ : ∀T:Type.∀f:T → T → bool.∀l1,l2:ne_list T.
+   (∀x,y:T.decidable (x = y)) →
+   (∀x,y.(x ≠ y → f x y = false)) →
+   (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+          ##[ ##1: #hh2; #H; #H1; nnormalize; #H2; napply (H1 hh1 hh2 ?);
+                   nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
+          ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
+          ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+          ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply refl_eq
+          ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
+                   nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
+                   napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H1 … H3) …);
+                   ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
+                   ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
+                            nrewrite > (symmetric_andbool (f hh1 hh2) false);
+                            nnormalize; napply refl_eq
+                   ##]
+          ##]
  ##]
 nqed.