Add support for recursive definitions to [Equations], deciding if a

definition is recursive or not based on occurence of a rec call in 
the body. Examples updated, enjoy!


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

1 files changed, 11 insertions, 18 deletions

diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index d08ce884c..3ef591959 100644
--- a/test-suite/success/Equations.v
+++ b/test-suite/success/Equations.v
@@ -6,7 +6,7 @@ Obligation Tactic := try equations.
 Equations neg (b : bool) : bool :=
 neg true := false ;
 neg false := true.
-
+ 
 Eval compute in neg.
 
 Require Import Coq.Lists.List.
@@ -27,20 +27,13 @@ Eval compute in (tail _ (cons 1 nil)).
 
 Equations app' {A} (l l' : list A) : (list A) :=
 app' A nil l := l ;
-app' A (cons a v) l := cons a (app v l).
+app' A (cons a v) l := cons a (app' A v l).
 
 Eval compute in app'.
 
-Fixpoint zip {A} (f : A -> A -> A) (l l' : list A) : list A :=
-  match l, l' with
-    | nil, nil => nil
-    | cons a v, cons b v' => cons (f a b) (zip f v v')
-    | _, _ => nil
-  end.
-
 Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) :=
 zip' A f nil nil := nil ;
-zip' A f (cons a v) (cons b w) := cons (f a b) (zip f v w) ;
+zip' A f (cons a v) (cons b w) := cons (f a b) (zip' _ f v w) ;
 zip' A f nil (cons b w) := nil ;
 zip' A f (cons a v) nil := nil.
 
@@ -50,7 +43,7 @@ Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] be
 
 Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) :=
 zip'' A f nil nil def := nil ;
-zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip f v w) ;
+zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' _ f v w def) ;
 zip'' A f nil (cons b w) def := def ;
 zip'' A f (cons a v) nil def := def.
 
@@ -64,15 +57,15 @@ Equations vhead A n (v : vector A (S n)) : A :=
 vhead A n (Vcons a v) := a.
 
 Eval compute in (vhead _ _ (Vcons 2 (Vcons 1 Vnil))).
-
-Axiom cheat : Π A, A.
+Eval compute in vhead.
 
 Equations vmap {A B} (f : A -> B) n (v : vector A n) : (vector B n) :=
 vmap A B f 0 Vnil := Vnil ;
-vmap A B f (S n) (Vcons a v) := Vcons (f a) (cheat _).
+vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap A B f n v).
 
 Eval compute in (vmap _ _ id _ (@Vnil nat)).
 Eval compute in (vmap _ _ id _ (@Vcons nat 2 _ Vnil)).
+Eval compute in vmap.
 
 Inductive fin : nat -> Set :=
 | fz : Π {n}, fin (S n)
@@ -86,13 +79,12 @@ Implicit Arguments finle [[n]].
 
 Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k :=
 trans (S n) fz j k leqz q := leqz ;
-trans (S n) (fs i) (fs j) fz (leqs p) q :=! q ;
-trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (cheat _).
+trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans _ _ _ _ p q).
 
 Lemma trans_eq1 n (j k : fin (S n)) q : trans (S n) fz j k leqz q = leqz.
 Proof. intros. simplify_equations ; reflexivity. Qed.
 
-Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (cheat _).
+Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans _ _ _ _ p q).
 Proof. intros. simplify_equations ; reflexivity. Qed.
 
 Section Image.
@@ -106,4 +98,5 @@ Section Image.
 
   Eval compute in inv.
 
-End Image.
\ No newline at end of file
+End Image.
+