Polynomials

Polynomials and a reflexive tactic for solving boolean goals (using heyting or classical boolean algebra). Original version by Rafael Bocquet, 2016. Updated to use Equations for all definitions by M. Sozeau, 2016-2017. If running this interactively you can ignore the printing and hide directives which are just used to instruct coqdoc.

We start with a simple definition deciding if some integer is equal to 0 or not. Integers are encoded using an inductive type Z with three constructors Z0, Zpos and Zneg, the latter two taking positive numbers as arguments. There is a single representant of 0 which we discriminate here. The second clause actually captures both the Zpos and Zneg constructors.

The specification of this test is that it returns true iff the variable is indeed different from 0 w.r.t. the standard Leibniz equality. We elide a simple proof by case analysis. Note that we use an implicit coercion from bool to Prop here, as is usual when doing boolean reflection.

Multivariate polynomials

Using an indexed inductive type, we ensure that polynomials of have a unique representation. The first index indicates that the polynom is null. The second index gives the number of free variables.

• poly_z represents the null polynomial.
• poly_c c represents the constant polynomial c where c is non-zero (i.e. has a proof of IsNZ c).
• poly_l n Q represents the injection of Q, a polynomial on n variables, as a polynomial on n+1 variables.
• Finally, poly_s P Q : poly _ (S n) represents where P cannot mention the variable but Q can mention the variables up to and including , and the multiplication is not trivial as Q is non-null.

These indices enforce a canonical representation by ordering the multiplications of the variables. A similar encoding is actually used in the ring tactic of Coq.

In addition to the usual eliminators of the inductive type generated by Coq, we automatically derive a few constructions on this poly datatype, and the mono datatype that follows, that will be used by the Equations command:

• Its Signature: as described earlier , this is the packing of a polynomial with its two indices, a boolean and a natural number in this case.
• Its NoConfusion property used to simplify equalities between constructors of the poly type (equation ).
• Finally, its Subterm relation, to be used when performing well-founded recursion on poly.

Monomials

Monomials represent parts of polynoms, and one can compute the coefficient constant by which each monomial is multiplied in a given polynom. Again the index of a mono gives the number of its free variables.

Our first interesting definition computes the coefficient in Z by which a monomial m is multiplied in a polynomial p.

The definition can be done using either the usual structural recursion of Coq or well-founded recursion. If we use structural recursion, the guardness check might not be able to verify the automatically generated proof that the function respects its graph, as it involves too much rewriting due to dependent pattern-matching. We could prove it using a dependent induction instead of using the raw fixpoint combinator as the recursion is on direct subterms of the monomial, but in general it could be arbitrarily complicated, so we present a version allowing deep pattern-matching and recursion. Note that this means we lose the definitional behavior of get_coef during proofs on open terms, but this can advantageously be replaced using explicit rewrite calls, providing much more control over simplification than the reduction tactics, especially in presence of recursive functions. The get_coef function still uses no axioms, so it can be used to compute as part of a reflexive tactic for example. We want to do recursion on the (dependent) m : mono n argument, using the derived mono_subterm relation, which expects an element in the signature of mono, { n : nat & mono n }, so we use pack m to lift m into its signature type (pack is just an abbreviation for the signature_pack overloaded constant defined in ). The rest of the definition is standard: to fetch a monomial coefficient, we simultaneously pattern-match on the monomial and polynomial. Note that many cases are impossible due to the invariants enforced in poly and mono. For example mono_z can only match polynomials built from poly_z or poly_c, etc.

Two detailed proofs

The monomial decomposition is actually a complete characterization of a polynomial: two polynomials with the same coefficients for every monomial are the same. To show this, we need a lemma that shows that every non-null polynomial, has a monomial with non-null coefficient: this proof is done by dependent induction on the polynomial p. Note that the index of p rules out the poly_z case.

Throughout the proof, we use the simp tactic defined by which is a wrapper around autorewrite using the hint database associated to the constant get_coef: the database contains the defining equations of get_coef as rewrite rules that can be used to simplify calls to get_coef in the goal.

