MetaPRL Computational Rewriting


MetaPRL defines two kinds of logical inferences: computational rewriting and inference rules. This page describes computational rewriting. Inference rules are described on the next page.


Rewrites are declared with the following form:

rewrite name [params] : [conditions] redex <--> contractum

A simple rewrite is defined as an equivalence between terms. For instance, the rewrite for beta-reduction is defined in the Itt_rfun module as follows:

rewrite reduceBeta : (lambda{v. 'b['v]} 'a) <--> 'b['a]

This rewrite pattern defines the beta redex, and its contractum. The contractum is formed by substitution. When the rewrite is applied to a beta-redex, the term matched by 'a is substituted for the variable matched by 'v in the body 'b.

Rewrites can also be conditional: they may depend on conditions provable in the context. Conditional rewrites are only defined for sequent calculi. Conditions are specified with the meta-implication -->. The following rewrite is an example of conditional rewriting in the Itt_int module:

rewrite unit : ('i != 0 in int) --> (('i /@ 'i) <--> 1)

Parameters provide extra variables and terms that are needed for rewriting. For example, a rewrite for reversing the beta reduction requires a term specifying the abstracted body (since it is not unique), a variable representing the bound variable, and also the argument of the application.

rewrite inverseBeta lambda{v. 'b['v]} 'a :
   'b['a] <--> (lambda{v. 'b['v]} 'a)


Rewrites are implemented with two forms: rewrites that are primitive to a logic use the prim_rw form:

prim_rw name [params] : [conditions] redex <--> contractum

If a declaration is given for the rewrite, the form in the prim_rw must be the same (with possible renaming in the bound variables).

Rewrites that are derived from previous rules in the logic are implemented with the interactive_rw form. The definition has the same form as the prim_rw:

interactive_rw name [params] : [conditions] redex <--> contractum

The interactive_rw form establishes a proof obligation, which may be fulfilled with the proof editor. The rewrite may be used whether it has been verified or not. When a logical theory is finished, the editor can be used to check for unsatisfied subproofs. Primitive rewrites never require a proof obligation, unsatisfied interactive rewrites generate an error during proof checking.