\[\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
p := ?Goal : nat
j := ?Goal0 : nat
============================
k * n + k * m = j * p
- Proof.
- rewrite <- Nat.mul_add_distr_l.
- 1 focused goal (shelved: 2)
n, m, k : nat
p := ?Goal : nat
j := ?Goal0 : nat
============================
k * (n + m) = j * p
- subst j p.
- 1 focused goal (shelved: 2)
n, m, k : nat
============================
k * (n + m) = ?Goal0 * ?Goal
- 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.