\[\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 derivation

Rocq comes with an extension called `Derive`, which supports program derivation. Typically in the style of Bird and Meertens formalism or derivations of program refinements. To use the Derive extension it must first be required with `From Corelib Require Derive`. When the extension is loaded, it provides the following command:

Command Derive open_binders in type as ident
Command Derive open_binders SuchThat type As ident

  where `open_binders` is a list of the form `identi : typei` which can appear in `type`. This command opens a new proof presenting the user with a goal for `type` in which each name `identi` is bound to an existential variable of same name `?ident__i` (these existential variables are shelved goals, as described in `shelve`).

  When the proof is complete, Rocq defines constants for each `identi` and for `ident`:

  - The first ones, named `identi`, are defined as the proof of the shelved goals (which are also the value of `?identi`). They are always transparent.

  - The final one is named `ident`. It has type `type`, and its body is the proof of the initially visible goal. It is opaque if the proof ends with `Qed`, and transparent if the proof ends with `Defined`.

Example

Module Nat.
  Interactive Module Nat started
Axiom mul_add_distr_l : forall n m p : nat, n * (m + p) = n * m + n * p.
  mul_add_distr_l is declared
End Nat.
  Module Nat is defined

From Corelib Require Derive.
  [Loading ML file rocq-runtime.plugins.derive ... done]
Section P.
Variables (n m k:nat).
  n is declared m is declared k is declared
Derive j p in ((k*n)+(k*m) = j*p) as h.
  1 focused goal (shelved: 2) n, m, k : nat j := ?j : nat p := ?p : nat ============================ k * n + k * m = j * p
Proof.
rewrite <- Nat.mul_add_distr_l.
  1 focused goal (shelved: 2) n, m, k : nat j := ?j : nat p := ?p : nat ============================ k * (n + m) = j * p
subst j p.
  1 focused goal (shelved: 2) n, m, k : nat ============================ k * (n + m) = ?j * ?p
reflexivity.
  No more goals.
Qed.
End P.
Print j.
  j = fun k : nat => k : nat -> nat Arguments j k%_nat_scope
Print p.
  p = fun n m : nat => n + m : nat -> nat -> nat Arguments p (n m)%_nat_scope
Check h.
  h : forall n m k : nat, k * n + k * m = j k * p n m

Any property can be used as `type`, not only an equation. In particular, it could be an order relation specifying some form of program refinement or a non-executable property from which deriving a program is convenient.

Note

The syntax `Derive open_binders SuchThat type As ident` is obsolete and to be avoided.

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