Chapter 22 Program

# Coq Reference Manual

# Chapter 22 Program

- 22.1 Elaborating programs
- 22.2 Solving obligations
- 22.3 Frequently Asked Questions

Matthieu Sozeau

The status of Program is experimental.

We present here the new Program tactic commands, used to build certified Coq programs, elaborating them from their algorithmic skeleton and a rich specification [126]. It can be sought of as a dual of extraction (see Chapter 21). The goal of Program is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is done using a technique originating from the “Predicate subtyping” mechanism of PVS[123], which generates type-checking conditions while typing a term constrained to a particular type. Here we insert existential variables in the term, which must be filled with proofs to get a complete Coq term. Program replaces the Program tactic by Catherine Parent [112] which had a similar goal but is no longer maintained.

The languages available as input are currently restricted to Coq’s term language, but may be extended to Objective Caml, Haskell and others in the future. We use the same syntax as Coq and permit to use implicit arguments and the existing coercion mechanism. Input terms and types are typed in an extended system (Russell) and interpreted into Coq terms. The interpretation process may produce some proof obligations which need to be resolved to create the final term.

## 22.1 Elaborating programs

The main difference from Coq is that an object in a type T : Set can be considered as an object of type { x : T | P} for any wellformed P : Prop. If we go from T to the subset of T verifying property P, we must prove that the object under consideration verifies it. Russell will generate an obligation for every such coercion. In the other direction, Russell will automatically insert a projection.

Another distinction is the treatment of pattern-matching. Apart from the following differences, it is equivalent to the standard `match` operation (see Section 4.5.4).

- Generation of equalities. A `match` expression is always generalized by the corresponding equality. As an example, the expression:
  `Coq` `<``match x with`
  `Coq` `<``| 0 =``>``t`
  `Coq` `<``| S n =``>``u`
  `Coq` `<``end.`

  will be first rewrote to:

  `Coq` `<``(match x as y return (x = y -``>``_) with`
  `Coq` `<``| 0 =``>``fun H : x = 0 -``>``t`
  `Coq` `<``| S n =``>``fun H : x = S n -``>``u`
  `Coq` `<``end) (refl_equal n).`

  This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited.

- Generation of inequalities. If a pattern intersects with a previous one, an inequality is added in the context of the second branch. See for example the definition of `div2` below, where the second branch is typed in a context where ∀ p, _ <> S (S p).
- Coercion. If the object being matched is coercible to an inductive type, the corresponding coercion will be automatically inserted. This also works with the previous mechanism.

To give more control over the generation of equalities, the typechecker will fall back directly to Coq’s usual typing of dependent pattern-matching if a `return` or `in` clause is specified. Likewise, the `if` construct is not treated specially by Program so boolean tests in the code are not automatically reflected in the obligations. One can use the `dec` combinator to get the correct hypotheses as in:

`Coq` `<``Program Definition id (n : nat) : { x : nat | x = n } :=`
`Coq` `<``if dec (leb n 0) then 0`
`Coq` `<``else S (pred n).`
`id has type-checked, generating 2 obligation(s)`
`Solving obligations automatically...`
`2 obligations remaining`
`Obligation 1 of id:`
`forall n : nat, leb n 0 = true -``>``0 = n.`
``
`Obligation 2 of id:`
`forall n : nat, leb n 0 = false -``>``S (pred n) = n.`
``

Finally, the let tupling construct `let (x1, ..., xn) := t in b` does not produce an equality, contrary to the let pattern construct `let ’(x1, ..., xn) := t in b`.

The next two commands are similar to their standard counterparts Definition (see Section 1.3.2) and Fixpoint (see Section 1.3.4) in that they define constants. However, they may require the user to prove some goals to construct the final definitions.

### 22.1.1 `Program Definition` ident`:=` term`.`

This command types the value term in Russell and generate proof obligations. Once solved using the commands shown below, it binds the final Coq term to the name ident in the environment.

Error messages:

1. ident `already exists`

Variants:

1. `Program Definition` ident`` `:`term`1``:=` term`2``.`
   It interprets the type term1, potentially generating proof obligations to be resolved. Once done with them, we have a Coq type term1′. It then checks that the type of the interpretation of term2 is coercible to term1′, and registers ident as being of type term1′ once the set of obligations generated during the interpretation of term2 and the aforementioned coercion derivation are solved.
2. `Program Definition` ident`` binder`1``…`binder`n``` `:`term`1``` `:=``` term`2``.`
   This is equivalent to
   `Program Definition` ident`` `: forall``` binder`1``…`binder`n``,``` term`1``` `:=`
   `fun` binder1…bindern `=>` term2 `.`

Error messages:

1. `In environment` `…``the term:` term`2``does not have type` term`1`.
   `Actually, it has type` term`3`.

See also: Sections 6.10.1, 6.10.2, 8.5.5

### 22.1.2 `Program Fixpoint` ident`` params`` `{order}``: type :=` term``

The structural fixpoint operator behaves just like the one of Coq (see Section 1.3.4), except it may also generate obligations. It works with mutually recursive definitions too.

`Coq` `<``Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x` `\``/ n = 2 * x + 1 } :=`
`Coq` `<``match n with`
`Coq` `<``| S (S p) =``>``S (div2 p)`
`Coq` `<``| _ =``>``O`
`Coq` `<``end.`
`Solving obligations automatically...`
`4 obligations remaining`

Here we have one obligation for each branch (branches for `0` and `(S 0)` are automatically generated by the pattern-matching compilation algorithm).

`Coq` `<``Obligation 1.`
`1 subgoal`
``
`p : nat`
`x : nat`
`o : p = x + (x + 0)` `\``/ p = x + (x + 0) + 1`
`============================`
`S (S p) = S (x + S (x + 0))` `\``/ S (S p) = S (x + S (x + 0) + 1)`

One can use a well-founded order or a measure as termination orders using the syntax:

`Coq` `<``Program Fixpoint div2 (n : nat) {measure n} :`
`Coq` `<``{ x : nat | n = 2 * x` `\``/ n = 2 * x + 1 } :=`
`Coq` `<``match n with`
`Coq` `<``| S (S p) =``>``S (div2 p)`
`Coq` `<``| _ =``>``O`
`Coq` `<``end.`

The order annotation can be either:

- `measure f (R)?` where `f` is a value of type `X` computed on any subset of the arguments and the optional (parenthesised) term `(R)` is a relation on `X`. By default `X` defaults to `nat` and `R` to `lt`.
- `wf R x` which is equivalent to `measure x (R)`.

##### Caution

When defining structurally recursive functions, the generated obligations should have the prototype of the currently defined functional in their context. In this case, the obligations should be transparent (e.g. defined using `Defined`) so that the guardedness condition on recursive calls can be checked by the kernel’s type-checker. There is an optimization in the generation of obligations which gets rid of the hypothesis corresponding to the functionnal when it is not necessary, so that the obligation can be declared opaque (e.g. using `Qed`). However, as soon as it appears in the context, the proof of the obligation is required to be declared transparent.

No such problems arise when using measures or well-founded recursion.

### 22.1.3 `Program Lemma` ident`: type.` ``

The Russell language can also be used to type statements of logical properties. It will generate obligations, try to solve them automatically and fail if some unsolved obligations remain. In this case, one can first define the lemma’s statement using `Program Definition` and use it as the goal afterwards. Otherwise the proof will be started with the elobarted version as a goal. The `Program` prefix can similarly be used as a prefix for `Variable`, `Hypothesis`, `Axiom` etc...

## 22.2 Solving obligations

The following commands are available to manipulate obligations. The optional identifier is used when multiple functions have unsolved obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified.

- `[Local|Global] Obligation Tactic :=` expr Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, e.g. using `Next`. Local makes the setting last only for the current module. Inside sections, local is the default.
- `Show Obligation Tactic` Displays the current default tactic.
- `Obligations [of` ident`]` Displays all remaining obligations.
- `Obligation num [of` ident`]` Start the proof of obligation `num`.
- `Next Obligation [of` ident`]` Start the proof of the next unsolved obligation.
- `Solve Obligations [of` ident`] [using` expr`]` Tries to solve each obligation of identusing the given tactic or the default one.
- `Solve All Obligations [using` expr`]` Tries to solve each obligation of every program using the given tactic or the default one (useful for mutually recursive definitions).
- `Admit Obligations [of` ident`]` Admits all obligations (does not work with structurally recursive programs).
- `Preterm [of` ident`]` Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging.
- `Set Transparent Obligations` Control whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque.

The module `Coq.Program.Tactics` defines the default tactic for solving obligations called `program_simpl`. Importing `Coq.Program.Program` also adds some useful notations, as documented in the file itself.

## 22.3 Frequently Asked Questions

- Ill-formed recursive definitions This error can happen when one tries to define a function by structural recursion on a subset object, which means the Coq function looks like:

  `Program Fixpoint f (x : A | P) := match x with A b => f b end.`

  Supposing b : A, the argument at the recursive call to f is not a direct subterm of x as b is wrapped inside an `exist` constructor to build an object of type `{x : A | P}`. Hence the definition is rejected by the guardedness condition checker. However one can use wellfounded recursion on subset objects like this:

      Program Fixpoint f (x : A | P) { measure (size x) } :=
        match x with A b => f b end.

  One will then just have to prove that the measure decreases at each recursive call. There are three drawbacks though:

  1. A measure function has to be defined;
  2. The reduction is a little more involved, although it works well using lazy evaluation;
  3. Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible.