From 1d7773584ddd6463b0941026f114b0173e3b6b72 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 22 Dec 2010 17:37:18 +0000 Subject: [PATCH] more theory for lists --- .../matita/nlibrary/datatypes/list.ma | 265 ++++++++++-------- 1 file changed, 152 insertions(+), 113 deletions(-) diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma index 2909baf84..87f917185 100644 --- a/helm/software/matita/nlibrary/datatypes/list.ma +++ b/helm/software/matita/nlibrary/datatypes/list.ma @@ -13,6 +13,8 @@ (**************************************************************************) include "logic/pts.ma". +include "logic/equality.ma". +include "arithmetics/nat.ma". ninductive list (A:Type[0]) : Type[0] ≝ | nil: list A @@ -56,7 +58,8 @@ match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l. #A;#l;nelim l;//; -#a;#l1;#IH;nnormalize;//; +#a;#l1;#IH;nnormalize; +nrewrite > IH;//; nqed. ntheorem associative_append: ∀A:Type[0].associative (list A) (append A). @@ -187,18 +190,20 @@ interpretation "list member" 'mem x l = (in_list ? x l). interpretation "list not member" 'notmem x l = (Not (in_list ? x l)). interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2). -naxiom not_in_list_nil : \forall A,x.\lnot in_list A x []. -(*intros.unfold.intro.inversion H - [intros;lapply (sym_eq ? ? ? H2);destruct Hletin - |intros;destruct H4] -qed.*) +nlemma not_in_list_nil : \forall A,x.\lnot in_list A x []. +#A x;@;#H1;ninversion H1; +##[#a0 al0 H2 H3;ndestruct (H3); +##|#a0 a1 al0 H2 H3 H4 H5;ndestruct (H5) +##] +nqed. -naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to +nlemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to x = a \lor in_list A x l. -(*intros;inversion H;intros - [destruct H2;left;reflexivity - |destruct H4;right;assumption] -qed.*) +#A a0 a1 al0 H1;ninversion H1 +##[#a2 al1 H2 H3;ndestruct (H3);@;@ +##|#a2 a3 al1 H2 H3 H4 H5;ndestruct (H5);@2;// +##] +nqed. nlemma in_list_tail : \forall A,l,x,y. in_list A x (y::l) \to x \neq y \to in_list A x l. @@ -210,45 +215,43 @@ ninversion H; ##] nqed. -naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. -(*intros;elim (in_list_cons_case ? ? ? ? H) - [assumption - |elim (not_in_list_nil ? ? H1)] -qed.*) +nlemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. +#A a0 a1 H1;ncases (in_list_cons_case ???? H1) +##[// +##|#H2;napply False_ind;ncases (not_in_list_nil ? a0);#H3;/2/ +##] +nqed. -naxiom in_list_to_in_list_append_l: \forall A.\forall x:A. +nlemma in_list_to_in_list_append_l: \forall A.\forall x:A. \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2). -(*intros. -elim H;simplify - [apply in_list_head - |apply in_list_cons;assumption - ] -qed.*) - -naxiom in_list_to_in_list_append_r: \forall A.\forall x:A. +#A a0 al0 al1 H1;nelim H1 +##[#a1 al2;@; +##|#a1 a2 al2 H2 H3;@2;// +##] +nqed. + +nlemma in_list_to_in_list_append_r: \forall A.\forall x:A. \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2). -(*intros 3. -elim l1;simplify - [assumption - |apply in_list_cons;apply H;assumption - ] -qed.*) - -naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A. +#A a0 al0 al1 H1;nelim al0 +##[napply H1 +##|#a1 al2 IH;@2;napply IH +##] +nqed. + +nlemma in_list_append_to_or_in_list: \forall A:Type.\forall x:A. \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1. -(*intros 3. -elim l - [right.apply H - |simplify in H1.inversion H1;intros; destruct; - [left.apply in_list_head - | elim (H l2) - [left.apply in_list_cons. assumption - |right.assumption - |assumption - ] - ] - ] -qed.*) +#A a0 al0;nelim al0 +##[#al1 H1;@2;napply H1 +##|#a1 al1 IH al2 H1;nnormalize in H1; + ncases (in_list_cons_case ???? H1);#H2 + ##[@;nrewrite > H2;@ + ##|ncases (IH … H2);#H3 + ##[@;@2;// + ##|@2;// + ##] + ##] +##] +nqed. nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ match l with @@ -260,78 +263,92 @@ nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ ] ]. -naxiom mem_true_to_in_list : +nlemma mem_true_to_in_list : \forall A,equ. (\forall x,y.equ x y = true \to x = y) \to \forall x,l.mem A equ x l = true \to in_list A x l. -(* intros 5.elim l - [simplify in H1;destruct H1 - |simplify in H2;apply (bool_elim ? (equ x a)) - [intro;rewrite > (H ? ? H3);apply in_list_head - |intro;rewrite > H3 in H2;simplify in H2; - apply in_list_cons;apply H1;assumption]] -qed.*) - -naxiom in_list_to_mem_true : +#A equ H1 a0 al0;nelim al0 +##[nnormalize;#H2;ndestruct (H2) +##|#a1 al1 IH H2;nwhd in H2:(??%?); + nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3 + ##[nrewrite > (H1 … H3);@ + ##|@2;napply IH;nrewrite > H3 in H2;nnormalize;//; + ##] +##] +nqed. + +nlemma in_list_to_mem_true : \forall A,equ. (\forall x.equ x x = true) \to \forall x,l.in_list A x l \to mem A equ x l = true. -(*intros 5.elim l - [elim (not_in_list_nil ? ? H1) - |elim H2 - [simplify;rewrite > H;reflexivity - |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]]. -qed.*) - -naxiom in_list_filter_to_p_true : \forall A,l,x,p. +#A equ H1 a0 al0;nelim al0 +##[#H2;napply False_ind;ncases (not_in_list_nil ? a0);/2/ +##|#a1 al1 IH H2;nelim H2 + ##[nnormalize;#a2 al2;nrewrite > (H1 …);@ + ##|#a2 a3 al2 H3 H4;nnormalize;ncases (equ a2 a3);nnormalize;//; + ##] +##] +nqed. + +nlemma in_list_filter_to_p_true : \forall A,l,x,p. in_list A x (filter A l p) \to p x = true. -(* intros 4;elim l - [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; - simplify in H1 - [elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H3;assumption - |apply (H H3)] - |apply (H H1)]] -qed.*) - -naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l. -(*intros 4;elim l - [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; - simplify in H1 - [elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H3;apply in_list_head - |apply in_list_cons;apply H;assumption] - |apply in_list_cons;apply H;assumption]] -qed.*) - -naxiom in_list_filter_r : \forall A,l,p,x. +#A al0 a0 p;nelim al0 +##[nnormalize;#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/ +##|#a1 al1 IH H1;nnormalize in H1;nlapply (refl ? (p a1)); + ngeneralize in match H1;ncases (p a1) in ⊢ (???% -> ???% → %); + ##[#H2 H3;ncases (in_list_cons_case ???? H2);#H4 + ##[nrewrite > H4;// + ##|napply (IH H4); + ##] + ##|#H2 H3;napply (IH H2); + ##] +##] +nqed. + +nlemma in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l. +#A al0 p a0;nelim al0 +##[nnormalize;//; +##|#a1 al1 IH H1;nnormalize in H1; + nlapply (refl ? (p a1));ncases (p a1) in ⊢ (???% → %);#H2 + ##[nrewrite > H2 in H1;#H1;ncases (in_list_cons_case ???? H1);#H3 + ##[nrewrite > H3;@ + ##|@2;napply IH;napply H3 + ##] + ##|@2;napply IH;nrewrite > H2 in H1;#H1;napply H1; + ##] +##] +nqed. + +nlemma in_list_filter_r : \forall A,l,p,x. in_list A x l \to p x = true \to in_list A x (filter A l p). -(* intros 4;elim l - [elim (not_in_list_nil ? ? H) - |elim (in_list_cons_case ? ? ? ? H1) - [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head - |simplify;apply (bool_elim ? (p a));intro;simplify; - [apply in_list_cons;apply H;assumption - |apply H;assumption]]] -qed.*) - -naxiom incl_A_A: ∀T,A.incl T A A. -(*intros.unfold incl.intros.assumption. -qed.*) - -naxiom incl_append_l : ∀T,A,B.incl T A (A @ B). -(*unfold incl; intros;autobatch. -qed.*) - -naxiom incl_append_r : ∀T,A,B.incl T B (A @ B). -(*unfold incl; intros;autobatch. -qed.*) - -naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). -(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. -qed.*) +#A al0 p a0;nelim al0 +##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/ +##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3 + ##[nnormalize;nrewrite < H3;nrewrite > H2;@ + ##|nnormalize;ncases (p a1);nnormalize; + ##[@2;napply IH;// + ##|napply IH;// + ##] + ##] +##] +nqed. + +nlemma incl_A_A: ∀T,A.incl T A A. +#A al0 a0 H1;//; +nqed. + +nlemma incl_append_l : ∀T,A,B.incl T A (A @ B). +#A al0 al1 a0 H1;/2/; +nqed. + +nlemma incl_append_r : ∀T,A,B.incl T B (A @ B). +#A al0 al1 a0 H1;/2/; +nqed. + +nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). +#A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/; +#H3;@2;napply H1;//; +nqed. nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝ match l with @@ -443,15 +460,37 @@ nlemma map_compose : ##] nqed. -naxiom incl_incl_to_incl_append : +nlemma incl_incl_to_incl_append : ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'. +#A al0 al1 al2 al3 H1 H2 a0 H3; +ncases (in_list_append_to_or_in_list ???? H3);#H4; +##[napply in_list_to_in_list_append_l;napply H1;// +##|napply in_list_to_in_list_append_r;napply H2;// +##] +nqed. -naxiom eq_map_append : ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2. +nlemma eq_map_append : + ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2. +#A B f al1 al2;nelim al1 +##[@ +##|#a0 al3 IH;nnormalize;nrewrite > IH;@; +##] +nqed. -naxiom not_in_list_to_mem_false : +nlemma not_in_list_to_mem_false : ∀A,equ. (∀x,y.equ x y = true → x = y) → ∀x:A.∀l. x ∉ l → mem A equ x l = false. +#A equ H1 a0 al0;nelim al0 +##[#_;@ +##|#a1 al1 IH H2;nwhd in ⊢ (??%?); + nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3; + ##[napply False_ind;ncases H2;#H4;napply H4; + nrewrite > (H1 … H3);@ + ##|napply IH;@;#H4;ncases H2;#H5;napply H5;@2;// + ##] +##] +nqed. nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝ match l with -- 2.39.2