Lesson 2: Data Structures and Class Hierarchies

Brief recap:

We have seen so far:

• What is a Coq proof, its justification of truth.
• Typing judgments Γ ⊢ p : T
• Basic inductive types
• Library built-ins for logic and data types (nat, bool, list)
• Tension / duality of computation vs propositions
• Context management in interactive proofs, tacticals ⇒, : for stack manipulation
• Tactics have rewrite, move, apply, case, elim, simpl, ∃
• Intro patterns // and /=

Key points to see today:

• Reflection, views, characteristic predicates (30 mins)
• Smarter case analysis (15 mins)
• Structures and class hiearchies: subtypes (tuples), choice, finite types (45 mins)

Reflection and proving with computation

We will start today's lesson by discussing an often underused advantage of Coq, which is its ability to run complex programs quite efficiently as part of type-checking. Invoking a computational routine can be very convenient when trying to prove certain facts that can be decided by an algorithm. Thus, the core idea of proof by reflection is to move between the computational and the logical world, as it better suits our proof style. Let's first see an example with the less than relation as defined in Coq Standard library vs as it is defined in math-comp:

Moreover, the math-comp version, by virtue of being in bool, inherits some nice properties, like decidability, for free. But there are often many cases where the propositional version may be more convenient. The canonical example is case analysis on evidence: a proof of P ∨ Q can be analyzed directly using pattern matching or the case tactics, whereas a proof of P || Q = true requires a way more involved analyse. Assume a proposition P in Prop, that has a counterpart in bool such that "P provable if and only if p = true". Thus, ¬ P is provable iff p = false. In a sense, we want to state P ↔ p, but typing doesn't quite match. This equivalence relation is captured via the reflect datatype:

reflect P p contains evidence for the result of the computation p, together with a proof of the propositional property P or ¬P depending on the outcome of p. The math-comp library take advantage of this predicate extensively, and provides special support to ease its use via views. Views (https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.htmlviews-and-reflection) are a lightly programmable mechanism to transform equivalent propositions among themselves. Views are understood by intro patterns and [apply], and are usually applied with a [/view] syntax. Let's see an example:

Views do understand the reflect predicate, we thus can use them in proofs in a convenient way:

Note the suffix P which often denotes a reflection of "characteristic lemma"

Using case analysis effectively:

A little-known fact about Coq's case analysis tactics is that they will replace any subterm of the right type in the goal by its intances. This is a natural consequence of pattern matching, and can be used to our advantage to perform a lot of convenient proof resonings. Let's investigate this example taken from Coq's manual:

The above looked like magic! But indeed, let's review the reflect predicate again:

Indeeed, the relevant parameter appears as an index! math-comp provides special support for this (try case: andP), and we have other options like ifP, boolP, etc... This trick can be used with our own custom predicate, for example see the powerful leqP predicate:

Some other intersting views are:

A similar technique can be used to implement "small inversion", avoiding many of the pitfalls that regular inversion has in terms of proof maintenance.

Organizing common properties and libraries:

Once we have some basics of writing programs and proofs in Coq sorted out, the next natural question is how to organize them into libraries. For example, types may have some common property such as decidability of equality, countability, or finiteness. It'd be nice if we could have a single generic theory for all types sharing some common traits that we could share.

Types with Decidable Equality

A good example is indeed types that have decidable equality. Let's starts by proving this statement about equality and natural numbers:

This is a lemma that may need to use often, for example to reason about an indexing function. However, we already have the eqn function that in a sense does exactly the same than the proof, and moreover, it is faster to run. So we can maybe try to relate them with reflect?

That looks quite good, now we can prove the previous lemma in a bit more convenient way:

But not only nat has decidable equality, but many other types do, and we'd like to reason in our proofs with their richer theory. So in order to organize this, we will declare an interface eqType for types with decidable equality:

We did print the real thing as it is often convenient to see the not so rosy reality of optimized libraries. The above is the start of the implementation of a "mixin" object-oriented design pattern, so other structures can inherit efficiently from eqType, which in fact they do! Thanks to eqType we can now do some more interesting stuff. Let's do the proof again:

