diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 71 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 80 | ||||
| -rw-r--r-- | theories/Lists/ListTactics.v | 6 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 101 | ||||
| -rw-r--r-- | theories/Lists/SetoidPermutation.v | 125 | ||||
| -rw-r--r-- | theories/Lists/StreamMemo.v | 29 | ||||
| -rw-r--r-- | theories/Lists/Streams.v | 16 | ||||
| -rw-r--r-- | theories/Lists/TheoryList.v | 423 | ||||
| -rwxr-xr-x | theories/Lists/intro.tex | 6 | ||||
| -rw-r--r-- | theories/Lists/vo.itarget | 2 |
10 files changed, 302 insertions, 557 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 4c14008c..69475a6f 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: List.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import Le Gt Minus Min Bool. +Require Import Le Gt Minus Bool Setoid. Set Implicit Arguments. @@ -55,9 +53,16 @@ Section Lists. End Lists. -(* Keep these notations local to prevent conflicting notations *) -Local Notation "[ ]" := nil : list_scope. -Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope. + +(** Standard notations for lists. +In a special module to avoid conflict. *) +Module ListNotations. +Notation " [ ] " := nil : list_scope. +Notation " [ x ] " := (cons x nil) : list_scope. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +End ListNotations. + +Import ListNotations. (** ** Facts about lists *) @@ -119,7 +124,7 @@ Section Facts. unfold not; intros a H; inversion_clear H. Qed. - Theorem in_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2. + Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. Proof. induction l; simpl; destruct 1. subst a; auto. @@ -254,7 +259,7 @@ Section Facts. Qed. - (** Compatibility wtih other operations *) + (** Compatibility with other operations *) Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'. Proof. @@ -541,30 +546,21 @@ Section Elts. end. (** Compatibility of count_occ with operations on list *) - Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0. + Theorem count_occ_In (l : list A) (x : A) : In x l <-> count_occ l x > 0. Proof. - induction l as [|y l]. - simpl; intros; split; [destruct 1 | apply gt_irrefl]. - simpl. intro x; destruct (eq_dec y x) as [Heq|Hneq]. - rewrite Heq; intuition. - pose (IHl x). intuition. + induction l as [|y l]; simpl. + - split; [destruct 1 | apply gt_irrefl]. + - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition. Qed. - Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = []. + Theorem count_occ_inv_nil (l : list A) : + (forall x:A, count_occ l x = 0) <-> l = []. Proof. split. - (* Case -> *) - induction l as [|x l]. - trivial. - intro H. - elim (O_S (count_occ l x)). - apply sym_eq. - generalize (H x). - simpl. destruct (eq_dec x x) as [|HF]. - trivial. - elim HF; reflexivity. - (* Case <- *) - intro H; rewrite H; simpl; reflexivity. + - induction l as [|x l]; trivial. + intros H. specialize (H x). simpl in H. + destruct eq_dec as [_|NEQ]; [discriminate|now elim NEQ]. + - now intros ->. Qed. Lemma count_occ_nil : forall (x : A), count_occ [] x = 0. @@ -749,22 +745,11 @@ Section ListOps. Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}. - Lemma list_eq_dec : - forall l l':list A, {l = l'} + {l <> l'}. - Proof. - induction l as [| x l IHl]; destruct l' as [| y l']. - left; trivial. - right; apply nil_cons. - right; unfold not; intro HF; apply (nil_cons (sym_eq HF)). - destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; - try (right; unfold not; intro HF; injection HF; intros; contradiction). - rewrite xeqy; rewrite leql'; left; trivial. - Qed. - + Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}. + Proof. decide equality. Defined. End ListOps. - (***************************************************) (** * Applying functions to the elements of a list *) (***************************************************) @@ -1643,7 +1628,7 @@ Proof. exact Forall2_nil. Qed. Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l', Forall2 R (l1 ++ l2) l' -> - exists l1', exists l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'. + exists l1' l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'. Proof. induction l1; intros. exists [], l'; auto. @@ -1654,7 +1639,7 @@ Qed. Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l, Forall2 R l (l1' ++ l2') -> - exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2. + exists l1 l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2. Proof. induction l1'; intros. exists [], l; auto. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 56df3f9c..b846c48d 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListSet.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** A Library for finite sets, implemented as lists *) (** List is loaded, but not exported. @@ -87,15 +85,15 @@ Section first_definitions. Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}. Proof. - unfold set_In in |- *. + unfold set_In. (*** Realizer set_mem. Program_all. ***) simple induction x. auto. intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq. - rewrite eq; simpl in |- *; auto with datatypes. + rewrite eq; simpl; auto with datatypes. elim Ha0. auto with datatypes. - right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2]; + right; simpl; unfold not; intros [Hc1| Hc2]; auto with datatypes. Qed. @@ -104,7 +102,7 @@ Section first_definitions. (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z). Proof. - simple induction x; simpl in |- *; intros. + simple induction x; simpl; intros. assumption. elim (Aeq_dec a a0); auto with datatypes. Qed. @@ -115,11 +113,11 @@ Section first_definitions. (~ set_In a x -> P z) -> P (if set_mem a x then y else z). Proof. - simple induction x; simpl in |- *; intros. - apply H0; red in |- *; trivial. + simple induction x; simpl; intros. + apply H0; red; trivial. case (Aeq_dec a a0); auto with datatypes. intro; apply H; intros; auto. - apply H1; red in |- *; intro. + apply H1; red; intro. case H3; auto. Qed. @@ -127,7 +125,7 @@ Section first_definitions. Lemma set_mem_correct1 : forall (a:A) (x:set), set_mem a x = true -> set_In a x. Proof. - simple induction x; simpl in |- *. + simple induction x; simpl. discriminate. intros a0 l; elim (Aeq_dec a a0); auto with datatypes. Qed. @@ -135,7 +133,7 @@ Section first_definitions. Lemma set_mem_correct2 : forall (a:A) (x:set), set_In a x -> set_mem a x = true. Proof. - simple induction x; simpl in |- *. + simple induction x; simpl. intro Ha; elim Ha. intros a0 l; elim (Aeq_dec a a0); auto with datatypes. intros H1 H2 [H3| H4]. @@ -146,17 +144,17 @@ Section first_definitions. Lemma set_mem_complete1 : forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x. Proof. - simple induction x; simpl in |- *. + simple induction x; simpl. tauto. intros a0 l; elim (Aeq_dec a a0). intros; discriminate H0. - unfold not in |- *; intros; elim H1; auto with datatypes. + unfold not; intros; elim H1; auto with datatypes. Qed. Lemma set_mem_complete2 : forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false. Proof. - simple induction x; simpl in |- *. + simple induction x; simpl. tauto. intros a0 l; elim (Aeq_dec a a0). intros; elim H0; auto with datatypes. @@ -167,7 +165,7 @@ Section first_definitions. forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x). Proof. - unfold set_In in |- *; simple induction x; simpl in |- *. + unfold set_In; simple induction x; simpl. auto with datatypes. intros a0 l H [Ha0a| Hal]. elim (Aeq_dec b a0); left; assumption. @@ -178,11 +176,11 @@ Section first_definitions. forall (a b:A) (x:set), a = b -> set_In a (set_add b x). Proof. - unfold set_In in |- *; simple induction x; simpl in |- *. + unfold set_In; simple induction x; simpl. auto with datatypes. intros a0 l H Hab. elim (Aeq_dec b a0); - [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *; + [ rewrite Hab; intro Hba0; rewrite Hba0; simpl; auto with datatypes | auto with datatypes ]. Qed. @@ -200,13 +198,13 @@ Section first_definitions. forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x. Proof. - unfold set_In in |- *. + unfold set_In. simple induction x. - simpl in |- *; intros [H1| H2]; auto with datatypes. - simpl in |- *; do 3 intro. + simpl; intros [H1| H2]; auto with datatypes. + simpl; do 3 intro. elim (Aeq_dec b a0). - simpl in |- *; tauto. - simpl in |- *; intros; elim H0. + simpl; tauto. + simpl; intros; elim H0. trivial with datatypes. tauto. tauto. @@ -222,7 +220,7 @@ Section first_definitions. Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set. Proof. - simple induction x; simpl in |- *. + simple induction x; simpl. discriminate. intros; elim (Aeq_dec a a0); intros; discriminate. Qed. @@ -231,13 +229,13 @@ Section first_definitions. Lemma set_union_intro1 : forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). Proof. - simple induction y; simpl in |- *; auto with datatypes. + simple induction y; simpl; auto with datatypes. Qed. Lemma set_union_intro2 : forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y). Proof. - simple induction y; simpl in |- *. + simple induction y; simpl. tauto. intros; elim H0; auto with datatypes. Qed. @@ -255,7 +253,7 @@ Section first_definitions. forall (a:A) (x y:set), set_In a (set_union x y) -> set_In a x \/ set_In a y. Proof. - simple induction y; simpl in |- *. + simple induction y; simpl. auto with datatypes. intros. generalize (set_add_elim _ _ _ H0). @@ -282,11 +280,11 @@ Section first_definitions. Proof. simple induction x. auto with datatypes. - simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy. - simpl in |- *; rewrite Ha0a. + simpl; intros a0 l Hrec y [Ha0a| Hal] Hy. + simpl; rewrite Ha0a. generalize (set_mem_correct1 a y). generalize (set_mem_complete1 a y). - elim (set_mem a y); simpl in |- *; intros. + elim (set_mem a y); simpl; intros. auto with datatypes. absurd (set_In a y); auto with datatypes. elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ]. @@ -297,9 +295,9 @@ Section first_definitions. Proof. simple induction x. auto with datatypes. - simpl in |- *; intros a0 l Hrec y. + simpl; intros a0 l Hrec y. generalize (set_mem_correct1 a0 y). - elim (set_mem a0 y); simpl in |- *; intros. + elim (set_mem a0 y); simpl; intros. elim H0; eauto with datatypes. eauto with datatypes. Qed. @@ -308,10 +306,10 @@ Section first_definitions. forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y. Proof. simple induction x. - simpl in |- *; tauto. - simpl in |- *; intros a0 l Hrec y. + simpl; tauto. + simpl; intros a0 l Hrec y. generalize (set_mem_correct1 a0 y). - elim (set_mem a0 y); simpl in |- *; intros. + elim (set_mem a0 y); simpl; intros. elim H0; [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ]. eauto with datatypes. @@ -331,8 +329,8 @@ Section first_definitions. set_In a x -> ~ set_In a y -> set_In a (set_diff x y). Proof. simple induction x. - simpl in |- *; tauto. - simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay. + simpl; tauto. + simpl; intros a0 l Hrec y [Ha0a| Hal] Hay. rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay). elim (set_mem a y); [ intro Habs; discriminate Habs | auto with datatypes ]. @@ -343,8 +341,8 @@ Section first_definitions. forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x. Proof. simple induction x. - simpl in |- *; tauto. - simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y). + simpl; tauto. + simpl; intros a0 l Hrec y; elim (set_mem a0 y). eauto with datatypes. intro; generalize (set_add_elim _ _ _ H). intros [H1| H2]; eauto with datatypes. @@ -352,7 +350,7 @@ Section first_definitions. Lemma set_diff_elim2 : forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y. - intros a x y; elim x; simpl in |- *. + intros a x y; elim x; simpl. intros; contradiction. intros a0 l Hrec. apply set_mem_ind2; auto. @@ -361,7 +359,7 @@ Section first_definitions. Qed. Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x). - red in |- *; intros a x H. + red; intros a x H. apply (set_diff_elim2 _ _ _ H). apply (set_diff_elim1 _ _ _ H). Qed. diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index 08669499..74336555 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListTactics.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import BinPos. Require Import List. @@ -62,7 +60,7 @@ Ltac Find_at a l := match l with | nil => fail 100 "anomaly: Find_at" | a :: _ => eval compute in n - | _ :: ?l => find (Psucc n) l + | _ :: ?l => find (Pos.succ n) l end in find 1%positive l. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index ec31f37d..0fd1693e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -6,10 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: SetoidList.v 12919 2010-04-10 16:30:44Z herbelin $ *) - Require Export List. -Require Export Sorting. +Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. @@ -82,6 +80,10 @@ Qed. Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. +Lemma incl_nil l : inclA nil l. +Proof. intro. intros. inversion H. Qed. +Hint Resolve incl_nil : list. + (** lists with same elements modulo [eqA] at the same place *) Inductive eqlistA : list A -> list A -> Prop := @@ -159,8 +161,7 @@ Qed. Hint Resolve In_InA. Lemma InA_split : forall l x, InA x l -> - exists l1, exists y, exists l2, - eqA x y /\ l = l1++y::l2. + exists l1 y l2, eqA x y /\ l = l1++y::l2. Proof. induction l; intros; inv. exists (@nil A); exists a; exists l; auto. @@ -198,7 +199,29 @@ Proof. rewrite <- In_rev; auto. Qed. +(** Some more facts about InA *) + +Lemma InA_singleton x y : InA x (y::nil) <-> eqA x y. +Proof. + rewrite InA_cons, InA_nil; tauto. +Qed. + +Lemma InA_double_head x y l : + InA x (y :: y :: l) <-> InA x (y :: l). +Proof. + rewrite !InA_cons; tauto. +Qed. + +Lemma InA_permute_heads x y z l : + InA x (y :: z :: l) <-> InA x (z :: y :: l). +Proof. + rewrite !InA_cons; tauto. +Qed. +Lemma InA_app_idem x l : InA x (l ++ l) <-> InA x l. +Proof. + rewrite InA_app_iff; tauto. +Qed. Section NoDupA. @@ -269,7 +292,56 @@ Proof. eapply NoDupA_split; eauto. Qed. -Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> +Lemma NoDupA_singleton x : NoDupA (x::nil). +Proof. + repeat constructor. inversion 1. +Qed. + +End NoDupA. + +Section EquivlistA. + +Global Instance equivlistA_cons_proper: + Proper (eqA ==> equivlistA ==> equivlistA) (@cons A). +Proof. + intros ? ? E1 ? ? E2 ?; now rewrite !InA_cons, E1, E2. +Qed. + +Global Instance equivlistA_app_proper: + Proper (equivlistA ==> equivlistA ==> equivlistA) (@app A). +Proof. + intros ? ? E1 ? ? E2 ?. now rewrite !InA_app_iff, E1, E2. +Qed. + +Lemma equivlistA_cons_nil x l : ~ equivlistA (x :: l) nil. +Proof. + intros E. now eapply InA_nil, E, InA_cons_hd. +Qed. + +Lemma equivlistA_nil_eq l : equivlistA l nil -> l = nil. +Proof. + destruct l. + - trivial. + - intros H. now apply equivlistA_cons_nil in H. +Qed. + +Lemma equivlistA_double_head x l : equivlistA (x :: x :: l) (x :: l). +Proof. + intro. apply InA_double_head. +Qed. + +Lemma equivlistA_permute_heads x y l : + equivlistA (x :: y :: l) (y :: x :: l). +Proof. + intro. apply InA_permute_heads. +Qed. + +Lemma equivlistA_app_idem l : equivlistA (l ++ l) l. +Proof. + intro. apply InA_app_idem. +Qed. + +Lemma equivlistA_NoDupA_split 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. @@ -289,9 +361,7 @@ Proof. rewrite <-H,<-EQN; auto. Qed. -End NoDupA. - - +End EquivlistA. Section Fold. @@ -587,10 +657,9 @@ Proof. Qed. (** For compatibility, can be deduced from [InfA_compat] *) -Lemma InfA_eqA : - forall l x y, eqA x y -> InfA y l -> InfA x l. +Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. Proof. - intros l x y H; rewrite H; auto. + intros H; now rewrite H. Qed. Hint Immediate InfA_ltA InfA_eqA. @@ -747,7 +816,7 @@ rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. -Implicit Arguments eq [ [A] ]. +Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. @@ -784,9 +853,11 @@ Qed. End Filter. End Type_with_equality. - Hint Constructors InA eqlistA NoDupA sort lelistA. +Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _. +Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _. + Section Find. Variable A B : Type. @@ -837,7 +908,6 @@ Qed. End Find. - (** Compatibility aliases. [Proper] is rather to be used directly now.*) Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) := @@ -851,4 +921,3 @@ Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) := Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) := Proper (eqA==>eqB==>eqB) f. - diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v new file mode 100644 index 00000000..b0657b63 --- /dev/null +++ b/theories/Lists/SetoidPermutation.v @@ -0,0 +1,125 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +Require Import SetoidList. + +Set Implicit Arguments. +Unset Strict Implicit. + +(** Permutations of list modulo a setoid equality. *) + +(** Contribution by Robbert Krebbers (Nijmegen University). *) + +Section Permutation. +Context {A : Type} (eqA : relation A) (e : Equivalence eqA). + +Inductive PermutationA : list A -> list A -> Prop := + | permA_nil: PermutationA nil nil + | permA_skip x₁ x₂ l₁ l₂ : + eqA x₁ x₂ -> PermutationA l₁ l₂ -> PermutationA (x₁ :: l₁) (x₂ :: l₂) + | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l) + | permA_trans l₁ l₂ l₃ : + PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃. +Local Hint Constructors PermutationA. + +Global Instance: Equivalence PermutationA. +Proof. + constructor. + - intro l. induction l; intuition. + - intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition. + - exact permA_trans. +Qed. + +Global Instance PermutationA_cons : + Proper (eqA ==> PermutationA ==> PermutationA) (@cons A). +Proof. + repeat intro. now apply permA_skip. +Qed. + +Lemma PermutationA_app_head l₁ l₂ l : + PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂). +Proof. + induction l; trivial; intros. apply permA_skip; intuition. +Qed. + +Global Instance PermutationA_app : + Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A). +Proof. + intros l₁ l₂ Pl k₁ k₂ Pk. + induction Pl. + - easy. + - now apply permA_skip. + - etransitivity. + * rewrite <-!app_comm_cons. now apply permA_swap. + * rewrite !app_comm_cons. now apply PermutationA_app_head. + - do 2 (etransitivity; try eassumption). + apply PermutationA_app_head. now symmetry. +Qed. + +Lemma PermutationA_app_tail l₁ l₂ l : + PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l). +Proof. + intros E. now rewrite E. +Qed. + +Lemma PermutationA_cons_append l x : + PermutationA (x :: l) (l ++ x :: nil). +Proof. + induction l. + - easy. + - simpl. rewrite <-IHl. intuition. +Qed. + +Lemma PermutationA_app_comm l₁ l₂ : + PermutationA (l₁ ++ l₂) (l₂ ++ l₁). +Proof. + induction l₁. + - now rewrite app_nil_r. + - rewrite <-app_comm_cons, IHl₁, app_comm_cons. + now rewrite PermutationA_cons_append, <-app_assoc. +Qed. + +Lemma PermutationA_cons_app l l₁ l₂ x : + PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂). +Proof. + intros E. rewrite E. + now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc. +Qed. + +Lemma PermutationA_middle l₁ l₂ x : + PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂). +Proof. + now apply PermutationA_cons_app. +Qed. + +Lemma PermutationA_equivlistA l₁ l₂ : + PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂. +Proof. + induction 1. + - reflexivity. + - now apply equivlistA_cons_proper. + - now apply equivlistA_permute_heads. + - etransitivity; eassumption. +Qed. + +Lemma NoDupA_equivlistA_PermutationA l₁ l₂ : + NoDupA eqA l₁ -> NoDupA eqA l₂ -> + equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂. +Proof. + intros Pl₁. revert l₂. induction Pl₁ as [|x l₁ E1]. + - intros l₂ _ H₂. symmetry in H₂. now rewrite (equivlistA_nil_eq eqA). + - intros l₂ Pl₂ E2. + destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]]. + { rewrite <-E2. intuition. } + subst. transitivity (y :: l₁); [intuition |]. + apply PermutationA_cons_app, IHPl₁. + now apply NoDupA_split with y. + apply equivlistA_NoDupA_split with x y; intuition. +Qed. + +End Permutation. diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index 1ab4fa9d..67882cde 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,10 +32,10 @@ Fixpoint memo_get (n:nat) (l:Stream A) : A := 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 _)). +{ induction n as [| n Hrec]; try (intros m; reflexivity). 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_Sm; auto. } +intros n; transitivity (f (n + 0)); try exact (F1 n 0). rewrite <- plus_n_O; auto. Qed. @@ -57,11 +57,10 @@ Definition imemo_list := let f0 := f 0 in 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. +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 (eq_sym (Hg_correct m))). + simpl; intros m; rewrite <- Hg_correct, Hrec, <- plus_n_Sm; auto. } +destruct n as [| n]; try reflexivity. unfold imemo_list; simpl; rewrite F1. rewrite <- plus_n_O; auto. Qed. @@ -82,7 +81,7 @@ Inductive memo_val: Type := Fixpoint is_eq (n m : nat) : {n = m} + {True} := match n, m return {n = m} + {True} with - | 0, 0 =>left True (refl_equal 0) + | 0, 0 =>left True (eq_refl 0) | 0, S m1 => right (0 = S m1) I | S n1, 0 => right (S n1 = 0) I | S n1, S m1 => @@ -98,7 +97,7 @@ match v with 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 + | eq_refl => fun v1 : A n => v1 end | right _ => fun _ : A m => f n end x @@ -115,7 +114,7 @@ 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). +assert (e = eq_refl n). apply eq_proofs_unicity. induction x as [| x Hx]; destruct y as [| y]. left; auto. @@ -144,7 +143,7 @@ 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). +assert (e = eq_refl n). apply eq_proofs_unicity. induction x as [| x Hx]; destruct y as [| y]. left; auto. @@ -169,11 +168,11 @@ Open Scope Z_scope. Fixpoint tfact (n: nat) := match n with | O => 1 - | S n1 => Z_of_nat n * tfact n1 + | S n1 => Z.of_nat n * tfact n1 end. Definition lfact_list := - dimemo_list _ tfact (fun n z => (Z_of_nat (S n) * z)). + dimemo_list _ tfact (fun n z => (Z.of_nat (S n) * z)). Definition lfact n := dmemo_get _ tfact n lfact_list. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 02d17211..e1122cf9 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Streams.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. (** Streams *) @@ -51,21 +49,21 @@ Qed. Lemma tl_nth_tl : forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s). Proof. - simple induction n; simpl in |- *; auto. + simple induction n; simpl; auto. Qed. Hint Resolve tl_nth_tl: datatypes v62. Lemma Str_nth_tl_plus : forall (n m:nat) (s:Stream), Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s. -simple induction n; simpl in |- *; intros; auto with datatypes. +simple induction n; simpl; intros; auto with datatypes. rewrite <- H. rewrite tl_nth_tl; trivial with datatypes. Qed. Lemma Str_nth_plus : forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s. -intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus; +intros; unfold Str_nth; rewrite Str_nth_tl_plus; trivial with datatypes. Qed. @@ -91,7 +89,7 @@ Qed. Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1. coinduction Eq_sym. -case H; intros; symmetry in |- *; assumption. +case H; intros; symmetry ; assumption. case H; intros; assumption. Qed. @@ -112,10 +110,10 @@ Qed. Theorem eqst_ntheq : forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2. -unfold Str_nth in |- *; simple induction n. +unfold Str_nth; simple induction n. intros s1 s2 H; case H; trivial with datatypes. intros m hypind. -simpl in |- *. +simpl. intros s1 s2 H. apply hypind. case H; trivial with datatypes. diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v deleted file mode 100644 index 498a9dca..00000000 --- a/theories/Lists/TheoryList.v +++ /dev/null @@ -1,423 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: TheoryList.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(** Some programs and results about lists following CAML Manual *) - -Require Export List. -Set Implicit Arguments. - -Local Notation "[ ]" := nil (at level 0). -Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). - -Section Lists. - -Variable A : Type. - -(**********************) -(** The null function *) -(**********************) - -Definition Isnil (l:list A) : Prop := nil = l. - -Lemma Isnil_nil : Isnil nil. -Proof. -red in |- *; auto. -Qed. -Hint Resolve Isnil_nil. - -Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l). -Proof. -unfold Isnil in |- *. -intros; discriminate. -Qed. - -Hint Resolve Isnil_nil not_Isnil_cons. - -Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}. -Proof. -intro l; case l; auto. -(* -Realizer (fun l => match l with - | nil => true - | _ => false - end). -*) -Qed. - -(************************) -(** The Uncons function *) -(************************) - -Lemma Uncons : - forall l:list A, {a : A & {m : list A | a :: m = l}} + {Isnil l}. -Proof. -intro l; case l. -auto. -intros a m; intros; left; exists a; exists m; reflexivity. -(* -Realizer (fun l => match l with - | nil => error - | (cons a m) => value (a,m) - end). -*) -Qed. - -(********************************) -(** The head function *) -(********************************) - -Lemma Hd : - forall l:list A, {a : A | exists m : list A, a :: m = l} + {Isnil l}. -Proof. -intro l; case l. -auto. -intros a m; intros; left; exists a; exists m; reflexivity. -(* -Realizer (fun l => match l with - | nil => error - | (cons a m) => value a - end). -*) -Qed. - -Lemma Tl : - forall l:list A, - {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}. -Proof. -intro l; case l. -exists (nil (A:=A)); auto. -intros a m; intros; exists m; left; exists a; reflexivity. -(* -Realizer (fun l => match l with - | nil => nil - | (cons a m) => m - end). -*) -Qed. - -(****************************************) -(** Length of lists *) -(****************************************) - -(* length is defined in List *) -Fixpoint Length_l (l:list A) (n:nat) : nat := - match l with - | nil => n - | _ :: m => Length_l m (S n) - end. - -(* A tail recursive version *) -Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}. -Proof. -induction l as [| a m lrec]. -intro n; exists n; simpl in |- *; auto. -intro n; elim (lrec (S n)); simpl in |- *; intros. -exists x; transitivity (S (n + length m)); auto. -(* -Realizer Length_l. -*) -Qed. - -Lemma Length : forall l:list A, {m : nat | length l = m}. -Proof. -intro l. apply (Length_l_pf l 0). -(* -Realizer (fun l -> Length_l_pf l O). -*) -Qed. - -(*******************************) -(** Members of lists *) -(*******************************) -Inductive In_spec (a:A) : list A -> Prop := - | in_hd : forall l:list A, In_spec a (a :: l) - | in_tl : forall (l:list A) (b:A), In a l -> In_spec a (b :: l). -Hint Resolve in_hd in_tl. -Hint Unfold In. -Hint Resolve in_cons. - -Theorem In_In_spec : forall (a:A) (l:list A), In a l <-> In_spec a l. -split. -elim l; - [ intros; contradiction - | intros; elim H0; [ intros; rewrite H1; auto | auto ] ]. -intros; elim H; auto. -Qed. - -Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}. - -Fixpoint mem (a:A) (l:list A) : bool := - match l with - | nil => false - | b :: m => if eqA_dec a b then true else mem a m - end. - -Hint Unfold In. -Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}. -Proof. -induction l. -auto. -elim (eqA_dec a a0). -auto. -simpl in |- *. elim IHl; auto. -(* -Realizer mem. -*) -Qed. - -(*********************************) -(** Index of elements *) -(*********************************) - -Require Import Le. -Require Import Lt. - -Inductive nth_spec : list A -> nat -> A -> Prop := - | nth_spec_O : forall (a:A) (l:list A), nth_spec (a :: l) 1 a - | nth_spec_S : - forall (n:nat) (a b:A) (l:list A), - nth_spec l n a -> nth_spec (b :: l) (S n) a. -Hint Resolve nth_spec_O nth_spec_S. - -Inductive fst_nth_spec : list A -> nat -> A -> Prop := - | fst_nth_O : forall (a:A) (l:list A), fst_nth_spec (a :: l) 1 a - | fst_nth_S : - forall (n:nat) (a b:A) (l:list A), - a <> b -> fst_nth_spec l n a -> fst_nth_spec (b :: l) (S n) a. -Hint Resolve fst_nth_O fst_nth_S. - -Lemma fst_nth_nth : - forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a. -Proof. -induction 1; auto. -Qed. -Hint Immediate fst_nth_nth. - -Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n. -Proof. -induction 1; auto. -Qed. - -Lemma nth_le_length : - forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l. -Proof. -induction 1; simpl in |- *; auto with arith. -Qed. - -Fixpoint Nth_func (l:list A) (n:nat) : Exc A := - match l, n with - | a :: _, S O => value a - | _ :: l', S (S p) => Nth_func l' (S p) - | _, _ => error - end. - -Lemma Nth : - forall (l:list A) (n:nat), - {a : A | nth_spec l n a} + {n = 0 \/ length l < n}. -Proof. -induction l as [| a l IHl]. -intro n; case n; simpl in |- *; auto with arith. -intro n; destruct n as [| [| n1]]; simpl in |- *; auto. -left; exists a; auto. -destruct (IHl (S n1)) as [[b]| o]. -left; exists b; auto. -right; destruct o. -absurd (S n1 = 0); auto. -auto with arith. -(* -Realizer Nth_func. -*) -Qed. - -Lemma Item : - forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}. -Proof. -intros l n; case (Nth l (S n)); intro. -case s; intro a; left; exists a; auto. -right; case o; intro. -absurd (S n = 0); auto. -auto with arith. -Qed. - -Require Import Minus. -Require Import DecBool. - -Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat := - match l with - | nil => fun p => error - | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p)) - end. - -Lemma Index_p : - forall (a:A) (l:list A) (p:nat), - {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}. -Proof. -induction l as [| b m irec]. -auto. -intro p. -destruct (eqA_dec a b) as [e| e]. -left; exists p. -destruct e; elim minus_Sn_m; trivial; elim minus_n_n; auto with arith. -destruct (irec (S p)) as [[n H]| ]. -left; exists n; auto with arith. -elim minus_Sn_m; auto with arith. -apply lt_le_weak; apply lt_O_minus_lt; apply nth_lt_O with m a; - auto with arith. -auto. -Qed. - -Lemma Index : - forall (a:A) (l:list A), - {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}. - -Proof. -intros a l; case (Index_p a l 1); auto. -intros [n P]; left; exists n; auto. -rewrite (minus_n_O n); trivial. -(* -Realizer (fun a l -> Index_p a l (S O)). -*) -Qed. - -Section Find_sec. -Variables R P : A -> Prop. - -Inductive InR : list A -> Prop := - | inR_hd : forall (a:A) (l:list A), R a -> InR (a :: l) - | inR_tl : forall (a:A) (l:list A), InR l -> InR (a :: l). -Hint Resolve inR_hd inR_tl. - -Definition InR_inv (l:list A) := - match l with - | nil => False - | b :: m => R b \/ InR m - end. - -Lemma InR_INV : forall l:list A, InR l -> InR_inv l. -Proof. -induction 1; simpl in |- *; auto. -Qed. - -Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l. -Proof. -intros a l H; exact (InR_INV H). -Qed. - -Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m). -Proof. -intros l m [| ]. -induction 1; simpl in |- *; auto. -intro. induction l; simpl in |- *; auto. -Qed. - -Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m. -Proof. -intros l m; elim l; simpl in |- *; auto. -intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto. -intros; elim Hrec; auto. -Qed. - -Hypothesis RS_dec : forall a:A, {R a} + {P a}. - -Fixpoint find (l:list A) : Exc A := - match l with - | nil => error - | a :: m => ifdec (RS_dec a) (value a) (find m) - end. - -Lemma Find : forall l:list A, {a : A | In a l & R a} + {AllS P l}. -Proof. -induction l as [| a m [[b H1 H2]| H]]; auto. -left; exists b; auto. -destruct (RS_dec a). -left; exists a; auto. -auto. -(* -Realizer find. -*) -Qed. - -Variable B : Type. -Variable T : A -> B -> Prop. - -Variable TS_dec : forall a:A, {c : B | T a c} + {P a}. - -Fixpoint try_find (l:list A) : Exc B := - match l with - | nil => error - | a :: l1 => - match TS_dec a with - | inleft (exist c _) => value c - | inright _ => try_find l1 - end - end. - -Lemma Try_find : - forall l:list A, {c : B | exists2 a : A, In a l & T a c} + {AllS P l}. -Proof. -induction l as [| a m [[b H1]| H]]. -auto. -left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto. -destruct (TS_dec a) as [[c H1]| ]. -left; exists c. -exists a; auto. -auto. -(* -Realizer try_find. -*) -Qed. - -End Find_sec. - -Section Assoc_sec. - -Variable B : Type. -Fixpoint assoc (a:A) (l:list (A * B)) : - Exc B := - match l with - | nil => error - | (a', b) :: m => ifdec (eqA_dec a a') (value b) (assoc a m) - end. - -Inductive AllS_assoc (P:A -> Prop) : list (A * B) -> Prop := - | allS_assoc_nil : AllS_assoc P nil - | allS_assoc_cons : - forall (a:A) (b:B) (l:list (A * B)), - P a -> AllS_assoc P l -> AllS_assoc P ((a, b) :: l). - -Hint Resolve allS_assoc_nil allS_assoc_cons. - -(* The specification seems too weak: it is enough to return b if the - list has at least an element (a,b); probably the intention is to have - the specification - - (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}. -*) - -Lemma Assoc : - forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}. -Proof. -induction l as [| [a' b] m assrec]. auto. -destruct (eqA_dec a a'). -left; exact b. -destruct assrec as [b'| ]. -left; exact b'. -right; auto. -(* -Realizer assoc. -*) -Qed. - -End Assoc_sec. - -End Lists. - -Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons : datatypes. -Hint Immediate fst_nth_nth: datatypes. diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex index 0051e2c2..d372de8e 100755 --- a/theories/Lists/intro.tex +++ b/theories/Lists/intro.tex @@ -13,12 +13,8 @@ This library includes the following files: \item {\tt ListSet.v} contains definitions and properties of finite sets, implemented as lists. -\item {\tt TheoryList.v} contains complementary results on lists. Here - a more theoretic point of view is assumed : one extracts functions - from propositions, rather than defining functions and then prove them. - \item {\tt Streams.v} defines the type of infinite lists (streams). It is a - coinductive type. Basic facts are stated and proved. The streams are + co-inductive type. Basic facts are stated and proved. The streams are also polymorphic. \end{itemize} diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget index d2a31367..04994f59 100644 --- a/theories/Lists/vo.itarget +++ b/theories/Lists/vo.itarget @@ -2,6 +2,6 @@ ListSet.vo ListTactics.vo List.vo SetoidList.vo +SetoidPermutation.vo StreamMemo.vo Streams.vo -TheoryList.vo |