diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/ExternalProvers.tex | 58 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
| -rw-r--r-- | plugins/dp/dp_gappa.ml | 445 | ||||
| -rw-r--r-- | plugins/dp/g_dp.ml4 | 8 | ||||
| -rw-r--r-- | plugins/dp/test_gappa.v | 91 |
6 files changed, 1 insertions, 603 deletions
@@ -31,6 +31,7 @@ Tactics when one knows which side is true. - Tactic "exists" and "eexists" supports iteration using comma-separated arguments. +- Tactic "gappa" has been removed from the Dp plugin. Tactic Language diff --git a/doc/refman/ExternalProvers.tex b/doc/refman/ExternalProvers.tex deleted file mode 100644 index b1a9a3740..000000000 --- a/doc/refman/ExternalProvers.tex +++ /dev/null @@ -1,58 +0,0 @@ - -\achapter{Calling external provers} - -\asection{The \texttt{gappa} tactic} -\aauthor{Sylvie Boldo, Guillaume Melquiond, Jean-Christophe Filliātre} -\tacindex{gappa} - -The \texttt{gappa} tactic invokes the Gappa -tool\footnote{\url{http://lipforge.ens-lyon.fr/www/gappa/}} to solve -properties about floating-point or fixed-point arithmetic. It can also -solve simple inequalities over real numbers. - -The Gappa tool must be installed and its executable (called -\texttt{gappa}) must be in the user program path. The Coq support -library for Gappa must also be installed (it is available from Gappa's -web site). This library provides a \texttt{Gappa\_tactic} module, -which must be loaded for the tactic to work properly. - -The \texttt{gappa} tactic only handles goals and hypotheses that are -double inequalities $f_1 \le e \le f_2$ where $f_1$ and $f_2$ are -dyadic constants and $e$ a real-valued expression. Here is an example -of a goal solved by \texttt{gappa}: -\begin{verbatim} -Lemma test_gappa : - forall x y:R, - 3/4 <= x <= 3 -> - 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)). -Proof. - gappa. -Qed. -\end{verbatim} - -Gappa supports floating-point rounding operations (as functions over -real numbers). Here is an example involving double-precision -floating-point numbers with rounding toward zero: -\begin{verbatim} -Definition rnd := gappa_rounding (rounding_float roundZR 53 1074). - -Lemma test_gappa2 : - 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. -\end{verbatim} -The function \texttt{gappa\_rounding} declares a rounding mode -recognized by the \texttt{gappa} tactic. Rounding modes are built -using constants such as \texttt{rounding\_float} and -\texttt{roundZR} provided by the Gappa support library. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 2a6dfe035..946bfda12 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -110,7 +110,6 @@ Options A and B of the licence are {\em not} elected.} \include{Program.v}% \include{Polynom.v}% = Ring \include{Setoid.v}% Tactique pour les setoides -\include{ExternalProvers}% Tactiques appelant des prouveurs externes %BEGIN LATEX \RefManCutCommand{ENDADDENDUM=\thepage} %END LATEX diff --git a/plugins/dp/dp_gappa.ml b/plugins/dp/dp_gappa.ml deleted file mode 100644 index 9c035aa85..000000000 --- a/plugins/dp/dp_gappa.ml +++ /dev/null @@ -1,445 +0,0 @@ - -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 = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ 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 999999. Print %s.proof." - (Filename.chop_suffix gappa_out2 ".v") gappa2; - close_out c; - let lambda = temp_file "gappa_lambda" in - let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ 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/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 index 4842e36aa..e027c882e 100644 --- a/plugins/dp/g_dp.ml4 +++ b/plugins/dp/g_dp.ml4 @@ -44,14 +44,6 @@ 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 ] diff --git a/plugins/dp/test_gappa.v b/plugins/dp/test_gappa.v deleted file mode 100644 index eb65a59d6..000000000 --- a/plugins/dp/test_gappa.v +++ /dev/null @@ -1,91 +0,0 @@ -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. - - |