Lesson 8: Proof automation

Goals

• This lecture explains how to use proof-automation tactics in MathComp
• ... and how to implement such proof-automation tactics for MathComp, but very briefly (because this is still an active research subject and intricate.)

Tools we use

• The Mczify library adapts the lia and nia tactics to MathComp.
  • This adaptation is done by relying on the zify tactic, which provides an extensible preprocessing facility for the lia tactic.
• The Algebra Tactics library provides a reimplementation of ring, field, lra, nra, and psatz tactics for MathComp.
  • These tactics (lia too) use large-scale Boolean reflection (cf. Lesson 1): they have proof procedures implemented in Coq, and run them inside the Coq kernel to check that the goal propositions hold.
  • This reimplementation is done by reimplementing reification procedures in Coq-Elpi and reusing the proof procedures bundled in Coq. A reification procedure is a meta-function that takes the goal and produces a syntax tree representing the goal, that we can manipulate inside Coq. Coq-Elpi allows us to write Coq plugins in Elpi, a dialect of a higher-order logic programming language called λProlog.

lia: linear integer arithmetic (a.k.a. Presburger arithmetic) solver

This tactic provides a certifying decision procedure for quantifier-free linear integer arithmetic.

The zify and lia tactics support some bool operators.

Some advanced features of the lia tactic

The lia tactic performs normalization with respect to (semi)ring axioms, and can actually solve some non-linear problems.

The Mczify library also pre-processes Euclidean division and the divisibility relation.

nia: non-linear integer arithmetic solver

The nia tactic is an extension of the lia tactic that allows for some non-linear reasoning by propagating positivity and negativity conditions through multiplication and exponentiation.

Instructing the zify tactic to pre-process new arithmetic operators

The zify and lia tactics do not recognize user-defined operators out of the box:

Declare an instance of type UnOp triple, and register it through the Add Zify UnOp command:

Then, the zify tactic starts recognizing the new operator triple:

ring: polynomial equation solver

This tactic provides a certified decision procedure for polynomial equations over commutative rings.

It works for any abstract or concrete commutative rings:

Some advanced features of the ring tactic

The ring tactic can prove polynomial equations modulo monomial equalities:

The Algebra Tactics library implements preprocessors to push down homomorphism applications:

field: rational equation solver

This tactic provides a certified decision procedure for rational equations over fields.

For a partially ordered field (numFieldType), non-nullity conditions of the form n%:R != 0 and n%:~R != 0 where n is a non-zero constant are trivial, and thus are not generated.

As in the ring tactic, the field tactic supports homomorphisms and reasoning modulo monomial equalities.

lra and nra: linear and non-linear real arithmetic

NB: The support for the lra and nra tactics in Algebra Tactics is experimental for the moment.

For realFieldTypes, division and multiplicative inverse are avairable.

These tactics work for any abstract or concrete realDomainType or realFieldType.

How do they work? -- proof by large-scale reflection

We first prove the following reflection lemma (but do not try to understand the formal statement and proof).

Let us apply the above lemma to the example below.

The only missing piece in turning this methodology into a fully-automated tactic is how to obtain the variable map and the polynomial expressions from the goal, which is called reification.

Further reading

• Benjamin Grégoire, Assia Mahboubi. Proving Equalities in a Commutative Ring Done Right in Coq. In: TPHOLs 2005.

  This paper explains the implementation of the ring tactic.

• Frédéric Besson. Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: TYPES 2006.

  This paper explains the implementation of the lia, nia, lra, nra, and psatz tactics.

• Kazuhiko Sakaguchi. Reflexive tactics for algebra, revisited. In: ITP 2022.

  This paper explains:

  • a toy reflexive tactic for zmodType equations,
  • its reification procedure implemented in Coq-Elpi, that works in the presence of an inheritance hierarchy and overloaded operators (cf. Lesson 5),
  • how to preprocess homomorphisms by reflection efficiently, and
  • the application of Mczify and Algebra Tactics to the formal proof of the irrationality of ζ(3).

  The insights from the following papers are the key ingredients of reification in the presence of overloaded operators:
  • Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi. Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. In: IJCAR 2020.
  • Georges Gonthier, Enrico Tassi. A Language of Patterns for Subterm Selection. In: ITP 2012.

• Enrico Tassi. Coq-Elpi.

A takeaway

A better understanding of the principles of MathComp leads us to better design and implementation of tools for MathComp. In my opinion, the principles of MathComp are that:

• relying on the computational power of the logic (dependent type theory) makes formal proofs easier and more efficient to check, and
• to properly do so, we have to carefully design computational behaviors of our definitions.