coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Equality learning in linear arithmetic

From: Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>
To: coq-club AT inria.fr
Cc: Alexandre Maréchal <alex.marechal AT univ-grenoble-alpes.fr>
Subject: [Coq-Club] Equality learning in linear arithmetic
Date: Wed, 12 Apr 2017 17:24:17 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Sylvain.Boulme AT univ-grenoble-alpes.fr; spf=Neutral smtp.mailfrom=Sylvain.Boulme AT univ-grenoble-alpes.fr; spf=None smtp.helo=postmaster AT zm23-mta-out-2.grenet.fr
Ironport-phdr: 9a23:4b8DQxGF+zEzZCS9gaAp+Z1GYnF86YWxBRYc798ds5kLTJ7yo8+wAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95PWSJBH42ybIUBAOQOMulEoIfwvEcOoBikCAWwGO/ixD1Fi3nr1qM6yeQhFgTG0RQ9EdMOtHTUss/6NKYUUe+t0aTIyijDb/dT2TDn9YPFdQ0voPGIXbJua8XRyE8vGxnYg1WXtIzlOzaV2foWvmiG6epgVPyvh3coqwFrvDevwMAshZLNho0L01zL7yF5wJ4rKt2jUkJ7b8SkHYJWuiqHOYV2RcYiTHtpuCY80rAJo4S7czQKyJQm2R7QdeeHf5GP4hL+SuaePy14hG57d7KknRqy/1KgxvXzVsm1zFZKrjdFncLWun8R0BzT786KQeZ+8Ee5wTuDyg7e5v1eLUwpkafXN4QtzqM0m5YOq0jOHiH7lF3rgKKYakko4PWk5uD7brn8u5OQK4t5hhvjPqkghMCyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07iqjYsJXEKckVv6K5BhNV3Zw65xa4EjemzM0UkWcdIFJKYhKIkY7pNE/SIPziA/e/mUygkDZtx//YIr3sGojBI3bfnLv7YLpw71JQxBAuwd1b+p5YELEMLfzrVk/0rtPYDxs5MwKuw+bgDdVwzp4QWGKLAq+HKqzSsFmI6vgyLumLeY8VvDP9JOY+6v7zi385mEEdcbCm3ZsNdn+4GPNmLF6dYXXym9sOC2MKvhIgQ+zxklGCXyRTa26oX60g/jE7FJ6mDYDbS4+xh7yBxT63EYFSZmBbEV+BCmzodoWBW/cUci2eOM5hkjoeVbigUYAtzx+utBWpg4Zge+HT42gTsY/p/Nlz/eza0x8ophJuCMHI6HCJUWh1mFQiQCIy2SE39XdszkmK0K4+qftFEdlez+5PUxl/OoTRyetwD923UwbZc8zPRkzwEYbuOi04Ut9km4xGWE16Adj3y0mbhyc=

Hi all,

We are pleased to announce that we have developed yet another tactic
for solving linear arithmetic goals in Coq. The main feature of our
tactic with respect to similar tactics (lra, fourier, omega, 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.

Our tactic, called 'vpl', works on the 'Qc' type of canonical
rationals. For instance, let us consider the following goal (which
does not exactly fit into linear arithmetic because of the 'f'
uninterpreted symbol).

Goal forall (x: Qc) (f: Qc -> Qc),
x <= 1
-> (f x) < (f 1)
-> x < 1.

Typically, 'vpl' simplifies the above goal into the following one:

x : Qc
f : Qc -> Qc
vpl : x = 1 # 1
______________________________________(1/1)
f (1 # 1) < f (1 # 1) -> False

which is proved by a second call to 'vpl'.

This tactic is highly experimental and, currently, it only works on Qc
(so, it is not a replacement for micromega tactics).

Source and opam package are available from
https://github.com/VERIMAG-Polyhedra/VplTactic

A preprint describes this tactic on:
https://hal.archives-ouvertes.fr/hal-01505598

Feedbacks and suggestions are welcome,

Sylvain Boulmé and Alexandre Maréchal.

[Coq-Club] Equality learning in linear arithmetic, Sylvain Boulmé, 04/12/2017