Déplacement des propriétés générales de BinList dans List et des tactiques de

BinList dans un nouveau ListTactics.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9290 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 101 insertions, 86 deletions

diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v
index c3f5bdc9ad..0d0fe5a444 100644
--- a/contrib/setoid_ring/BinList.v
+++ b/contrib/setoid_ring/BinList.v
@@ -9,14 +9,13 @@
 Set Implicit Arguments.
 Require Import BinPos.
 Require Export List.
+Require Export ListTactics.
 Open Scope positive_scope.
 
-Section LIST.
+Section MakeBinList.
  Variable A : Type.
  Variable default : A.
 
- Definition hd l := match l with hd :: _ => hd | _ => default end. 
-
  Fixpoint jump (p:positive) (l:list A) {struct p} : list A :=
   match p with
   | xH => tail l
@@ -26,19 +25,11 @@ Section LIST.
 
  Fixpoint nth (p:positive) (l:list A) {struct p} : A:=
   match p with
-  | xH => hd l
+  | xH => hd default l
   | xO p => nth p (jump p l)
   | xI p => nth p (jump p (tail l))
   end. 
 
- Fixpoint rev_append (rev l : list A) {struct l} : list A :=
-  match l with
-  | nil => rev
-  | (cons h t) => rev_append (cons h rev) t 
-  end.
- 
- Definition rev l : list A := rev_append nil l.
-
  Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
  Proof. 
   induction j;simpl;intros.
@@ -79,7 +70,7 @@ Section LIST.
  Qed.
 
  
- Lemma nth_jump : forall p l, nth p (tail l) = hd (jump p l).
+ Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l).
  Proof.
   induction p;simpl;intros.
   rewrite <-jump_tl;rewrite IHp;trivial.
@@ -97,61 +88,4 @@ Section LIST.
   trivial.
  Qed.
 
-End 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.
+End MakeBinList.
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index 2be6f5fc75..989ec5ce2b 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -1048,8 +1048,8 @@ Section MakeRingPol.
  Fixpoint add_mult_dev (rP:R) (P:Pol) (fv lm:list R) {struct P} : R :=
   (* rP + P@l * lm *)
   match P with
-  | Pc c => if c ?=! cI then mkadd_mult rP (rev lm) 
-    else mkadd_mult rP (cons [c] (rev lm))
+  | Pc c => if c ?=! cI then mkadd_mult rP (rev' lm) 
+    else mkadd_mult rP (cons [c] (rev' lm))
   | Pinj j Q => add_mult_dev rP Q (jump j fv) lm
   | PX P i Q => 
      let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in
@@ -1065,7 +1065,7 @@ Section MakeRingPol.
  Fixpoint mult_dev (P:Pol) (fv lm : list R) {struct P} : R :=
   (* P@l * lm *)							      
   match P with
-  | Pc c => if c ?=! cI then mkmult1 (rev lm) else mkmult [c] (rev lm)
+  | Pc c => if c ?=! cI then mkmult1 (rev' lm) else mkmult [c] (rev' lm)
   | Pinj j Q => mult_dev Q (jump j fv) lm
   | PX P i Q => 
      let rP := mult_dev P fv (powl i (hd 0 fv) lm) in
@@ -1099,7 +1099,7 @@ Section MakeRingPol.
  Qed.
 
  Lemma mkmult_rev_append : forall lm l r,
-  mkmult r (rev_append l lm) == mkmult (mkmult r l) lm.
+  mkmult r (rev_append lm l) == mkmult (mkmult r l) lm.
  Proof.
  induction lm; simpl in |- *; intros.
  rrefl.
@@ -1109,11 +1109,11 @@ Section MakeRingPol.
  Qed.
 
  Lemma powl_mkmult_rev : forall p r x lm,
-  mkmult r (rev (powl p x lm)) == mkmult (pow x p * r) (rev lm).
+  mkmult r (rev' (powl p x lm)) == mkmult (pow x p * r) (rev' lm).
  Proof.
   induction p;simpl;intros.
   repeat rewrite IHp.
-  unfold rev;simpl.
+  unfold rev';simpl.
   repeat rewrite mkmult_rev_append.
   simpl.
   setoid_replace (pow x p * (pow x p * r) * x) 
@@ -1122,18 +1122,18 @@ Section MakeRingPol.
   repeat rewrite IHp.
   setoid_replace (pow x p * (pow x p * r) ) 
     with (pow x p * pow x p * r);Esimpl.
-  unfold rev;simpl. repeat rewrite mkmult_rev_append;simpl.
+  unfold rev';simpl. repeat rewrite mkmult_rev_append;simpl.
   rewrite (ARmul_sym ARth);rrefl.
  Qed.
 
  Lemma Pphi_add_mult_dev : forall P rP fv lm, 
-    rP + P@fv * mkmult1 (rev lm) == add_mult_dev rP P fv lm.
+    rP + P@fv * mkmult1 (rev' lm) == add_mult_dev rP P fv lm.
  Proof.
   induction P;simpl;intros.
   assert (H := (morph_eq CRmorph) c cI).
    destruct (c ?=! cI).
     rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl.
-    destruct (rev lm);Esimpl;rrefl.
+    destruct (rev' lm);Esimpl;rrefl.
     rewrite mkmult1_mkmult;rrefl.
    apply IHP.
    replace (match P3 with
@@ -1156,7 +1156,7 @@ Section MakeRingPol.
  Qed.
                                      
  Lemma Pphi_mult_dev : forall P fv lm,
-	 P@fv * mkmult1 (rev lm) == mult_dev P fv lm.
+	 P@fv * mkmult1 (rev' lm) == mult_dev P fv lm.
  Proof.
   induction P;simpl;intros.
    assert (H := (morph_eq CRmorph) c cI).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index cd6ce35cf7..2232d084ee 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -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.
 
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
new file mode 100644
index 0000000000..961101d65c
--- /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$ 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.