Imported Upstream version 8.1~gammaupstream/8.1.gamma

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.