diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 115 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 10 | ||||
| -rw-r--r-- | theories/Lists/ListTactics.v | 2 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 497 | ||||
| -rw-r--r-- | theories/Lists/StreamMemo.v | 205 | ||||
| -rw-r--r-- | theories/Lists/Streams.v | 84 |
6 files changed, 703 insertions, 210 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c80d0b15..a72283d9 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1,15 +1,14 @@ - (************************************************************************) - (* v * The Coq Proof Assistant / The Coq Development Team *) - (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) - (* \VV/ **************************************************************) - (* // * This file is distributed under the terms of the *) - (* * GNU Lesser General Public License Version 2.1 *) - (************************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) - (*i $Id: List.v 9290 2006-10-26 19:20:42Z herbelin $ i*) +(*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*) Require Import Le Gt Minus Min Bool. -Require Import Setoid. Set Implicit Arguments. @@ -82,8 +81,6 @@ End Lists. Implicit Arguments nil [A]. Infix "::" := cons (at level 60, right associativity) : list_scope. Infix "++" := app (right associativity, at level 60) : list_scope. - -Ltac now_show c := change c in |- *. Open Scope list_scope. @@ -314,7 +311,27 @@ Section Facts. now_show (H = a \/ In a (y ++ m)). elim H2; auto. Qed. - + + Lemma app_inv_head: + forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Proof. + induction l; simpl; auto; injection 1; auto. + Qed. + + Lemma app_inv_tail: + forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Proof. + intros l l1 l2; revert l1 l2 l. + induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; + simpl; auto; intros l H. + absurd (length (x2 :: l2 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite <- H; auto with arith. + absurd (length (x1 :: l1 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite H; auto with arith. + injection H; clear H; intros; f_equal; eauto. + Qed. End Facts. @@ -512,6 +529,20 @@ Section Elts. exists (a::l'); exists a'; auto. Qed. + Lemma removelast_app : + forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'. + Proof. + induction l. + simpl; auto. + simpl; intros. + assert (l++l' <> nil). + destruct l. + simpl; auto. + simpl; discriminate. + specialize (IHl l' H). + destruct (l++l'); [elim H0; auto|f_equal; auto]. + Qed. + (****************************************) (** ** Counting occurences of a element *) @@ -534,8 +565,7 @@ Section Elts. simpl; intros; split; [destruct 1 | apply gt_irrefl]. simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq]. rewrite Heq; intuition. - rewrite <- (IHl x). - tauto. + pose (IHl x). intuition. Qed. Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil. @@ -668,8 +698,8 @@ Section ListOps. rewrite app_nth1; auto. rewrite (minus_plus_simpl_l_reverse (length l) n 1). replace (1 + length l) with (S (length l)); auto with arith. - rewrite <- minus_Sn_m; auto with arith; simpl. - apply IHl; auto. + rewrite <- minus_Sn_m; auto with arith. + apply IHl ; auto with arith. rewrite rev_length; auto. Qed. @@ -899,7 +929,7 @@ Section ListOps. apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app. apply perm_skip. apply (IH a l1' l2 l3' l4); auto. - (* swap *) + (* contradict *) intros x y l l' Hp IH; intros. break_list l1 b l1' H; break_list l3 c l3' H0. auto. @@ -1345,7 +1375,7 @@ End Fold_Right_Recursor. destruct n; destruct d; simpl; auto. destruct a; destruct (split l); simpl; auto. destruct a; destruct (split l); simpl in *; auto. - rewrite IHl; simpl; auto. + apply IHl. Qed. Lemma split_length_l : forall (l:list (A*B)), @@ -1618,7 +1648,7 @@ Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons (**************************************) -(* ** Cutting a list at some position *) +(** * Cutting a list at some position *) (**************************************) Section Cutting. @@ -1651,6 +1681,45 @@ Section Cutting. f_equal; auto. Qed. + Lemma firstn_length : forall n l, length (firstn n l) = min n (length l). + Proof. + induction n; destruct l; simpl; auto. + Qed. + + Lemma removelast_firstn : forall n l, n < length l -> + removelast (firstn (S n) l) = firstn n l. + Proof. + induction n; destruct l. + simpl; auto. + simpl; auto. + simpl; auto. + intros. + simpl in H. + change (firstn (S (S n)) (a::l)) with ((a::nil)++firstn (S n) l). + change (firstn (S n) (a::l)) with (a::firstn n l). + rewrite removelast_app. + rewrite IHn; auto with arith. + + clear IHn; destruct l; simpl in *; try discriminate. + inversion_clear H. + inversion_clear H0. + Qed. + + Lemma firstn_removelast : forall n l, n < length l -> + firstn n (removelast l) = firstn n l. + Proof. + induction n; destruct l. + simpl; auto. + simpl; auto. + simpl; auto. + intros. + simpl in H. + change (removelast (a :: l)) with (removelast ((a::nil)++l)). + rewrite removelast_app. + simpl; f_equal; auto with arith. + intro H0; rewrite H0 in H; inversion_clear H; inversion_clear H1. + Qed. + End Cutting. @@ -1672,8 +1741,8 @@ Section ReDun. inversion_clear 1; auto. inversion_clear 1. constructor. - swap H0. - apply in_or_app; destruct (in_app_or _ _ _ H); simpl; tauto. + contradict H0. + apply in_or_app; destruct (in_app_or _ _ _ H0); simpl; tauto. apply IHl with a0; auto. Qed. @@ -1682,8 +1751,8 @@ Section ReDun. induction l; simpl. inversion_clear 1; auto. inversion_clear 1. - swap H0. - destruct H. + contradict H0. + destruct H0. subst a0. apply in_or_app; right; red; auto. destruct (IHl _ _ H1); auto. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 4e009ed5..021a64c1 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListSet.v 6844 2005-03-16 13:09:55Z herbelin $ i*) +(*i $Id: ListSet.v 10616 2008-03-04 17:33:35Z letouzey $ i*) (** A Library for finite sets, implemented as lists *) @@ -20,7 +20,7 @@ Set Implicit Arguments. Section first_definitions. - Variable A : Set. + Variable A : Type. Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}. Definition set := list A. @@ -100,7 +100,7 @@ Section first_definitions. Qed. Lemma set_mem_ind : - forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set), + forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z). Proof. @@ -110,7 +110,7 @@ Section first_definitions. Qed. Lemma set_mem_ind2 : - forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set), + forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> (~ set_In a x -> P z) -> P (if set_mem a x then y else z). @@ -373,7 +373,7 @@ End first_definitions. Section other_definitions. - Variables A B : Set. + Variables A B : Type. Definition set_prod : set A -> set B -> set (A * B) := list_prod (A:=A) (B:=B). diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index e46f1279..515ed138 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListTactics.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: ListTactics.v 9427 2006-12-11 18:46:35Z bgregoir $ i*) Require Import BinPos. Require Import List. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index eb40594b..4edc1581 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: SetoidList.v 8853 2006-05-23 18:17:38Z herbelin $ *) +(* $Id: SetoidList.v 10616 2008-03-04 17:33:35Z letouzey $ *) Require Export List. Require Export Sorting. @@ -21,7 +21,7 @@ Unset Strict Implicit. found in [Sorting]. *) Section Type_with_equality. -Variable A : Set. +Variable A : Type. Variable eqA : A -> A -> Prop. (** Being in a list modulo an equality relation over type [A]. *) @@ -32,6 +32,18 @@ Inductive InA (x : A) : list A -> Prop := Hint Constructors InA. +Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l. +Proof. + intuition. + inversion H; auto. +Qed. + +Lemma InA_nil : forall x, InA x nil <-> False. +Proof. + intuition. + inversion H. +Qed. + (** An alternative definition of [InA]. *) Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l. @@ -53,7 +65,28 @@ Hint Constructors NoDupA. (** lists with same elements modulo [eqA] *) -Definition eqlistA l l' := forall x, InA x l <-> InA x l'. +Definition equivlistA l l' := forall x, InA x l <-> InA x l'. + +(** lists with same elements modulo [eqA] at the same place *) + +Inductive eqlistA : list A -> list A -> Prop := + | eqlistA_nil : eqlistA nil nil + | eqlistA_cons : forall x x' l l', + eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l'). + +Hint Constructors eqlistA. + +(** Compatibility of a boolean function with respect to an equality. *) + +Definition compat_bool (f : A->bool) := forall x y, eqA x y -> f x = f y. + +(** Compatibility of a function upon natural numbers. *) + +Definition compat_nat (f : A->nat) := forall x y, eqA x y -> f x = f y. + +(** Compatibility of a predicate with respect to an equality. *) + +Definition compat_P (P : A->Prop) := forall x y, eqA x y -> P x -> P y. (** Results concerning lists modulo [eqA] *) @@ -91,6 +124,35 @@ exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. Qed. +Lemma InA_app : forall l1 l2 x, + InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. +Proof. + induction l1; simpl in *; intuition. + inversion_clear H; auto. + elim (IHl1 l2 x H0); auto. +Qed. + +Lemma InA_app_iff : forall l1 l2 x, + InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2. +Proof. + split. + apply InA_app. + destruct 1; generalize H; do 2 rewrite InA_alt. + destruct 1 as (y,(H1,H2)); exists y; split; auto. + apply in_or_app; auto. + destruct 1 as (y,(H1,H2)); exists y; split; auto. + apply in_or_app; auto. +Qed. + +Lemma InA_rev : forall p m, + InA p (rev m) <-> InA p m. +Proof. + intros; do 2 rewrite InA_alt. + split; intros (y,H); exists y; intuition. + rewrite In_rev; auto. + rewrite <- In_rev; auto. +Qed. + (** Results concerning lists modulo [eqA] and [ltA] *) Variable ltA : A -> A -> Prop. @@ -106,10 +168,12 @@ Hint Immediate ltA_eqA eqA_ltA. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). +Hint Constructors lelistA sort. + Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. Proof. - intro s; case s; constructor; inversion_clear H0. + destruct l; constructor; inversion_clear H0; eapply ltA_trans; eauto. Qed. @@ -153,6 +217,26 @@ intros; eapply SortA_InfA_InA; eauto. apply InA_InfA. Qed. +Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). +Proof. + induction l1; simpl; auto. + inversion_clear 1; auto. +Qed. + +Lemma SortA_app : + forall l1 l2, SortA l1 -> SortA l2 -> + (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> + SortA (l1 ++ l2). +Proof. + induction l1; simpl in *; intuition. + inversion_clear H. + constructor; auto. + apply InfA_app; auto. + destruct l2; auto. +Qed. + +Section NoDupA. + Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. Proof. simple induction l; auto. @@ -185,7 +269,6 @@ intros. apply (H1 x); auto. Qed. - Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). Proof. induction l. @@ -206,33 +289,240 @@ rewrite In_rev; auto. inversion H4. Qed. +Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). +Proof. + induction l; simpl in *; inversion_clear 1; auto. + constructor; eauto. + contradict H0. + rewrite InA_app_iff in *; rewrite InA_cons; intuition. +Qed. -Lemma InA_app : forall l1 l2 x, - InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. +Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l'). Proof. - induction l1; simpl in *; intuition. - inversion_clear H; auto. - elim (IHl1 l2 x H0); auto. + induction l; simpl in *; inversion_clear 1; auto. + constructor; eauto. + assert (H2:=IHl _ _ H1). + inversion_clear H2. + rewrite InA_cons. + red; destruct 1. + apply H0. + rewrite InA_app_iff in *; rewrite InA_cons; auto. + apply H; auto. + constructor. + contradict H0. + rewrite InA_app_iff in *; rewrite InA_cons; intuition. + eapply NoDupA_split; eauto. Qed. - Hint Constructors lelistA sort. +End NoDupA. -Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). +(** Some results about [eqlistA] *) + +Section EqlistA. + +Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'. Proof. - induction l1; simpl; auto. - inversion_clear 1; auto. +induction 1; auto; simpl; congruence. Qed. -Lemma SortA_app : - forall l1 l2, SortA l1 -> SortA l2 -> - (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> - SortA (l1 ++ l2). +Lemma eqlistA_app : forall l1 l1' l2 l2', + eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2'). Proof. - induction l1; simpl in *; intuition. - inversion_clear H. - constructor; auto. - apply InfA_app; auto. - destruct l2; auto. +intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto. +Qed. + +Lemma eqlistA_rev_app : forall l1 l1', + eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> + eqlistA ((rev l1)++l2) ((rev l1')++l2'). +Proof. +induction 1; auto. +simpl; intros. +do 2 rewrite app_ass; simpl; auto. +Qed. + +Lemma eqlistA_rev : forall l1 l1', + eqlistA l1 l1' -> eqlistA (rev l1) (rev l1'). +Proof. +intros. +rewrite (app_nil_end (rev l1)). +rewrite (app_nil_end (rev l1')). +apply eqlistA_rev_app; auto. +Qed. + +Lemma SortA_equivlistA_eqlistA : forall l l', + SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'. +Proof. +induction l; destruct l'; simpl; intros; auto. +destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4. +destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4. +inversion_clear H; inversion_clear H0. +assert (forall y, InA y l -> ltA a y). +intros; eapply SortA_InfA_InA with (l:=l); eauto. +assert (forall y, InA y l' -> ltA a0 y). +intros; eapply SortA_InfA_InA with (l:=l'); eauto. +clear H3 H4. +assert (eqA a a0). + destruct (H1 a). + destruct (H1 a0). + assert (InA a (a0::l')) by auto. + inversion_clear H8; auto. + assert (InA a0 (a::l)) by auto. + inversion_clear H8; auto. + elim (@ltA_not_eqA a a); auto. + apply ltA_trans with a0; auto. +constructor; auto. +apply IHl; auto. +split; intros. +destruct (H1 x). +assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto. +elim (@ltA_not_eqA a x); eauto. +destruct (H1 x). +assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto. +elim (@ltA_not_eqA a0 x); eauto. +Qed. + +End EqlistA. + +(** A few things about [filter] *) + +Section Filter. + +Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). +Proof. +induction l; simpl; auto. +inversion_clear 1; auto. +destruct (f a); auto. +constructor; auto. +apply In_InfA; auto. +intros. +rewrite filter_In in H; destruct H. +eapply SortA_InfA_InA; eauto. +Qed. + +Lemma filter_InA : forall f, (compat_bool f) -> + forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. +Proof. +intros; do 2 rewrite InA_alt; intuition. +destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. +destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. + rewrite (H _ _ H0); auto. +destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition. + rewrite <- (H _ _ H0); auto. +Qed. + +Lemma filter_split : + forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> + forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l. +Proof. +induction l; simpl; intros; auto. +inversion_clear H0. +pattern l at 1; rewrite IHl; auto. +case_eq (f a); simpl; intros; auto. +assert (forall e, In e l -> f e = false). + intros. + assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). + case_eq (f e); simpl; intros; auto. + elim (@ltA_not_eqA e e); auto. + apply ltA_trans with a; eauto. +replace (List.filter f l) with (@nil A); auto. +generalize H3; clear; induction l; simpl; auto. +case_eq (f a); auto; intros. +rewrite H3 in H; auto; try discriminate. +Qed. + +End Filter. + +Section Fold. + +Variable B:Type. +Variable eqB:B->B->Prop. + +(** Compatibility of a two-argument function with respect to two equalities. *) +Definition compat_op (f : A -> B -> B) := + forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y'). + +(** Two-argument functions that allow to reorder their arguments. *) +Definition transpose (f : A -> B -> B) := + forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). + +Variable st:Setoid_Theory _ eqB. +Variable f:A->B->B. +Variable i:B. +Variable Comp:compat_op f. + +Lemma fold_right_eqlistA : + forall s s', eqlistA s s' -> + eqB (fold_right f i s) (fold_right f i s'). +Proof. +induction 1; simpl; auto. +refl_st. +Qed. + +Variable Ass:transpose f. + +Lemma fold_right_commutes : forall s1 s2 x, + eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). +Proof. +induction s1; simpl; auto; intros. +refl_st. +trans_st (f a (f x (fold_right f i (s1++s2)))). +Qed. + +Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> + NoDupA (x::l) -> NoDupA (l1++y::l2) -> + equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2). +Proof. + intros; intro a. + generalize (H2 a). + repeat rewrite InA_app_iff. + do 2 rewrite InA_cons. + inversion_clear H0. + assert (SW:=NoDupA_swap H1). + inversion_clear SW. + rewrite InA_app_iff in H0. + split; intros. + assert (~eqA a x). + contradict H3; apply InA_eqA with a; auto. + assert (~eqA a y). + contradict H8; eauto. + intuition. + assert (eqA a x \/ InA a l) by intuition. + destruct H8; auto. + elim H0. + destruct H7; [left|right]; eapply InA_eqA; eauto. +Qed. + +Lemma fold_right_equivlistA : + forall s s', NoDupA s -> NoDupA s' -> + equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). +Proof. + simple induction s. + destruct s'; simpl. + intros; refl_st; auto. + unfold equivlistA; intros. + destruct (H1 a). + assert (X : InA a nil); auto; inversion X. + intros x l Hrec s' N N' E; simpl in *. + assert (InA x s'). + rewrite <- (E x); auto. + destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). + subst s'. + trans_st (f x (fold_right f i (s1++s2))). + apply Comp; auto. + apply Hrec; auto. + inversion_clear N; auto. + eapply NoDupA_split; eauto. + eapply equivlistA_NoDupA_split; eauto. + trans_st (f y (fold_right f i (s1++s2))). + apply Comp; auto; refl_st. + sym_st; apply fold_right_commutes. +Qed. + +Lemma fold_right_add : + forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s -> + equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). +Proof. + intros; apply (@fold_right_equivlistA s' (x::s)); auto. Qed. Section Remove. @@ -279,7 +569,7 @@ destruct H0; apply eqA_trans with a; auto. split. inversion_clear 1. split; auto. -swap n. +contradict n. apply eqA_trans with y; auto. rewrite (IHl x y) in H0; destruct H0; auto. destruct 1; inversion_clear H; auto. @@ -298,14 +588,14 @@ rewrite removeA_InA. intuition. Qed. -Lemma removeA_eqlistA : forall l l' x, - ~InA x l -> eqlistA (x :: l) l' -> eqlistA l (removeA x l'). +Lemma removeA_equivlistA : forall l l' x, + ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l'). Proof. -unfold eqlistA; intros. +unfold equivlistA; intros. rewrite removeA_InA. split; intros. rewrite <- H0; split; auto. -swap H. +contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. @@ -313,160 +603,17 @@ inversion_clear H1; auto. elim H2; auto. Qed. -Let addlistA x l l' := forall y, InA y l' <-> eqA x y \/ InA y l. - -Lemma removeA_add : - forall s s' x x', NoDupA s -> NoDupA (x' :: s') -> - ~ eqA x x' -> ~ InA x s -> - addlistA x s (x' :: s') -> addlistA x (removeA x' s) s'. -Proof. -unfold addlistA; intros. -inversion_clear H0. -rewrite removeA_InA; auto. -split; intros. -destruct (eqA_dec x y); auto; intros. -right; split; auto. -destruct (H3 y); clear H3. -destruct H6; intuition. -swap H4; apply InA_eqA with y; auto. -destruct H0. -assert (InA y (x' :: s')) by (rewrite H3; auto). -inversion_clear H6; auto. -elim H1; apply eqA_trans with y; auto. -destruct H0. -assert (InA y (x' :: s')) by (rewrite H3; auto). -inversion_clear H7; auto. -elim H6; auto. -Qed. - -Section Fold. - -Variable B:Set. -Variable eqB:B->B->Prop. - -(** Two-argument functions that allow to reorder its arguments. *) -Definition transpose (f : A -> B -> B) := - forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). - -(** Compatibility of a two-argument function with respect to two equalities. *) -Definition compat_op (f : A -> B -> B) := - forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y'). - -(** Compatibility of a function upon natural numbers. *) -Definition compat_nat (f : A -> nat) := - forall x x' : A, eqA x x' -> f x = f x'. - -Variable st:Setoid_Theory _ eqB. -Variable f:A->B->B. -Variable Comp:compat_op f. -Variable Ass:transpose f. -Variable i:B. - -Lemma removeA_fold_right_0 : - forall s x, ~InA x s -> - eqB (fold_right f i s) (fold_right f i (removeA x s)). -Proof. - simple induction s; simpl; intros. - refl_st. - destruct (eqA_dec x a); simpl; intros. - absurd_hyp e; auto. - apply Comp; auto. -Qed. - -Lemma removeA_fold_right : - forall s x, NoDupA s -> InA x s -> - eqB (fold_right f i s) (f x (fold_right f i (removeA x s))). -Proof. - simple induction s; simpl. - inversion_clear 2. - intros. - inversion_clear H0. - destruct (eqA_dec x a); simpl; intros. - apply Comp; auto. - apply removeA_fold_right_0; auto. - swap H2; apply InA_eqA with x; auto. - inversion_clear H1. - destruct n; auto. - trans_st (f a (f x (fold_right f i (removeA x l)))). -Qed. - -Lemma fold_right_equal : - forall s s', NoDupA s -> NoDupA s' -> - eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). -Proof. - simple induction s. - destruct s'; simpl. - intros; refl_st; auto. - unfold eqlistA; intros. - destruct (H1 a). - assert (X : InA a nil); auto; inversion X. - intros x l Hrec s' N N' E; simpl in *. - trans_st (f x (fold_right f i (removeA x s'))). - apply Comp; auto. - apply Hrec; auto. - inversion N; auto. - apply removeA_NoDupA; auto; apply eqA_trans. - apply removeA_eqlistA; auto. - inversion_clear N; auto. - sym_st. - apply removeA_fold_right; auto. - unfold eqlistA in E. - rewrite <- E; auto. -Qed. - -Lemma fold_right_add : - forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s -> - addlistA x s s' -> eqB (fold_right f i s') (f x (fold_right f i s)). -Proof. - simple induction s'. - unfold addlistA; intros. - destruct (H2 x); clear H2. - assert (X : InA x nil); auto; inversion X. - intros x' l' Hrec s x N N' IN EQ; simpl. - (* if x=x' *) - destruct (eqA_dec x x'). - apply Comp; auto. - apply fold_right_equal; auto. - inversion_clear N'; trivial. - unfold eqlistA; unfold addlistA in EQ; intros. - destruct (EQ x0); clear EQ. - split; intros. - destruct H; auto. - inversion_clear N'. - destruct H2; apply InA_eqA with x0; auto. - apply eqA_trans with x; auto. - assert (X:InA x0 (x' :: l')); auto; inversion_clear X; auto. - destruct IN; apply InA_eqA with x0; auto. - apply eqA_trans with x'; auto. - (* else x<>x' *) - trans_st (f x' (f x (fold_right f i (removeA x' s)))). - apply Comp; auto. - apply Hrec; auto. - apply removeA_NoDupA; auto; apply eqA_trans. - inversion_clear N'; auto. - rewrite removeA_InA; intuition. - apply removeA_add; auto. - trans_st (f x (f x' (fold_right f i (removeA x' s)))). - apply Comp; auto. - sym_st. - apply removeA_fold_right; auto. - destruct (EQ x'). - destruct H; auto; destruct n; auto. -Qed. +End Remove. End Fold. -End Remove. - End Type_with_equality. -Hint Constructors InA. -Hint Constructors NoDupA. -Hint Constructors sort. -Hint Constructors lelistA. +Hint Unfold compat_bool compat_nat compat_P. +Hint Constructors InA NoDupA sort lelistA eqlistA. Section Find. -Variable A B : Set. +Variable A B : Type. Variable eqA : A -> A -> Prop. Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x. Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z. diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v new file mode 100644 index 00000000..bdbe0ecc --- /dev/null +++ b/theories/Lists/StreamMemo.v @@ -0,0 +1,205 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Eqdep_dec. +Require Import Streams. + +(** * Memoization *) + +(** Successive outputs of a given function [f] are stored in + a stream in order to avoid duplicated computations. *) + +Section MemoFunction. + +Variable A: Type. +Variable f: nat -> A. + +CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)). + +Definition memo_list := memo_make 0. + +Fixpoint memo_get (n:nat) (l:Stream A) : A := + match n with + | O => hd l + | S n1 => memo_get n1 (tl l) + end. + +Theorem memo_get_correct: forall n, memo_get n memo_list = f n. +Proof. +assert (F1: forall n m, memo_get n (memo_make m) = f (n + m)). + induction n as [| n Hrec]; try (intros m; refine (refl_equal _)). + intros m; simpl; rewrite Hrec. + rewrite plus_n_Sm; auto. +intros n; apply trans_equal with (f (n + 0)); try exact (F1 n 0). +rewrite <- plus_n_O; auto. +Qed. + +(** Building with possible sharing using a iterator [g] : + We now suppose in addition that [f n] is in fact the [n]-th + iterate of a function [g]. +*) + +Variable g: A -> A. + +Hypothesis Hg_correct: forall n, f (S n) = g (f n). + +CoFixpoint imemo_make (fn:A) : Stream A := + let fn1 := g fn in + Cons fn1 (imemo_make fn1). + +Definition imemo_list := let f0 := f 0 in + Cons f0 (imemo_make f0). + +Theorem imemo_get_correct: forall n, memo_get n imemo_list = f n. +Proof. +assert (F1: forall n m, + memo_get n (imemo_make (f m)) = f (S (n + m))). + induction n as [| n Hrec]; try (intros m; exact (sym_equal (Hg_correct m))). + simpl; intros m; rewrite <- Hg_correct; rewrite Hrec; rewrite <- plus_n_Sm; auto. +destruct n as [| n]; try apply refl_equal. +unfold imemo_list; simpl; rewrite F1. +rewrite <- plus_n_O; auto. +Qed. + +End MemoFunction. + +(** For a dependent function, the previous solution is + reused thanks to a temporarly hiding of the dependency + in a "container" [memo_val]. *) + +Section DependentMemoFunction. + +Variable A: nat -> Type. +Variable f: forall n, A n. + +Inductive memo_val: Type := + memo_mval: forall n, A n -> memo_val. + +Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} := + match n, m return {n = m} + {True} with + | 0, 0 =>left True (refl_equal 0) + | 0, S m1 => right (0 = S m1) I + | S n1, 0 => right (S n1 = 0) I + | S n1, S m1 => + match is_eq n1 m1 with + | left H => left True (f_equal S H) + | right _ => right (S n1 = S m1) I + end + end. + +Definition memo_get_val n (v: memo_val): A n := +match v with +| memo_mval m x => + match is_eq n m with + | left H => + match H in (@eq _ _ y) return (A y -> A n) with + | refl_equal => fun v1 : A n => v1 + end + | right _ => fun _ : A m => f n + end x +end. + +Let mf n := memo_mval n (f n). + +Definition dmemo_list := memo_list _ mf. + +Definition dmemo_get n l := memo_get_val n (memo_get _ n l). + +Theorem dmemo_get_correct: forall n, dmemo_get n dmemo_list = f n. +Proof. +intros n; unfold dmemo_get, dmemo_list. +rewrite (memo_get_correct memo_val mf n); simpl. +case (is_eq n n); simpl; auto; intros e. +assert (e = refl_equal n). + apply eq_proofs_unicity. + induction x as [| x Hx]; destruct y as [| y]. + left; auto. + right; intros HH; discriminate HH. + right; intros HH; discriminate HH. + case (Hx y). + intros HH; left; case HH; auto. + intros HH; right; intros HH1; case HH. + injection HH1; auto. +rewrite H; auto. +Qed. + +(** Finally, a version with both dependency and iterator *) + +Variable g: forall n, A n -> A (S n). + +Hypothesis Hg_correct: forall n, f (S n) = g n (f n). + +Let mg v := match v with + memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end. + +Definition dimemo_list := imemo_list _ mf mg. + +Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n. +Proof. +intros n; unfold dmemo_get, dimemo_list. +rewrite (imemo_get_correct memo_val mf mg); simpl. +case (is_eq n n); simpl; auto; intros e. +assert (e = refl_equal n). + apply eq_proofs_unicity. + induction x as [| x Hx]; destruct y as [| y]. + left; auto. + right; intros HH; discriminate HH. + right; intros HH; discriminate HH. + case (Hx y). + intros HH; left; case HH; auto. + intros HH; right; intros HH1; case HH. + injection HH1; auto. +rewrite H; auto. +intros n1; unfold mf; rewrite Hg_correct; auto. +Qed. + +End DependentMemoFunction. + +(** An example with the memo function on factorial *) + +(* +Require Import ZArith. +Open Scope Z_scope. + +Fixpoint tfact (n: nat) := + match n with + | O => 1 + | S n1 => Z_of_nat n * tfact n1 + end. + +Definition lfact_list := + dimemo_list _ tfact (fun n z => (Z_of_nat (S n) * z)). + +Definition lfact n := dmemo_get _ tfact n lfact_list. + +Theorem lfact_correct n: lfact n = tfact n. +Proof. +intros n; unfold lfact, lfact_list. +rewrite dimemo_get_correct; auto. +Qed. + +Fixpoint nop p := + match p with + | xH => 0 + | xI p1 => nop p1 + | xO p1 => nop p1 + end. + +Fixpoint test z := + match z with + | Z0 => 0 + | Zpos p1 => nop p1 + | Zneg p1 => nop p1 + end. + +Time Eval vm_compute in test (lfact 2000). +Time Eval vm_compute in test (lfact 2000). +Time Eval vm_compute in test (lfact 1500). +Time Eval vm_compute in (lfact 1500). +*) + diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 7bc6a09d..49990502 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Streams.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Streams.v 9967 2007-07-11 15:25:03Z roconnor $ i*) Set Implicit Arguments. @@ -14,9 +14,9 @@ Set Implicit Arguments. Section Streams. -Variable A : Set. +Variable A : Type. -CoInductive Stream : Set := +CoInductive Stream : Type := Cons : A -> Stream -> Stream. @@ -146,6 +146,15 @@ Inductive Exists ( x: Stream ) : Prop := CoInductive ForAll (x: Stream) : Prop := HereAndFurther : P x -> ForAll (tl x) -> ForAll x. +Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x). +Proof. +induction m. + tauto. +intros x [_ H]. +simpl. +apply IHm. +assumption. +Qed. Section Co_Induction_ForAll. Variable Inv : Stream -> Prop. @@ -162,15 +171,78 @@ End Stream_Properties. End Streams. Section Map. -Variables A B : Set. +Variables A B : Type. Variable f : A -> B. CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)). + +Lemma Str_nth_tl_map : forall n s, Str_nth_tl n (map s)= map (Str_nth_tl n s). +Proof. +induction n. +reflexivity. +simpl. +intros s. +apply IHn. +Qed. + +Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s). +Proof. +intros n s. +unfold Str_nth. +rewrite Str_nth_tl_map. +reflexivity. +Qed. + +Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P +(map s)) S <-> ForAll P (map S). +Proof. +intros P S. +split; generalize S; clear S; cofix; intros S; constructor; +destruct H as [H0 H]; firstorder. +Qed. + +Lemma Exists_map : forall (P:Stream B -> Prop) (S:Stream A), Exists (fun s => P +(map s)) S -> Exists P (map S). +Proof. +intros P S H. +(induction H;[left|right]); firstorder. +Defined. + End Map. Section Constant_Stream. -Variable A : Set. +Variable A : Type. Variable a : A. CoFixpoint const : Stream A := Cons a const. End Constant_Stream. -Unset Implicit Arguments.
\ No newline at end of file +Section Zip. + +Variable A B C : Type. +Variable f: A -> B -> C. + +CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C := +Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)). + +Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), + Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b). +Proof. +induction n. +reflexivity. +intros [x xs] [y ys]. +unfold Str_nth in *. +simpl in *. +apply IHn. +Qed. + +Lemma Str_nth_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth n (zipWith a + b)= f (Str_nth n a) (Str_nth n b). +Proof. +intros. +unfold Str_nth. +rewrite Str_nth_tl_zipWith. +reflexivity. +Qed. + +End Zip. + +Unset Implicit Arguments. |