\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Program¶

Author: Matthieu Sozeau

We present here the Program tactic commands, used to build certified Coq programs, elaborating them from their algorithmic skeleton and a rich specification [Soz07]. It can be thought of as a dual of Extraction. 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 [ROS98], 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 [Par95] 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 OCaml, 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.

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 well-formed 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 Extended pattern matching).

Generation of equalities. A match expression is always generalized by the corresponding equality. As an example, the expression:
```
match x with
| 0 => t
| S n => u
end.
```
will be first rewritten to:
```
(match x as y return (x = y -> _) with
| 0 => fun H : x = 0 -> t
| S n => fun H : x = S n -> u
end) (eq_refl x).
```
This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited.
Generation of disequalities. If a pattern intersects with a previous one, a disequality 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.

There are flags to control the generation of equalities and coercions.

Flag Program Cases¶: This flag controls the special treatment of pattern matching generating equalities and disequalities when using Program (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm of Coq (see Extended pattern matching) when this flag is deactivated.

Flag Program Generalized Coercion¶: This flag controls the coercion of general inductive types when using Program (the flag is on by default). Coercion of subset types and pairs is still active in this case.

Flag Program Mode¶: This flag enables the program mode, in which 1) typechecking allows subset coercions and 2) the elaboration of pattern matching of Fixpoint and Definition acts as if the program attribute has been used, generating obligations if there are unresolved holes after typechecking.

Attribute program= yesno?¶: This boolean attribute allows using or disabling the Program mode on a specific definition. An alternative and commonly used syntax is to use the legacy Program prefix (cf. legacy_attr) as it is elsewhere in this chapter.

Syntactic control over equalities¶

To give more control over the generation of equalities, the type checker 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:

Require Import Program Arith.: [Loading ML file extraction_plugin.cmxs (using legacy method) ... done] [Loading ML file ring_plugin.cmxs (using legacy method) ... done]

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

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 and Fixpoint in that they define constants. However, they may require the user to prove some goals to construct the final definitions.

Program Definition¶

A Definition command with the program attribute types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the final Coq term to the name ident in the global environment.

Program Definition ident_decl : type := term

Interprets the type type, potentially generating proof obligations to be resolved. Once done with them, we have a Coq type type₀. It then elaborates the preterm term into a Coq term term₀, checking that the type of term₀ is coercible to type₀, and registers ident as being of type type₀ once the set of obligations generated during the interpretation of term₀ and the aforementioned coercion derivation are solved.

Error Non extensible universe declaration not supported with monomorphic Program Definition.¶: The absence of additional universes or constraints cannot be properly enforced even without Program.

Program Fixpoint¶

A Fixpoint command with the program attribute may also generate obligations. It works with mutually recursive definitions too. For example:

Require Import Program Arith.

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

The Fixpoint command may include an optional fixannot annotation, which can be:

measure f R where f is a value of type X computed on any subset of the arguments and the optional term R is a relation on X. X defaults to nat and R to lt.
wf R x which is equivalent to measure x R.

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

Obligation 1.: 1 goal p, 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)

Require Import Program Arith.

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

