improved simpl

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

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 8d32b1d9f..b4de4932e 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -21,4 +21,27 @@ with copy_of_compute_size_tree (t:tree) : nat :=
 Eval simpl in (copy_of_compute_size_forest leaf).
 
 
+(* Another interesting case: Hrec has to occurrences: one cannot be folded
+   back to f while the second can. *)
+Parameter g : (nat->nat)->nat->nat->nat.
 
+Definition f (n n':nat) :=
+  nat_rec (fun _ => nat -> nat)
+    (fun x => x)
+    (fun k Hrec => g Hrec (Hrec k))
+    n n'.
+
+Goal forall a b, f (S a) b = b.
+intros.
+simpl.
+admit.
+Qed. (* Qed will fail if simpl performs eta-expansion *)
+
+(* Yet another example. *)
+
+Require Import List.
+
+Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i.
+simpl.
+admit.
+Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *)