Proofs

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

Multiple derivations conjoined with and are used if the justification proves a conjunction. It will not work to write name : judgment1 and judgment2 by ...; each conjunct needs its own name.

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.

In place of a derivation, one may use the syntax

• use inversion of (rule)? rule_name on name

if the case analysis of name has only one case (rule_name) and that rule has no premises. This derivation doesn't prove anything, but it performs any unification of variables presumed by the case. This special form (new to SASyLF 1.2.3) is useful for inverting equality judgments which require absolute identity. As of SASyLF 1.2.5, the rule could have premises; they are simply ignored. As of SASyLF 1.5.0, the of rule rule_name part can be omitted altogether, and one can invert a single case syntax as well, with the names of any new subparts given in a where clause.

In place of a derivation, one may also use the syntax (new to SASyLF 1.2.6)

• use induction on name

which marks that induction will be on the given derivation/nonterminal without forcing an immediate case analysis. It has been a long-standing annoyance that these were coupled. Starting in SASyLF 1.3.1, instead of a name, one may use a comma-separated series of names for lexicographic induction. Furthermore, one may use, in place of a name, a set of names ({ name , ... }) for unordered induction which means that some permutation of the names has every corresponding argument to the induction hypothesis staying the same or getting smaller, with at least one getting smaller.

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. 1.3.1 and later: If the derivation being proved is a disjunction (judgments ored together), then the derivation named may be any one of the constituents.

• 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)? 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.

  As of 1.5.0, one can invert an 'or' clause with only one remaining option (presumably after a do case analysis) by using by inversion of or on name

• by contradiction on name

  (This syntax was added in SASyLF 1.2.3) If case analysis on name needs no cases, then you can use this form of justification.

• 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. If the rule comes from another module, the rule-name must be qualified with the module name: module-name.rule-name

• 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.

  If the theorem is in another module, then the name must be qualified with the module.

• 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, buggy and basically deprecated.

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. The names of variables must not change.

• 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 names of variables must not change. 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.

  Substitution was given a cleaner semantics in 1.2.6/1.3.1. Assuming we have

  d1: bindings, x : T, other bindings |- t[x] : T'
  d2: bindings |- t2 : T
  

  then substitution on d1, d2 will give us

  bindings, other bindings |- t[t2] : T'
  

  Substitution requires that the second argument be an instance of the judgment which has the special rule for the binding. The bindings of the second derivation must appear in the same order at the start of the second derivation. Different than weakening or exchange above, the bindings in common may have different variable names. This ability is important when performing contraction like operations:

  d1 : Gamma, x1 : T, x : T |- t[x,x1] : T' by ...
  d2 : Gamma, x : T |- x : T by ...
  d3 : Gamma, x : T |- t[x,x] : T' by substitution on d1, d2
  

Cases

There are three forms for cases: those for syntax, those for judgments, and those for disjunctions.

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 before 1.3.3 did 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 be 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. The rule-name should not be qualified, even if it comes from another module.

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. This situation enables the use of the by contradiction on name justification.

Context Cases

TODO

Disjunction Cases

If the derivation being matched is a disjunction (using the or syntax of SASyLF 1.3.1 and later), then the case has the form

case or name : premise is
    proof
end case

A disjunction derivation is true if there is a derivation for one of the parts; the case handles this one. To cover all cases, one must have a case for each part.

Partial Case Analysis

When writing a proof, one may wish to handle certain situations up-front in a partial case analysis. Starting in SASyLF 1.3.1, one can write

do case analysis on name
    case1
    case2
    ...
end case analysis

Each case should prove the statement required by the context. The case analysis need not be complete, and this form cannot be used as the last statement in a series precisely because it doesn't finish the proof. But the cases that are handled here will not need to be handled later. This can reduce a Cartesian product of cases to a more manageable number, as seen in the proof of cut elimination.

Explicit Rebinding

A rule case or an inversion of a rule may imply a rebinding of a variable. For instance, using the typical definition of equality, if one has a derivation d: n1 = n2 then when writing use inversion of eq on d, then n1 and n2 are bound to each other. As of SASyLF 1.3.5, one may explain this rebinding using a 'where' clause as in where n1 := n2. The rebinding could be described in the opposite direction too in this instance. In general 'where' clauses are written as follows:

• where v := syntax ( and v := syntax )*

SASyLF has an option (--compwhere on the command line, or in the SASyLF preferences of Eclipse) to make such explicit rebinding mandatory.

Last Derivation

The last derivation of a block should be for the judgment being proved. As a special case (since 1.3.1), if this is an empty disjunction (contradiction) it is accepted as a proof for anything. This last judgment must be the empty disjunction, not a judgment that case analysis can show is uninhabited; for the latter case, you must continue to use a case analysis, for example by contradiction on.

Starting in SASyLF 1.3.3, if the judgment being proved is an or judgment, the last derivation may prove one of the disjuncts instead, or even a disjunct with fewer elements all included in the judgment to be proved. In this case the proof by syntax cannot be used since it would be claiming that the last derivation was the desired disjunction.