Investigate the abella_schemas branch by Olivier Savary-Belanger

[chaudhuri]

Olivier has been doing an internship at INRIA/LIX and has come up with an interesting implementation of context schemas.

• [ ] summarize the features for the Abella devs
• [ ] make the barnch merge-able into master
• [ ] make a post fo the Abella user mailing list asking for comments
• [ ] merge into master

[lambdacalculator]

This was removed from the 2.0.4 release, but I wanted to add a few observations about context reasoning in the hopes that, when schemas are eventually revived, some of these ideas might make it into the implementation.

First, there are three situations that have come up in my developments that were outside of the previous schema implementation (see below for some examples):

1. A context definition might not end in a nil case, but in another context predicate. This occurs when we want to prove a theorem in a particular context, but the induction introduces new assumptions that are different from those in that context. So we define an extended context predicate whose base case is the existing one and whose other clauses are the new assumption blocks. (Note: it is sometimes possible instead to use a single, combined context definition in this case, but not always.)
2. A multi-argument context relation might include arguments that have types other than olist. For example, I might define substitutions in the object language and extend them to substitutions on contexts in the meta language. The validity predicate for context substitutions would include as arguments an object-level substitution, say of type subst, and two meta-level contexts, as olists.
3. A multi-argument context relation might, in its various inductive clauses, not change particular arguments on the inductive call. For example, suppose we have a context predicate with two different types of assumptions, say of x A and typ t, and we want to be able to split this context into a typing context and a type-variable context. Such a context definition would have a nil case, one case for of x A, which would add this assumption to the second argument and leave the third unchanged, and one case for typ t that would add this to the third argument and leave the second unchanged.

Also, here is a list of features that I would hope a good schema implementation would have:

• The inversion theorems that are automatically proven upon a schema definition should be as strong as possible. This was not the case before. (I'll give an example of what I mean by "as strong as possible" below.)
• When doing a case on an assumption of the form {G |- p M}, where G has been predicated to satisfy some schema, we should only be given variable cases for the clauses of the schema that match p M after backchaining. In particular, if no clauses of the schema match then we should not be given a variable case at all. (This is a really big issue for me; I'll mention an example below.)
• We should be able to have automatically proved, either on demand (say as a tactic) or maybe even when there is a schema conflict during unification, lemmas stating that one context predicate implies another, for example if the second predicate adds additional assumption blocks, or the assumption blocks are more general. This corresponds to "world subsumption" in Twelf.

Here is an example of what I mean by "as strong as possible" that also illustrates one of my other points above. Consider this context definition from one of my recent developments:

% Extended subtitutions S : G' -> G
Define xsubst : olist -> olist -> olist -> prop by
  xsubst S P' P := subst S P' P;    % original substitution predicate
  nabla x x', xsubst (for x x' :: S) (dim x' :: G') (dim x :: G) := xsubst S G' G;
  nabla a a', xsubst (sub a a' :: S) (tm a' :: G') (tm a :: G) := xsubst S G' G.

Here are two of the context inversion lemmas that I'm calling as strong as possible:

Theorem xsubst_inv1 : forall S G' G E,
  xsubst S G' G -> member E S ->
    (exists X R', E = for X R' /\ is_name/dim X  /\ {G' |- dim R'} /\ member (dim X) G) \/  % from subst_inv1
    (exists X X', E = for X X' /\ is_name/dim X /\ is_name/dim X' /\ member (dim X') G' /\ member (dim X) G) \/
    (exists A A', E = sub A A' /\ is_name/tm A /\ is_name/tm A' /\ member (tm A') G' /\ member (tm A) G).

Theorem xsubst_inv3 : forall S G' G E,
  xsubst S G' G -> member E G ->
    (exists X R', E = dim X /\ is_name/dim X /\ member (for X R') S /\ {G' |- dim R'}) \/  % from subst_inv3
    (exists X X', E = dim X /\ is_name/dim X /\ is_name/dim X' /\ member (for X X') S /\ member (dim X') G') \/
    (exists A A', E = tm A /\ is_name/tm A /\ is_name/tm A' /\ member (sub A A') S /\ member (tm A') G').

(I'll use the built-in polymorphic is_name instead of my duplicated monomorphic versions when it is available again. Also, in my hand-proven theorems, I've combined the first and second disjuncts in each theorem because they provably overlap, but I wouldn't necessarily expect this to be detected in every case automatically.)

Finally, concerning caseing on assumptions of the form {G |- p M}, let me mention one situation in a current development. I've defined a substitution predicate in the object language that puts the substitution itself in the context, as with subst and xsubst above, so that my substitution judgments look like {S |- sub M M'}, for example. The problem comes when I want to unfold the definition of substitution. Every time I unfold one substitution, I get two subgoals, one of which I want, and the other which is a spurious variable case. However, if S were an instance of a schema, it would be known that sub couldn't occur in S and I wouldn't be given a nested set of subgoals. This becomes particularly troublesome when I have to unfold (as I had to do) nine substitutions in a row and have to deal with subgoals like 1.29.1.1.1.1.1.1.1.1.1 (the one I want) plus 9 others I don't want (1.29.(1.)*.2), instead of no subgoals at all.

I hope these examples and suggestions will be helpful when schemas are revisited.