Ajout d'un test sur EAuto

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

1 files changed, 31 insertions, 0 deletions

diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
new file mode 100644
index 0000000000..7681c8aa4e
--- /dev/null
+++ b/test-suite/success/eauto.v
@@ -0,0 +1,31 @@
+Require PolyList.
+
+Parameter in_list : (list nat*nat)->nat->Prop.
+Definition not_in_list : (list nat*nat)->nat->Prop
+	:= [l,n]~(in_list l n).
+
+(* Hints Unfold not_in_list. *)
+
+Axiom lem1 : (l1,l2:(list nat*nat))(n:nat)
+		(not_in_list (app l1 l2) n)->(not_in_list l1 n).
+
+Axiom lem2 : (l1,l2:(list nat*nat))(n:nat)
+		(not_in_list (app l1 l2) n)->(not_in_list l2 n).
+
+Axiom lem3 : (l:(list nat*nat))(n,p,q:nat)
+		(not_in_list (cons (p,q) l) n)->(not_in_list l n).
+
+Axiom lem4 : (l1,l2:(list nat*nat))(n:nat)
+	(not_in_list l1 n)->(not_in_list l2 n)->(not_in_list (app l1 l2) n).
+
+Hints Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal (l:(list nat*nat))(n,p,q:nat)
+		(not_in_list (cons (p,q) l) n)->(not_in_list l n).
+Intros.
+EAuto with essai.
+Save.
+
+
+
+