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 substituion. 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 primrw form:
primrw name [params] : [conditiona] redex <--> contractum
If a declaration is given for the rewrite, the form in the primrw must be the same (with possible renamining in the bound variables).
Rewrites that are derived from previous rules in the logic are implemented with the interactiverw form. The definition has the same form as the primrw:
interactiverw name [params] : [conditions] redex <--> contractum
The interactiverw 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, unstaisfied interactive rewrites generate an error during proof checking.