Im trying the theorem proving tool of TLA+ to prove safety properties of an algorithm. But i found that TLAPS cant figure very "simple" mathematical facts.
My first problem was with:
EXTENDS Naturals
CONSTANTS x,y
ASSUME x \in Nat /\ y \in Nat
LEMMA x=y+1 => y<x
OBVIOUS
TLAPS cant do it alone with any backend prover. I also tried using specific backend provers with other tactics:
LEMMA x=y+1 => y<x
BY IsaM("blast")
But also failed. In similar way, other kind of simple facts cant be checked, for example:
LEMMA x<y => x<y+0
I have used some of those backend theorem provers in the past, like the Z Solver or Isabelle, and from what i remember they are very powerful. I think im missing something here... or i don't understand the TLAPS proof organizer or i still need to load some other module with axioms?.
It seems you hit a bug in TLAPM -- at least in the development version on my machine. The reason is that the SMT translation does not pick up the second assumption. Without the domain restriction, none of the assertions should be provable. As a hot fix, I added the domain restrictions to the local lemma. I can now prove:
LEMMA ASSUME x \in Nat, y \in Nat
PROVE x=y+1 => y < x BY SMT
Another way to get around it for the moment is to have named assumptions which are invoked whenever needed:
ASSUME DOM == x \in Nat /\ y \in Nat
LEMMA x=y+1 => y < x BY SMT, DOM
should go through. In both cases you have to add EXTENDS TLAPS at the beginning of your spec to enable the SMT keyword.
I will also report the bug to the maintainers.
Update: it seems that global assumptions are generally disregarded by TLAPM (afaik for performance reasons). The version with named assumptions is the preferred way to go.