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 options to control the generation of equalities and coercions.
-
Flag
Program Cases¶ This 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 option is deactivated.
-
Flag
Program Generalized Coercion¶ This controls the coercion of general inductive types when using Program (the option is on by default). Coercion of subset types and pairs is still active in this case.
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 ... done] [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... 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. Also, term :> explicitly asks the system to
coerce term to its support type. It can be useful in notations, for
example:
- Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
This notation denotes equality on subset types using equality on their support types, avoiding uses of proof-irrelevance that would come up when reasoning with equality on the subset types themselves.
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¶
-
Command
Program Definition ident := term¶ This command 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
identin the environment.-
Variant
Program Definition ident : type := term It 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 pretermterminto a Coq term term\(_{0}\), checking that the type of term\(_{0}\) is coercible to type\(_{0}\), and registersidentas being of type type\(_{0}\) once the set of obligations generated during the interpretation of term\(_{0}\) and the aforementioned coercion derivation are solved.
-
Variant
Program Fixpoint¶
The optional order annotation follows the grammar:
order ::= measureterm(term)? | wftermterm
measure f ( R )wherefis a value of typeXcomputed on any subset of the arguments and the optional (parenthesised) term(R)is a relation onX. By defaultXdefaults tonatandRtolt.wf R xwhich is equivalent tomeasure x (R).
The structural fixpoint operator behaves just like the one of Coq (see
Fixpoint), except it may also generate obligations. It works
with mutually recursive definitions too.
- 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
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 subgoal 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').
ご用心
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¶
-
Command
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 Definitionand use it as the goal afterwards. Otherwise the proof will be started with the elaborated version as a goal. TheProgramprefix can similarly be used as a prefix forVariable,Hypothesis,Axiometc.
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
Local|Global? Obligation Tactic := tactic¶ 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.Localmakes the setting last only for the current module. Inside sections, local is the default.
-
Command
Show Obligation Tactic¶ Displays the current default tactic.
-
Command
Solve Obligations of ident? with tactic?¶ Tries to solve each obligation of
identusing the giventacticor the default one.
-
Command
Solve All Obligations with tactic?¶ 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).注釈
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¶ Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque.
-
Flag
Hide Obligations¶ Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation.
-
Flag
Shrink Obligations¶ Deprecated since 8.7
This option (on by default) controls whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies.
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 tofis not a direct subterm ofxasbis wrapped inside anexistconstructor 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.