8.6 Quote
The tactic Quote allows to use Barendregt's so-called
2-level approach without writing any ML code. Suppose you have a
language L of
'abstract terms' and a type A of 'concrete terms'
and a function f : L -> A. If L is a simple
inductive datatype and f a simple fixpoint, Quote f
will replace the head of current goal a convertible term with the form
(f t). L must have a constructor of type: A
-> L.
Here is an example:
Coq < Require Quote.
[Reinterning Quote...done]
Coq < Parameters A,B,C:Prop.
A is assumed
B is assumed
C is assumed
Coq < Inductive Type formula :=
Coq < | f_and : formula -> formula -> formula (* binary constructor *)
Coq < | f_or : formula -> formula -> formula
Coq < | f_not : formula -> formula (* unary constructor *)
Coq < | f_true : formula (* 0-ary constructor *)
Coq < | f_const : Prop -> formula. (* contructor for constants *)
Coq <
Coq < Fixpoint interp_f [f:formula] : Prop :=
Coq < Cases f of
Coq < | (f_and f1 f2) => (interp_f f1)/\(interp_f f2)
Coq < | (f_or f1 f2) => (interp_f f1)\/(interp_f f2)
Coq < | (f_not f1) => ~(interp_f f1)
Coq < | f_true => True
Coq < | (f_const c) => c
Coq < end.
formula_ind is defined
formula_rec is defined
formula_rect is defined
formula is defined
Coq <
Coq < Goal A/\(A\/True)/\~B/\(A <-> A).
Coq < Coq < Coq < Coq < Coq < Coq < Coq < interp_f is recursively defined
Coq < Quote interp_f.
Coq < 1 subgoal
============================
A/\(A\/True)/\~B/\(A<->A)
The algorithm to perform this inversion is: try to match the
term with right-hand sides expression of f. If there is a
match, apply the corresponding left-hand side and call yourself
recursively on sub-terms. If there is no match, we are at a leaf:
return the corresponding constructor (here f_const) applied
to the term.
Error messages:
-
Quote: not a simple fixpoint
Happens when Quote is not able to perform inversion properly.
8.6.1 Introducing variables map
The normal use of Quote is to make proofs by reflection: one
defines a function simplify : formula -> formula and proves a
theorem simplify_ok: (f:formula)(interp_f (simplify f)) ->
(interp_f f). Then, one can simplify formulas by doing:
Quote interp_f.
Apply simplify_ok.
Compute.
But there is a problem with leafs: in the example above one cannot
write a function that implements, for example, the logical simplifications
A Ù A ® A or A Ù ¬ A ® False. This is
because the Prop is impredicative.
It is better to use that type of formulas:
Coq < Inductive Set formula :=
Coq < | f_and : formula -> formula -> formula
Coq < | f_or : formula -> formula -> formula
Coq < | f_not : formula -> formula
Coq < | f_true : formula
Coq < | f_atom : index -> formula. (* contructor for variables *)
index is defined in module Quote. Equality on that
type is decidable so we are able to simplify A Ù A into A at
the abstract level.
When there are variables, there are bindings, and Quote
provides also a type (varmap A) of bindings from
index to any set A, and a function
varmap_find to search in such maps. The interpretation
function has now another argument, a variables map:
Coq < Fixpoint interp_f [vm:(varmap Prop); f:formula] : Prop :=
Coq < Cases f of
Coq < | (f_and f1 f2) => (interp_f vm f1)/\(interp_f vm f2)
Coq < | (f_or f1 f2) => (interp_f vm f1)\/(interp_f vm f2)
Coq < | (f_not f1) => ~(interp_f vm f1)
Coq < | f_true => True
Coq < | (f_atom i) => (varmap_find True i vm)
Coq < end.
Current goals aborted
Quote handles this second case properly:
Coq < Goal A/\(B\/A)/\(A\/~B).
Coq < Coq < Coq < Coq < Coq < formula_ind is defined
formula_rec is defined
formula_rect is defined
formula is defined
Coq < Quote interp_f.
Coq < Coq < Coq < Coq < Coq < Coq < Coq < interp_f is recursively defined
It builds vm and t such that (f vm t) is
convertible with the conclusion of current goal.
8.6.2 Combining variables and constants
One can have both variables and constants in abstracts terms; that is
the case, for example, for the Ring tactic (chapter
20). Then one must provide to Quote a list of
constructors of constants. For example, if the list is
[O S] then closed natural numbers will be considered as
constants and other terms as variables.
Example:
Coq < Inductive Type formula :=
Coq < | f_and : formula -> formula -> formula
Coq < | f_or : formula -> formula -> formula
Coq < | f_not : formula -> formula
Coq < | f_true : formula
Coq < | f_const : Prop -> formula (* constructor for constants *)
Coq < | f_atom : index -> formula. (* constructor for variables *)
Coq <
Coq < Fixpoint interp_f [vm:(varmap Prop); f:formula] : Prop :=
Coq < Cases f of
Coq < | (f_and f1 f2) => (interp_f vm f1)/\(interp_f vm f2)
Coq < | (f_or f1 f2) => (interp_f vm f1)\/(interp_f vm f2)
Coq < | (f_not f1) => ~(interp_f vm f1)
Coq < | f_true => True
Coq < | (f_const c) => c
Coq < | (f_atom i) => (varmap_find True i vm)
Coq < end.
Coq <
Coq < Goal A/\(A\/True)/\~B/\(C<->C).
Coq < Quote interp_f [A B].
Coq < Coq < Coq < Coq < Coq < Coq < formula_ind is defined
formula_rec is defined
formula_rect is defined
formula is defined
Coq < Undo. Quote interp_f [B C iff].
Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < Coq < interp_f is recursively defined
Warning: This tactic is new and experimental. Since function inversion
is undecidable in general case, don't expect miracles from it !
See also: file theories/DEMOS/DemoQuote.v
See also: comments of source file tactics/contrib/polynom/quote.ml
See also: the tactic Ring (chapter 20)