More succinct README

1 files changed, 68 insertions, 270 deletions

diff --git a/README.md b/README.md
index 691ef54..5001ad9 100644
--- a/README.md
+++ b/README.md
@@ -1,290 +1,88 @@
 # SMTCoq
 
-SMTCoq is a Coq tool that checks proof witnesses coming from external
-SAT and SMT solvers.
+## Presentation
+SMTCoq is a [Coq](http://coq.inria.fr) plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:
+* a certified checker for proof witnesses coming from the SAT solver [ZChaff](http://www.princeton.edu/~chaff/zchaff.html) and the SMT solvers [veriT](http://www.verit-solver.org) and [CVC4](http://cvc4.cs.stanford.edu/web). This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
+* decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT, CVC4, and their combination.
 
-It relies on a certified checker for such witnesses. On top of it,
-vernacular commands and tactics to interface with the SAT solver zChaff
-and the SMT solvers veriT and CVC4 are provided. It is designed in a modular way
-allowing to extend it easily to other solvers.
+## Installation and use
+SMTCoq is freely available as an [https://coq.inria.fr/opam/extra-dev/packages/coq-smtcoq](opam package) and on [GitHub](https://github.com/smtcoq/smtcoq). See the [https://github.com/smtcoq/smtcoq/blob/master/INSTALL.md](INSTALL.md) file for instructions on how to install SMTCoq and the supported provers.
 
-<!--- Extraction is probably broken
-SMTCoq also provides an extracted version of the checker, that can be
-run outside Coq.
---->
+See [the examples](https://github.com/smtcoq/smtcoq/blob/master/examples/Example.v) to see how to use SMTCoq. More details are given in the [https://github.com/smtcoq/smtcoq/blob/master/USE.md](USE.md) file.
 
-<!--- The current stable version is version 1.3. --->
+SMTCoq is distributed under the CeCILL-C license.
 
+## Example
+Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory.
 
-## Installation
-
-See the INSTALL.md file for instructions.
-
-
-## License
-
-SMTCoq is released under the CeCILL-C license; see LICENSE for more
-details.
-
-
-## Want to participate?
-
-SMTCoq is an ambitious, collaborative project: everyone is welcome!
-There are many and varied enhancement to do. You can have a look at the
-[task list](https://github.com/smtcoq/smtcoq/issues/40) or propose your
-own improvements!
-
-
-## Use
-
-Examples are given in the file examples/Example.v. They are meant to be
-easily re-usable for your own usage.
-
-
-### Overview
-
-After installation, the SMTCoq module can be used in Coq files via the
-`Require Import SMTCoq.` command. For each supported solver, it
-provides:
-
-- a vernacular command to check answers: `XXX_Checker "problem_file"
-  "witness_file"` returns `true` only if `witness_file` contains a proof
-  of the unsatisfiability of the problem stated in `problem_file`;
-
-- a vernacular command to safely import theorems:
-  `XXX_Theorem theo "problem_file" "witness_file"` produces a Coq term
-  `theo` whose type is the theorem stated in `problem_file` if
-  `witness_file` is a proof of the unsatisfiability of it, and fails
-  otherwise.
-
-- safe tactics to try to solve a Coq goal using the chosen solver (or a
-  combination of solvers).
-
-<!--- Extraction is probably broken
-The SMTCoq checker can also be extracted to OCaml and then used
-independently from Coq.
---->
-
-We now give more details for each solver.
-
-<!--- Extraction is probably broken
-We now give more details for each solver, and explanations on
-extraction.
---->
-
-
-### zChaff
-
-Compile and install zChaff as explained in the installation
-instructions. In the following, we consider that the command `zchaff` is
-in your `PATH` environment variable.
-
-
-#### Checking zChaff answers of unsatisfiability and importing theorems
-
-To check the result given by zChaff on an unsatisfiable dimacs file
-`file.cnf`:
-
-- Produce a zChaff proof witness: `zchaff file.cnf`. This command
-  produces a proof witness file named `resolve_trace`.
-
-- In a Coq file `file.v`, put:
 ```coq
 Require Import SMTCoq.
-Zchaff_Checker "file.cnf" "resolve_trace".
-```
 
-- Compile `file.v`: `coqc file.v`. If it returns `true` then zChaff
-  indeed proved that the problem was unsatisfiable.
+Section group.
+  Variable e : Z, inv : Z -> Z, op : Z -> Z -> Z.
 
-- You can also produce Coq theorems from zChaff proof witnesses: the
-  commands
-```coq
-Require Import SMTCoq.
-Zchaff_Theorem theo "file.cnf" "resolve_trace".
-```
-will produce a Coq term `theo` whose type is the theorem stated in
-`file.cnf`.
+  Hypothesis associative :
+    forall a b c, op a (op b c) = op (op a b) c.
+  Hypothesis identity : forall a, (op e a = a).
+  Hypothesis inverse : forall a, (op (inv a) a = e).
 
+  Add_lemmas associative identity inverse.
 
-#### zChaff as a Coq decision procedure
+  Lemma identity' :
+    forall a, (op a e = a).
+  Proof. smt. Qed.
 
-The `zchaff` tactic can be used to solve any goal of the form:
-```coq
-forall l, b1 = b2
-```
-where `l` is a quantifier-free list of terms and `b1` and `b2` are
-expressions of type `bool`.
+  Lemma inverse' :
+    forall a, (op a (inv a) = e).
+  Proof. smt. Qed.
 
-A more efficient version of this tactic, called `zchaff_no_check`,
-performs only the check at `Qed`. (Thus it is safe, but a proof may fail
-at `Qed` even if everything went through during proof elaboration.)
+  Lemma unique_identity e':
+    (forall z, op e' z = z) -> e' = e.
+  Proof. intros pe'; smt pe'. Qed.
 
-
-### veriT
-
-Compile and install veriT as explained in the installation instructions.
-In the following, we consider that the command `veriT` is in your `PATH`
-environment variable.
-
-
-#### Checking veriT answers of unsatisfiability and importing theorems
-
-To check the result given by veriT on an unsatisfiable SMT-LIB2 file
-`file.smt2`:
-
-- Produce a veriT proof witness:
-```coq
-veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-e --disable-ackermann --input=smtlib2 --proof=file.log file.smt2
-```
-This command produces a proof witness file named `file.log`.
-
-- In a Coq file `file.v`, put:
-```coq
-Require Import SMTCoq.
-Section File.
-  Verit_Checker "file.smt2" "file.log".
-End File.
+  Clear_lemmas.
+End group.
 ```
 
-- Compile `file.v`: `coqc file.v`. If it returns `true` then veriT
-  indeed proved that the problem was unsatisfiable.
-
-- You can also produce Coq theorems from veriT proof witnesses: the
-  commands
-```coq
-Require Import SMTCoq.
-Section File.
-  Verit_Theorem theo "file.smt2" "file.log".
-End File.
-```
-will produce a Coq term `theo` whose type is the theorem stated in
-`file.smt2`.
-
-The theories that are currently supported by these commands are `QF_UF`
-(theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL`
-(integer difference logic), and their combinations.
-
-
-#### veriT as a Coq decision procedure
-
-The `verit_bool [h1 ...]` tactic can be used to solve any goal of the form:
-```coq
-forall l, b1 = b2
-```
-where `l` is a quantifier-free list of terms and `b1` and `b2` are
-expressions of type `bool`. This tactic **supports quantifiers**: it takes
-optional arguments which are names of universally quantified
-lemmas/hypotheses that can be used to solve the goal. These lemmas can
-also be given once and for all using the `Add_lemmas` command (see
-[examples/Example.v](https://github.com/smtcoq/smtcoq/blob/master/examples/Example.v)
-for details).
-
-In addition, the `verit` tactic applies to Coq goals of sort `Prop`: it
-first converts the goal into a term of type `bool` (thanks to the
-`reflect` predicate of `SSReflect`), and then calls the previous tactic
-`verit_bool`.
-
-The theories that are currently supported by these tactics are `QF_UF`
-(theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL`
-(integer difference logic), and their combinations.
-
-A more efficient version of this tactic, called `verit_no_check`,
-performs only the check at `Qed`. (Thus it is safe, but a proof may fail
-at `Qed` even if everything went through during proof elaboration.)
-
-
-### CVC4
-
-Compile and install `CVC4` as explained in the installation
-instructions. In the following, we consider that the command `cvc4` is
-in your `PATH` environment variable.
-
-
-#### Checking CVC4 answers of unsatisfiability and importing theorems
-
-To check the result given by CVC4 on an unsatisfiable SMT-LIB2 file
-`name.smt2`:
-
-- Produce a CVC4 proof witness:
-
-```bash
-cvc4 --dump-proof --no-simplification --fewer-preprocessing-holes --no-bv-eq --no-bv-ineq --no-bv-algebraic name.smt2 > name.lfsc
-```
-
-This set of commands produces a proof witness file named `name.lfsc`.
-
-- In a Coq file `name.v`, put:
-```coq
-Require Import SMTCoq Bool List.
-Import ListNotations BVList.BITVECTOR_LIST FArray.
-Local Open Scope list_scope.
-Local Open Scope farray_scope.
-Local Open Scope bv_scope.
-
-Section File.
-  Lfsc_Checker "name.smt2" "name.lfsc".
-End File.
-```
-
-- Compile `name.v`: `coqc name.v`. If it returns `true` then the problem
-  is indeed unsatisfiable.
-
-NB: Use `cvc4tocoq` script in `src/lfsc/tests` to automatize the above steps.
-
-- Ex: `./cvc4tocoq name.smt2` returns `true` only if the problem
-  `name.smt2` has been proved unsatisfiable by CVC4.
-
-The theories that are currently supported by these commands are `QF_UF`
-(theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL`
-(integer difference logic), `QF_BV` (theory of fixed-size bit vectors),
-`QF_A` (theory of arrays), and their combinations.
-
-
-#### CVC4 as a Coq decision procedure
-
-The `cvc4_bool` tactic can be used to solve any goal of the form:
-```coq
-forall l, b1 = b2
-```
-
-where `l` is a quantifier-free list of terms and `b1` and `b2` are
-expressions of type `bool`.
-
-In addition, the `cvc4` tactic applies to Coq goals of sort `Prop`: it
- first converts the goal into a term of type `bool` (thanks to the
- `reflect` predicate of `SSReflect`), it then calls the previous tactic
- `cvc4_bool`, and it finally converts any unsolved subgoals returned by
- CVC4 back to `Prop`, thus offering to the user the possibility to solve
- these (usually simpler) subgoals.
-
-The theories that are currently supported by these tactics are `QF_UF`
-(theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL`
-(integer difference logic), `QF_BV` (theory of fixed-size bit vectors),
-`QF_A` (theory of arrays), and their combinations.
-
-A more efficient version of this tactic, called `cvc4_no_check`,
-performs only the check at `Qed`. (Thus it is safe, but a proof may fail
-at `Qed` even if everything went through during proof elaboration.)
-
-
-### The smt tactic
-
-The more powerful tactic `smt` combines all the previous tactics: it
-first converts the goal to a term of type `bool` (thanks to the
-`reflect` predicate of `SSReflect`), it then calls a combination of the
-`cvc4_bool` and `verit_bool` tactics, and it finally converts any
-unsolved subgoals back to `Prop`, thus offering to the user the
-possibility to solve these (usually simpler) subgoals.
-
-A more efficient version of this tactic, called `smt_no_check`,
-performs only the check at `Qed`. (Thus it is safe, but a proof may fail
-at `Qed` even if everything went through during proof elaboration.)
-
+## Want to participate?
 
-### Conversion tactics
+SMTCoq is an ambitious, collaborative project: everyone is welcome!
+There are many and varied enhancement to do. You can have a look at the
+[task list](https://github.com/smtcoq/smtcoq/issues/40) or propose your
+own improvements!
 
-SMTCoq provides conversion tactics, to inject various integer types into
-the type Z supported by SMTCoq. They can be called before the other
-SMTCoq tactics. These tactics are named `nat_convert`, `N_convert` and
-`pos_convert`. They can be combined.
+## People
+### Current team
+* [Clark Barrett](http://www.cs.nyu.edu/~barrett) (Stanford University)
+* [Valentin Blot](https://valentinblot.org/pro) (Université Paris-Sud, Université Paris-Diderot)
+* Amina Bousalem (Université Paris-Sud)
+* [Burak Ekici](http://ekiciburak.github.io/) (The University of Iowa)
+* Quentin Garchery (Université Paris-Sud, Inria)
+* [Benjamin Grégoire](https://www-sop.inria.fr/members/Benjamin.Gregoire/) (Inria Sophia Antipolis)
+* [Guy Katz](http://stanford.edu/~guyk) (Stanford University)
+* [Chantal Keller](https://www.lri.fr/~keller/index-en.html) (Université Paris-Sud)
+* [Alain Mebsout](https://mebsout.github.io/) (OcamlPro)
+* [Andrew Reynolds](http://homepage.divms.uiowa.edu/~ajreynol) (The University of Iowa)
+* [Laurent Théry](https://www-sop.inria.fr/marelle/Laurent.Thery/moi.html) (Inria Sophia Antipolis)
+* [Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/) (The University of Iowa)
+
+### Past contributors
+* Mikaël Armand (Inria Sophia Antipolis)
+* Germain Faure (Inria Saclay)
+* Tianyi Liang (The University of Iowa)
+* [Benjamin Werner](http://www.lix.polytechnique.fr/Labo/Benjamin.Werner) (École polytechnique)
+
+
+## Publications
+### Reference
+[A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses](http://hal.inria.fr/docs/00/63/91/30/PDF/cpp11.pdf), Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin, [CPP - Certified Programs and Proofs - First International Conference - 2011](http://formes.asia/cpp).
+
+### Other publications
+1. [SMTCoq: A plug-in for integrating SMT solvers into Coq (Tool Paper)](http://homepage.divms.uiowa.edu/~tinelli/papers/EkiEtAl-CAV-17.pdf), Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark, [CAV - International Conference on Computer Aided Verification](http://cavconference.org/2017) - 2017.
+2. [Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)](https://hal.inria.fr/hal-01388984/document), Ekici, Burak; Katz, Guy; Keller, Chantal; Mebsout, Alain; Reynolds, Andrew; Tinelli, Cesare, [HaTT - on Hammers for Type Theories - First International Workshop](https://hatt2016.inria.fr) - 2016.
+3. [Verifying SAT and SMT in Coq for a fully automated decision procedure](http://hal.inria.fr/docs/00/61/40/41/PDF/ArmandAl.pdf), Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin, [PSATTT - International Workshop on Proof-Search in Axiomatic Theories and Type Theories](http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT11) - 2011.
+4. SMTCoq : automatisation expressive et extensible dans Coq, Blot, Valentin; Bousalem, Amina; Garchery, Quentin; Keller, Chantal, [JFLA - Journées Francophones des Langages Applicatifs](http://dpt-info.u-strasbg.fr/~magaud/JFLA2019) - 2019.
+
+
+## Talk
+[Overview of SMTCoq (February, 2019)](https://github.com/smtcoq/smtcoq.github.io/blob/master/documents/overview_19-02-11.pdf)