'apply' incorrectly raises variables while guessing instances

[kyagrd]

Kind nm type.

Theorem forall-nabla-em: forall (x : nm), nabla y, (x = y) \/ (x = y -> false).
intros. right. search. % indeed freshness implies inequality
%QED

%% This one should not have been proven
Theorem nabla-forall-em: nabla y, forall (x : nm), (x = y) \/ (x = y -> false).
intros. apply forall-nabla-em with x = x n1. search.
%%%% It just got proved ... a disaster !?!?!?!

My understanding is that nabla only guarantee freshness over previously introduced variables but not for following quantification. However, I was able to prove that universal quantification following nabla has a excluded middle.

Here, the apply tactic instantiates x in forall-nabla-em with (x n1) and Abella aromatically instantiated y with n1. This is clearly wrong because n1 is not fresh for (x n1) in general for all x, in particular, when x = z\z. So substituting x with x n1 and assigning y with the same nominal constant used in the substitution just before seems like a bug in Abella.

I am using the current master branch version of Abella.

$ abella -v 2.0.5-dev

[kyagrd]

Here is another example from Alwen Tiu illustrating the same problem in one theorem,

Type q nm -> nm -> prop.
Theorem wrong: (forall (x:nm), nabla (y:nm), q x y) -> nabla (y:nm), forall (x:nm), q x y.
   intros.
   apply H1 with x = (x n1).
   search.

[chaudhuri]

I don't agree with this fix. Please see my personal email, Yuting.

[chaudhuri]

After a bunch of poking and prodding, I think this fix works by accident. The used_nominals field is populated by mysterious things. In the example that I posted to the list, used_nominals actually turns out to be empty!

I think the minus with the support of the lemma term overapproximates the correct answer.

[yvting]

First, used_nominals contains nominal constants provided by withs for instantiating nabla-quantified variables. For example, the following code snippet generates [n1] as used_nominals:

Kind i type.

Type p   i -> i -> i -> prop.

Theorem foo : forall (x:i), nabla (y:i) (z:i), p x y z.
skip.

Theorem bar : forall (x:i), false.
intros.
  apply foo with x = x, y = n1.

In the case of your example:

Kind nm type.

Theorem fast_false : false.
assert forall (x:nm), nabla y, (x = y -> false) /\ true.
apply H1 with x = n1.
backchain H2.

The apply tactic instantiates the forall-quantified variable x with a nominal constant. It does not instantiate the nabla-quantified variable y through with. As a result, used_nominals is empty.

# Second, I disagree that my fix works accidently. I tried to understand the heuristic underlying the implementation of the apply tactic and came up with a minimal modification that I believe fixes the problem. I shall summarize my understanding as follows.

Assume we have a hypothesis of the following form

H1: forall x1 ... xn, nabla y1 ... ym, S1 -> ... -> Sk -> A.

For simplicity of the discussion, let us ignore the support of with in apply at first. When H1 is applied to a list of arguments P1,...,Pk, the implementation of apply assumes that nominal constants used to instantiate x1,...,xn and y1,...,ym come from the following sources:

• the nominal constants in H1
• the nominal constants in P1,...,Pk
• fresh nominal constants that do no occur in H1 or P1,...,Pk (called dummy nominals in the implementation). Since at most m fresh nominal constants will be used to instantiate y1,...,ym, the implementation introduces m dummy nominals (introducing any extra fresh nominal constants will not affect the result of unification).

Those nominal constants form the support in the implementation of the apply tactic.

Now, the implementation picks m constants from the support with matching types as the instances for y1,...,ym. It then raises x1,...,xn over the remaining nominal constants in the support (Note that x1,...,xn should not be raised over the instances for y1,...,ym because of the ordering of quantifiers). It finally tries to unify the instantiated S1,...,Sk with the arguments P1,...,Pk and produces a new proof state.

The problem with the above heuristic is that the instances for y1,...,ym should not come from the nominal constants in H1 because this violates the freshness side-condition of the proof rules for nabla.

In other words, the candidates of the instances for y1,...,ym should be chosen from the following subset of support:

• the nominal constants in P1,...,Pk
• m fresh nominal constants that do no occur in H1 or P1,...,Pk

The key point of my fix has been summarized.

The support of partial instantiation of quantified variables through with further complicates the issue. I shall explain this feature a bit.

Let's consider the following instance of apply

apply H1 to P1 ... Pk with x1=t1,...,xi=ti,y1=n1,...,yj=nj

Without loss of generality we assume the first i variables in x1,...,xn and the first j variables in y1,...,ym are instantaited. The implementation of apply does the following:

• it instantiates x1,...,xi in H1
• it checks n1,...,nj do not occur in H1 after the instantiation (necessary to respect the nabla rules)
• it instantiates y1,...,yj
• it collects [n1,...,nj] in used_nominals

The rest of the procedure follows what I described above, except that used_nominals are excluded from support because they should not be chosen as instances for the remaining nabla quantified variables or raised over by the remaining forall quantified variables.

Now, come back to your example:

Kind nm type.

Theorem fast_false : false.
assert forall (x:nm), nabla y, (x = y -> false) /\ true.
apply H1 with x = n1.
backchain H2.

The apply tactic first instantiates x, resulting in the following hypothesis and used_nominals = []:

nabla y, (n1 = y -> false) /\ true.

It then computes support, which is [n1,n2] where n2 is a fresh nominal constant. It then chooses n1 as an instance for y. The last step triggered the bug because y should not be instantiated with a nominal constant that already occurs in the hypothesis.

I agree that the current implementation of apply is a bit messy and the heuristic underlying it is hard to understand. Still, I believe my fix is a valid one. Of course, if you have any alternative solution or good idea of refactoring the implementation I am all ears.

[yvting]

A few more comments on the following statement.

I think the minus with the support of the lemma term overapproximates the correct answer.

I don't think there exists the correct answer for instantiating quantified variables for the apply tactic. There can be many strategies for finding such instantiation that are correct. The current implementation simply follows a particular strategy, which is driven by the following intuition from my understanding.

When applying the term:

forall x1 ... xn, nabla y1 ... ym, S1 -> ... -> Sk -> A.

to arguments P1,...,Pk, nominal constants for instantiating x1,...,xn and y1,...,ym can be chosen from ones that already occur in the applied term and the arguments, and any other fresh nominal constants. However, there are further constraints on what nominal constants can be used for instantiating y1,...,ym:

1. They must not already occur in terms for instantiating x1,...,xn;
2. They must not already occur in S1 -> ... -> Sk -> A.

Such constraints are necessary to satisfy the side condition of the nabla-left rule. The first constraint is already satisfied by the implementation before my fix (by choosing m nominal constants from support for y1,...,ym and raising x1,...,xn over the remaining ones). However, the second constraint was not satisfied, leading to the bug we have. My fix exactly adds the checking of the second constraint and (I believe) fixes the bug.