From: Wilmer Ricciotti Date: Wed, 26 Mar 2008 17:59:11 +0000 (+0000) Subject: Reorganization of list library (step 1) X-Git-Tag: make_still_working~5493 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bfb7fbf61e86114e49cb3671503e8307a4582342;p=helm.git Reorganization of list library (step 1) --- diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma index 2a5367834..3bd8d2bdc 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma @@ -165,21 +165,21 @@ lemma boundinenv_natinfv : \forall x,G. (\exists B,T.(in_list ? (mk_bound B x T) G)) \to (in_list ? x (fv_env G)). intros 2;elim G - [elim H;elim H1;lapply (in_list_nil ? ? H2);elim Hletin - |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3) - [rewrite < H4;simplify;apply in_Base - |simplify;apply in_Skip;apply H;apply (ex_intro ? ? a); + [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin + |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3) + [rewrite < H4;simplify;apply in_list_head + |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a); apply (ex_intro ? ? a1);assumption]] qed. lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to \exists B,T.(in_list ? (mk_bound B x T) G). intros 2;elim G 0 - [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin - |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1) - [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base + [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin + |intros 3;elim t;simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_list_head |elim (H H2);elim H3;apply (ex_intro ? ? a); - apply (ex_intro ? ? a1);apply in_Skip;assumption]] + apply (ex_intro ? ? a1);apply in_list_cons;assumption]] qed. lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to @@ -194,8 +194,8 @@ qed. lemma incl_cons : \forall x,l1,l2. (incl ? l1 l2) \to (incl nat (x :: l1) (x :: l2)). -intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1) - [rewrite > H2;apply in_Base|apply in_Skip;apply (H ? H2)] +intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H2;apply in_list_head|apply in_list_cons;apply (H ? H2)] qed. lemma WFT_env_incl : \forall G,T.(WFType G T) \to @@ -223,22 +223,22 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. (y \neq x) \to (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))). intros 10;elim H - [simplify in H1;elim (in_cons_case ? ? ? ? H1) + [simplify in H1;elim (in_list_cons_case ? ? ? ? H1) [destruct H3;elim (H2);reflexivity - |simplify;apply (in_Skip ? ? ? ? H3);] - |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2) - [rewrite > H4;apply in_Base - |apply (in_Skip ? ? ? ? (H1 H4 H3))]] + |simplify;apply (in_list_cons ? ? ? ? H3);] + |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2) + [rewrite > H4;apply in_list_head + |apply (in_list_cons ? ? ? ? (H1 H4 H3))]] qed. lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to (in_list ? x (fv_type (subst_type_nat T U n))). intros 3;elim T - [simplify in H;elim (in_list_nil ? ? H) + [simplify in H;elim (not_in_list_nil ? ? H) |2,3:simplify;simplify in H;assumption - |*:simplify in H2;simplify;elim (append_to_or_in_list ? ? ? ? H2) - [1,3:apply in_list_append1;apply (H ? H3) - |*:apply in_list_append2;apply (H1 ? H3)]] + |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2) + [1,3:apply in_list_to_in_list_append_l;apply (H ? H3) + |*:apply in_list_to_in_list_append_r;apply (H1 ? H3)]] qed. (*** lemma on fresh names ***) @@ -250,11 +250,11 @@ cut (\forall l:(list nat).\exists n.\forall m. [apply a |apply H;constructor 1] |intros;elim l - [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1) + [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1) |elim H; apply (ex_intro ? ? (S (max a t))). intros.unfold. intro. - elim (in_cons_case ? ? ? ? H3) + elim (in_list_cons_case ? ? ? ? H3) [rewrite > H4 in H2.autobatch |elim H4 [apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch @@ -266,24 +266,24 @@ qed. lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to (in_list ? x (fv_env G)). intros 4.elim H - [simplify in H2;elim (in_cons_case ? ? ? ? H2) - [rewrite > H3;assumption|elim (in_list_nil ? ? H3)] - |simplify in H1;elim (in_list_nil ? x H1) - |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5);autobatch - |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5) + [simplify in H2;elim (in_list_cons_case ? ? ? ? H2) + [rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)] + |simplify in H1;elim (not_in_list_nil ? x H1) + |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch + |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5) [apply (H2 H6) |elim (fresh_name ((fv_type t1) @ (fv_env l))); cut (¬ (a ∈ (fv_type t1)) ∧ ¬ (a ∈ (fv_env l))) [elim Hcut;lapply (H4 ? H9 H8) [cut (x ≠ a) - [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin) + [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin) [elim (Hcut1 H10) |assumption] |intro;apply H8;applyS H6] |apply in_FV_subst;assumption] |split - [intro;apply H7;apply in_list_append1;assumption - |intro;apply H7;apply in_list_append2;assumption]]]] + [intro;apply H7;apply in_list_to_in_list_append_l;assumption + |intro;apply H7;apply in_list_to_in_list_append_r;assumption]]]] qed. (*** lemmata relating subtyping and well-formedness ***) @@ -339,13 +339,13 @@ lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to (in_list ? (mk_bound B x T) G) \to (in_list ? (mk_bound B x U) G) \to T = U. intros 6;elim H - [lapply (in_list_nil ? ? H1);elim Hletin - |elim (in_cons_case ? ? ? ? H6) - [destruct H7;destruct;elim (in_cons_case ? ? ? ? H5) + [lapply (not_in_list_nil ? ? H1);elim Hletin + |elim (in_list_cons_case ? ? ? ? H6) + [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5) [destruct H7;reflexivity |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); apply (ex_intro ? ? T);assumption] - |elim (in_cons_case ? ? ? ? H5) + |elim (in_list_cons_case ? ? ? ? H5) [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); apply (ex_intro ? ? U);assumption |apply (H2 H8 H7)]]] diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma index 8558725cc..fc3621618 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma @@ -43,8 +43,8 @@ intros 4;elim H [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) |apply (WFE_cons ? ? ? ? H6 H8);autobatch |unfold;intros;inversion H9;intros - [destruct H11;apply in_Base - |destruct H13;apply in_Skip;apply (H7 ? H10)]]] + [destruct H11;apply in_list_head + |destruct H13;apply in_list_cons;apply (H7 ? H10)]]] qed. theorem narrowing:∀X,G,G1,U,P,M,N. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma index f96e07679..decaf1b74 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma @@ -43,8 +43,8 @@ intros 4;elim H [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) |apply (WFE_cons ? ? ? ? H6 H8);autobatch |unfold;intros;inversion H9;intros - [destruct H11;apply in_Base - |destruct H13;apply in_Skip;apply (H7 ? H10)]]] + [destruct H11;apply in_list_head + |destruct H13;apply in_list_cons;apply (H7 ? H10)]]] qed. theorem narrowing:∀X,G,G1,U,P,M,N. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma index 4f5e15422..bd7018d3c 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma @@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/Fsub/util". include "logic/equality.ma". include "nat/compare.ma". include "list/list.ma". +include "list/in.ma". (*** useful definitions and lemmas not really related to Fsub ***) @@ -43,92 +44,15 @@ apply (leb_elim m n) ] qed. -inductive in_list (A:Type): A → (list A) → Prop ≝ -| in_Base : ∀ x,l.(in_list A x (x::l)) -| in_Skip : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). - notation > "hvbox(x ∈ l)" non associative with precedence 30 for @{ 'inlist $x $l }. notation < "hvbox(x \nbsp ∈ \nbsp l)" non associative with precedence 30 for @{ 'inlist $x $l }. interpretation "item in list" 'inlist x l = - (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l). - -definition incl : \forall A.(list A) \to (list A) \to Prop \def - \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m). - -(* FIXME: use the map in library/list (when there will be one) *) -definition map : \forall A,B,f.((list A) \to (list B)) \def - \lambda A,B,f.let rec map (l : (list A)) : (list B) \def - match l in list return \lambda l0:(list A).(list B) with - [nil \Rightarrow (nil B) - |(cons (a:A) (t:(list A))) \Rightarrow - (cons B (f a) (map t))] in map. - -lemma 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. - -lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t). -intros;inversion H;intros - [destruct H2;left;symmetry;reflexivity - |destruct H4;right;applyS H1] -qed. - -lemma append_nil:\forall A:Type.\forall l:list A. l@[]=l. -intros. -elim l;intros;autobatch. -qed. - -lemma append_cons:\forall A.\forall a:A.\forall l,l1. -l@(a::l1)=(l@[a])@l1. -intros. -rewrite > associative_append. -reflexivity. -qed. - -lemma in_list_append1: \forall A.\forall x:A. -\forall l1,l2. x \in l1 \to x \in l1@l2. -intros. -elim H - [simplify.apply in_Base - |simplify.apply in_Skip.assumption - ] -qed. - -lemma in_list_append2: \forall A.\forall x:A. -\forall l1,l2. x \in l2 \to x \in l1@l2. -intros 3. -elim l1 - [simplify.assumption - |simplify.apply in_Skip.apply H.assumption - ] -qed. - -theorem append_to_or_in_list: \forall A:Type.\forall x:A. -\forall l,l1. x \in l@l1 \to (x \in l) \lor (x \in l1). -intros 3. -elim l - [right.apply H - |simplify in H1.inversion H1;intros; destruct; - [left.apply in_Base - | elim (H l2) - [left.apply in_Skip. assumption - |right.assumption - |assumption - ] - ] - ] -qed. + (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l). lemma max_case : \forall m,n.(max m n) = match (leb m n) with [ true \Rightarrow n | false \Rightarrow m ]. intros;elim m;simplify;reflexivity; -qed. - -lemma incl_A_A: ∀T,A.incl T A A. -intros.unfold incl.intros.assumption. qed. \ No newline at end of file diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index 077c40477..1c79ebc48 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/matita/library/decidable_kit/list_aux.ma @@ -18,12 +18,7 @@ include "list/list.ma". include "decidable_kit/eqtype.ma". include "nat/plus.ma". -(* ### some functions on lists (some can be moved to list.ma ### *) - -let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := - match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)]. - -definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l. +(* ### some functions on lists ### *) definition count : ∀T : eqType.∀f : T → bool.∀l : list T. nat := λT:eqType.λf,l. @@ -34,31 +29,6 @@ let rec mem (d : eqType) (x : d) (l : list d) on l : bool ≝ [ nil ⇒ false | cons y tl ⇒ orb (cmp d x y) (mem d x tl)]. -definition iota : nat → nat → list nat ≝ - λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. - -let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝ - match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. - -(* ### induction principle for functions visiting 2 lists in parallel *) -lemma list_ind2 : - ∀T1,T2:Type.∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop. - length ? l1 = length ? l2 → - (P (nil ?) (nil ?)) → - (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → - P l1 l2. -intros (T1 T2 l1 l2 P Hl Pnil Pcons); -generalize in match Hl; clear Hl; generalize in match l2; clear l2; -elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]] -intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] -intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption; -qed. - -lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. -intros (A B f g l Efg); elim l; simplify; [1: reflexivity ]; -rewrite > (Efg t); rewrite > H; reflexivity; -qed. - (* ### eqtype for lists ### *) let rec lcmp (d : eqType) (l1,l2 : list d) on l1 : bool ≝ match l1 with @@ -101,5 +71,4 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ] apply H'; reflexivity;]]]] qed. -definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d). - \ No newline at end of file +definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d). \ No newline at end of file diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma new file mode 100644 index 000000000..cd372394b --- /dev/null +++ b/helm/software/matita/library/list/in.ma @@ -0,0 +1,156 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "datatypes/bool.ma". +include "datatypes/constructors.ma". +include "list/list.ma". + +inductive in_list (A:Type): A → (list A) → Prop ≝ +| in_list_head : ∀ x,l.(in_list A x (x::l)) +| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). + +definition incl : \forall A.(list A) \to (list A) \to Prop \def + \lambda A,l,m.\forall x.in_list A x l \to in_list A x m. + +lemma 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. + +lemma 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. + +lemma in_list_tail : \forall l,x,y. + in_list nat x (y::l) \to x \neq y \to in_list nat x l. +intros 4;elim (in_list_cons_case ? ? ? ? H) + [elim (H2 H1) + |assumption] +qed. + +lemma 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. + +lemma 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. + +lemma 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. + +theorem 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. + +let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ + match l with + [ nil ⇒ false + | (cons a l') ⇒ + match eq x a with + [ true ⇒ true + | false ⇒ mem A eq x l' + ] + ]. + +lemma 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 t)) + [intro;rewrite > (H ? ? H3);apply in_list_head + |intro;rewrite > H3 in H2;simplify in H2; + apply in_list_cons;apply H1;assumption]] +qed. + +lemma 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 a a1));intro;rewrite > H5; + reflexivity]]. +qed. + +lemma in_list_filter_to_p_true : \forall l,x,p. +in_list nat x (filter nat l p) \to p x = true. +intros 3;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;assumption + |apply (H H3)] + |apply (H H1)]] +qed. + +lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l. +intros 3;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p t));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. + +lemma in_list_filter_r : \forall l,p,x. + in_list nat x l \to p x = true \to in_list nat x (filter nat l p). +intros 3;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 t));intro;rewrite > H4;simplify + [apply in_list_cons;apply H;assumption + |apply H;assumption]]] +qed. + +lemma incl_A_A: ∀T,A.incl T A A. +intros.unfold incl.intros.assumption. +qed. \ No newline at end of file diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index ba4f61bc4..a180cbabc 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -14,7 +14,10 @@ set "baseuri" "cic:/matita/list/". include "logic/equality.ma". +include "datatypes/bool.ma". include "higher_order_defs/functions.ma". +include "nat/plus.ma". +include "nat/orders.ma". inductive list (A:Type) : Type := | nil: list A @@ -92,6 +95,13 @@ theorem cons_append_commute: reflexivity; qed. +lemma append_cons:\forall A.\forall a:A.\forall l,l1. +l@(a::l1)=(l@[a])@l1. +intros. +rewrite > associative_append. +reflexivity. +qed. + inductive permutation (A:Type) : list A -> list A -> Prop \def | refl : \forall l:list A. permutation ? l l | swap : \forall l:list A. \forall x,y:A. @@ -143,3 +153,46 @@ let rec nth (A:Type) l d n on n ≝ ] | S n' ⇒ nth A (tail ? l) d n' ]. + +let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝ + match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. + +let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := + match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)]. + +definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l. + +definition filter \def + \lambda T:Type.\lambda l:list T.\lambda p:T \to bool. + foldr T (list T) + (\lambda x,l0.match (p x) with [ true => x::l0 | false => l0]) [] l. + +definition iota : nat → nat → list nat ≝ + λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. + +(* ### induction principle for functions visiting 2 lists in parallel *) +lemma list_ind2 : + ∀T1,T2:Type.∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop. + length ? l1 = length ? l2 → + (P (nil ?) (nil ?)) → + (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → + P l1 l2. +intros (T1 T2 l1 l2 P Hl Pnil Pcons); +generalize in match Hl; clear Hl; generalize in match l2; clear l2; +elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]] +intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] +intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption; +qed. + +lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. +intros (A B f g l Efg); elim l; simplify; [1: reflexivity ]; +rewrite > (Efg t); rewrite > H; reflexivity; +qed. + +lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l. +intros;elim l + [simplify;apply le_n + |simplify;apply (bool_elim ? (p t));intro + [simplify;apply le_S_S;assumption + |simplify;apply le_S;assumption]] +qed. \ No newline at end of file diff --git a/helm/software/matita/library/list/sort.ma b/helm/software/matita/library/list/sort.ma index d182ed6d6..c67b28227 100644 --- a/helm/software/matita/library/list/sort.ma +++ b/helm/software/matita/library/list/sort.ma @@ -12,22 +12,29 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/list/sort/". - include "datatypes/bool.ma". include "datatypes/constructors.ma". -include "list/list.ma". +include "list/in.ma". + +inductive sorted (A:Type) (P:A \to A \to Prop): list A \to Prop \def +| sort_nil : sorted A P [] +| sort_cons : \forall x,l.sorted A P l \to (\forall y.in_list ? y l \to P x y) + \to sorted A P (x::l). + +lemma sorted_cons_to_sorted : \forall A,P,x,l.sorted A P (x::l) \to sorted A P l. +intros;inversion H;intros + [destruct H1 + |destruct H4;assumption] +qed. + +lemma sorted_to_minimum : \forall A,P,x,l.sorted A P (x::l) \to + \forall y.in_list ? y l \to P x y. +intros;inversion H;intros; + [destruct H2 + |destruct H5;apply H4;assumption] +qed. + -let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ - match l with - [ nil ⇒ false - | (cons a l') ⇒ - match eq x a with - [ true ⇒ true - | false ⇒ mem A eq x l' - ] - ]. - let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝ match l with [ nil ⇒ true @@ -39,6 +46,45 @@ let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝ ] ]. +lemma sorted_to_eq_sorted_b_true : + \forall A,ord,ordb. + (\forall x,y.ord x y \to ordb x y = true) \to + \forall l.sorted A ord l \to ordered A ordb l = true. +intros 5;elim l + [reflexivity + |simplify;rewrite > H1;generalize in match H2;cases l1;intros + [reflexivity + |simplify;rewrite > H + [reflexivity + |apply (sorted_to_minimum ? ? ? ? H3);apply in_list_head] + |apply sort_nil + |apply (sorted_cons_to_sorted ? ? ? ? H3)]] +qed. + +(* + TODO + per far funzionare questa dimostrazione bisogna appoggiarsi a un + eqb (e utilizzare quindi in_list <-> mem), oppure modificare la definizione + di sorted in modo che non si appoggi più a in_list: + sorted [] + sorted [x] per ogni x + sorted x::y::l se ord x y e sorted y::l + +lemma eq_sorted_b_true_to_sorted : + \forall A,ord,ordb. + (\forall x,y.ordb x y = true \to ord x y) \to + \forall l.ordered A ordb l = true \to sorted A ord l. +intros 5;elim l + [apply sort_nil + |apply sort_cons + [apply H1;simplify in H2;generalize in match H2;cases l1;intros + [reflexivity + |simplify in H3;simplify;apply (andb_true_true_r ? ? H3)] + |intros;apply H;generalize in match H2; + generalize in match (in_list_to_mem_true ? ? ? ? H + [ +*) + let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝ match l with [ nil ⇒ [x] diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index 628a91f10..d1ad9e12e 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -15,7 +15,8 @@ include "nat/sqrt.ma". include "nat/chebyshev_teta.ma". include "nat/chebyshev.ma". -include "list/list.ma". +include "list/in.ma". +include "list/sort.ma". include "nat/o.ma". let rec list_divides l n \def @@ -32,18 +33,6 @@ definition lprim : nat \to list nat \def | false => aux m1 (n-m1::acc)]] in aux (pred n) []. -let rec filter A l p on l \def - match l with - [ nil => nil A - | cons (a:A) (tl:list A) => match (p a) with - [ true => a::(filter A tl p) - | false => filter A tl p ]]. - -let rec length A (l:list A) on l \def - match l with - [ nil => O - | cons (a:A) (tl:list A) => S (length A tl) ]. - let rec list_n_aux n k \def match n with [ O => nil nat @@ -62,76 +51,6 @@ let rec sieve_aux l1 l2 t on t \def definition sieve : nat \to list nat \def \lambda m.sieve_aux [] (list_n m) m. -definition ord_list \def - \lambda l. - \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a. - -definition in_list \def - \lambda A.\lambda a:A.\lambda l:list A. - \exists l1,l2.l = l1@(a::l2). - -lemma in_list_filter_to_p_true : \forall l,x,p. -in_list nat x (filter nat l p) \to p x = true. -intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0 - [simplify;intro;elim l1 - [simplify in H;destruct H - |simplify in H1;destruct H1] - |intros;simplify in H1;apply (bool_elim ? (p t));intro; - rewrite > H3 in H1;simplify in H1 - [generalize in match H1;elim l2 - [simplify in H4;destruct H4;assumption - |simplify in H5;destruct H5;apply (H l3);assumption] - |apply (H l2);assumption]] -qed. - -lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l). -intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a)); -apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity. -qed. - -lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l. -intros;elim H;elim H2;generalize in match H3;elim a - [simplify in H4;destruct H4;elim H1;reflexivity - |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1); - reflexivity] -qed. - -lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l. -intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0 - [simplify;intro;elim l1 - [simplify in H3;destruct H3 - |simplify in H4;destruct H4] - |intros;simplify in H4;apply (bool_elim ? (p t));intro - [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2 - [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1); - simplify;reflexivity - |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);] - |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]] -qed. - -lemma in_list_filter_r : \forall l,p,x.in_list nat x l \to p x = true \to in_list nat x (filter nat l p). -intros;elim H;elim H2;rewrite > H3;elim a - [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p)); - reflexivity - |simplify;elim (p t);simplify - [apply in_list_cons;assumption - |assumption]] -qed. - -lemma in_list_head : \forall x,l.in_list nat x (x::l). -intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity; -qed. - -lemma 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;elim H;elim H1;clear H H1;generalize in match H2;elim a1 - [simplify in H;destruct H;left;reflexivity - |simplify in H1;destruct H1;right; - apply (ex_intro ? ? l1); - apply (ex_intro ? ? a2); - reflexivity] -qed. - lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to \exists p.p \leq m \land prime p \land p \divides n. intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split @@ -144,42 +63,8 @@ intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split assumption] qed. - -lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l. -intros;elim l - [simplify;apply le_n - |simplify;apply (bool_elim ? (p t));intro - [simplify;apply le_S_S;assumption - |simplify;apply le_S;assumption]] -qed. - -inductive sorted (P:nat \to nat \to Prop): list nat \to Prop \def -| sort_nil : sorted P [] -| sort_cons : \forall x,l.sorted P l \to (\forall y.in_list ? y l \to P x y) - \to sorted P (x::l). - -definition sorted_lt : list nat \to Prop \def \lambda l.sorted lt l. - -definition sorted_gt : list nat \to Prop \def \lambda l.sorted gt l. - -lemma sorted_cons_to_sorted : \forall P,x,l.sorted P (x::l) \to sorted P l. -intros;inversion H;intros - [destruct H1 - |destruct H4;assumption] -qed. - -lemma sorted_to_minimum : \forall P,x,l.sorted P (x::l) \to - \forall y.in_list ? y l \to P x y. -intros;inversion H;intros; - [destruct H2 - |destruct H5;apply H4;assumption] -qed. - -lemma not_in_list_nil : \forall A,a.\lnot in_list A a []. -intros;intro;elim H;elim H1;generalize in match H2;elim a1 - [simplify in H3;destruct H3 - |simplify in H4;destruct H4] -qed. +definition sorted_lt \def sorted ? lt. +definition sorted_gt \def sorted ? gt. lemma sieve_prime : \forall t,k,l2,l1. (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land @@ -235,7 +120,7 @@ intro.elim t 0 |apply (trans_le ? ? ? H11); elim (in_list_cons_case ? ? ? ? H19) [rewrite > H20;apply le_n - |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]] + |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]] |apply in_list_head] |elim (H3 t1);elim H11 [elim H13;apply lt_to_le;assumption @@ -253,7 +138,7 @@ intro.elim t 0 |rewrite < H10;elim (H3 t1);elim H11 [elim H13;apply lt_to_le;assumption |apply in_list_head]] - |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);apply (in_list_filter ? ? ? H9)]] + |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]] |elim (H2 p);elim (H9 H8);split [assumption |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]] @@ -294,7 +179,7 @@ intro.elim t 0 |apply in_list_head]]] |elim (in_list_cons_case ? ? ? ? H13) [rewrite > H14;apply le_n - |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]] + |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]] |elim (H3 x);split;intros; [split [elim H7 @@ -332,41 +217,28 @@ intro.elim t 0 [assumption |intros;unfold;elim (H2 y);elim (H8 H7); apply H11;apply in_list_head] - |generalize in match (sorted_cons_to_sorted ? ? ? H6);elim l + |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l [simplify;assumption |simplify;elim (notb (divides_b t1 t2));simplify - [lapply (sorted_cons_to_sorted ? ? ? H8);lapply (H7 Hletin); - apply (sort_cons ? ? ? Hletin1);intros; - apply (sorted_to_minimum ? ? ? H8);apply (in_list_filter ? ? ? H9); - |apply H7;apply (sorted_cons_to_sorted ? ? ? H8)]]]]] -qed. - -lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. -intros;elim H;elim H1;generalize in match H2;elim a - [simplify in H3;destruct H3;reflexivity - |simplify in H4;destruct H4;generalize in match Hcut1;elim l - [simplify in H4;destruct H4 - |simplify in H5;destruct H5]] + [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin); + apply (sort_cons ? ? ? ? Hletin1);intros; + apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9); + |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]] qed. lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to k \leq n. intros 2;elim m [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;elim H1;elim H2;generalize in match H3;elim a - [simplify in H4;destruct H4;apply le_n - |simplify in H5;destruct H5;apply lt_to_le;apply (H (S k)); - apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]] + |simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H2;apply le_n + |apply lt_to_le;apply H;assumption]] qed. lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n). -intros;elim H - [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? []); - simplify;reflexivity - |generalize in match H2;elim H1 - [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? [3]);simplify;reflexivity - |simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (list_n_aux n2 3)); - simplify;reflexivity]] +intros;elim H;simplify + [apply in_list_head + |generalize in match H2;elim H1;simplify;apply in_list_head] qed. lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n. @@ -376,11 +248,10 @@ qed. lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1. intros 2;elim m [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;elim H1;elim H2;generalize in match H3;elim a - [simplify in H4;destruct H4;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O; + |simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O; rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n - |simplify in H5;destruct H5;rewrite < plus_n_Sm;apply (H (S k)); - apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]] + |rewrite < plus_n_Sm;apply (H (S k));assumption]] qed. lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m. @@ -469,9 +340,9 @@ lemma sieve_sorted : \forall n.sorted_gt (sieve n). intros;elim (decidable_le 2 n) [elim (sieve_sound1 ? H);assumption |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n - [intro;apply sort_nil + [intro;simplify;apply sort_nil |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin); - apply sort_nil]] + simplify;apply sort_nil]] qed. lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to