Program Fixpoint div2 (n : nat) {measure n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := match n with | S (S p) => S (div2 p) | _ => O end.: div2 has type-checked, generating 6 obligations Solving obligations automatically... div2_obligation_1 is defined div2_obligation_6 is defined 4 obligations remaining Obligation 2 of div2: (forall (n : nat) (div2 : forall n0 : nat, n0 < n -> {x : nat | n0 = 2 * x \/ n0 = 2 * x + 1}) (p : nat) (Heq_n : S (S p) = n), (fun x : nat => S (S p) = 2 * x \/ S (S p) = 2 * x + 1) (S (` (div2 p ((fun (n0 : nat) (div3 : forall n1 : nat, n1 < n0 -> {x : nat | n1 = 2 * x \/ n1 = 2 * x + 1}) (p0 : nat) (Heq_n0 : S (S p0) = n0) => div2_obligation_1 n0 div3 p0 Heq_n0) n div2 p Heq_n))))). Obligation 3 of div2: (forall n : nat, (forall n0 : nat, n0 < n -> {x : nat | n0 = 2 * x \/ n0 = 2 * x + 1}) -> forall wildcard' : nat, (forall p : nat, S (S p) <> wildcard') -> wildcard' = n -> (fun x : nat => wildcard' = 2 * x \/ wildcard' = 2 * x + 1) 0). Obligation 4 of div2: (forall (n : nat) (div2 : forall n0 : nat, n0 < n -> {x : nat | n0 = 2 * x \/ n0 = 2 * x + 1}), let program_branch_0 := fun (p : nat) (Heq_n : S (S p) = n) => exist (fun x : nat => S (S p) = 2 * x \/ S (S p) = 2 * x + 1) (S (` (div2 p ((fun (n0 : nat) (div3 : forall n1 : nat, n1 < n0 -> {x : nat | n1 = 2 * x \/ n1 = 2 * x + 1}) (p0 : nat) (Heq_n0 : S (S p0) = n0) => div2_obligation_1 n0 div3 p0 Heq_n0) n div2 p Heq_n)))) (div2_obligation_2 n div2 p Heq_n) in let program_branch_1 := fun (wildcard' : nat) (H : forall p : nat, S (S p) <> wildcard') (Heq_n : wildcard' = n) => exist (fun x : nat => wildcard' = 2 * x \/ wildcard' = 2 * x + 1) 0 (div2_obligation_3 n div2 wildcard' H Heq_n) in let wildcard' := 0 in forall p : nat, S (S p) <> wildcard'). Obligation 5 of div2: (forall (n : nat) (div2 : forall n0 : nat, n0 < n -> {x : nat | n0 = 2 * x \/ n0 = 2 * x + 1}), let program_branch_0 := fun (p : nat) (Heq_n : S (S p) = n) => exist (fun x : nat => S (S p) = 2 * x \/ S (S p) = 2 * x + 1) (S (` (div2 p ((fun (n0 : nat) (div3 : forall n1 : nat, n1 < n0 -> {x : nat | n1 = 2 * x \/ n1 = 2 * x + 1}) (p0 : nat) (Heq_n0 : S (S p0) = n0) => div2_obligation_1 n0 div3 p0 Heq_n0) n div2 p Heq_n)))) (div2_obligation_2 n div2 p Heq_n) in let program_branch_1 := fun (wildcard' : nat) (H : forall p : nat, S (S p) <> wildcard') (Heq_n : wildcard' = n) => exist (fun x : nat => wildcard' = 2 * x \/ wildcard' = 2 * x + 1) 0 (div2_obligation_3 n div2 wildcard' H Heq_n) in nat -> let wildcard' := 1 in forall p : nat, S (S p) <> wildcard').

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 functional 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.

Program Lemma¶

A Lemma command with the program attribute uses the Russell language to type statements of logical properties. It generates obligations, tries to solve them automatically and fails if some unsolved obligations remain. In this case, one can first define the lemma’s statement using Definition and use it as the goal afterwards. Otherwise the proof will be started with the elaborated version as a goal. The program attribute can similarly be used with Variable, Hypothesis, Axiom etc.

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.

Command Obligation Tactic := ltac_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 Obligation.

This command supports the local, export and global attributes. local makes the setting last only for the current module. local is the default inside sections while global otherwise. export and global may be used together.

When global is used without export and when no explicit locality is used outside sections, the meaning is different from the usual meaning of global: the command's effect persists after the current module is closed (as with the usual global), but it is also reapplied when the module or any of its parents is imported. This will change in a future version.

Command Show Obligation Tactic¶: Displays the current default tactic.

Command Obligations of ident?¶: Displays all remaining obligations.

Command Obligation natural of ident? : type with ltac_expr??¶: Start the proof of obligation natural.

Command Next Obligation of ident? with ltac_expr?¶: Start the proof of the next unsolved obligation.

Command Solve Obligations of ident? with ltac_expr?¶: Tries to solve each obligation of ident using the given ltac_expr or the default one.

Command Solve All Obligations with ltac_expr?¶: Tries to solve each obligation of every program using the given tactic or the default one (useful for mutually recursive definitions).

Command Admit Obligations of ident?¶: Admits all obligations (of ident).

Note

Does not work with structurally recursive programs.

Command Preterm of ident?¶: Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging.

Flag Transparent Obligations¶: This flag controls 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.

Frequently Asked Questions¶

Error Ill-formed recursive definition.¶

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:

A measure function has to be defined;

The reduction is a little more involved, although it works well using lazy evaluation;

Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible.