From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- contrib/dp/Dp.v | 120 ++++++++++++ contrib/dp/TODO | 4 - contrib/dp/dp.ml | 316 +++++++++++++++++++++++++++----- contrib/dp/dp.mli | 8 + contrib/dp/dp_cvcl.ml | 112 ------------ contrib/dp/dp_cvcl.mli | 4 - contrib/dp/dp_gappa.ml | 445 +++++++++++++++++++++++++++++++++++++++++++++ contrib/dp/dp_simplify.ml | 117 ------------ contrib/dp/dp_simplify.mli | 4 - contrib/dp/dp_sorts.ml | 51 ------ contrib/dp/dp_sorts.mli | 4 - contrib/dp/dp_why.ml | 12 ++ contrib/dp/dp_why.mli | 17 ++ contrib/dp/dp_zenon.ml | 103 ----------- contrib/dp/dp_zenon.mli | 5 +- contrib/dp/dp_zenon.mll | 181 ++++++++++++++++++ contrib/dp/fol.mli | 9 +- contrib/dp/g_dp.ml4 | 43 ++++- contrib/dp/test2.v | 8 +- contrib/dp/test_gappa.v | 91 +++++++++ contrib/dp/tests.v | 116 +++++++++--- contrib/dp/zenon.v | 94 ++++++++++ 22 files changed, 1393 insertions(+), 471 deletions(-) create mode 100644 contrib/dp/Dp.v delete mode 100644 contrib/dp/dp_cvcl.ml delete mode 100644 contrib/dp/dp_cvcl.mli create mode 100644 contrib/dp/dp_gappa.ml delete mode 100644 contrib/dp/dp_simplify.ml delete mode 100644 contrib/dp/dp_simplify.mli delete mode 100644 contrib/dp/dp_sorts.ml delete mode 100644 contrib/dp/dp_sorts.mli create mode 100644 contrib/dp/dp_why.mli delete mode 100644 contrib/dp/dp_zenon.ml create mode 100644 contrib/dp/dp_zenon.mll create mode 100644 contrib/dp/test_gappa.v create mode 100644 contrib/dp/zenon.v (limited to 'contrib/dp') diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v new file mode 100644 index 00000000..857c182c --- /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: Dp.v 10739 2008-04-01 14:45:20Z herbelin $ *) + +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/TODO b/contrib/dp/TODO index 387cacdf..44349e21 100644 --- a/contrib/dp/TODO +++ b/contrib/dp/TODO @@ -21,8 +21,4 @@ TODO BUGS ---- -- value = Some : forall A:Set, A -> option A - - -> eta_expanse échoue sur assert false (ligne 147) - diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index 131dd029..79ffaf3f 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -13,6 +13,8 @@ open Util open Pp +open Libobject +open Summary open Term open Tacmach open Tactics @@ -25,12 +27,46 @@ open Coqlib open Hipattern open Libnames open Declarations +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 + +let (dp_timeout_obj,_) = + declare_object + {(default_object "Dp_timeout") with + cache_function = (fun (_,x) -> set_timeout x); + load_function = (fun _ (_,x) -> set_timeout x); + export_function = (fun x -> Some x)} + +let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) + +let (dp_debug_obj,_) = + declare_object + {(default_object "Dp_debug") with + cache_function = (fun (_,x) -> set_debug x); + load_function = (fun _ (_,x) -> set_debug x); + export_function = (fun x -> Some x)} + +let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) + +let (dp_trace_obj,_) = + declare_object + {(default_object "Dp_trace") with + cache_function = (fun (_,x) -> set_trace x); + load_function = (fun _ (_,x) -> set_trace x); + export_function = (fun x -> Some x)} + +let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x) let logic_dir = ["Coq";"Logic";"Decidable"] let coq_modules = init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules + @ [["Coq"; "ZArith"; "BinInt"]] @ [["Coq"; "omega"; "OmegaLemmas"]] let constant = gen_constant_in_modules "dp" coq_modules @@ -52,6 +88,7 @@ let coq_Zneg = lazy (constant "Zneg") let coq_xH = lazy (constant "xH") let coq_xI = lazy (constant "xI") let coq_xO = lazy (constant "xO") +let coq_iff = lazy (constant "iff") (* not Prop typed expressions *) exception NotProp @@ -104,7 +141,7 @@ let coq_rename_vars env vars = type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *) let decomp_type_quantifiers env t = let rec loop vars t = match kind_of_term t with - | Prod (n, a, t) when is_Set a -> + | Prod (n, a, t) when is_Set a || is_Type a -> loop ((n,a) :: vars) t | _ -> let vars, env = coq_rename_vars env vars in @@ -116,7 +153,7 @@ let decomp_type_quantifiers env t = (* same thing with lambda binders (for axiomatize body) *) let decomp_type_lambdas env t = let rec loop vars t = match kind_of_term t with - | Lambda (n, a, t) when is_Set a -> + | Lambda (n, a, t) when is_Set a || is_Type a -> loop ((n,a) :: vars) t | _ -> let vars, env = coq_rename_vars env vars in @@ -314,7 +351,7 @@ and make_term_abstraction tv env c = *) and tr_decl env id ty = let tv, env, t = decomp_type_quantifiers env ty in - if is_Set t then + if is_Set t || is_Type t then DeclType (id, List.length tv) else if is_Prop t then DeclPred (id, List.length tv, []) @@ -329,8 +366,8 @@ and tr_decl env id ty = DeclPred(id, List.length tv, l) else let s = Typing.type_of env Evd.empty t in - if is_Set s then - DeclFun(id, List.length tv, l, tr_type tv env t) + if is_Set s || is_Type s then + DeclFun (id, List.length tv, l, tr_type tv env t) else raise NotFO @@ -364,17 +401,18 @@ and axiomatize_body env r id d = match r with begin match (Global.lookup_constant c).const_body with | Some b -> let b = force b in - let tv, env, b = decomp_type_lambdas env b in let axioms = (match d with | DeclPred (id, _, []) -> + let tv, env, b = decomp_type_lambdas env b in let value = tr_formula tv [] env b in [id, Iff (Fatom (Pred (id, [])), value)] | DeclFun (id, _, [], _) -> + let tv, env, b = decomp_type_lambdas env b in let value = tr_term tv [] env b in [id, Fatom (Eq (Fol.App (id, []), value))] | DeclFun (id, _, l, _) | DeclPred (id, _, l) -> - Format.eprintf "axiomatize_body %S@." id; + (*Format.eprintf "axiomatize_body %S@." id;*) let b = match kind_of_term b with (* a single recursive function *) | Fix (_, (_,_,[|b|])) -> @@ -391,6 +429,7 @@ and axiomatize_body env r id d = match r with | _ -> b in + let tv, env, b = decomp_type_lambdas env b in let vars, t = decompose_lam b in let n = List.length l in let k = List.length vars in @@ -401,21 +440,21 @@ and axiomatize_body env r id d = match r with let vars = List.rev vars in let bv = vars in let vars = List.map (fun x -> string_of_id x) vars in - let fol_var x = - Fol.App (x, []) in + let fol_var x = Fol.App (x, []) in let fol_vars = List.map fol_var vars in let vars = List.combine vars l in begin match d with - | DeclFun _ -> + | DeclFun (_, _, _, ty) -> begin match kind_of_term t with | Case (ci, _, e, br) -> equations_for_case env id vars tv bv ci e br | _ -> - let p = - Fatom (Eq (App (id, fol_vars), - tr_term tv bv env t)) + let t = tr_term tv bv env t in + let ax = + add_proof (Fun_def (id, vars, ty, t)) in - [id, foralls vars p] + let p = Fatom (Eq (App (id, fol_vars), t)) in + [ax, foralls vars p] end | DeclPred _ -> let value = tr_formula tv bv env t in @@ -436,7 +475,7 @@ and axiomatize_body env r id d = match r with | IndRef i -> iter_all_constructors i (fun _ c -> - let rc = reference_of_constr c in + let rc = global_of_constr c in try begin match tr_global env rc with | DeclFun (_, _, [], _) -> () @@ -453,18 +492,20 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with iter_all_constructors ci.ci_ind (fun j cj -> try - let cjr = reference_of_constr cj in + let cjr = global_of_constr cj in begin match tr_global env cjr with | DeclFun (idc, _, l, _) -> let b = br.(j) in let rec_vars, b = decompose_lam b in let rec_vars, env = coq_rename_vars env rec_vars in - let b = substl (List.map mkVar rec_vars) b in + let coq_rec_vars = List.map mkVar rec_vars in + let b = substl coq_rec_vars b in let rec_vars = List.rev rec_vars in + let coq_rec_term = applist (cj, List.rev coq_rec_vars) in + let b = replace_vars [x, coq_rec_term] b in let bv = bv @ rec_vars in let rec_vars = List.map string_of_id rec_vars in - let fol_var x = - Fol.App (x, []) in + let fol_var x = Fol.App (x, []) in let fol_rec_vars = List.map fol_var rec_vars in let fol_rec_term = App (idc, fol_rec_vars) in let rec_vars = List.combine rec_vars l in @@ -558,7 +599,7 @@ and tr_formula tv bv env f = Fatom (Pred (rename_global (VarRef id), [])) | _, [t;a;b] when c = build_coq_eq () -> let ty = Typing.type_of env Evd.empty t in - if is_Set ty then + if is_Set ty || is_Type ty then let _ = tr_type tv env t in Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b)) else @@ -581,6 +622,8 @@ and tr_formula tv bv env f = And (tr_formula tv bv env a, tr_formula tv bv env b) | _, [a;b] when c = build_coq_or () -> Or (tr_formula tv bv env a, tr_formula tv bv env b) + | _, [a;b] when c = Lazy.force coq_iff -> + Iff (tr_formula tv bv env a, tr_formula tv bv env b) | Prod (n, a, b), _ -> if is_imp_term f then Imp (tr_formula tv bv env a, tr_formula tv bv env b) @@ -632,55 +675,164 @@ let tr_goal gl = hyps, c -type prover = Simplify | CVCLite | Harvey | Zenon +type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ()) let sprintf = Format.sprintf +let file_contents f = + let buf = Buffer.create 1024 in + try + let c = open_in f in + begin try + while true do + let s = input_line c in Buffer.add_string buf s; + Buffer.add_char buf '\n' + done; + assert false + with End_of_file -> + close_in c; + Buffer.contents buf + end + with _ -> + sprintf "(cannot open %s)" f + +let timeout_sys_command cmd = + if !debug then Format.eprintf "command line: %s@." cmd; + let out = Filename.temp_file "out" "" in + let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in + let ret = Sys.command cmd in + if !debug then + Format.eprintf "Output file %s:@.%s@." out (file_contents out); + ret, out + +let timeout_or_failure c cmd out = + if c = 152 then + Timeout + else + Failure + (sprintf "command %s failed with output:\n%s " cmd (file_contents out)) + +let prelude_files = ref ([] : string list) + +let set_prelude l = prelude_files := l + +let (dp_prelude_obj,_) = + declare_object + {(default_object "Dp_prelude") with + cache_function = (fun (_,x) -> set_prelude x); + load_function = (fun _ (_,x) -> set_prelude x); + export_function = (fun x -> Some x)} + +let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x) + +let why_files f = String.concat " " (!prelude_files @ [f]) + let call_simplify fwhy = - let cmd = sprintf "why --simplify %s" fwhy in - if Sys.command cmd <> 0 then error ("Call to " ^ cmd ^ " failed"); + let cmd = + sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in let cmd = - sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" fsx + sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out" + !timeout fsx in let out = Sys.command cmd in - let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout in + let r = + if out = 0 then Valid None else if out = 1 then Invalid else Timeout + in if not !debug then remove_files [fwhy; fsx]; r +let call_ergo fwhy = + let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in + let ftrace = Filename.temp_file "ergo_trace" "" in + let cmd = + if !trace then + sprintf "ergo -cctrace %s %s" ftrace fwhy + else + sprintf "ergo %s" fwhy + in + let ret,out = timeout_sys_command cmd in + let r = + if ret <> 0 then + timeout_or_failure ret cmd out + else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then + Valid (if !trace then Some ftrace else None) + else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then + DontKnow + else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then + Invalid + else + Failure ("command failed: " ^ cmd) + in + if not !debug then remove_files [fwhy; out]; + r + let call_zenon fwhy = - let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in + let cmd = + sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy) + in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in + let out = Filename.temp_file "dp_out" "" in let cmd = - sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn + sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out + in + let c = Sys.command cmd in + if not !debug then remove_files [fwhy; fznn]; + if c = 137 then + Timeout + else begin + if c <> 0 then anomaly ("command failed: " ^ cmd); + if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then + error "Zenon failed"; + let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in + if c = 0 then Valid (Some out) else Invalid + end + +let call_yices fwhy = + let cmd = + sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy) + in + if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); + let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in + let cmd = + sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out" + !timeout fsmt in let out = Sys.command cmd in let r = - if out = 0 then Valid - else if out = 1 then Invalid - else if out = 137 then Timeout - else anomaly ("malformed Zenon input file " ^ fznn) + if out = 0 then Valid None else if out = 1 then Invalid else Timeout in - if not !debug then remove_files [fwhy; fznn]; + if not !debug then remove_files [fwhy; fsmt]; r let call_cvcl fwhy = - let cmd = sprintf "why --cvcl %s" fwhy in + let cmd = + sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy) + in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in let cmd = - sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" fcvc + sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out" + !timeout fcvc in let out = Sys.command cmd in - let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout in + let r = + if out = 0 then Valid None else if out = 1 then Invalid else Timeout + in if not !debug then remove_files [fwhy; fcvc]; r let call_harvey fwhy = - let cmd = sprintf "why --harvey %s" fwhy in + let cmd = + sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy) + in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in @@ -688,7 +840,8 @@ let call_harvey fwhy = let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in let outf = Filename.temp_file "rv" ".out" in let out = - Sys.command (sprintf "timeout 10 rv -e\"-T 2000\" %s > %s 2>&1" f outf) + Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1" + !timeout f outf) in let r = if out <> 0 then @@ -697,40 +850,69 @@ let call_harvey fwhy = let cmd = sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf in - if Sys.command cmd = 0 then Valid else Invalid + if Sys.command cmd = 0 then Valid None else Invalid in if not !debug then remove_files [fwhy; frv; outf]; r +let call_gwhy fwhy = + let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in + if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy)); + NoAnswer + +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; - if !debug then ignore (Sys.command (sprintf "cat %s" fwhy)); match prover with | Simplify -> call_simplify fwhy + | Ergo -> call_ergo fwhy + | Yices -> call_yices fwhy | Zenon -> call_zenon fwhy | CVCLite -> call_cvcl fwhy | Harvey -> call_harvey fwhy + | Gwhy -> call_gwhy fwhy let dp prover gl = + Coqlib.check_required_library ["Coq";"ZArith";"ZArith"]; let concl_type = pf_type_of gl (pf_concl gl) in if not (is_Prop concl_type) then error "Conclusion is not a Prop"; try let q = tr_goal gl in begin match call_prover prover q with - | Valid -> Tactics.admit_as_an_axiom gl + | 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" | Timeout -> error "Timeout" + | Failure s -> error s + | NoAnswer -> Tacticals.tclIDTAC gl end with NotFO -> error "Not a first order goal" - + let simplify = tclTHEN intros (dp Simplify) +let ergo = tclTHEN intros (dp Ergo) +let yices = tclTHEN intros (dp Yices) let cvc_lite = tclTHEN intros (dp CVCLite) let harvey = dp Harvey let zenon = tclTHEN intros (dp Zenon) +let gwhy = tclTHEN intros (dp Gwhy) let dp_hint l = let env = Global.env () in @@ -741,7 +923,8 @@ let dp_hint l = if is_Prop s then try let id = rename_global r in - let d = Axiom (id, tr_formula [] [] env ty) in + let tv, env, ty = decomp_type_quantifiers env ty in + let d = Axiom (id, tr_formula tv [] env ty) in add_global r (Gfo d); globals_stack := d :: !globals_stack with NotFO -> @@ -757,3 +940,52 @@ let dp_hint l = end in List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l) + +let (dp_hint_obj,_) = + declare_object + {(default_object "Dp_hint") with + cache_function = (fun (_,l) -> dp_hint l); + load_function = (fun _ (_,l) -> dp_hint l); + export_function = (fun x -> Some x)} + +let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l) + +let dp_predefined qid s = + let r = Nametab.global qid in + let ty = Global.type_of_global r in + let env = Global.env () in + let id = rename_global r in + try + let d = match tr_decl env id ty with + | DeclType (_, n) -> DeclType (s, n) + | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty) + | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl) + | Axiom _ as d -> d + in + match d with + | Axiom _ -> msg_warning (str " ignored (axiom)") + | d -> add_global r (Gfo d) + with NotFO -> + msg_warning (str " ignored (not a first order declaration)") + +let (dp_predefined_obj,_) = + declare_object + {(default_object "Dp_predefined") with + cache_function = (fun (_,(id,s)) -> dp_predefined id s); + load_function = (fun _ (_,(id,s)) -> dp_predefined id s); + export_function = (fun x -> Some x)} + +let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s)) + +let _ = declare_summary "Dp options" + { freeze_function = + (fun () -> !debug, !trace, !timeout, !prelude_files); + unfreeze_function = + (fun (d,tr,tm,pr) -> + debug := d; trace := tr; timeout := tm; prelude_files := pr); + init_function = + (fun () -> + debug := false; trace := false; timeout := 10; + prelude_files := []); + survive_module = true; + survive_section = true } diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli index 3dad469c..6dbc05e1 100644 --- a/contrib/dp/dp.mli +++ b/contrib/dp/dp.mli @@ -3,10 +3,18 @@ open Libnames open Proof_type val simplify : tactic +val ergo : tactic +val yices : tactic val cvc_lite : tactic val harvey : tactic val zenon : tactic +val gwhy : tactic val dp_hint : reference list -> unit +val dp_timeout : int -> unit +val dp_debug : bool -> unit +val dp_trace : bool -> unit +val dp_prelude : string list -> unit +val dp_predefined : reference -> string -> unit diff --git a/contrib/dp/dp_cvcl.ml b/contrib/dp/dp_cvcl.ml deleted file mode 100644 index 05d43081..00000000 --- a/contrib/dp/dp_cvcl.ml +++ /dev/null @@ -1,112 +0,0 @@ - -open Format -open Fol - -let rec print_list sep print fmt = function - | [] -> () - | [x] -> print fmt x - | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r - -let space fmt () = fprintf fmt "@ " -let comma fmt () = fprintf fmt ",@ " - -let rec print_term fmt = function - | Cst n -> - fprintf fmt "%d" n - | Plus (a, b) -> - fprintf fmt "@[(%a@ +@ %a)@]" print_term a print_term b - | Moins (a, b) -> - fprintf fmt "@[(%a@ -@ %a)@]" print_term a print_term b - | Mult (a, b) -> - fprintf fmt "@[(%a@ *@ %a)@]" print_term a print_term b - | Div (a, b) -> - fprintf fmt "@[(%a@ /@ %a)@]" print_term a print_term b - | App (id, []) -> - fprintf fmt "@[%s@]" id - | App (id, tl) -> - fprintf fmt "@[%s(%a)@]" id print_terms tl - -and print_terms fmt tl = - print_list comma print_term fmt tl - -let rec print_predicate fmt p = - let pp = print_predicate in - match p with - | True -> - fprintf fmt "TRUE" - | False -> - fprintf fmt "FALSE" - | Fatom (Eq (a, b)) -> - fprintf fmt "@[(%a = %a)@]" print_term a print_term b - | Fatom (Le (a, b)) -> - fprintf fmt "@[(%a@ <= %a)@]" print_term a print_term b - | Fatom (Lt (a, b))-> - fprintf fmt "@[(%a@ < %a)@]" print_term a print_term b - | Fatom (Ge (a, b)) -> - 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, [])) -> - 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) -> - fprintf fmt "@[(%a@ AND@ %a)@]" pp a pp b - | Or (a, b) -> - fprintf fmt "@[(%a@ OR@ %a)@]" pp a pp b - | Not a -> - fprintf fmt "@[(NOT@ %a)@]" pp a - | Forall (id, t, p) -> - 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 - | [] -> 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 - | DeclVar (id, [e], t) -> - fprintf fmt "@[%s: [%s -> %s];@]@\n" - id e t - | DeclVar (id, l, t) -> - fprintf fmt "@[%s: [[%s] -> %s];@]@\n" - id (string_of_type_list l) t - | 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 - | Assert (id, f) -> - fprintf fmt "@[ASSERT %% %s@\n %a;@]@\n" id print_predicate f - in - List.iter print_decl decls; - fprintf fmt "QUERY %a;" print_predicate concl - -let call q = - let f = Filename.temp_file "coq_dp" ".cvc" in - let c = open_out f in - let fmt = formatter_of_out_channel c in - fprintf fmt "@[%a@]@." print_query q; - close_out c; - ignore (Sys.command (sprintf "cat %s" f)); - let cmd = - 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 - if out = 0 then Valid else if out = 1 then Invalid else Timeout - (* TODO: effacer le fichier f et le fichier out *) - - diff --git a/contrib/dp/dp_cvcl.mli b/contrib/dp/dp_cvcl.mli deleted file mode 100644 index 03b6d347..00000000 --- a/contrib/dp/dp_cvcl.mli +++ /dev/null @@ -1,4 +0,0 @@ - -open Fol - -val call : query -> prover_answer diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml new file mode 100644 index 00000000..70439a97 --- /dev/null +++ b/contrib/dp/dp_gappa.ml @@ -0,0 +1,445 @@ + +open Format +open Util +open Pp +open Term +open Tacmach +open Tactics +open Tacticals +open Names +open Nameops +open Termops +open Coqlib +open Hipattern +open Libnames +open Declarations +open Evarutil + +let debug = ref false + +(* 1. gappa syntax trees and output *) + +module Constant = struct + + open Bigint + + type t = { mantissa : bigint; base : int; exp : bigint } + + let create (b, m, e) = + { mantissa = m; base = b; exp = e } + + let of_int x = + { mantissa = x; base = 1; exp = zero } + + let print fmt x = match x.base with + | 1 -> fprintf fmt "%s" (to_string x.mantissa) + | 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp) + | 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp) + | _ -> assert false + +end + +type binop = Bminus | Bplus | Bmult | Bdiv + +type unop = Usqrt | Uabs | Uopp + +type rounding_mode = string + +type term = + | Tconst of Constant.t + | Tvar of string + | Tbinop of binop * term * term + | Tunop of unop * term + | Tround of rounding_mode * term + +type pred = + | Pin of term * Constant.t * Constant.t + +let rec print_term fmt = function + | Tconst c -> Constant.print fmt c + | Tvar s -> pp_print_string fmt s + | Tbinop (op, t1, t2) -> + let op = match op with + | Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/" + in + fprintf fmt "(%a %s %a)" print_term t1 op print_term t2 + | Tunop (Uabs, t) -> + fprintf fmt "|%a|" print_term t + | Tunop (Uopp | Usqrt as op, t) -> + let s = match op with + | Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false + in + fprintf fmt "(%s(%a))" s print_term t + | Tround (m, t) -> + fprintf fmt "(%s(%a))" m print_term t + +let print_pred fmt = function + | Pin (t, c1, c2) -> + fprintf fmt "%a in [%a, %a]" + print_term t Constant.print c1 Constant.print c2 + +let temp_file f = if !debug then f else Filename.temp_file f ".v" +let remove_file f = if not !debug then try Sys.remove f with _ -> () + +let read_gappa_proof f = + let buf = Buffer.create 1024 in + Buffer.add_char buf '('; + let cin = open_in f in + let rec skip_space () = + let c = input_char cin in if c = ' ' then skip_space () else c + in + while input_char cin <> '=' do () done; + try + while true do + let c = skip_space () in + if c = ':' then raise Exit; + Buffer.add_char buf c; + let s = input_line cin in + Buffer.add_string buf s; + Buffer.add_char buf '\n'; + done; + assert false + with Exit -> + close_in cin; + remove_file f; + Buffer.add_char buf ')'; + Buffer.contents buf + +exception GappaFailed +exception GappaProofFailed + +let patch_gappa_proof fin fout = + let cin = open_in fin in + let cout = open_out fout in + let fmt = formatter_of_out_channel cout in + let last = ref "" in + let defs = ref "" in + try + while true do + let s = input_line cin in + if s = "Qed." then + fprintf fmt "Defined.@\n" + else begin + begin + try Scanf.sscanf s "Lemma %s " + (fun n -> defs := n ^ " " ^ !defs; last := n) + with Scanf.Scan_failure _ -> + try Scanf.sscanf s "Definition %s " + (fun n -> defs := n ^ " " ^ !defs) + with Scanf.Scan_failure _ -> + () + end; + fprintf fmt "%s@\n" s + end + done + with End_of_file -> + close_in cin; + fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last; + close_out cout + +let call_gappa hl p = + let gappa_in = temp_file "gappa_input" in + let c = open_out gappa_in in + let fmt = formatter_of_out_channel c in + fprintf fmt "@[{ "; + List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl; + fprintf fmt "%a }@]@." print_pred p; + close_out c; + let gappa_out = temp_file "gappa_output" in + let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in + let out = Sys.command cmd in + if out <> 0 then raise GappaFailed; + remove_file gappa_in; + let gappa_out2 = temp_file "gappa2" in + patch_gappa_proof gappa_out gappa_out2; + remove_file gappa_out; + let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in + let out = Sys.command cmd in + if out <> 0 then raise GappaProofFailed; + let gappa_out3 = temp_file "gappa3" in + let c = open_out gappa_out3 in + let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in + Printf.fprintf c + "Require \"%s\". Set Printing Depth 9999999. Print %s.proof." + (Filename.chop_suffix gappa_out2 ".v") gappa2; + close_out c; + let lambda = temp_file "gappa_lambda" in + let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in + let out = Sys.command cmd in + if out <> 0 then raise GappaProofFailed; + remove_file gappa_out2; remove_file gappa_out3; + remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o"); + read_gappa_proof lambda + +(* 2. coq -> gappa translation *) + +exception NotGappa + +let logic_dir = ["Coq";"Logic";"Decidable"] +let coq_modules = + init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules + @ [["Coq"; "ZArith"; "BinInt"]; + ["Coq"; "Reals"; "Rdefinitions"]; + ["Coq"; "Reals"; "Raxioms";]; + ["Coq"; "Reals"; "Rbasic_fun";]; + ["Coq"; "Reals"; "R_sqrt";]; + ["Coq"; "Reals"; "Rfunctions";]; + ["Gappa"; "Gappa_tactic";]; + ["Gappa"; "Gappa_fixed";]; + ["Gappa"; "Gappa_float";]; + ["Gappa"; "Gappa_round_def";]; + ["Gappa"; "Gappa_pred_bnd";]; + ["Gappa"; "Gappa_definitions";]; + ] + +let constant = gen_constant_in_modules "gappa" coq_modules + +let coq_refl_equal = lazy (constant "refl_equal") +let coq_Rle = lazy (constant "Rle") +let coq_R = lazy (constant "R") +(* +let coq_Rplus = lazy (constant "Rplus") +let coq_Rminus = lazy (constant "Rminus") +let coq_Rmult = lazy (constant "Rmult") +let coq_Rdiv = lazy (constant "Rdiv") +let coq_powerRZ = lazy (constant "powerRZ") +let coq_R1 = lazy (constant "R1") +let coq_Ropp = lazy (constant "Ropp") +let coq_Rabs = lazy (constant "Rabs") +let coq_sqrt = lazy (constant "sqrt") +*) + +let coq_convert = lazy (constant "convert") +let coq_reUnknown = lazy (constant "reUnknown") +let coq_reFloat2 = lazy (constant "reFloat2") +let coq_reFloat10 = lazy (constant "reFloat10") +let coq_reInteger = lazy (constant "reInteger") +let coq_reBinary = lazy (constant "reBinary") +let coq_reUnary = lazy (constant "reUnary") +let coq_reRound = lazy (constant "reRound") +let coq_roundDN = lazy (constant "roundDN") +let coq_roundUP = lazy (constant "roundUP") +let coq_roundNE = lazy (constant "roundNE") +let coq_roundZR = lazy (constant "roundZR") +let coq_rounding_fixed = lazy (constant "rounding_fixed") +let coq_rounding_float = lazy (constant "rounding_float") +let coq_boAdd = lazy (constant "boAdd") +let coq_boSub = lazy (constant "boSub") +let coq_boMul = lazy (constant "boMul") +let coq_boDiv = lazy (constant "boDiv") +let coq_uoAbs = lazy (constant "uoAbs") +let coq_uoNeg = lazy (constant "uoNeg") +let coq_uoSqrt = lazy (constant "uoSqrt") +let coq_subset = lazy (constant "subset") +let coq_makepairF = lazy (constant "makepairF") + +let coq_true = lazy (constant "true") +let coq_false = lazy (constant "false") + +let coq_Z0 = lazy (constant "Z0") +let coq_Zpos = lazy (constant "Zpos") +let coq_Zneg = lazy (constant "Zneg") +let coq_xH = lazy (constant "xH") +let coq_xI = lazy (constant "xI") +let coq_xO = lazy (constant "xO") +let coq_IZR = lazy (constant "IZR") + +(* translates a closed Coq term p:positive into a FOL term of type int *) +let rec tr_positive p = match kind_of_term p with + | Term.Construct _ when p = Lazy.force coq_xH -> + 1 + | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> + 2 * (tr_positive a) + 1 + | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> + 2 * (tr_positive a) + | Term.Cast (p, _, _) -> + tr_positive p + | _ -> + raise NotGappa + +(* translates a closed Coq term t:Z into a term of type int *) +let rec tr_arith_constant t = match kind_of_term t with + | Term.Construct _ when t = Lazy.force coq_Z0 -> 0 + | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a + | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a) + | Term.Cast (t, _, _) -> tr_arith_constant t + | _ -> raise NotGappa + +(* translates a closed Coq term p:positive into a FOL term of type bigint *) +let rec tr_bigpositive p = match kind_of_term p with + | Term.Construct _ when p = Lazy.force coq_xH -> + Bigint.one + | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> + Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a)) + | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> + (Bigint.mult_2 (tr_bigpositive a)) + | Term.Cast (p, _, _) -> + tr_bigpositive p + | _ -> + raise NotGappa + +(* translates a closed Coq term t:Z into a term of type bigint *) +let rec tr_arith_bigconstant t = match kind_of_term t with + | Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero + | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a + | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> + Bigint.neg (tr_bigpositive a) + | Term.Cast (t, _, _) -> tr_arith_bigconstant t + | _ -> raise NotGappa + +let decomp c = + let c, args = decompose_app c in + kind_of_term c, args + +let tr_bool c = match decompose_app c with + | c, [] when c = Lazy.force coq_true -> true + | c, [] when c = Lazy.force coq_false -> false + | _ -> raise NotGappa + +let tr_float b m e = + (b, tr_arith_bigconstant m, tr_arith_bigconstant e) + +let tr_binop c = match decompose_app c with + | c, [] when c = Lazy.force coq_boAdd -> Bplus + | c, [] when c = Lazy.force coq_boSub -> Bminus + | c, [] when c = Lazy.force coq_boMul -> Bmult + | c, [] when c = Lazy.force coq_boDiv -> Bdiv + | _ -> assert false + +let tr_unop c = match decompose_app c with + | c, [] when c = Lazy.force coq_uoNeg -> Uopp + | c, [] when c = Lazy.force coq_uoSqrt -> Usqrt + | c, [] when c = Lazy.force coq_uoAbs -> Uabs + | _ -> raise NotGappa + +let tr_var c = match decomp c with + | Var x, [] -> string_of_id x + | _ -> assert false + +let tr_mode c = match decompose_app c with + | c, [] when c = Lazy.force coq_roundDN -> "dn" + | c, [] when c = Lazy.force coq_roundNE -> "ne" + | c, [] when c = Lazy.force coq_roundUP -> "up" + | c, [] when c = Lazy.force coq_roundZR -> "zr" + | _ -> raise NotGappa + +let tr_rounding_mode c = match decompose_app c with + | c, [a;b] when c = Lazy.force coq_rounding_fixed -> + let a = tr_mode a in + let b = tr_arith_constant b in + sprintf "fixed<%d,%s>" b a + | c, [a;p;e] when c = Lazy.force coq_rounding_float -> + let a = tr_mode a in + let p = tr_positive p in + let e = tr_arith_constant e in + sprintf "float<%d,%d,%s>" p (-e) a + | _ -> + raise NotGappa + +(* REexpr -> term *) +let rec tr_term c0 = + let c, args = decompose_app c0 in + match kind_of_term c, args with + | _, [a] when c = Lazy.force coq_reUnknown -> + Tvar (tr_var a) + | _, [a; b] when c = Lazy.force coq_reFloat2 -> + Tconst (Constant.create (tr_float 2 a b)) + | _, [a; b] when c = Lazy.force coq_reFloat10 -> + Tconst (Constant.create (tr_float 10 a b)) + | _, [a] when c = Lazy.force coq_reInteger -> + Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero)) + | _, [op;a;b] when c = Lazy.force coq_reBinary -> + Tbinop (tr_binop op, tr_term a, tr_term b) + | _, [op;a] when c = Lazy.force coq_reUnary -> + Tunop (tr_unop op, tr_term a) + | _, [op;a] when c = Lazy.force coq_reRound -> + Tround (tr_rounding_mode op, tr_term a) + | _ -> + msgnl (str "tr_term: " ++ Printer.pr_constr c0); + assert false + +let tr_rle c = + let c, args = decompose_app c in + match kind_of_term c, args with + | _, [a;b] when c = Lazy.force coq_Rle -> + begin match decompose_app a, decompose_app b with + | (ac, [at]), (bc, [bt]) + when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert -> + at, bt + | _ -> + raise NotGappa + end + | _ -> + raise NotGappa + +let tr_pred c = + let c, args = decompose_app c in + match kind_of_term c, args with + | _, [a;b] when c = build_coq_and () -> + begin match tr_rle a, tr_rle b with + | (c1, t1), (t2, c2) when t1 = t2 -> + begin match tr_term c1, tr_term c2 with + | Tconst c1, Tconst c2 -> + Pin (tr_term t1, c1, c2) + | _ -> + raise NotGappa + end + | _ -> + raise NotGappa + end + | _ -> + raise NotGappa + +let is_R c = match decompose_app c with + | c, [] when c = Lazy.force coq_R -> true + | _ -> false + +let tr_hyps = + List.fold_left + (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) [] + +let constr_of_string gl s = + let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in + Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s) + +let var_name = function + | Name id -> + let s = string_of_id id in + let s = String.sub s 1 (String.length s - 1) in + mkVar (id_of_string s) + | Anonymous -> + assert false + +let build_proof_term c0 = + let bl,c = decompose_lam c0 in + List.fold_right + (fun (x,t) pf -> + mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |])) + bl c0 + +let gappa_internal gl = + try + let c = tr_pred (pf_concl gl) in + let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in + let pf = constr_of_string gl s in + let pf = build_proof_term pf in + Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl + with + | NotGappa -> error "not a gappa goal" + | GappaFailed -> error "gappa failed" + | GappaProofFailed -> error "incorrect gappa proof term" + +let gappa_prepare = + let id = Ident (dummy_loc, id_of_string "gappa_prepare") in + lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id))) + +let gappa gl = + Coqlib.check_required_library ["Gappa"; "Gappa_tactic"]; + Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl + +(* +Local Variables: +compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt" +End: +*) + diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml deleted file mode 100644 index d5376b8d..00000000 --- a/contrib/dp/dp_simplify.ml +++ /dev/null @@ -1,117 +0,0 @@ - -open Format -open Fol - -let is_simplify_ident s = - let is_simplify_char = function - | 'a'..'z' | 'A'..'Z' | '0'..'9' -> true - | _ -> false - in - try - String.iter (fun c -> if not (is_simplify_char c) then raise Exit) s; true - with Exit -> - false - -let ident fmt s = - if is_simplify_ident s then fprintf fmt "%s" s else fprintf fmt "|%s|" s - -let rec print_list sep print fmt = function - | [] -> () - | [x] -> print fmt x - | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r - -let space fmt () = fprintf fmt "@ " -let comma fmt () = fprintf fmt ",@ " - -let rec print_term fmt = function - | Cst n -> - fprintf fmt "%d" n - | Plus (a, b) -> - fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b - | Moins (a, b) -> - fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b - | Mult (a, b) -> - fprintf fmt "@[(*@ %a@ %a)@]" print_term a print_term b - | Div (a, b) -> - fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b - | App (id, []) -> - fprintf fmt "%a" ident id - | App (id, tl) -> - fprintf fmt "@[(%a@ %a)@]" ident id print_terms tl - -and print_terms fmt tl = - print_list space print_term fmt tl - -let rec print_predicate fmt p = - let pp = print_predicate in - match p with - | True -> - fprintf fmt "TRUE" - | False -> - fprintf fmt "FALSE" - | Fatom (Eq (a, b)) -> - fprintf fmt "@[(EQ %a@ %a)@]" print_term a print_term b - | Fatom (Le (a, b)) -> - fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b - | Fatom (Lt (a, b))-> - fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b - | Fatom (Ge (a, b)) -> - 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 "@[(EQ (%a@ %a) |@@true|)@]" ident id print_terms tl - | Imp (a, b) -> - fprintf fmt "@[(IMPLIES@ %a@ %a)@]" pp a pp b - | And (a, b) -> - fprintf fmt "@[(AND@ %a@ %a)@]" pp a pp b - | Or (a, b) -> - fprintf fmt "@[(OR@ %a@ %a)@]" pp a pp b - | Not a -> - fprintf fmt "@[(NOT@ %a)@]" pp a - | Forall (id, _, p) -> - fprintf fmt "@[(FORALL (%a)@ %a)@]" ident id pp p - | Exists (id, _, p) -> - fprintf fmt "@[(EXISTS (%a)@ %a)@]" ident id pp p - -(** -let rec string_list l = match l with - [] -> "" - | [e] -> e - | e::l' -> e ^ " " ^ (string_list l') -**) - -let print_query fmt (decls,concl) = - let print_decl = function - | DeclVar (id, [], t) -> - fprintf fmt "@[;; %s : %s@]@\n" id t - | DeclVar (id, l, t) -> - fprintf fmt "@[;; %s : %a -> %s@]@\n" - id (print_list comma pp_print_string) l t - | DeclPred (id, []) -> - fprintf fmt "@[;; %s : BOOLEAN @]@\n" id - | DeclPred (id, l) -> - fprintf fmt "@[;; %s : %a -> BOOLEAN@]@\n" - id (print_list comma pp_print_string) l - | DeclType id -> - fprintf fmt "@[;; %s : TYPE@]@\n" id - | Assert (id, f) -> - fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f - in - List.iter print_decl decls; - fprintf fmt "%a@." print_predicate concl - -let call q = - let f = Filename.temp_file "coq_dp" ".sx" in - let c = open_out f in - let fmt = formatter_of_out_channel c in - fprintf fmt "@[%a@]@." print_query q; - close_out c; - ignore (Sys.command (sprintf "cat %s" f)); - let cmd = - sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" f - in - prerr_endline cmd; flush stderr; - let out = Sys.command cmd in - if out = 0 then Valid else if out = 1 then Invalid else Timeout - (* TODO: effacer le fichier f et le fichier out *) diff --git a/contrib/dp/dp_simplify.mli b/contrib/dp/dp_simplify.mli deleted file mode 100644 index 03b6d347..00000000 --- a/contrib/dp/dp_simplify.mli +++ /dev/null @@ -1,4 +0,0 @@ - -open Fol - -val call : query -> prover_answer diff --git a/contrib/dp/dp_sorts.ml b/contrib/dp/dp_sorts.ml deleted file mode 100644 index 7dbdfa56..00000000 --- a/contrib/dp/dp_sorts.ml +++ /dev/null @@ -1,51 +0,0 @@ - -open Fol - -let term_has_sort x s = Fatom (Pred ("%sort_" ^ s, [x])) - -let has_sort x s = term_has_sort (App (x, [])) s - -let rec form = function - | True | False | Fatom _ as f -> f - | Imp (f1, f2) -> Imp (form f1, form f2) - | And (f1, f2) -> And (form f1, form f2) - | Or (f1, f2) -> Or (form f1, form f2) - | Not f -> Not (form f) - | Forall (x, ("INT" as t), f) -> Forall (x, t, form f) - | Forall (x, t, f) -> Forall (x, t, Imp (has_sort x t, form f)) - | Exists (x, ("INT" as t), f) -> Exists (x, t, form f) - | Exists (x, t, f) -> Exists (x, t, Imp (has_sort x t, form f)) - -let sort_ax = let r = ref 0 in fun () -> incr r; "sort_ax_" ^ string_of_int !r - -let hyp acc = function - | Assert (id, f) -> - (Assert (id, form f)) :: acc - | DeclVar (id, _, "INT") as d -> - d :: acc - | DeclVar (id, [], t) as d -> - (Assert (sort_ax (), has_sort id t)) :: d :: acc - | DeclVar (id, l, t) as d -> - let n = ref 0 in - let xi = - List.fold_left - (fun l t -> incr n; ("x" ^ string_of_int !n, t) :: l) [] l - in - let f = - List.fold_left - (fun f (x,t) -> if t = "INT" then f else Imp (has_sort x t, f)) - (term_has_sort - (App (id, List.rev_map (fun (x,_) -> App (x,[])) xi)) t) - xi - in - let f = List.fold_left (fun f (x,t) -> Forall (x, t, f)) f xi in - (Assert (sort_ax (), f)) :: d :: acc - | DeclPred _ as d -> - d :: acc - | DeclType t as d -> - (DeclPred ("%sort_" ^ t, [t])) :: d :: acc - -let query (hyps, f) = - let hyps' = List.fold_left hyp [] hyps in - List.rev hyps', form f - diff --git a/contrib/dp/dp_sorts.mli b/contrib/dp/dp_sorts.mli deleted file mode 100644 index 9e74f997..00000000 --- a/contrib/dp/dp_sorts.mli +++ /dev/null @@ -1,4 +0,0 @@ - -open Fol - -val query : query -> query diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml index e1ddb039..e24049ad 100644 --- a/contrib/dp/dp_why.ml +++ b/contrib/dp/dp_why.ml @@ -4,6 +4,18 @@ open Format open Fol +type proof = + | Immediate of Term.constr + | Fun_def of string * (string * typ) list * typ * term + +let proofs = Hashtbl.create 97 +let proof_name = + let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r + +let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n + +let find_proof = Hashtbl.find proofs + let rec print_list sep print fmt = function | [] -> () | [x] -> print fmt x diff --git a/contrib/dp/dp_why.mli b/contrib/dp/dp_why.mli new file mode 100644 index 00000000..b38a3d37 --- /dev/null +++ b/contrib/dp/dp_why.mli @@ -0,0 +1,17 @@ + +open Fol + +(* generation of the Why file *) + +val output_file : string -> query -> unit + +(* table to translate the proofs back to Coq (used in dp_zenon) *) + +type proof = + | Immediate of Term.constr + | Fun_def of string * (string * typ) list * typ * term + +val add_proof : proof -> string +val find_proof : string -> proof + + diff --git a/contrib/dp/dp_zenon.ml b/contrib/dp/dp_zenon.ml deleted file mode 100644 index 57b0a44f..00000000 --- a/contrib/dp/dp_zenon.ml +++ /dev/null @@ -1,103 +0,0 @@ - -open Format -open Fol - -let rec print_list sep print fmt = function - | [] -> () - | [x] -> print fmt x - | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r - -let space fmt () = fprintf fmt "@ " - -let rec print_term fmt = function - | Cst n -> - fprintf fmt "%d" n - | Plus (a, b) -> - fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b - | Moins (a, b) -> - fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b - | Mult (a, b) -> - fprintf fmt "@[(*@ %a@ %a)@]" print_term a print_term b - | Div (a, b) -> - fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b - | App (id, []) -> - fprintf fmt "%s" id - | App (id, tl) -> - fprintf fmt "@[(%s@ %a)@]" id print_terms tl - -and print_terms fmt tl = - print_list space print_term fmt tl - -let rec print_predicate fmt p = - let pp = print_predicate in - match p with - | True -> - fprintf fmt "True" - | False -> - fprintf fmt "False" - | Fatom (Eq (a, b)) -> - fprintf fmt "@[(= %a@ %a)@]" print_term a print_term b - | Fatom (Le (a, b)) -> - fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b - | Fatom (Lt (a, b))-> - fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b - | Fatom (Ge (a, b)) -> - 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 - | Imp (a, b) -> - fprintf fmt "@[(=>@ %a@ %a)@]" pp a pp b - | And (a, b) -> - fprintf fmt "@[(/\\@ %a@ %a)@]" pp a pp b - | Or (a, b) -> - fprintf fmt "@[(\\/@ %a@ %a)@]" pp a pp b - | Not a -> - fprintf fmt "@[(-.@ %a)@]" pp a - | Forall (id, t, p) -> - fprintf fmt "@[(A. ((%s \"%s\")@ %a))@]" id t pp p - | Exists (id, t, p) -> - fprintf fmt "@[(E. ((%s \"%s\")@ %a))@]" id t pp p - -let rec string_of_type_list = function - | [] -> "" - | 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 - | DeclVar (id, l, t) -> - fprintf fmt "@[;; %s: %s%s@]@\n" - id (string_of_type_list l) t - | DeclPred (id, l) -> - fprintf fmt "@[;; %s: %sBOOLEAN@]@\n" - id (string_of_type_list l) - | DeclType id -> - fprintf fmt "@[;; %s: TYPE@]@\n" id - | Assert (id, f) -> - fprintf fmt "@[\"%s\" %a@]@\n" id print_predicate f - in - List.iter print_decl decls; - fprintf fmt "$goal %a@." print_predicate concl - -let call q = - let f = Filename.temp_file "coq_dp" ".znn" in - let c = open_out f in - let fmt = formatter_of_out_channel c in - fprintf fmt "@[%a@]@." print_query q; - close_out c; - ignore (Sys.command (sprintf "cat %s" f)); - let cmd = - sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" f - in - prerr_endline cmd; flush stderr; - let out = Sys.command cmd in - if out = 0 then Valid - else if out = 1 then Invalid - else if out = 137 then Timeout - else Util.anomaly "malformed Zenon input file" - (* TODO: effacer le fichier f et le fichier out *) - - diff --git a/contrib/dp/dp_zenon.mli b/contrib/dp/dp_zenon.mli index 03b6d347..0a727d1f 100644 --- a/contrib/dp/dp_zenon.mli +++ b/contrib/dp/dp_zenon.mli @@ -1,4 +1,7 @@ open Fol -val call : query -> prover_answer +val set_debug : bool -> unit + +val proof_from_file : string -> Proof_type.tactic + diff --git a/contrib/dp/dp_zenon.mll b/contrib/dp/dp_zenon.mll new file mode 100644 index 00000000..2fc2a5f4 --- /dev/null +++ b/contrib/dp/dp_zenon.mll @@ -0,0 +1,181 @@ + +{ + + open Lexing + open Pp + open Util + open Names + open Tacmach + open Dp_why + open Tactics + open Tacticals + + let debug = ref false + let set_debug b = debug := b + + let buf = Buffer.create 1024 + + let string_of_global env ref = + Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref) + + let axioms = ref [] + + (* we cannot interpret the terms as we read them (since some lemmas + may need other lemmas to be already interpreted) *) + type lemma = { l_id : string; l_type : string; l_proof : string } + type zenon_proof = lemma list * string + +} + +let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+ +let space = [' ' '\t' '\r'] + +rule start = parse +| "(* BEGIN-PROOF *)" "\n" { scan lexbuf } +| _ { start lexbuf } +| eof { anomaly "malformed Zenon proof term" } + +(* here we read the lemmas and the main proof term; + meanwhile we maintain the set of axioms that were used *) + +and scan = parse +| "Let" space (ident as id) space* ":" + { let t = read_coq_term lexbuf in + let p = read_lemma_proof lexbuf in + let l,pr = scan lexbuf in + { l_id = id; l_type = t; l_proof = p } :: l, pr } +| "Definition theorem:" + { let t = read_main_proof lexbuf in [], t } +| _ | eof + { anomaly "malformed Zenon proof term" } + +and read_coq_term = parse +| "." "\n" + { let s = Buffer.contents buf in Buffer.clear buf; s } +| "coq__" (ident as id) (* a Why keyword renamed *) + { Buffer.add_string buf id; read_coq_term lexbuf } +| ("dp_axiom__" ['0'-'9']+) as id + { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf } +| _ as c + { Buffer.add_char buf c; read_coq_term lexbuf } +| eof + { anomaly "malformed Zenon proof term" } + +and read_lemma_proof = parse +| "Proof" space + { read_coq_term lexbuf } +| _ | eof + { anomaly "malformed Zenon proof term" } + +(* skip the main proof statement and then read its term *) +and read_main_proof = parse +| ":=" "\n" + { read_coq_term lexbuf } +| _ + { read_main_proof lexbuf } +| eof + { anomaly "malformed Zenon proof term" } + + +{ + + let read_zenon_proof f = + Buffer.clear buf; + let c = open_in f in + let lb = from_channel c in + let p = start lb in + close_in c; + if not !debug then begin try Sys.remove f with _ -> () end; + p + + let constr_of_string gl s = + let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in + Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s) + + (* we are lazy here: we build strings containing Coq terms using a *) + (* pretty-printer Fol -> Coq *) + module Coq = struct + open Format + open Fol + + let rec print_list sep print fmt = function + | [] -> () + | [x] -> print fmt x + | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r + + let space fmt () = fprintf fmt "@ " + let comma fmt () = fprintf fmt ",@ " + + let rec print_typ fmt = function + | Tvar x -> fprintf fmt "%s" x + | Tid ("int", []) -> fprintf fmt "Z" + | Tid (x, []) -> fprintf fmt "%s" x + | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t + | Tid (x,tl) -> + fprintf fmt "(%s %a)" x (print_list comma print_typ) tl + + let rec print_term fmt = function + | Cst n -> + fprintf fmt "%d" n + | Plus (a, b) -> + fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b + | Moins (a, b) -> + fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b + | Mult (a, b) -> + fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b + | Div (a, b) -> + fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b + | App (id, []) -> + fprintf fmt "%s" id + | App (id, tl) -> + fprintf fmt "@[(%s %a)@]" id print_terms tl + + and print_terms fmt tl = + print_list space print_term fmt tl + + (* builds the text for "forall vars, f vars = t" *) + let fun_def_axiom f vars t = + let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in + fprintf str_formatter + "@[(forall %a, %s %a = %a)@]@." + (print_list space binder) vars f + (print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars + print_term t; + flush_str_formatter () + + end + + let prove_axiom id = match Dp_why.find_proof id with + | Immediate t -> + exact_check t + | Fun_def (f, vars, ty, t) -> + tclTHENS + (fun gl -> + let s = Coq.fun_def_axiom f vars t in + if !debug then Format.eprintf "axiom fun def = %s@." s; + let c = constr_of_string gl s in + assert_tac true (Name (id_of_string id)) c gl) + [tclTHEN intros reflexivity; tclIDTAC] + + let exact_string s gl = + let c = constr_of_string gl s in + exact_check c gl + + let interp_zenon_proof (ll,p) = + let interp_lemma l gl = + let ty = constr_of_string gl l.l_type in + tclTHENS + (assert_tac true (Name (id_of_string l.l_id)) ty) + [exact_string l.l_proof; tclIDTAC] + gl + in + tclTHEN (tclMAP interp_lemma ll) (exact_string p) + + let proof_from_file f = + axioms := []; + msgnl (str "proof_from_file " ++ str f); + let zp = read_zenon_proof f in + msgnl (str "proof term is " ++ str (snd zp)); + tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp) + +} diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli index a85469cc..b94bd3e3 100644 --- a/contrib/dp/fol.mli +++ b/contrib/dp/fol.mli @@ -45,4 +45,11 @@ type query = decl list * form (* prover result *) -type prover_answer = Valid | Invalid | DontKnow | Timeout +type prover_answer = + | Valid of string option + | Invalid + | DontKnow + | Timeout + | NoAnswer + | Failure of string + diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4 index eb7fb73b..99bcf477 100644 --- a/contrib/dp/g_dp.ml4 +++ b/contrib/dp/g_dp.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_dp.ml4 7165 2005-06-24 12:56:46Z coq $ *) +(* $Id: g_dp.ml4 10924 2008-05-13 14:01:11Z filliatr $ *) open Dp @@ -16,6 +16,14 @@ TACTIC EXTEND Simplify [ "simplify" ] -> [ simplify ] END +TACTIC EXTEND Ergo + [ "ergo" ] -> [ ergo ] +END + +TACTIC EXTEND Yices + [ "yices" ] -> [ yices ] +END + TACTIC EXTEND CVCLite [ "cvcl" ] -> [ cvc_lite ] END @@ -28,6 +36,18 @@ TACTIC EXTEND Zenon [ "zenon" ] -> [ zenon ] END +TACTIC EXTEND Gwhy + [ "gwhy" ] -> [ gwhy ] +END + +TACTIC EXTEND Gappa_internal + [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ] +END + +TACTIC EXTEND Gappa + [ "gappa" ] -> [ Dp_gappa.gappa ] +END + (* should be part of basic tactics syntax *) TACTIC EXTEND admit [ "admit" ] -> [ Tactics.admit_as_an_axiom ] @@ -36,3 +56,24 @@ END VERNAC COMMAND EXTEND Dp_hint [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ] END + +VERNAC COMMAND EXTEND Dp_timeout +| [ "Dp_timeout" natural(n) ] -> [ dp_timeout n ] +END + +VERNAC COMMAND EXTEND Dp_prelude +| [ "Dp_prelude" string_list(l) ] -> [ dp_prelude l ] +END + +VERNAC COMMAND EXTEND Dp_predefined +| [ "Dp_predefined" global(g) "=>" string(s) ] -> [ dp_predefined g s ] +END + +VERNAC COMMAND EXTEND Dp_debug +| [ "Dp_debug" ] -> [ dp_debug true; Dp_zenon.set_debug true ] +END + +VERNAC COMMAND EXTEND Dp_trace +| [ "Dp_trace" ] -> [ dp_trace true ] +END + diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v index 4e933a3c..3e4c0f6d 100644 --- a/contrib/dp/test2.v +++ b/contrib/dp/test2.v @@ -5,6 +5,10 @@ Require Import List. Open Scope list_scope. Open Scope Z_scope. +Dp_debug. +Dp_timeout 3. +Require Export zenon. + Definition neg (z:Z) : Z := match z with | Z0 => Z0 | Zpos p => Zneg p @@ -18,9 +22,7 @@ Open Scope nat_scope. Print plus. Goal forall x, x+0=x. - induction x. - zenon. - zenon. + induction x; ergo. (* simplify resoud le premier, pas le second *) Admitted. diff --git a/contrib/dp/test_gappa.v b/contrib/dp/test_gappa.v new file mode 100644 index 00000000..eb65a59d --- /dev/null +++ b/contrib/dp/test_gappa.v @@ -0,0 +1,91 @@ +Require Export Gappa_tactic. +Require Export Reals. + +Open Scope Z_scope. +Open Scope R_scope. + +Lemma test_base10 : + forall x y:R, + 0 <= x <= 4 -> + 0 <= x * (24 * powerRZ 10 (-1)) <= 10. +Proof. + gappa. +Qed. + +(* +@rnd = float< ieee_32, zr >; +a = rnd(a_); b = rnd(b_); +{ a in [3.2,3.3] /\ b in [1.4,1.9] -> + rnd(a - b) - (a - b) in [0,0] } +*) + +Definition rnd := gappa_rounding (rounding_float roundZR 43 (120)). + +Lemma test_float3 : + forall a_ b_ a b : R, + a = rnd a_ -> + b = rnd b_ -> + 52 / 16 <= a <= 53 / 16 -> + 22 / 16 <= b <= 30 / 16 -> + 0 <= rnd (a - b) - (a - b) <= 0. +Proof. + unfold rnd. + gappa. +Qed. + +Lemma test_float2 : + forall x y:R, + 0 <= x <= 1 -> + 0 <= y <= 1 -> + 0 <= gappa_rounding (rounding_float roundNE 53 (1074)) (x+y) <= 2. +Proof. + gappa. +Qed. + +Lemma test_float1 : + forall x y:R, + 0 <= gappa_rounding (rounding_fixed roundDN (0)) x - + gappa_rounding (rounding_fixed roundDN (0)) y <= 0 -> + Rabs (x - y) <= 1. +Proof. + gappa. +Qed. + +Lemma test1 : + forall x y:R, + 0 <= x <= 1 -> + 0 <= -y <= 1 -> + 0 <= x * (-y) <= 1. +Proof. + gappa. +Qed. + +Lemma test2 : + forall x y:R, + 3/4 <= x <= 3 -> + 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)). +Proof. + gappa. +Qed. + +Lemma test3 : + forall x y z:R, + 0 <= x - y <= 3 -> + -2 <= y - z <= 4 -> + -2 <= x - z <= 7. +Proof. + gappa. +Qed. + +Lemma test4 : + forall x1 x2 y1 y2 : R, + 1 <= Rabs y1 <= 1000 -> + 1 <= Rabs y2 <= 1000 -> + - powerRZ 2 (-53) <= (x1 - y1) / y1 <= powerRZ 2 (-53) -> + - powerRZ 2 (-53) <= (x2 - y2) / y2 <= powerRZ 2 (-53) -> + - powerRZ 2 (-51) <= (x1 * x2 - y1 * y2) / (y1 * y2) <= powerRZ 2 (-51). +Proof. + gappa. +Qed. + + diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v index 52a57a0c..a6d4f2e1 100644 --- a/contrib/dp/tests.v +++ b/contrib/dp/tests.v @@ -2,48 +2,115 @@ Require Import ZArith. Require Import Classical. +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. -zenon. +simplify. Qed. - (* Examples in the Propositional Calculus and theory of equality *) Parameter A C : Prop. Goal A -> A. -zenon. +simplify. Qed. Goal A -> (A \/ C). -zenon. +simplify. Qed. Parameter x y z : Z. Goal x = y -> y = z -> x = z. - -zenon. +ergo. Qed. Goal ((((A -> C) -> A) -> A) -> C) -> C. -zenon. +ergo. Qed. - (* Arithmetic *) Open Scope Z_scope. Goal 1 + 1 = 2. -simplify. +yices. Qed. @@ -57,14 +124,12 @@ Qed. Goal (forall (x y : Z), x = y) -> 0=1. try zenon. -simplify. +ergo. Qed. Goal forall (x: nat), (x + 0 = x)%nat. -induction x0. -zenon. -zenon. +induction x0; ergo. Qed. @@ -106,7 +171,7 @@ Inductive even : Z -> Prop := unlike CVC Lite *) Goal even 4. -cvcl. +ergo. Qed. @@ -115,8 +180,7 @@ 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. +yices. Qed. @@ -133,8 +197,7 @@ Dp_hint add_S. unlike zenon *) Goal forall n : nat, add n 0 = n. - -induction n ; zenon. +induction n ; yices. Qed. @@ -144,8 +207,8 @@ Definition pred (n : nat) : nat := match n with end. Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat. - -zenon. +yices. +(*zenon.*) Qed. @@ -157,7 +220,7 @@ end. Goal forall n : nat, plus n 0%nat = n. -induction n; zenon. +induction n; ergo. Qed. @@ -173,8 +236,11 @@ with odd_b (n : nat) : bool := match n with end. Goal even_b (S (S O)) = true. - +ergo. +(* +simplify. zenon. +*) Qed. @@ -184,7 +250,8 @@ 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. +yices. +(*zenon.*) Qed. @@ -194,7 +261,8 @@ Qed. Parameter poly_f : forall A:Set, A->A. Goal forall x:nat, poly_f nat x = poly_f nat x. -zenon. +ergo. +(*zenon.*) Qed. diff --git a/contrib/dp/zenon.v b/contrib/dp/zenon.v new file mode 100644 index 00000000..4ad00a11 --- /dev/null +++ b/contrib/dp/zenon.v @@ -0,0 +1,94 @@ +(* Copyright 2004 INRIA *) +(* $Id: zenon.v 10739 2008-04-01 14:45:20Z herbelin $ *) + +Require Export Classical. + +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. -- cgit v1.2.3