Note that there was a quite magic process in which Coq realized that nat has an eqType instance. The mechanism implementing this is called "Canonical Structures" and it is a form of inference that can be triggered by unification. The implementation is a low level detail, and end-users have better tools this days, for example "Hierarchy Builder" that will help them manage all these structures. Other systems like Lean have built-in support (using type classes). Having eqType available allows us to have some nice functions, and a membership predicate:

That's great, and moreover math-comp provides facilities to build class instances for isomorphic types. This saves a lot of time and effort. math-comp provides a very rich hierarchy or algebraic structures, which we will explore soon. See https://math-comp.github.io/htmldoc/libgraph.html Let's explore that graph and the documentation a bit. Some relevant classes at this stage are:

• eqType: types with decidable equality, operator ==, main theory
• eqP subType P A: types that meet a decidable (thus irrelevant) predicate; subTypes of A convertibles to A. For example the set of all even natural numbers: { x : nat | even x }.
• choiceType: eqTypes with a choice principle, main theory xchoose, xchooseP
• countType: choiceTypes that are in bijection with the naturals, pickle, unpickle
• finType: countTypes that are finite, large theory of cardinality, decidable quantification, etc...

SubTypes

"subtypes" are a key building block of many objects in math-comp. The key idea stems from the fact that boolean predicates on types have a single inhabitant, thus they are "irrelevant" in terms of equality. We can then just ignore the predicate when comparing two elements of a subType. math-comp will infer a subType structure automatically in many cases:

Finite Types

Finite types (finType) inherit from eqType and choiceType, and provide an extra axiom:

The axiom states that every element of the type appears once in the enumeration. Note how this promises nothing about the order! Thus, proofs relying on the enumeration of the elements for a finite type need to work up to permutation of the list. (We have not covered this in the class, but math-comp provides very powerful tools to reason up to permutation. Finite types provide some operations related to cardinalatiy, and the corresponding boolean quantifiers.

As it is usual in mathcomp, types built from other finTypes are automatically inferred to be a finType:

Ordinals and tuples

Subtypes have many applications in mathematics and computer science. Two of the core math-comp building types are ordinal and tuple:

One core advante of subtypes is that they allow to reuse the existing operators, for example, we can map easily over a tuple:

A tuple over a finite type is a finite type. Tuples are of fundamental importance as we will use them to build finitely supported functions which are the base for matrices.

Canonical Structures

As we have seen, it is customary to pack the definition of an structure and its properties into a record. For example, types with decidable equality are packed as eqType, which thanks to a coercion can be used a Type. However, it is very common that we will have the following situation: (∀ {T : eqType}, (x y : T), ...) 3 4 That is to say, x y have type ?T.(type) (due to the coercion), as ?T is implicit and just a meta-variable at this point. Thus, we got a unification problem ?T.(type) = nat, which is hard to solve as it would mean we need to synthesize an implementation de eqType for nat on on the fly. Instead, we can tell Coq to consider a hint when this kind of unification problem appears. What we can say to Coq is that indeed, every unification problem that that has the shape of ?T : eqType |- ?T.(type) = nat , should be solved by using the existing nat_eqP instance. "Canonical" structures provides us the way to indicate this.

Coercions

Coercions allow the type inference to relate to different types by inserting (or synthesising) a type casting from a type to another. A good example is just the above equation. We have T : eqType and we need in (x : T) that T is a Type however it is an eqType. But Coq knows how to repair this, and will insert the .(type) projection so we now have (x : T.(type), with this correctly typing.

Building instances easily

math-comp allows to build instances more easily by showing a bijection to a type with an existing instance:

Status in Coq

As of today, defining our own structures requires too much boiler-plate. Lean has better support for this (with trade-offs) , whereas Coq has an experimental plugin called hierarchy builder that greatly helps.

A small declarative interpreter

We end the lesson by developing a verified Datalog interpreter step-by-step, in very few lines, thanks to the math-comp theory on finite types (and a smart trick).

Finitely-many literals.

Build a finType instance for lit

Now you can read from here

Interpretations are set of literals

A literal is true in i if it belongs (the negated version would be \isnot) Notation lit_true i l := (l \in i). We define naïve clauses.

A clause is true.

fwd chain is an interpretation transformer that takes a program and a current interpretation and extends it with the new deducible facts.

if the program p has a model m then fwd_chain has a fixpoint m' s.t m' is a model for p and a better or equal model than m

Exercise: Add variables