Dp : ajoût des existentiels

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

4 files changed, 133 insertions, 98 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index ecc9cd6be..6b1987b9a 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -497,8 +497,17 @@ and tr_formula bv env f =
 	  in
 	  let bv = id :: bv in
 	  Forall (string_of_id id, t, tr_formula bv env b)
-    | _, [a] when c = build_coq_ex () ->
-	assert false (* TODO Exists (tr_formula bv env a) *)
+    | _, [_; a] when c = build_coq_ex () ->
+	begin match kind_of_term a with
+	  | Lambda(Name n, ty, t) ->
+	      let id = string_of_id n in
+	      (match tr_type env ty with
+		 | [], ty ->
+		     let t = subst1 (mkVar n) t in
+		     Exists (id, ty, tr_formula (n::bv) env t)
+		 | l, _ -> raise NotFO)
+	  | _ -> assert false
+		(* a must be a Lambda since we are in the ex case *) end
     | _ ->
 	begin try
 	  let r = global_of_constr c in
@@ -538,7 +547,7 @@ type prover = Simplify | CVCLite | Harvey | Zenon
 
 let call_prover prover q = match prover with
   | Simplify -> Dp_simplify.call q
-  | CVCLite -> error "CVCLite not yet interfaced"
+  | CVCLite -> Dp_cvcl.call q
   | Harvey -> error "haRVey not yet interfaced"
   | Zenon -> Dp_zenon.call q
   
@@ -558,7 +567,7 @@ let dp prover gl =
   
 
 let simplify = tclTHEN intros (dp Simplify)
-let cvc_lite = dp CVCLite
+let cvc_lite = tclTHEN intros (dp CVCLite)
 let harvey = dp Harvey
 let zenon = tclTHEN intros (dp Zenon)
 
diff --git a/contrib/dp/dp_cvcl.ml b/contrib/dp/dp_cvcl.ml
index 602d12203..05d430812 100644
--- a/contrib/dp/dp_cvcl.ml
+++ b/contrib/dp/dp_cvcl.ml
@@ -22,9 +22,9 @@ let rec print_term fmt = function
   | Div (a, b) ->
       fprintf fmt "@[(%a@ /@ %a)@]" print_term a print_term b
   | App (id, []) ->
-      fprintf fmt "%s" id
+      fprintf fmt "@[%s@]" id
   | App (id, tl) ->
-      fprintf fmt "@[(%s@(%a))@]" id print_terms tl
+      fprintf fmt "@[%s(%a)@]" id print_terms tl
 
 and print_terms fmt tl = 
   print_list comma print_term fmt tl
@@ -46,8 +46,10 @@ let rec print_predicate fmt p =
       fprintf fmt "@[(%a@ >= %a)@]" print_term a print_term b
   | Fatom (Gt (a, b)) ->
       fprintf fmt "@[(%a@ > %a)@]" print_term a print_term b
-  | Fatom (Pred (id, tl)) -> 
-      fprintf fmt "@[(%s@(%a))@]" id print_terms tl
+  | Fatom (Pred (id, [])) ->
+      fprintf fmt "@[%s@]" id
+  | Fatom (Pred (id, tl)) ->
+      fprintf fmt "@[%s(%a)@]" id print_terms tl
   | Imp (a, b) ->
       fprintf fmt "@[(%a@ => %a)@]" pp a pp b
   | And (a, b) ->
@@ -57,37 +59,40 @@ let rec print_predicate fmt p =
   | Not a ->
       fprintf fmt "@[(NOT@ %a)@]" pp a
   | Forall (id, t, p) -> 
-      fprintf fmt "@[(FORALL (%s:%s)@ %a)@]" id t pp p
-(*
-  | Exists (id,n,t,p) -> 
-      let id' = next_away id (predicate_vars p) in
-      let p' = subst_in_predicate (subst_onev n id') p in
-      fprintf fmt "@[(EXISTS (%a)@ %a)@]" Ident.print id' pp p'
-*)
-  | Exists _ ->
-      assert false (*TODO*)
+      fprintf fmt "@[(FORALL (%s:%s): %a)@]" id t pp p
+  | Exists (id, t, p) -> 
+      fprintf fmt "@[(EXISTS (%s:%s): %a)@]" id t pp p
 
 let rec string_of_type_list  = function
-  | [] -> ""
-  | e :: l' -> e ^ " -> " ^ (string_of_type_list l')
+  | [] -> assert false
+  | [e] -> e
+  | e :: l' -> e ^ ", " ^ (string_of_type_list l')
 
 let print_query fmt (decls,concl) =
   let print_decl = function
     | DeclVar (id, [], t) ->
-	fprintf fmt "@[%s: %s@]@\n" id t
+	fprintf fmt "@[%s: %s;@]@\n" id t
+    | DeclVar (id, [e], t) ->
+	fprintf fmt "@[%s: [%s -> %s];@]@\n"
+	  id e t
     | DeclVar (id, l, t) ->
-	fprintf fmt "@[%s: %s%s@]@\n"
+	fprintf fmt "@[%s: [[%s] -> %s];@]@\n"
 	  id (string_of_type_list l) t
-    | DeclPred (id, l) -> 
-	fprintf fmt "@[%s: %sBOOLEAN@]@\n"
+    | DeclPred (id, []) ->
+	fprintf fmt "@[%s: BOOLEAN;@]@\n" id
+     | DeclPred (id, [e]) ->
+	fprintf fmt "@[%s: [%s -> BOOLEAN];@]@\n"
+	  id e
+   | DeclPred (id, l) ->
+	fprintf fmt "@[%s: [[%s] -> BOOLEAN];@]@\n"
 	  id (string_of_type_list l)
     | DeclType id ->
-	fprintf fmt "@[%s: TYPE@]@\n" id
+	fprintf fmt "@[%s: TYPE;@]@\n" id
     | Assert (id, f)  -> 
-	fprintf fmt "@[ASSERT %s@\n %a@]@\n" id print_predicate f
+	fprintf fmt "@[ASSERT %% %s@\n %a;@]@\n" id print_predicate f
   in
   List.iter print_decl decls;
-  fprintf fmt "PUSH; %a@; POP;" print_predicate concl
+  fprintf fmt "QUERY %a;" print_predicate concl
 
 let call q = 
   let f = Filename.temp_file "coq_dp" ".cvc" in
@@ -97,7 +102,7 @@ let call q =
   close_out c;
   ignore (Sys.command (sprintf "cat %s" f));
   let cmd = 
-    sprintf "timeout 10 cvcl-1.1.0 %s > out 2>&1 && grep -q -w Valid out" f
+    sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" f
   in
   prerr_endline cmd; flush stderr;
   let out = Sys.command cmd in
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index fc0724dc7..3015b03e0 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -70,14 +70,8 @@ let rec print_predicate fmt p =
       fprintf fmt "@[(NOT@ %a)@]" pp a
   | Forall (id, _, p) -> 
       fprintf fmt "@[(FORALL (%a)@ %a)@]" ident id pp p
-(*
-  | Exists (id,n,t,p) -> 
-      let id' = next_away id (predicate_vars p) in
-      let p' = subst_in_predicate (subst_onev n id') p in
-      fprintf fmt "@[(EXISTS (%a)@ %a)@]" Ident.print id' pp p'
-*)
-  | Exists _ ->
-      assert false (*TODO*)
+  | Exists (id, _, p) -> 
+      fprintf fmt "@[(EXISTS (%a)@ %a)@]" ident id pp p
 
 let rec string_of_type_list  = function
   | [] -> ""
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index 6209d4539..ef6d177cd 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -4,7 +4,7 @@ Require Import ZArith.
 Require Import Classical.
 
 
-(* Premier exemple avec traduction de l'égalité et du 0 *)
+(* First example with the 0 and the equality translated *)
 
 Goal 0 = 0.
 
@@ -12,7 +12,8 @@ simplify.
 Qed.
 
 
-(* Exemples dans le calcul propositionnel *)
+(* Examples in the Propositional Calculus
+   and theory of equality *)
 
 Parameter A C : Prop.
 
@@ -28,8 +29,6 @@ zenon.
 Qed.
 
 
-(* Arithmétique de base *)
-
 Parameter x y z : Z.
 
 Goal x = y -> y = z -> x = z.
@@ -37,7 +36,27 @@ Goal x = y -> y = z -> x = z.
 zenon.
 Qed.
 
-(* Ajoût de quantificateurs universels *)
+
+Goal ((((A -> C) -> A) -> A) -> C) -> C.
+
+simplify.
+Qed.
+
+
+(* Arithmetic *)
+
+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.
 
@@ -45,7 +64,20 @@ simplify.
 Qed.
 
 
-(* Définition de fonctions *) 
+Goal forall (x y : Z), x + y = y + x.
+
+induction x ; simplify.
+Qed.
+
+
+(* No decision procedure can solve this problem 
+  Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a.
+  simplify.
+  Qed.
+*)
+
+
+(* Functions definitions *) 
 
 Definition fst (x y : Z) : Z := x.
 
@@ -54,7 +86,8 @@ Goal forall (g : Z -> Z) (x y : Z), g (fst x y) = g x.
 simplify.
 Qed.
 
-(* Exemple d'éta-expansion *)
+
+(* Eta-expansion example *)
 
 Definition snd_of_3 (x y z : Z) : Z := y.
 
@@ -66,112 +99,106 @@ simplify.
 Qed.
 
 
-(* Définition de types inductifs - appel de la fonction injection *)
+(* Inductive types definitions - call to injection function *)
 
-Inductive new : Set :=
-| B : new
-| N : new -> new.
+Inductive even : Z -> Prop :=
+| even_0 : even 0
+| even_plus2 : forall z : Z, even z -> even (z + 2).
 
-Inductive even_p : new -> Prop :=
-| even_p_B : even_p B
-| even_p_N : forall n : new, even_p n -> even_p (N (N n)).
 
-Goal even_p (N (N (N (N B)))).
-
-simplify.
-Qed.
+(* Simplify and Zenon can't prove this goal before the timeout
+   unlike CVC Lite *)
 
-Goal even_p (N (N (N (N B)))).
+Goal even 4.
 
-zenon.
+cvcl.
 Qed.
 
 
-(* A noter que simplify ne parvient pas à résoudre ce problème
-   avant le timemout au contraire de zenon *)
-
-Definition skip_z (z : Z) (n : new) := n.
+Definition skip_z (z : Z) (n : nat) := n.
 
 Definition skip_z1 := skip_z.
 
-Goal forall (z : Z) (n : new), skip_z z n = skip_z1 z n.
+Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n.
 
 zenon.
 Qed.
 
 
-(* Définition d'axiomes et ajoût de dp_hint *)
+(* Axioms definitions and dp_hint *)
 
-Parameter add : new -> new -> new.
-Axiom add_B : forall (n : new), add B n = n.
-Axiom add_N : forall (n1 n2 : new), add (N n1) n2 = N (add n1 n2).
+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 add_B.
-Dp add_N.
+Dp add_0.
+Dp add_S.
 
-(* Encore un exemple que simplify ne résout pas avant le timeout *)
+(* Simplify can't prove this goal before the tiemout 
+   unlike zenon *)
 
-Goal forall n : new, add n B = n.
+Goal forall n : nat, add n 0 = n.
 
 induction n ; zenon.
 Qed.
 
 
-Definition newPred (n : new) : new := match n with
-  | B => B
-  | N n' => n'
+Definition pred (n : nat) : nat := match n with
+  | 0%nat => 0%nat
+  | S n' => n'
 end.
 
-Goal forall n : new, n <> B -> newPred (N n) <> B.
+Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat.
 
 zenon.
 Qed.
 
 
-Fixpoint newPlus (n m : new) {struct n} : new :=
+Fixpoint plus (n m : nat) {struct n} : nat :=
   match n with
-  | B => m
-  | N n' => N (newPlus n' m)
+  | 0%nat => m
+  | S n' => S (plus n' m)
 end.
 
-Goal forall n : new, newPlus n B = n.
+Goal forall n : nat, plus n 0%nat = n.
 
 induction n; zenon.
 Qed.
 
 
-Definition h (n : new) (z : Z) : Z := match n with
-  | B => z + 1
-  | N n' => z - 1
-end.
-
-
-
-(* mutually recursive functions *)
+(* Mutually recursive functions *)
 
-Fixpoint even (n:nat) : bool := match n with
+Fixpoint even_b (n : nat) : bool := match n with
   | O => true
-  | S m => odd m
+  | S m => odd_b m
 end
-with odd (n:nat) : bool := match n with
+with odd_b (n : nat) : bool := match n with
   | O => false
-  | S m => even m
+  | S m => even_b m
 end.
 
-Goal even (S (S O)) = true.
+Goal even_b (S (S O)) = true.
+
 zenon.
+Qed.
 
-(* anonymous mutually recursive functions : no equations are produced *)
 
-Definition f := 
-  fix even (n:nat) : bool := match n with
-  | O => true
-  | S m => odd m
+(* 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 odd (n:nat) : bool := match n with
-  | O => false
-  | S m => even m
+  with odd2 (n : nat) : bool := match n with
+    | O => false
+    | S m => even2 m
   end for even.
 
-Goal f (S (S O)) = true.
+   Thus this goal is unsolvable
+
+Goal mrf (S (S O)) = true.
+
 zenon.
+
+*)
\ No newline at end of file