Unification failure (nominal reasoning) over a disjunction of object logic propositions

[kyagrd]

I've copied and pasted the exactly the same lemma whose argument is a disjunction of object logic propositions. When trying to prove it by itself Abella complains that unification fails by nominal reasoning, which I have no idea what the reason is.

Theorem lemma_bad : forall L1 L2 P1 P2, ({L1 |- P1} \/ {L2 |- P2}) -> false.
skip.      

Theorem lemma_bad2 : forall L1 L2 P1 P2, ({L1 |- P1} \/ {L2 |- P2}) -> false.
intros. apply lemma_bad to H1. % think this should obviously work but outputs error

And this is what I get from abella output.

Welcome to Abella 2.0.5-dev

Abella < Theorem lemma_bad : forall L1 L2 P1 P2, ({L1 |- P1} \/ {L2 |- P2}) -> false.

============================
 forall L1 L2 P1 P2, {L1 |- P1} \/ {L2 |- P2} -> false

lemma_bad < skip.      
Proof completed.

Abella < Theorem lemma_bad2 : forall L1 L2 P1 P2, ({L1 |- P1} \/ {L2 |- P2}) -> false.

============================
 forall L1 L2 P1 P2, {L1 |- P1} \/ {L2 |- P2} -> false

lemma_bad2 < intros.

Variables: L1 L2 P1 P2
H1 : {L1 |- P1} \/ {L2 |- P2}
============================
 false

lemma_bad2 < apply lemma_bad to H1.
Error: While matching argument #1:
Unification failure (nominal reasoning)

Variables: L1 L2 P1 P2
H1 : {L1 |- P1} \/ {L2 |- P2}
============================
 false

P.S. replacing disjunction (\/) above into conjunction (/\) or implication (->) ends up with the same error as well.

P.S.2. for comparison, below works well. (This is logically equivalent to conjunction of the two arguments, but when we turn it into conjunction it fails as noted above).

Theorem lemma_bad : forall L1 L2 P1 P2, {L1 |- P1} -> {L2 |- P2} -> false.
skip.      

Theorem lemma_bad2 : forall L1 L2 P1 P2, {L1 |- P1} -> {L2 |- P2} -> false.
intros. apply lemma_bad to H1 H2. % Proof completes succesfully

[kyagrd]

Above is a very degenerate minimal example with the absurdity in the conclusion. The actual situation I came across was more close to like this.

Theorem lemmaGOOD : forall L P A, {L |- P} -> {L, A |- P}.    
intros. search.

Theorem lemmaGOOD2 : forall L P A, {L |- P} -> {L, A |- P}.
intros.
backchain lemmaGOOD with A = A. % works well and proof completes

Theorem lemmaBAD : forall L1 L2 P1 P2 A1 A2, {L1 |- P1} \/ {L2 |- P2} ->
      {L1, A1 |- P1} \/ {L2, A2 |- P2}.
skip.      

Theorem lemmaBAD2 : forall A1 A2 L1 L2 P1 P2, {L1 |- P1} \/ {L2 |- P2} ->
      {L1, A1 |- P1} \/ {L2, A2 |- P2}.
intros.
apply lemmaBAD to H1 with A1 = A1, A2 = A2. % error: Unification failure (nominal reasoning)

[chaudhuri]

Thanks for this. There are multiple bugs here -- a corner case of the apply tactic that seems dodgily implemented and a bad error message from the unification engine.

[chaudhuri]

This is an issue with AC0-unification of object sequent contexts and requires a bit of thought. A quick fix is unlikely, but I will fix the error message that incorrectly mentions nominals.

Meanwhile, you can easily work around the issue by giving the full instantiation for the variables that occur in object sequent contexts.

apply lemmaBAD to H1 with A1 = A1, A2 = A2, L1 = L1, L2 = L2.

[kyagrd]

@chaudhuri Thanks for working on the fix and also for the tip to work around!

[kyagrd]

@chaudhuri Thanks to your tip on the workaround, I was able to prove the lemma I was working on.

https://github.com/kyagrd/NonBisim2DF/tree/cbd059576a05e380bbd942b117487849051ba5ff/spi

This is a real working example I came across this bug while trying to formalize observer theories and intruder deduction for the spi calculus. The lemma itself is not so much profound but It is kind of an interesting example that demonstrates Abella's action with several different kinds of object level contexts and its related properties.