diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-15 17:45:57 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-15 17:45:57 +0000 |
commit | 84592f2d128fcb322a59b40bb4ce6dc6e388943f (patch) | |
tree | bdd46f7bf82300fa2a343a0adae1a8539430d136 | |
parent | bb3aa221cec09dc997b0f7dac7bc4e1a1b51c744 (diff) |
Ajout de fonctions sur les listes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8632 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/Lists/MoreList.v | 45 | ||||
-rw-r--r-- | theories/Lists/SetoidList.v | 12 |
2 files changed, 56 insertions, 1 deletions
diff --git a/theories/Lists/MoreList.v b/theories/Lists/MoreList.v index fd264c423..0382d3066 100644 --- a/theories/Lists/MoreList.v +++ b/theories/Lists/MoreList.v @@ -419,7 +419,7 @@ Qed. (** [filter] *) -Fixpoint filter (l:list A) {struct l} : list A := +Fixpoint filter (l:list A) : list A := match l with | nil => nil | x :: l => if f x then x::(filter l) else filter l @@ -433,8 +433,51 @@ intros. case_eq (f a); intros; simpl; intuition congruence. Qed. +Fixpoint find (l:list A) : option A := + match l with + | nil => None + | x :: tl => if f x then Some x else find tl + end. + +Fixpoint partition (l:list A) {struct l} : list A * list A := + match l with + | nil => (nil, nil) + | x :: tl => let (g,d) := partition tl in + if f x then (x::g,d) else (g,x::d) + end. + End Bool. +Section Split. + +Fixpoint split (l:list (A*B)) : list A * list B := + match l with + | nil => (nil, nil) + | (x,y) :: tl => let (g,d) := split tl in (x::g, y::d) + end. + +(** [combine] stops on the shorter list *) +Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) := + match l,l' with + | x::tl, y::tl' => (x,y)::(combine tl tl') + | _, _ => nil + end. + +End Split. + +Section Remove. + +Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + +Fixpoint remove : (x : A) (l : list A){struct l} : list A := + match l with + | nil => nil + | y::tl => if (eq_dec x y) then remove tl else y::(remove tl) + end. + +End Remove. + + End MoreLists. Hint Rewrite diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 9d3581a5c..f43aeeddd 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -229,6 +229,18 @@ Proof. destruct l2; auto. Qed. +Section Remove. + +Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. + +Fixpoint removeA : (x : A) (l : list A){struct l} : list A := + match l with + | nil => nil + | y::tl => if (eqA_dec x y) then removeA tl else y::(removeA tl) + end. + +End Remove. + End Type_with_equality. Hint Constructors InA. |