The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

We are glad to release the following pieces of software:

1) A library on terms, rewrite systems and termination that we expect to 
extend further later. It includes a formalization of polynomials with multiple 
variables.

2) An extension of Coq V8 including the previous library for the automatic 
verification of polynomial interpretations provided by CiME 
http://cime.lri.fr/. It offers a mechanism for switching between Coq and CiME 
to tune CiME parameters and find a termination proof in it if necessary.

More information is available on http://www.loria.fr/~blanqui/termin.html.

Comments are welcome!

Sebastien Hinderer and Frederic Blanqui, LORIA.



Example of Coq session:

Require Export PolynomialInterpretation.

Variable G : Set.
Symbol Gzero : G.
Symbol Ginv : G -> G.
Symbol Gplus : G -> G -> G.
Rules [x, y, z : G] {
  (Gplus x Gzero) => x;
  (Gplus x (Ginv x)) => Gzero;
  (Gplus (Gplus x y) z) => (Gplus x (Gplus y z))
}.

Termin Gplus.

(* Here, CiME is automatically called to find a polynomial interpretation. 
Then, a Coq termination proof is automatically built, checked and added in the 
current environment. *)