From 44c3d5dfdf11a3fc948006e7da2ca70e9cd77357 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 3 Dec 2008 18:13:19 +0000
Subject: improved simpl

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/simpl.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 8d32b1d9fa..b4de4932ec 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!) *)
-- 
cgit v1.2.3