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:
  1. 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)