Can't solve even when conclusion matches assumption exactly

[talex5]

TLAPS is failing to prove a very simple claim, and showing this in "Interesting Obligations":

ASSUME NEW CONSTANT BufferSize,
       NEW VARIABLE Sent,
       NEW VARIABLE Got,
       NEW CONSTANT n \in Nat,
       \A n_1 \in Nat : Sent >= n_1 => [](Sent >= n_1) 
PROVE  \A n_1 \in Nat : Sent >= n_1 => [](Sent >= n_1)

I suppose this is to do with the coalescing, but the error is a bit confusing! Is there some way to get tlapm to show what it actually sent to the solver?

BY PTL works in this case, but similar cases with ASSUME / PROVE don't. e.g.

EXTENDS Naturals, TLAPS

VARIABLES Sent

LEMMA L1 ==
  ASSUME NEW n \in Nat
  PROVE  Sent >= n => [](Sent >= n)
OMITTED

THEOREM
  ASSUME NEW n \in Nat
  PROVE  Sent >= n + 1 => [](Sent >= n + 1)
<1> DEFINE F(i) == Sent >= i => [](Sent >= i)
<1> ASSUME NEW n_1 \in Nat
           PROVE F(n_1)
    BY L1
<1> HIDE DEF F
<1> F(n + 1) OBVIOUS
<1> QED BY DEF F

I haven't been able to track it down, but it seems that renaming variables (e.g. changing i to n in the definition of F) often fixes these problems, and they remain fixed when renaming them back again!

I'm using the rolling release (tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz), with:

$ /opt/tlapm/bin/tlapm --version
80088ef

[talex5]

OK, I have some better evidence now for a caching bug:

I copied the entire text to a new spec (test2) and <1>a fails there!

I'm pressing ^G^G at the top of each file to refresh all the proofs. I can see that it is refreshing both (it's not the lost keyboard short-cuts bug). It consistently fails to prove in test2 and consistently succeeds for test.

[muenchnerkindl]

Thank you for reporting this. Indeed, there appears to be an issue with the names of bound variables in temporal formulas. The following passes on my side (I took care to use distinct variable names):

---- MODULE CoalescingBug ----
EXTENDS Naturals, TLAPS

VARIABLES sent

LEMMA L1 == 
    ASSUME NEW n \in Nat
    PROVE  sent >= n => [](sent >= n)
PROOF OMITTED 

THEOREM
    ASSUME NEW m \in Nat
    PROVE  sent >= m+1 => [](sent >= m+1)
<1>. DEFINE F(i) == sent >= i => [](sent >= i)
<1>1. \A n \in Nat : F(n)   BY L1
<1>2. F(m+1)
  <2>. HIDE DEF F 
  <2>. QED  BY <1>1
<1>. QED  BY <1>2

=====

When renaming the bound variable n to i in step <1>1, the proof still appears to pass. However, when fingerprints are deleted (for example by removing the .tlacache directory), the proof fails.

Re your question on inspecting the exact goal that is sent to the backends, use the option --debug tempfiles. This will conserve the files sent to the backends in the .tlacache directory.

[isheff]

We encountered the (I suspect same) problem, with the example:

ASSUME NEW A,
       NEW TEMPORAL P(_)
PROVE ([] (\A r \in A : P(r))) 
      =>
      ([] (\A s \in A : P(s))) 

It can be done with some work-arounds, but the provers can't see the alpha-equivalence due to the issue with the names of bound variables in temporal formulas.