## MetaPRL Computational Rewriting

### Introduction

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.

### Declarations

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)

### Implementations

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.