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

2 files changed, 15 insertions, 81 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).