Introduction

The body of a theorem is a block of steps (derivations), the last of which must be the result to be proved. This page describes how each step in a proof is structured, and how steps can be proved in SASyLF.

The meta-syntax ( stuff )? is used to express optional parts and ellipsis (...) to indicate appropriate repetion.

Details

A derivation has the form:

• name : judgment (and name : judgment ...)? by justification

Alternately, the last derivation of a block may use the keyword proof to substitute for all that comes before the keyword by; it is implied that one is justifying the result that must be proved.

Justification

This section described each of the ways in which derivations can be justified:

• by unproved

This justification is accepted with a warning. This justification is useful when writing a proof to outline steps before the proof is completed.

• by name

This proves the current derivation by referencing a previous derivation.

• by name , name , ...

This proves a conjunction derivation (an and judgment) by showing how each part was proved earlier.

• by case analysis on name : case1 case2 ... end case analysis

This justification is delegated to a case analysis on a target, an existing derivation or syntax term. Each case has a pattern that must match the target. Pattern matching is at a single level only. Each case has a block of derivations, the last of which must be the derivation being proved here (and which therefore may use the proof keyword).

• by induction on name : case1 case2 ... end induction

This justification is a case analysis that, at the same time, indicates the inductive term, judgment which must be an explicit input of the theorem. This form of justification can only be done at the top-level of a theorem, and there can only be one induction justification per theorem.

• by inversion of rule-name on name

If a case analysis would need only one case and there is at least one premise, then it can be written as a justification of the premises (conjoined by and if there are more than one) using this form.
An older form of inversion may be used if one is interested in only a single premise (even if multiple premises exist for the rule), and this premise does not require the binding of new variables. Then one can justify just this single premise by inversion.

• by rule rule-name (on name , name ...)?

The derivation is justified by applying the given named rule to the previously proved derivations. The derivations must satisfy the rule's premises, in order.

• by theorem theorem-name (on name , (syntax) , ...)?

The derivation is proved by calling a theorem with the given inputs; judgment inputs are provided using previously proved derivations, syntax inputs by giving the syntax, which if more than a single term, must be parenthesized.
If the theorem being called is the one being proved, or a mutually inductive theorem, then the provided input for the induction variable must be a subderivation / subsyntax of the input for this theorem. If the mutually inductive theorem occurs earlier in the file, the inductive argument may be the same as the one for this theorem.

• by induction hypothesis (on ...)?

This is an inductive (recursive) call to the theorem being proved. Otherwise, it works the same as a theorem call (see previous).

• by solve

This justification asks SASyLF to try to find a proof. If it can, it prints the steps. Automatic solving is very limited.

The following three justifications concern contexts and bindings:

• by weakening on name

This justification applies if the derivation can be proved from an existing derivation by adding additional variables/assumptions.

• by exchange on name

This justification applies if the derivation can be proved from an existing derivation by reordering variable bindings and/or assumptions. The new derivation must not move uses of a variable out of scope.

• by substitution on name, name

This justification applies if the derivation can be proved from an existing derivation (first argument) with an assumption supplied (second argument). The assumption must be an instance of the special rule related to the binding being replaced. It is not a syntax term to substitute for the bound variable.

Cases

There are two forms for cases: those for syntax and those for judgments.

Syntax Case

If the target of the case analysis is a syntax term (instance of a syntactic nonterminal), then (aside from variables) one must provide one case for each production for the nonterminal. Each case takes the form

case production is proof end case

All the variables in the production must be new, for example by adding a suffix such as 1 or '. If the syntax term is bound in a non-empty context and a variable is one of the possibilities for the nonterminal, then one must provide a variable case that shows a possible binding for the variable in the context (using a new context):

case x assumes (Gamma', x:T) is proof end case

SASyLF currently does not support case analysis of terms using a variable, such as t1[x].

Rule Case

If target of a case analysis is an instance of a judgment, then each case must be a rule case of the form:

case rule

name : premise
...
---------------- rule-name
name : result

is

proof

end case

Each premise and the result must be named, although the result is usually named _ because there's no need to get a new name for the target derivation we are pattern matching.

The case must have the most general instance of the rule whose result matches the target derivation. If the rule result cannot be made to match the target, it is an error to have a case for the rule at all. In the body of the proof, one can use the named premises to justify other derivations. One may also assume the unification implied by the pattern match. All uses inside the local proof of any derivation from outside the scope of the pattern match are localized through application of the required unification.

If, because of pattern matching, only one case is possible, inversion (q.v.) may be a good option to use. If no case applies at all, then the case analysis can be empty. This allows us to justify any (type valid) judgment at all.

TODO: var binding cases