     Next: Differences in the Up: Differences in the Previous: Elimination Rules

## Equality and Simplification Rules

Another major difference between the Lambda--prl rules and the Nuprl rules is the treatment of equality and simplification. The logic of Lambda--prl is sufficiently simple that all equality reasoning can be lumped into a single rule. Similarly, simplification of terms is handled by a single rule. The two are combined, together with some elementary arithmetic reasoning, into a decision procedure called arith which handles nearly all of the low--level details of Lambda--prl proofs. However, the additional expressiveness of the Nuprl logic prevents such a simple solution. For each term constructor there is a rule of equality, for each elimination form there is a computation rule, and there is a general rule of substitution.

For instance, the equality rule for inl is as follows. >> inl( ) = inl( ) in | by intro >> = in  >> in For decide there are two equality rules: the basic equality rule for the constructor and a computation rule. The goals are, respectively, >> decide( ; ; ) = decide( ; ; ) in and >> decide(inl( ); ; ) = in Equations obtained with these rules can be used by the equality and substitution rules.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995