diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 48 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 78 | ||||
| -rw-r--r-- | theories/Lists/ListTactics.v | 4 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 90 | ||||
| -rw-r--r-- | theories/Lists/SetoidPermutation.v | 125 | ||||
| -rw-r--r-- | theories/Lists/StreamMemo.v | 29 | ||||
| -rw-r--r-- | theories/Lists/Streams.v | 14 | ||||
| -rw-r--r-- | theories/Lists/vo.itarget | 1 |
8 files changed, 281 insertions, 108 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ecadddbc..69475a6f 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) (************************************************************************) -Require Import Le Gt Minus Bool. +Require Import Le Gt Minus Bool Setoid. Set Implicit Arguments. @@ -546,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. @@ -754,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 *) (***************************************************) diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index d67baf57..b846c48d 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -85,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. @@ -102,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. @@ -113,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. @@ -125,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. @@ -133,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]. @@ -144,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. @@ -165,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. @@ -176,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. @@ -198,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. @@ -220,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. @@ -229,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. @@ -253,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). @@ -280,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 ]. @@ -295,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. @@ -306,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. @@ -329,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 ]. @@ -341,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. @@ -350,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. @@ -359,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 3343aa6f..74336555 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -60,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 97915055..0fd1693e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -7,7 +7,7 @@ (***********************************************************************) Require Export List. -Require Export Sorting. +Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. @@ -199,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. @@ -270,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. @@ -290,9 +361,7 @@ Proof. rewrite <-H,<-EQN; auto. Qed. -End NoDupA. - - +End EquivlistA. Section Fold. @@ -588,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. @@ -785,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. @@ -838,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) := @@ -852,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 45490c62..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-2010 *) +(* <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 7a6f38fc..e1122cf9 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -49,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. @@ -89,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. @@ -110,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/vo.itarget b/theories/Lists/vo.itarget index adcfba49..04994f59 100644 --- a/theories/Lists/vo.itarget +++ b/theories/Lists/vo.itarget @@ -2,5 +2,6 @@ ListSet.vo ListTactics.vo List.vo SetoidList.vo +SetoidPermutation.vo StreamMemo.vo Streams.vo |