1 files changed, 220 insertions, 0 deletions
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
new file mode 100644
index 00000000..52a57a0c
--- /dev/null
+++ b/contrib/dp/tests.v
@@ -0,0 +1,220 @@
+
+Require Import ZArith.
+Require Import Classical.
+
+(* First example with the 0 and the equality translated *)
+
+Goal 0 = 0.
+zenon.
+Qed.
+
+
+(* Examples in the Propositional Calculus
+   and theory of equality *)
+
+Parameter A C : Prop.
+
+Goal A -> A.
+zenon.
+Qed.
+
+
+Goal A -> (A \/ C).
+
+zenon.
+Qed.
+
+
+Parameter x y z : Z.
+
+Goal x = y -> y = z -> x = z.
+
+zenon.
+Qed.
+
+
+Goal ((((A -> C) -> A) -> A) -> C) -> C.
+
+zenon.
+Qed.
+
+
+(* Arithmetic *)
+Open Scope Z_scope.
+
+Goal 1 + 1 = 2.
+simplify.
+Qed.
+
+
+Goal 2*x + 10 = 18 -> x = 4.
+
+simplify.
+Qed.
+
+
+(* Universal quantifier *)
+
+Goal (forall (x y : Z), x = y) -> 0=1.
+try zenon.
+simplify.
+Qed.
+
+Goal forall (x: nat), (x + 0 = x)%nat.
+
+induction x0.
+zenon.
+zenon.
+Qed.
+
+
+(* No decision procedure can solve this problem 
+  Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a.
+*)
+
+
+(* Functions definitions *) 
+
+Definition fst (x y : Z) : Z := x.
+
+Goal forall (g : Z -> Z) (x y : Z), g (fst x y) = g x.
+
+simplify.
+Qed.
+
+
+(* Eta-expansion example *)
+
+Definition snd_of_3 (x y z : Z) : Z := y.
+
+Definition f : Z -> Z -> Z := snd_of_3 0.
+
+Goal forall (x y z z1 : Z), snd_of_3 x y z = f y z1.
+
+simplify.
+Qed.
+
+
+(* Inductive types definitions - call to incontrib/dp/jection function *)
+
+Inductive even : Z -> Prop :=
+| even_0 : even 0
+| even_plus2 : forall z : Z, even z -> even (z + 2).
+
+
+(* Simplify and Zenon can't prove this goal before the timeout
+   unlike CVC Lite *)
+
+Goal even 4.
+cvcl.
+Qed.
+
+
+Definition skip_z (z : Z) (n : nat) := n.
+
+Definition skip_z1 := skip_z.
+
+Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n.
+
+zenon.
+Qed.
+
+
+(* Axioms definitions and dp_hint *)
+
+Parameter add : nat -> nat -> nat.
+Axiom add_0 : forall (n : nat), add 0%nat n = n.
+Axiom add_S : forall (n1 n2 : nat), add (S n1) n2 = S (add n1 n2).
+
+Dp_hint add_0.
+Dp_hint add_S.
+
+(* Simplify can't prove this goal before the timeout 
+   unlike zenon *)
+
+Goal forall n : nat, add n 0 = n.
+
+induction n ; zenon.
+Qed.
+
+
+Definition pred (n : nat) : nat := match n with
+  | 0%nat => 0%nat
+  | S n' => n'
+end.
+
+Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat.
+
+zenon.
+Qed.
+
+
+Fixpoint plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0%nat => m
+  | S n' => S (plus n' m)
+end.
+
+Goal forall n : nat, plus n 0%nat = n.
+
+induction n; zenon.
+Qed.
+
+
+(* Mutually recursive functions *)
+
+Fixpoint even_b (n : nat) : bool := match n with
+  | O => true
+  | S m => odd_b m
+end
+with odd_b (n : nat) : bool := match n with
+  | O => false
+  | S m => even_b m
+end.
+
+Goal even_b (S (S O)) = true.
+
+zenon.
+Qed.
+
+
+(* sorts issues *)
+
+Parameter foo : Set.         
+Parameter ff : nat -> foo -> foo -> nat.
+Parameter g : foo -> foo.
+Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.
+zenon.
+Qed.
+
+
+
+(* abstractions *)
+
+Parameter poly_f : forall A:Set, A->A.
+
+Goal forall x:nat, poly_f nat x = poly_f nat x.
+zenon.
+Qed.
+
+
+
+(* Anonymous mutually recursive functions : no equations are produced
+
+Definition mrf :=
+  fix even2 (n : nat) : bool := match n with
+    | O => true
+    | S m => odd2 m
+  end
+  with odd2 (n : nat) : bool := match n with
+    | O => false
+    | S m => even2 m
+  end for even.
+
+   Thus this goal is unsolvable
+
+Goal mrf (S (S O)) = true.
+
+zenon.
+
+*)