\[\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 Rocq 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 Rocq 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 Rocq 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 is Rocq's term language. We use the same syntax as Rocq and permit to use implicit arguments and the existing coercion mechanism. Input terms and types are typed in an extended system (Russell) and elaborated into Rocq terms. The elaboration process may produce some proof obligations which need to be resolved to create the final term.

## Elaborating programs

The main difference from plain Rocq 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 Rocq (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= yes​no?

  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:

From Corelib.Program Require Import Basics Tactics.

Program Definition id (n : nat) : { x : nat | x = n } := if sumbool_of_bool (Nat.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, Nat.leb n 0 = true -> (fun x : nat => x = n) 0). Obligation 2 of id: (forall n : nat, Nat.leb n 0 = false -> (fun x : nat => x = n) (S (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 Rocq 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 Rocq type `type0`. It then elaborates the preterm `term` into a Rocq term `term0`, checking that the type of `term0` is coercible to `type0`, and registers `ident` as being of type `type0` once the set of obligations generated during the interpretation of `term0` 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:

From Corelib.Program Require Import Basics Tactics.

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)

From Corelib.Program Require Import Basics Tactics Wf.

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 5 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 (proj1_sig (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 (proj1_sig (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 (proj1_sig (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'). Obligation 6 of div2: (well_founded (MR lt (fun recarg : nat => let n := recarg in n))).

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 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 := generic_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 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? with generic_tactic?

  Start the proof of obligation `natural`.

Command Next Obligation of ident? with generic_tactic?

  Start the proof of the next unsolved obligation.

Command Final Obligation of ident? with generic_tactic?

  Like `Next Obligation`, starts the proof of the next unsolved obligation. Additionally, at `Qed` time, after the automatic solver has run on any remaining obligations, Rocq checks that no obligations remain for the given `ident` 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 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 `Corelib.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 Rocq 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.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF