traces Ergo

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

4 files changed, 152 insertions, 3 deletions

diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v
new file mode 100644
index 0000000000..db028a5ea2
--- /dev/null
+++ b/contrib/dp/Dp.v
@@ -0,0 +1,120 @@
+(* Calls to external decision procedures *)
+
+Require Export ZArith.
+Require Export Classical.
+
+(* Zenon *)
+
+(*  Copyright 2004 INRIA  *)
+(*  $Id: zenon.v,v 1.6 2006-02-16 09:22:46 doligez Exp $  *)
+
+Lemma zenon_nottrue :
+  (~True -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_noteq : forall (T : Type) (t : T),
+  ((t <> t) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_and : forall P Q : Prop,
+  (P -> Q -> False) -> (P /\ Q -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_or : forall P Q : Prop,
+  (P -> False) -> (Q -> False) -> (P \/ Q -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_imply : forall P Q : Prop,
+  (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_equiv : forall P Q : Prop,
+  (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notand : forall P Q : Prop,
+  (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notor : forall P Q : Prop,
+  (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notimply : forall P Q : Prop,
+  (P -> ~Q -> False) -> (~(P -> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_notequiv : forall P Q : Prop,
+  (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
+Proof. tauto. Qed.
+
+Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
+  (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
+  ((P t) -> False) -> ((forall x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
+  (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
+Proof. firstorder. Qed.
+
+Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
+  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
+Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
+
+Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
+Proof. auto. Qed.
+
+Lemma zenon_equal_step :
+  forall (S T : Type) (fa fb : S -> T) (a b : S),
+  (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
+Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
+
+Lemma zenon_pnotp : forall P Q : Prop,
+  (P = Q) -> (P -> ~Q -> False).
+Proof. intros P Q Ha. rewrite Ha. auto. Qed.
+
+Lemma zenon_notequal : forall (T : Type) (a b : T),
+  (a = b) -> (a <> b -> False).
+Proof. auto. Qed.
+
+Ltac zenon_intro id :=
+  intro id || let nid := fresh in (intro nid; clear nid)
+.
+
+Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
+Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
+Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
+Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
+Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
+Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
+Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
+Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
+Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
+Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
+
+Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
+Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.
+
+(* Ergo *)
+
+Set Implicit Arguments.
+Section congr.
+  Variable t:Type.
+Lemma ergo_eq_concat_1 : 
+  forall (P:t -> Prop) (x y:t),
+    P x -> x = y -> P y.
+Proof.
+  intros; subst; auto.
+Qed.
+
+Lemma ergo_eq_concat_2 : 
+  forall (P:t -> t -> Prop) (x1 x2 y1 y2:t),
+    P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2.
+Proof.
+  intros; subst; auto.
+Qed.
+
+End congr.
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 9636206b03..8ac31ce932 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -29,6 +29,8 @@ open Dp_why
 
 let debug = ref false
 let set_debug b = debug := b
+let trace = ref false
+let set_trace b = trace := b
 let timeout = ref 10
 let set_timeout n = timeout := n
 
@@ -661,13 +663,20 @@ let call_simplify fwhy =
   r
 
 let call_ergo fwhy =
+  let ftrace = Filename.temp_file "ergo_trace" "" in
   let cmd = 
-    sprintf "timeout %d ergo %s > out 2>&1 && grep -q -w Valid out" 
-      !timeout fwhy
+    if !trace then
+      sprintf 
+	"timeout %d ergo -cctrace %s %s > out 2>&1 && grep -q -w Valid out"  
+	!timeout ftrace fwhy
+    else
+      sprintf "timeout %d ergo %s > out 2>&1 && grep -q -w Valid out" 
+	!timeout fwhy
   in
   let out = Sys.command cmd in
   let r = 
-    if out = 0 then Valid None else if out = 1 then Invalid else Timeout 
+    if out = 0 then Valid (if !trace then Some ftrace else None)
+    else if out = 1 then Invalid else Timeout 
   in
   if not !debug then remove_files [fwhy];
   r
@@ -746,6 +755,20 @@ let call_harvey fwhy =
   if not !debug then remove_files [fwhy; frv; outf];
   r
 
+let ergo_proof_from_file f gl =
+  let s =
+    let buf = Buffer.create 1024 in
+    let c = open_in f in
+    try
+      while true do Buffer.add_string buf (input_line c) done; assert false
+    with End_of_file ->
+      close_in c;
+      Buffer.contents buf
+  in
+  let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in
+  let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in
+  exact_check t gl
+
 let call_prover prover q =
   let fwhy = Filename.temp_file "coq_dp" ".why" in
   Dp_why.output_file fwhy q;
@@ -765,6 +788,7 @@ let dp prover gl =
     let q = tr_goal gl in
     begin match call_prover prover q with
       | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
+      | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
       | Valid _ -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"
       | DontKnow -> error "Don't know"
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 181df6b373..1e47c950fc 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -12,5 +12,6 @@ val zenon : tactic
 val dp_hint : reference list -> unit
 val set_timeout : int -> unit
 val set_debug : bool -> unit
+val set_trace : bool -> unit
 
 
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 46ae400d2c..3e083dbd11 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -53,3 +53,7 @@ VERNAC COMMAND EXTEND Dp_debug
 | [ "Dp_debug" ] -> [ set_debug true; Dp_zenon.set_debug true ]
 END
 
+VERNAC COMMAND EXTEND Dp_trace
+| [ "Dp_trace" ] -> [ set_trace true ]
+END
+