Request for aliases - Githubissues

It would be nice if Abella allowed as aliases for Theorem the commands Lemma, Proposition, Corollary, Example, Conjecture (and others I might be overlooking).

Also, Abella used to have a command, Axiom, that was replaced in Version 1.1 with Theorem + skip. However, I think there is a distinction to be made here: an axiom is something that you use but never plan to prove, whereas skip is a development device that allows you to omit a proof temporarily with the intent of providing one later. (And you could always display "Axiom" in a red font, like you do with "skip" in the emacs interface.) An axiom is also something that could play into a kind of theory modularity the way that the experimental Import .. with does with definitions.

Finally, it would be nice if I could write G ,, E as an alias for E :: G. Then the context of {G, E |- P} would be G ,, E and the definition of context predicates would look more like traditional definitions. Also, we could write a sensible definition of append for contexts:

Define append : olist -> olist -> olist -> prop by
  append G nil G;
  append G1 (G2 ,, E) (G3 ,, E) := append G1 G2 G3.

I say sensible, because what you would want to write as {G1, G2 |- P} would become {G1_G2 |- P} where append G1 G2 G1_G2, and {G1, of x T, G2 x |- P x} would become {G1_x_G2 x |- P x} where append (G1 ,, of x T) (G2 x) (G1_x_G2 x).

Even better, of course, would be to have a built-in append and allow contexts like the above, but then you are doing associativity reasoning during unification of contexts, and I'm not sure how difficult that would be.

EDIT (5/2/17): Looking back over the uses of "split contexts" in my developments, whenever I would want to write {G1, G2 |- P}, G1 is always fixed, and only G2 changes in applications of the IH. A typical example is the substitution theorem for a dependently-typed system, where the variable being substituted for is in the middle of the context, and the substitution is applied to all assumptions to the right of it. (You don't have exchange because of the dependencies between assumptions.)

The consequence is that you wouldn't have to do general associativity reasoning with split contexts, at least in all of my use-cases; you'd just have to match context segments from left to right, with the commas acting as fixed positions in the context across which you were not allowed to match. That is, matching G1,G2 against G3,G4 would match G1 against G3 and G2 against G4. And if you tried to match G against G1,G2, then G would have to match G1 and G2 would have to be nil.

abella-prover / abella

Request for aliases #88