VplTactic (A Coq Tactic from Verified Polyhedra Library)
Current version: 0.4.2
The VPL is an Ocaml library allowing to compute with convex polyhedra. It provides standard operators -- certified in Coq -- to use this library as an abstract domain of polyhedra.
The VplTactic is a tactic to solve arithmetic goals in Coq. It is
implemented through a Coq plugin that invokes the guard operator of
the VPL. The main feature of our tactic with respect to similar
lia) is that our tactic never
fails. Indeed, when it can not prove the goal, it tries to simplify
the goal and in particular to replace inequalities by equalities. See
examples below. Currently, this tactic is highly experimental and it only works on
which is a canonical type of rationals.
If you find a bug or have any comment, please contact us
Main Contributors: Alexandre Maréchal and Sylvain Boulmé. Developed at Verimag and supported by ANR Verasco and ERC Stator.
First, add the following lines at the head of your Coq files:
Require Import BinInt. Require Import VplTactic.Tactic. Add Field Qcfield: Qcft (decidable Qc_eq_bool_correct, constants [vpl_cte]).
VplTactic.Tactic actually provides several variants of our tactic.
The most complex is
Lemma ex_intro (x: Qc) (f: Qc -> Qc): x <= 1 -> (f x) < (f 1) -> x < 1. Proof. vpl_auto. Qed.
vpl_auto is a macro for
vpl_reduce; vpl_post where
is the main call to the VPL oracle. It try to find a polyhedron in
your goal and then, it simplifies this polyhedron.
For example, consider the following goal:
Goal forall (v1 v2 v3: Qc) (f: Qc -> Qc), f ((v2 - 1)*v3) <> f ((2#3) * v1 * v2) -> v1+3 <= (v2 + v3) -> v1 <= 3*(v3-v2-1) -> 2*v1 < 3*(v3-2).
vpl_reduce tactic simplifies this goal into
H : f ((v2 - (1 # 1)) * v3) = f ((2 # 3) * v1 * v2) -> False ============================ v1 = (-3 # 1) + (3 # 2) * v3 -> v2 = (1 # 2) * v3 -> False
Hence, the linear inequalities of the initial goal have been replaced
by linear equalities. Then,
vpl_post proves the remaining goal by
vpl tactic is a slight variant of
vpl_reduce which rewrites
the discovered equalities in the remaining goal: it is a macro for
If needed, you may also directly invoke some subcomponent of
vpl_reduce, see file
theories/Tactic.v. You may also find
examples in file
Our ITP'18 paper presents this tactic in details.
See External Dependencies of VPL
coq required version coq 8.9 (use older opam packages of coq-vpltactic for older versions of coq)
First, add the following repository in your opam system:
opam repo add vpl https://raw.githubusercontent.com/VERIMAG-Polyhedra/opam-vpl/master
Then, install the following package:
opam install coq-vpltactic
This will also install other
Browsing the sources
Following usual conventions in Coq projects, directories are organized as follows:
ocamlcode for the plugin (reification + oracle wrapper).
Input.vfinds a polyhedron from the goal
Output.vexports back the reduced polyhedron into the goal
Reduction.vtransforms the input goal into the output goal (thanks to a "script" provided by the VPL oracle)
Tactic.vis the main file
Currently, the code is not really documented (sorry!). It only includes a few comments inside.