Nuprl Basics - Proofs

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Proofs

Nuprl employs a "sequent style" logic for making arguments about Types and Propositions. The assertions at each proof step must be in the form of Sequents, which usually involve variable declarations for arbitrary hypothetical values and assumptions made for the sake of argument. A proof is a tree of sequents labelled with "justifications"; the sequent at the root of a subtree is called the "goal", and the sequents of the children are called the "subgoals". The Nuprl system actually generates the subgoals from the goal and its justification, and such subgoal generation is called "refinement" since one often thinks of this step as refining a problem specification into sufficient subproblems. Such a problem is completely solved, or a proof is "complete", when there are no remaining subgoals.

A goal, a justification, and the resultant subgoals constitute a "proof step", sometimes called an "inference step"; the goal and subgoals are often called the "conclusion" and "premises" of the inference. A principle aim of the Nuprl system design is to assist in the relatively easy generation of "valid" inferences, i.e., inferences whose conclusions are true if their premises are, and yet to permit these inferences within a proof to be appropriate to a human reader, i.e., rather high-level.

Although ultimately inferences are justified by low level rules, one major style of proof is to formulate each step in a manner that seems evident, or at least plausible, to a human reader, and to make the "granularity" coarse enough so that the whole proof is not too tedious to read or comprehend as a whole. This is technically possible because of programs called "tactics".

Usually, for the reader of a proof, the most interesting thing about tactic code of a justification is which lemmas, definitions, or hypotheses it refers to, and what witnesses are provided (Note that hypotheses are often referred by number, negative numbers indicating counting backwards from the conclusion as zero). Sometimes the code is elided in favor of a user-created summary comment which is displayed instead (of course the tactic code is still there somewhere).

Tactics

In Nuprl, a justification is "tactic" code. Given a collection of prespecified "primitive" inference forms, a tactic is a program for reducing a desired proof goal to premises by composing primitive inferences. A tactic is essentially a program for constructing such an inference tree, and one chooses which tactics to apply according to how you want to generate subgoals from the goal. The execution of the tactic gives rise to an inference step, the premises being all the unproved leaf premises of the primitive proof tree. Further, to count as a tactic, although its execution might not terminate or might raise an exception, if it does terminate without exception, then it must be guaranteed to generate subgoals justifiable by primitive inferences.

In order to freely write heuristic tactics, one must have some practical criterion for recognizing tactics. In ML, this criterion is type checking a program to the type "tactic".

The labor of justifying an inference is divided between ascertaining that the program generating the subgoals is a tactic, and checking the primitive inference rules, which are presumably formulated to make such verification feasible; primitive inference forms tend to be expressed schematically. In contrast, the justification of complex forms of inference via tactics is in terms of the generic criterion for being a tactic (i.e. that the result of execution determines a primitive proof tree), and is not schematically described.