Coq comes with an extension called
Derive, which supports program
derivation. Typically in the style of Bird and Meertens or derivations
of program refinements. To use the Derive extension it must first be
Require Coq.derive.Derive. When the extension is loaded,
it provides the following command:
Derive ident1 SuchThat one_term As ident2¶
ident1can appear in
one_term. This command opens a new proof presenting the user with a goal for
one_termin which the name
ident1is bound to an existential variable
?x(formally, there are other goals standing for the existential variables but they are shelved, as described in
When the proof ends two constants are defined:
The first one is named
ident1and is defined as the proof of the shelved goal (which is also the value of
?x). It is always transparent.
The second one is named
ident2. 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
- Require Coq.derive.Derive.
- [Loading ML file derive_plugin.cmxs ... done]
- Require Import Coq.Numbers.Natural.Peano.NPeano.
- Section P.
- Variables (n m k:nat).
- n is declared m is declared k is declared
- Derive p SuchThat ((k*n)+(k*m) = p) As h.
- 1 focused subgoal (shelved: 1) n, m, k : nat p := ?Goal : nat ============================ k * n + k * m = p
- rewrite <- Nat.mul_add_distr_l.
- 1 focused subgoal (shelved: 1) n, m, k : nat p := ?Goal : nat ============================ k * (n + m) = p
- subst p.
- 1 focused subgoal (shelved: 1) n, m, k : nat ============================ k * (n + m) = ?Goal
- No more subgoals.
- End P.
- Print p.
- p = fun n m k : nat => k * (n + m) : nat -> nat -> nat -> nat Arguments p (_ _ _)%nat_scope
- Check h.
- h : forall n m k : nat, k * n + k * m = p n m k
Any property can be used as
term, 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