Type incorrect applications over nominal variables by assert

[kyagrd]

Kind ty1 type.
Kind ty2 type.

Define name1 : ty1 -> prop by nabla x, name1 x.
Define name2 : ty2 -> prop by nabla x, name2 x.

Theorem bug1 : nabla x, name1 x.
intros.
assert name2 n1. % this is a type error but succeeds
%% H1 : name2 n1
%% =============
%%  name1 n1
search.

n1 is of type ty1 but being applied name2 by assertion.

Tested with the commit b58e4b86c3d7da52f3d959dfc802e412179b2b0d

[chaudhuri]

This is not a bug. You can see the quantification scopes of nominal constants more clearly if you do Set types on. Each nominal constant is effectively locally quantified per formula (that's a bit of a white lie but suffices for this case), so the two n1s are unrelated.

[lambdacalculator]

Can you elaborate on the "white lie" you refer to here? I've been tripped up several times by nominal-related issues, and it would be good to have a clear understanding of what is going on. For example, if nominals were really locally quantified, there wouldn't be any need for the permute tactic. However, I have occasionally found that tactic indispensable for setting up an application of the IH on a subterm with additional nominals when Abella doesn't choose the right names for them. My hunch is that this is correlated with a use of exchange in a paper proof, but it has always seemed a bit unclear to me.

[chaudhuri]

The white lie is that nominal constants are the alternative to local contexts in the two different presentations of nabla (G vs. LINC), so presenting it in the form of local contexts is slightly misleading. However, there is a way to move between the two formulations if you enrich LINC with exchange, weakening, and strengthening for local contexts (something like but not exactly Alwen Tiu's LG system).

The permute tactic is needed because Abella does not implement equivariant matching of nominal constants in the "trivial search" part of tactics such as apply. See #26. This is yet another departure in the Abella implementation from the G inference rules, where the initial rule matches the left and the right up to equivariance.

I don't see what permute has to do with exchange, since permuting names is allowed even in presentations of nabla without exchange for local contexts.

[lambdacalculator]

Is there anything that can be done with how Abella chooses nominals in a new hypothesis? Perhaps a heuristic could be implemented that could somehow keep nominals "aligned" across hypotheses, thereby lessening, or even virtually eliminating, the need for permute. In other words, guess the right permutation before assigning one.

[chaudhuri]

One thing that I have played with a bit a few years back is to "normalize" all nominals to n1, n2, ..., nk in a left-to-right reading of every hypothesis. This almost works, but I seem to recall that it does not entirely eliminate the need for permute. I don't recall off the top of my head what the exceptional case was. I probably have that branch lying around in one of my dozen computers so if I find it I'll put it on my Abella fork in github. (This change breaks too many existing proofs, so it won't be added to Abella until a major version bump.)

If you have an example that requires the use of permute a lot, I am curious to see it. I think I have been forced to use it maybe no more than twice in all my years with Abella.