--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/list_utility.ma".
+include "common/list_lemmas.ma".
+
+(* *************** *)
+(* LISTE GENERICHE *)
+(* *************** *)
+
+nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
+ #T; #l1;
+ nelim 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;
+ nelim 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_lenlist T1 l1 l2 H).
+ #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
+ nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_lenlist T1 l1 l2 H) H1);
+ 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.
+
+(* ************** *)
+(* NON-EMPTY LIST *)
+(* ************** *)
+
+nlemma symmetric_lennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
+ #T; #l1;
+ nelim 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;
+ 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;
+ ##[ ##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_lennelist T1 l1 l2 H).
+ #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
+ nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_lennelist T1 l1 l2 H) H1);
+ 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;
+ 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.
projects / helm.git / blobdiff