summaryrefslogtreecommitdiff
path: root/theories/Lists
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/Lists
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Lists')
-rw-r--r--theories/Lists/List.v28
-rw-r--r--theories/Lists/ListTactics.v69
2 files changed, 89 insertions, 8 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index df2b17e0..c80d0b15 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: List.v 9035 2006-07-09 15:42:09Z herbelin $ i*)
+ (*i $Id: List.v 9290 2006-10-26 19:20:42Z herbelin $ i*)
Require Import Le Gt Minus Min Bool.
Require Import Setoid.
@@ -39,6 +39,12 @@ Section Lists.
| x :: _ => value x
end.
+ Definition hd (default:A) (l:list) :=
+ match l with
+ | nil => default
+ | x :: _ => x
+ end.
+
Definition tail (l:list) : list :=
match l with
| nil => nil
@@ -670,21 +676,27 @@ Section ListOps.
(** An alternative tail-recursive definition for reverse *)
- Fixpoint rev_acc (l l': list A) {struct l} : list A :=
+ Fixpoint rev_append (l l': list A) {struct l} : list A :=
match l with
| nil => l'
- | a::l => rev_acc l (a::l')
+ | a::l => rev_append l (a::l')
end.
- Lemma rev_acc_rev : forall l l', rev_acc l l' = rev l ++ l'.
+ Definition rev' l : list A := rev_append l nil.
+
+ Notation rev_acc := rev_append (only parsing).
+
+ Lemma rev_append_rev : forall l l', rev_acc l l' = rev l ++ l'.
Proof.
induction l; simpl; auto; intros.
rewrite <- ass_app; firstorder.
Qed.
- Lemma rev_alt : forall l, rev l = rev_acc l nil.
+ Notation rev_acc_rev := rev_append_rev (only parsing).
+
+ Lemma rev_alt : forall l, rev l = rev_append l nil.
Proof.
- intros; rewrite rev_acc_rev.
+ intros; rewrite rev_append_rev.
apply app_nil_end.
Qed.
@@ -1336,14 +1348,14 @@ End Fold_Right_Recursor.
rewrite IHl; simpl; auto.
Qed.
- Lemma split_lenght_l : forall (l:list (A*B)),
+ Lemma split_length_l : forall (l:list (A*B)),
length (fst (split l)) = length l.
Proof.
induction l; simpl; auto.
destruct a; destruct (split l); simpl; auto.
Qed.
- Lemma split_lenght_r : forall (l:list (A*B)),
+ Lemma split_length_r : forall (l:list (A*B)),
length (snd (split l)) = length l.
Proof.
induction l; simpl; auto.
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
new file mode 100644
index 00000000..a3b4e647
--- /dev/null
+++ b/theories/Lists/ListTactics.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(* 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: ListTactics.v 9290 2006-10-26 19:20:42Z herbelin $ i*)
+
+Require Import BinPos.
+Require Import List.
+
+Ltac list_fold_right fcons fnil l :=
+ match l with
+ | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl)
+ | nil => fnil
+ end.
+
+Ltac list_fold_left fcons fnil l :=
+ match l with
+ | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
+ | nil => fnil
+ end.
+
+Ltac list_iter f l :=
+ match l with
+ | (cons ?x ?tl) => f x; list_iter f tl
+ | nil => idtac
+ end.
+
+Ltac list_iter_gen seq f l :=
+ match l with
+ | (cons ?x ?tl) =>
+ let t1 _ := f x in
+ let t2 _ := list_iter_gen seq f tl in
+ seq t1 t2
+ | nil => idtac
+ end.
+
+Ltac AddFvTail a l :=
+ match l with
+ | nil => constr:(cons a l)
+ | (cons a _) => l
+ | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l')
+ end.
+
+Ltac Find_at a l :=
+ let rec find n l :=
+ match l with
+ | nil => fail 100 "anomaly: Find_at"
+ | (cons a _) => eval compute in n
+ | (cons _ ?l) => find (Psucc n) l
+ end
+ in find 1%positive l.
+
+Ltac check_is_list t :=
+ match t with
+ | cons _ ?l => check_is_list l
+ | nil => idtac
+ | _ => fail 100 "anomaly: failed to build a canonical list"
+ end.
+
+Ltac check_fv l :=
+ check_is_list l;
+ match type of l with
+ | list _ => idtac
+ | _ => fail 100 "anomaly: built an ill-typed list"
+ end.