1 files changed, 300 insertions, 0 deletions
diff --git a/plugins/dp/tests.v b/plugins/dp/tests.v
new file mode 100644
index 00000000..dc85d2ee
--- /dev/null
+++ b/plugins/dp/tests.v
@@ -0,0 +1,300 @@
+
+Require Import ZArith.
+Require Import Classical.
+Require Export Reals.
+
+
+(* real numbers *)
+
+Lemma real_expr: (0 <= 9 * 4)%R.
+ergo.
+Qed.
+
+Lemma powerRZ_translation: (powerRZ 2 15 < powerRZ 2 17)%R.
+ergo.
+Qed.
+
+Dp_debug.
+Dp_timeout 3.
+
+(* module renamings *)
+
+Module M.
+  Parameter t : Set.
+End M.
+
+Lemma test_module_0 : forall x:M.t, x=x.
+ergo.
+Qed.
+
+Module N := M.
+
+Lemma test_module_renaming_0 : forall x:N.t, x=x.
+ergo.
+Qed.
+
+Dp_predefined M.t => "int".
+
+Lemma test_module_renaming_1 : forall x:N.t, x=x.
+ergo.
+Qed.
+
+(* Coq lists *)
+
+Require Export List.
+
+Lemma test_pol_0 : forall l:list nat, l=l.
+ergo.
+Qed.
+
+Parameter nlist: list nat -> Prop.
+
+Lemma poly_1 : forall l,  nlist l -> True.
+intros.
+simplify.
+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.
+Qed.
+
+(* polymorphism *)
+Require Import List.
+
+Inductive mylist (A:Set) : Set :=
+  mynil : mylist A
+| mycons : forall a:A, mylist A -> mylist A.
+
+Parameter my_nlist: mylist nat -> Prop.
+
+ Goal forall l,  my_nlist l -> True.
+ intros.
+ simplify.
+Qed.
+
+(* First example with the 0 and the equality translated *)
+
+Goal 0 = 0.
+simplify.
+Qed.
+
+(* Examples in the Propositional Calculus
+   and theory of equality *)
+
+Parameter A C : Prop.
+
+Goal A -> A.
+simplify.
+Qed.
+
+
+Goal A -> (A \/ C).
+
+simplify.
+Qed.
+
+
+Parameter x y z : Z.
+
+Goal x = y -> y = z -> x = z.
+ergo.
+Qed.
+
+
+Goal ((((A -> C) -> A) -> A) -> C) -> C.
+
+ergo.
+Qed.
+
+(* Arithmetic *)
+Open Scope Z_scope.
+
+Goal 1 + 1 = 2.
+yices.
+Qed.
+
+
+Goal 2*x + 10 = 18 -> x = 4.
+
+simplify.
+Qed.
+
+
+(* Universal quantifier *)
+
+Goal (forall (x y : Z), x = y) -> 0=1.
+try zenon.
+ergo.
+Qed.
+
+Goal forall (x: nat), (x + 0 = x)%nat.
+
+induction x0; ergo.
+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 dp/injection 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.
+ergo.
+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.
+yices.
+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 ; yices.
+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.
+yices.
+(*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; ergo.
+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.
+ergo.
+(*
+simplify.
+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.
+yices.
+(*zenon.*)
+Qed.
+
+
+
+(* abstractions *)
+
+Parameter poly_f : forall A:Set, A->A.
+
+Goal forall x:nat, poly_f nat x = poly_f nat x.
+ergo.
+(*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.
+
+*)