Coq tactic:

- documentation
- better error message when prover name is invalid
- no shortcut tactic ae, Z3, etc. anymore
parent 1dcd6400
......@@ -2,4 +2,64 @@
\label{chap:tactic}
\index{Coq proof assistant}
\todo{}
\why\ provides a Coq tactic to call external theorem provers as oracles.
\section{Installation}
You need Coq version 8.3 or greater. If this is the case, \why's
configuration detects it, then compiles and installs the Coq tactic.
The Coq tactic is installed in
\begin{center}
\textit{why3-lib-dir}\texttt{/coq-tactic/}
\end{center}
where \textit{why3-lib-dir} is \why's library directory, that is typically
\texttt{/usr/lib/why3} or \texttt{/usr/local/lib/why3}. This directory
is automatically added to Coq's load path if you are
calling Coq via \why (from \texttt{why3ide}, \texttt{why3replayer},
etc.). If you are calling Coq by yourself, you need to add
this directory to Coq's load path, either using Coq's command line
option \texttt{-I} or by adding
\begin{center}
\verb+Add LoadPath "+\textit{why3-lib-dir}\verb+/coq-tactic/".+
\end{center}
to your \texttt{\~{}/.coqrc} resource file.
\section{Usage}
The Coq tactic is called \texttt{why3} and is used as follows:
\begin{center}
\texttt{why3} \verb+"+\textit{prover-name}\verb+"+
$[$\texttt{timelimit} \textit{n}$]$.
\end{center}
The string \textit{prover-name} identifies one of the automated theorem provers
supported by \why, as reported by \verb+why3 --list-provers+.
The current goal is then translated to \why's logic and the prover is
called. If it reports the goal to be valid, then Coq's \texttt{admit}
tactic is used to assume the goal. The prover is called with a time
limit in seconds as given by \why's configuration file
(see page~\pageref{sec:whyconffile}). A different value may be given
using the \texttt{timelimit} keyword.
\paragraph{Error messages.} The following errors may be reported by
the Coq tactic.
\begin{description}
\item[\texttt{Not a first order goal}] ~\par
The Coq goal could not be translated to \why's logic.
\item[\texttt{Timeout}] ~\par
There was no answer from the prover within the given time limit.
\item[\texttt{Don't know}] ~\par
The prover stopped without validating the goal.
\item[\texttt{Invalid}] ~\par
The prover stopped, reporting the goal to be invalid.
\item[\texttt{Failure}] ~\par
The prover failed. Depending on the message that follows, you may
want to file a bug report, either to the \why\ developers or to the
prover developers.
\end{description}
%%% Local Variables:
%%% mode: latex
%%% compile-command: "make -C .. doc"
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
......@@ -846,6 +846,7 @@ to verified goals.
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}
\todo{THIS SECTION IS OUTDATED}
......
......@@ -13,6 +13,8 @@ Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
Require Import Why3.
(* Why3 goal *)
Theorem Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
((0%Z <= m)%Z -> ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
......@@ -21,11 +23,8 @@ intros x n m Hn Hm.
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
why3 "alt-ergo".
(*
ae.
ca marche !!
*)
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
......@@ -36,6 +35,7 @@ rewrite Hind; auto with zarith.
rewrite (Power_s x n0).
ring.
omega.
*)
Qed.
This diff is collapsed.
......@@ -160,13 +160,8 @@ Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) ->
((range a n) -> (surjective a n)).
(*
Add LoadPath "~/why3/src/coq-plugin".
Declare ML Module "whytac".
Ltac ae := why3 "alt-ergo".
*)
Require Import Why3.
Ltac ae := why3 "alt-ergo".
(* Why3 goal *)
Theorem permutation : forall (a:Type), forall (a1:(sparse_array a)),
......
......@@ -137,11 +137,11 @@
shape="ais_eltV0V1Iainfix &lt;V1alengthV0Aainfix &lt;=c0V1FIainfix =acardV0alengthV0Iasa_invV0F">
<proof
prover="2"
timelimit="15"
timelimit="10"
edited="vacid_0_sparse_array_WP_SparseArray_permutation_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.10"/>
<result status="valid" time="1.15"/>
</proof>
</goal>
<goal
......
Declare ML Module "why3tac".
Ltac ae := why3 "alt-ergo".
Ltac Z3 := why3 "z3-2".
Ltac spass := why3 "spass".
......@@ -24,4 +24,5 @@ open Why3tac
TACTIC EXTEND Why3
[ "why3" string(s) ] -> [ why3tac s ]
| [ "why3" string(s) "timelimit" integer(n) ] -> [ why3tac ~timelimit:n s ]
END
......@@ -3,6 +3,8 @@ Require Export ZArith.
Open Scope Z_scope.
Require Export List.
Ltac ae := why3 "alt-ergo".
Section S0.
Variable a:Set->Set.
......
......@@ -1085,7 +1085,7 @@ let tr_top_decl = function
| _, Lib.ClosedSection _
| _, Lib.FrozenState _ -> ()
let why3tac s gl =
let why3tac ?(timelimit=timelimit) s gl =
(* print_dep Format.err_formatter; *)
let concl_type = pf_type_of gl (pf_concl gl) in
if not (is_Prop concl_type) then error "Conclusion is not a Prop";
......@@ -1113,6 +1113,13 @@ let why3tac s gl =
| NotFO ->
if debug then Printexc.print_backtrace stderr; flush stderr;
error "Not a first order goal"
| Whyconf.ProverNotFound (_, s) ->
let pl = Mprover.fold (fun _ p l -> p.id :: l)
(get_provers config) [] in
let msg = pr_str "No such prover `" ++ pr_str s ++ pr_str "'." ++
pr_spc () ++ pr_str "Available provers are:" ++ pr_fnl () ++
prlist (fun s -> pr_str s ++ pr_fnl ()) (List.rev pl) in
errorlabstrm "Whyconf.ProverNotFound" msg
| e ->
Printexc.print_backtrace stderr; flush stderr;
Format.eprintf "@[exception: %a@]@." Exn_printer.exn_printer e;
......@@ -1120,6 +1127,6 @@ let why3tac s gl =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. src/coq-plugin/why3tac.cmxs"
compile-command: "unset LANG; make -C ../.. lib/coq-tactic/why3tac.cmxs"
End:
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment