Reductions

[John Tang Boyland]

SASyLF currently requires induction to be on a subterm, or a sub-premise of the induction argument. There is no support for multiple induction variables, or for computed subterms, such as greater-than.

[John Tang Boyland]

Twelf has a way to declare that a type family (usually a judgment or a meta-theorem) reduces an argument in some way. This enables one to prove that if n1 > n2 then n2 is a subterm of n1, and then to permit induction on n2 when the argument is n1.

It makes sense to add the equivalent idea to SASyLF as

judgment gt: n1 > n2
@Reduces(n2 < n1)

The same annotation could also be added to a theorem or lemma.

[John Tang Boyland]

After running into problems with Twelf's reduction system, I would like to change reduction to not require a subterm, but simply a term with fewer steps in it. So "<" would mean "smaller", not "subterm of".

[John Tang Boyland]

Syntax for multiple induction terms:

proof by induction on x,y,z:
   ...
end induction

and the one liner

use induction on x,y,z

to avoid the need to have a case analysis on x.

[John Tang Boyland]

use induction on x, {y, z}

implemented. {x, y} means that one of x and y, in either order, must be reduced in the call. Unlike Twelf's [X Y], this permits the arguments to be swapped.