MPRI PRFA (2-7-2) / 2024 / Live coding session 4

Records

In Coq you can write structures using what we call "records". They consists of various fields that each contain data of a given type. For instance, a (bad) type of rationals:

Under the hood, Coq will define an inductive type with one constructor called Build_bad_rational1

We can produce values as follows:

The names of the fields also correspond to what we call projections. They let us access the various values of a record.

NOTE: To write integers in Z, we can use numeral notations as long as we add %Z at the end to indicate that we don't mean a nat.

We can also produce values interactively.

We can also produce values interactively.

Actually products that are defined using an inductive type, can also be defined as records. For this we use parameters to records. They work like inductive parameters. In fact, records are syntactic sugar over inductive types with one constructor that takes all the fields as arguments, and we can even give a name to that constructor.

Actually it's annoying to have the underscores in mkpair _ _ 12 bool we're going to change that with the Arguments command.

You can also use do pattern matching using this constructor.

Since there is only one constructor, we can also use let

We can also use a more generic notation that doesn't require remembering the name of mkpair. It's maybe not as explicit so it's up to you to decide which version you prefer.

Generally, one uses the projections directly. They take the parameters as arguments so for convenience we declare them as implicit.

We can use records to represent more complex mathematical structures. See for instance the following record representing monoids.

Again we can build these structures interactively using refine.

We can prove things generically about monoids.

Products of monoids also yields a monoid.

Type classes

Say we want to use our monoid_fact on pairs of natural numbers. We can write the following:

But this doesn't tell us much. If we want to write it by hand, it actually doesn't really work because Coq can't find the monoid structure on its own.

The solution to this problem is called classes. It adapts the notion of type classes one finds in functional programming languages such as Haskell. Syntax is the same as for records but it is registered as a special structure for Coq. We move the carrier, neutral and operation as parameters because Coq will use them to guess which monoid structure we mean.

Instance is a a special command for definitions that register them as things Coq will use automatically if it has to find a value for Monoid nat 0 plus. Don't worry too much about the export thing. This is called an attribute and it just means that if someone imports the file, then the instance will still be available. We could instead use #[local] to restrict the instance to the module. It does not matter for the course.

Some lemmas we can prove using only the monoid structure on (ℕ,0,+). See how Coq infers which proofs we are talking about.

We can prove it in general on monoids with the same proof.

EXERCISE Complete the product instance.

Now you can see that Coq can infer complex monoid structures on its own!

Here is another example of class: decidable equality.

Note: `{Eq A} is short for {_ : Eq A} -- i.e. we don't have to give it a name. Indeed we don't care about the name of the instance because we don't need to refer to it explicitly, Coq finds it on its own.

Another useful tool is the refine attribute that also lets us give only partial instances. Note that it only works for Instance, not Definition.

Automation

Classes are one form of automation. There are others in Coq. The main one being tactics. Indeed they can be used to derive properties automatically. We will start by looking again at the In predicate. We'll start by proving some easy lemmas.

Ok, this we already know, but we can use the auto tactic to deal with some of this.

Now we would like auto to deal with In without the need to use simpl. It should also be able to deal with more complex examples like the following.

Applying the lemma by hand is not very nice, and rather tedious. We're going to declare hints so that auto knows how to use them. In fact, we're first going to declare a new database of hints dedicated to In. We call it indb, because why not?

We then add hints to the database using the Hint Resolve command. Like for instances, we need to specify a locality. It doesn't matter so we're going to go with export as before. We then give it the name of a definition (or lemma etc.) and after the colon the databases to which we want to add the hint.

If we do not use a HintDB Coq automatically uses core

Domain-specific automation tactics

lia

For linear integer arithmetic. Solves goals about nat / Z and addition, sometimes multiplication.

congruence

For equality. Solves goals about equality, knows about disjointness and difference of constructors.

tauto

For propositional logic. Solves (intuituinistic) propositional tautologies However, it's easy to use it for classical propositional logic as well:

Or without manual work

intuition / firstorder

Uses the tauto algorithm and calls a tactic on the leafs. tauto is intuition fail, i.e. no leafs allowed. intuition is intuition auto with core

Existential variables, again

auto also has an eauto variant. You can use it to deal with existential quantifiers. It is generally slower than auto so you can use it when auto fails.