tactique Gappa : mise en place

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

1 files changed, 20 insertions, 12 deletions

diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index 0284623c45..61de5d81cd 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -5,21 +5,29 @@ Require Import Classical.
 Dp_debug.
 Dp_timeout 3.
 
+(* Coq lists *)
 
-Inductive expr: Set := Some: expr -> expr -> expr | None: expr. 
-Parameter depth: expr -> expr -> nat. 
+Require Export List.
+Parameter nlist: list nat -> Prop.
 
-Fixpoint length (t: expr) : nat :=
-  match t with
-  | None => 0
-  | Some t1 t2 => depth t t1
-  end.
+ Goal forall l,  nlist l -> True.
+ intros. 
+ simplify.
 
-Goal forall e, length e = 0. 
-intros. 
-gwhy.
-ergo.
-Qed.
+(* user lists *)
+
+Inductive list (A:Set) : Set :=
+| nil : list A
+| cons: forall a:A, list A -> list A.
+
+Fixpoint app (A:Set) (l m:list A) {struct l} : list A :=
+match l with
+| nil => m
+| cons a l1 => cons A a (app A l1 m)
+end.
+
+Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True. 
+intros; ergo. 
 
 
 (* polymorphism *)