We first do an induction on p1 and then eliminate (dependently) p2, the first two branches need to consider variable-closed p2s while the next two branches have p2 : poly _ (S n), hence the poly_l and poly_s patterns. The elided rest of the tactic solves simple subgoals. We now focus on the case for poly_l on both sides. After some simplifications of the induction hypothesis using the Hcoef hypothesis, we get to the following goal:
  (b, b' : bool) (n : nat) (p1 : poly b n) (p2 : poly b' n)
  IHp1 : (b; p1) = (b'; p2)
  ============================
  (b; poly_l p1) = (b'; poly_l p2)

The IHp1 hypothesis, as a general equality between dependent pairs can again be eliminated dependently to substitute b' by b and p2 by p1 simultaneously, using dependent elimination IHp1 as [eq_refl], leaving us with a trivial subgoal.

The next step is to give an evaluation semantics to polynomials. We program eval p v where v is a valuation in Z for all the variables in p : poly _ n.

It is quite clear that two equal polynomials should have the same value for any valuation. To show this, we first need to prove that evaluating a null polynomial always computes to 0, whichever valuation is used.

This is a typical case where the proof directly follows the definition of eval. Instead of redoing the same case splits and induction that the function performs, we can directly appeal to its elimination principle using the funelim tactic.

This leaves us with two goals as the true index in p implies that the poly_c and poly_s clauses do not need to be considered. We have to show 0 = 0 for the case p = poly_z and eval q v = 0 for the poly_l recursive constructor, in which case the conclusion directly follows from the induction hypothesis correspondinng to the recursive call. The second subgoal is hence discharged with an assumption call. Addition is defined on two polynomials with the same number of variables and returns a (possibly null) polynomial with the same number of variables. We define an injection function to constructs objects in the dependent pair type {b : bool & poly b n}.

The definition shows the with feature of Equations, allowing to add a nested pattern-matching while defining the function, here in one case to inject an integer into a polynomial and in the poly_s, poly_s case to inspect a recursive call.

The functional elimination principle can be derived all the same for plus, allowing us to make quick work of the proof that it is a morphism for evaluation:

We skip the rest of the operations definition, poly_mult, poly_neg and poly_substract.

Equality can be decided using the difference of polynoms

Two polynomials with the same values are syntacically equal.

This is shown using poly_nz_eval: the difference of two polynomials with the same values is null. Then use poly_diff_z_eq

Multiplication of polynomials

This definition is a bit more laborious as there are inductive cases to treat on the second argument: it is not a simple structurally recursive definition. The poly_l_or_s definition is a smart constructor to construct p + X × q when q can be null.

Finally, the multiplication definition. This relies on the guard condition being able to unfold the definitions of mult_l and mult_s to see that multiplication is well-guarded.

The proof that multiplication is a morphism for evaluation works as usual by induction, using previously proved lemma to get equations in Z that the nia tactic can handle.

Boolean formulas

Armed with these definitions, we can define a reflexive tactic that solves boolean tautologies using a translation into polynomials on Z. We start with the syntax of our formulas, including variables of some type A, constants, conjunction disjunction and negation:

The have a straightforward evaluation semantics to booleans, assuming an interpretation of the variables into booleans.

close_formula allows to obtain a formula with a fixed finite number of free variables from a formula with with variables in nat.

Definitions of constant 0 poly_zero and 1 poly_one polynomials along with variable polynomials poly_var and corresponding evaluation lemmas

We define an injection of variables represented as indices in Fin.t n into non-null polynoms of n variables:

We can show that evaluation of the corresponding polynomial corresponds to simply fetching the value at the index in the valuation.

Finally, we explain our interpretation of formulas as polynomials:

The central theorem is that evaluating the formula in some valuation is the same as evaluating the translated polynomial.

From this, we can derive that two boolean formulas are equivalent if the translated polynomials are themselves syntactically equal, thanks to their canonical representation.

Completeness

For which theory do we have completeness? If you were attentive you might have guessed that the encodings of disjunction and conjunction are only complete for heyting boolean algebras but not classical boolean algebra, where negation is involutive. One can avoid this problem by doing a reduction transformation on polynomials. The interested reader can look at the development for that part. Completeness can be derived for the reducing version of the translation.

We have completeness for this form:

One can check that all definitions here are axiom free, and only the proofs which depend on unfolding lemmas use the functional_extensionality_dep axiom.

Reflexive tactic

From this it is possible to derive a tactic for checking equivalence of boolean formulas. We skip the standard reification machinery and check on a few examples that indeed our tactic computes.

Reify boolean formulas with variables in nat

The final reflexive tactic, taking either of the correctness lemmas as argument.

Examples