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
andDefinition
acts as if theprogram
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_{0}
. It then elaborates the preterm term
into a Coq
term term_{0}
, checking that the type of term_{0}
is coercible to
type_{0}
, and registers ident
as being of type type_{0}
once the
set of obligations generated during the interpretation of term_{0}
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.
See also
Sections Controlling reduction strategies and the conversion algorithm, unfold
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
wheref
is a value of typeX
computed on any subset of the arguments and the optional termR
is a relation onX
.X
defaults tonat
andR
tolt
.wf R x
which is equivalent tomeasure 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').
Note
The measure f R
and wf R x
annotations add an
implicit argument to the functions being defined. When the function
name is prefixed with @
(see Deactivation of implicit arguments for parsing),
the position of the extra argument needs to be taken into account,
e.g. by providing _
or an an explicit value.
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
andglobal
attributes.local
makes the setting last only for the current module.local
is the default inside sections whileglobal
otherwise.export
andglobal
may be used together.When
global
is used withoutexport
and when no explicit locality is used outside sections, the meaning is different from the usual meaning ofglobal
: the command's effect persists after the current module is closed (as with the usualglobal
), 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 Obligation natural of ident? : type with ltac_expr??¶
Start the proof of obligation
natural
.
- Command Final Obligation of ident? with ltac_expr?¶
Like
Next Obligation
, starts the proof of the next unsolved obligation. Additionally, atQed
time, after the automatic solver has run on any remaining obligations, Coq checks that no obligations remain for the givenident
when provided and otherwise in the current module.
- Command Solve Obligations of ident? with ltac_expr?¶
Tries to solve each obligation of
ident
using the givenltac_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 Stdlib.Program.Tactics
defines the default tactic for solving
obligations called program_simpl
. Importing Stdlib.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 tof
is not a direct subterm ofx
asb
is wrapped inside anexist
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.