Coq on Friday, July 9th

09:00‑10:00 Session 1
Location: AT 2.14
09:00 Sean Wilson, Jacques Fleuriot and Alan Smaill
Inductive Proof Automation for Coq

We introduce inductive proof automation for Coq that supports reasoning about inductively defined data types and recursively defined functions. This includes support for proofs involving case splits and situations where multiple inductive hypotheses appear in step case proofs. The automation uses the rippling heuristic to control rewriting in step case proofs and uses heuristics for generalising goals. Additionally, the automation caches lemmas found during proof attempts so that these lemmas may be reused in future proofs. We show that the techniques we present provide a high-level of automation for inductive proofs that improves upon what is already available in Coq. We also discuss a technique that, by inspecting finished proofs, can identify and then remove irrelevant subformulae from cached lemmas, making the latter more reusable. Finally, we compare our work to related research in the field.

09:30 Chung-Kil Hur
Heq: A Coq library for Heterogeneous Equality

We give an introduction to the library Heq, which provides a set of tactics to manipulate heterogeneous equality and explicit coercion, such as rewriting of heterogeneous equality and elimination and relocation of explicit coercions.

11:00‑12:30 Session 2
Location: AT 2.14
11:00 Jean-francois Monin
Proof Trick: Small Inversions

We show how an inductive hypothesis can be inverted using small proof terms and with minimal material. The technique works without any auxiliary type such as True, False, eq. It can also be used to discriminate, in some sense, the constructors of an inductive type of sort Prop in Coq.

11:30 anne mulhern
Strengthening the inversion Tactic in Coq

The entire contents are in the extended abstract, attached.

12:00 Keiko Nakata and Tarmo Uustalu
Mixed induction-coinduction at work for Coq

We present tricks to implement mixed induction-coinduction in Coq using Mendler-style coinduction. We demonstrate the tricks by formalizing termination-sensitive weak bisimilarity on interactive input-output resumptions with explicit internal actions (delays).

12:30 Paolo Herms
Certification of a chain for deductive program verification

We present an ongoing work aiming to formalise and verify the Frama-C - Jessie - Why chain in the Coq Proof Assistant.

14:00‑15:00 Session 3
Location: AT 2.14
14:00 Hugo Herbelin
to be anounced
14:30 Thomas Braibant and Damien Pous
Rewriting Modulo Associativity and Commutativity

Typical hand-written mathematical proofs deal with commutativity and associativity of operators in a liberal way. Unfortunately, formalizing these proofs in a proof assistant require to deal explicitly with boring term reorderings: applying a theorem or rewriting an hypothesis often requires to deal with parentheses.

Consider the following goal:

H: forall x y, x^2 + 2*x*y + y^2 == (x+y)^2 =========================================== a^2 + 2*a*b + c + 2*b^2 == ...

Typical Coq proofs would require either to make an explicit transitivity step to an expression that has the left-hand side of the equation as a sub-term, or to deal explicitly with the associativity and commutativity of the operators to reorder terms in an intricate way. To solve this shortcoming, we work on extending the usual rewrite tactic beyond the syntactic matching, to automatically exploit of the commutativity and associativity of some operators.

As a first step we focused on toplevel rewriting: given an equation to rewrite, our algorithm is decomposed into three steps: (1) we search for a matching modulo AC of the left-hand-side of the equation in the goal; (2) we use a reflexive decision procedure in Coq to prove the equality of the rewritten sub-term and the left-hand side of the equation; (3) we use the standard rewrite tactic to replace the rewritten sub-term with the right-hand side of the equation (by transitivity with the left-hand side)

At this point, it must be noted that even if we took some care implementing our matching function, it does not need to be trusted: it can be considered as an oracle, whose prophecies are checked by a certified decision procedure in Coq. Hence, we decided to write the matching function as an OCaml plug-in.

As explained above, the major drawback of our tactic is that it is currently limited to top-level rewriting. Therefore, the aforementioned example is still out of reach as it is stated. We plan to consider extensions of the rewritten equations: in the above case, one could transform the hypothesis as follows, for which our current tactic is sufficient:

H': forall p x y, x^2 + 2*x*y + y^2 + p == (x+y)^2 + p ======================================================= a^2 + 2*a*b + c + 2*b^2 == ...

We also plan to integrate our work with the new rewriting mechanisms of the forthcoming version 8.3 of Coq, to rewrite under arbitrary morphisms.

15:30‑17:00 Session 4
Location: AT 2.14
15:30 Bas Spitters and Eelis van der Weegen
Developing the algebraic hierarchy with type classes in Coq

Informal presentation:

We have been working on a new (engineering) foundation for formalized constructive mathematics, built on an algebraic hierarchy heavily based on Coq's new type classes, used in a systematic way in order to achieve:

* elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory); * clean expression terms that neither refer to proofs nor require deeply nested record projections; * fluent rewriting; * easy and flexible replacement and specialization of data representations and operations with more efficient versions; * ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.

16:00 Vladimir Komendantsky, Alexander Konovalov and Steve Linton
Experience of interfacing Coq+SSReflect and GAP

A theorem prover may significantly extend its functionality from the ability to communicate with computer algebra systems (CAS). Examples may include, but not limited to, retrieving objects from mathematical databases available in CAS, or computing results that can not be derived using the the theorem prover alone, but once known, may be verified in the prover or used as prover's axioms for further proofs. Such combinations may not only speed up prover's work, but also allow getting results that can not be obtained within any single prover.

Developers of existing interfaces between theorem provers and CAS may select various ways. For example, a prover may write CAS input files and then invoke it; the CAS will write prover's input to a file and exit; the prover will read it and perform further actions. This works, but has fairly serious limitations. A better setup might allow the prover to interact with other CAS while they run and provide a separate interface to each possible external CAS. However, achieving this is a major programming challenge, and an interface will be broken if the other system changes its I/O format, for example.

We report about the prototype implementation of the SCSCP client in Coq which allows to send OpenMath requests from Coq to a local or remote GAP SCSCP server, receive back results and represent them as Coq terms. This implementation provides an extendable and flexible framework: In the future it may support more kinds of mathematical objects. Moreover, thanks to the SCSCP flexibility, remote procedures in specific applications may be designed in a way to avoid some OpenMath-related restrictions. Another direction may be to add features to Coq SCSCP server to allow handling requests from other applications.

We follow the approach where the user takes care about programming the ``interface''. This interface delivers calls from Coq + SSReflect to GAP. The role of the user is to specify how OpenMath requests to GAP are formed from data in Coq and how incoming OpenMath objects will be translated to Coq terms. In particular, OpenMath objects are constructed using the subclass information given by coercions, while synthesis of a Coq term from a given OpenMath object re-uses the canonical structure mechanism. We allow for a manual definition of Coq terms that provide helper information for the automated tactic that performs data exchange between the two systems.

16:30 Yves Bertot and Assia Mahboubi
Root isolation for one-variable polynomials

Given a one variable polynomial with rational coefficients, we want to isolate its roots. In other words, we want to find a finite list of intervals such that each interval contains exactly one root of the polynomial and each root is in one of the intervals.

A first operation is to reduce the multiplicity of roots: find a new polynomial that has the same roots, but where each root has multiplicity one. This can easily be done by computing the greatest common divisor between the polynomial and its derivative. In the following, we thus assume that our polynomial only has simple roots.

The approach we study is based on Bernstein coefficients. These coefficients give a discrete approximation of the behavior of a polynomial in a given closed interval. We rely on a sufficient condition concerning these coefficients (let's call this condition C1): if the Bernstein coefficients, taken in order, have only one alternation, then the polynomial is guaranteed to have exactly one root in the corresponding interval.

The bulk of our work is to prove condition C1.

We study the relations between the coefficients and roots of a given polynomial on a given bounded interval and the coefficients and roots of the image of this polynomial after some transformations. These transformations relate the coefficients of a polynomial in the standard monomial basis to the coefficients of another polynomial in Bernstein bases. They also relate the positive roots of a polynomial to roots of the other polynomial in some bounded interval. In fact, this establishes a relation between condition C1 and Descartes'law of sign.

Three operations on polynomials make it possible to relate roots of various polynomials on various intervals. These operations actually make it possible to relate Bernstein Coefficients with plain coefficients of another polynomials, so that the roots of a polynomial inside a bounded interval are related to the roots of another polynomial between 0 and positive infinity. This establishes a relation between condition C1 and Descartes' law of sign.

In our development, we proved a simplified variant of Descartes's law of sign for the case where the signs of coefficients of a polynomial have only one alternation: In this case, the polynomial is guaranteed to have a single simple root between 0 (excluded) and positive infinity.

Another part of our work is to describe dichotomy. Knowing Bernstein coefficients for a polynomial and a given interval, it is easy to compute the Bernstein coefficients for the two half intervals, using the algorithm known as "de Casteljau". This increases the precision at which the polynomials behavior is described, so that condition C1 is guaranteed to eventually hold in the dichotomy process.

Most of our proofs were made using only rational numbers as numeric values. Thus, we work with type of numbers where equality and comparison are decidable and the process we described can effectively be used in a decision procedure.

When considering only rational numbers, the existence of roots takes a different meaning: if a polynomial has a single simple real root in an interval, this root may not be rational. However, we can use a corresponding property on rational numbers: there exists a sub-interval inside which the absolute value of the slope is bounded below, and such that the values of the polynomial at the sub-interval bounds have opposite signs. In a similar vein, the intermediate value theorem does not hold with rational numbers, but a corresponding statement, expressed as an epsilon-delta property, does. Our proof development relies on these facts.

This result can then be used for several purposes. First it opens the door for a representation of algebraic numbers as equivalence classes between pairs consisting of a polynomial with rational coefficients and an interval. Root isolation makes it possible to decide when two such pairs describe the same algebraic number. Second, it can be used as a basic bloc for a decision procedure deciding logical formulas with universal and existential quantification where atomic formulas are comparisons between polynomial formulas.

Berstein polynomials and de Casteljau's algorithm are intensively used in computer aided design.