| TLAPS was designed so that it allows the working proof engineer to decompose reasoning about specifications to proof obligations that are within the reach of automated theorem provers. It is not built upon a fixed proof calculus for logic, and if your objective is to learn principles of formal mathematical proof, you had probably better look at proof assistants such as Coq, Lean or Isabelle (although the latter may already contain too much automation for your taste).
Instead, TLAPS translates TLA+ formulas to the input languages of backend provers that are expected to be able to solve problems in logic, elementary set theory, and basic integer arithmetic. As Calvin explains, problems such as
\A p,q,r \in BOOLEAN : ((p = q) = r) = (p = (q = r)) or \A p,q,r \in BOOLEAN : ((p # q) = r) = (p = (q # r))
can thus be proved by "OBVIOUS". Also, these formulas are unprovable for non-Booleans: we would not expect (1 = 1) = 2, i.e. TRUE = 2, to imply that 1 = (1 = 2), i.e. 1 = FALSE. In fact, the semantics of TLA+ does not tell us if TRUE = 2 holds or does not hold.
However, the absence of an explicit proof calculus may indeed make the experience of using TLAPS somewhat frustrating because it is not obvious what the automatic backends can prove. For example, somewhat to my surprise, the theorem asserting that any value x is equal to the set of its elements (remember that in set theory, any value is a set)
LEMMA \A x : x = {y \in x : TRUE}
is proved by OBVIOUS, although it may not be obvious to someone who is not familiar with set theory. On the other hand,
LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n \div 2 = 0
fails, although it is true and looks obvious to a human – essentially because SMT solvers use incomplete heuristics for problems involving integer division.
Also, the untyped nature of TLA+ may cause seemingly "obvious" formulas to fail. The above examples show this (when omitting the BOOLEAN bound), as does
LEMMA \A n : n - n = 0
which is unprovable because we do not know how subtraction behaves outside of numeric domains. In actual algorithm verification, one must always rely on a type-correctness invariant. And yes, adding axioms is frowned upon in the community of users of proof assistants because they are prone to introducing inconsistencies.
–––
As to your question about extracting proofs from TLAPS, I also agree with Calvin. The Isabelle encoding does provide a bunch of axioms that underly TLA+ set theory, and in principle you could inspect a proof found by the Isabelle backend. Moreover, Zenon (one of the automatic backends built into TLAPS) can produce Isabelle proofs. We are also currently working on a reconstruction of SMT proofs (the main workhorse of TLAPS) that can be checked with Lambdapi, a foundational proof checker. However, the proofs that can be obtained in this way are essentially unreadable for humans, although they add confidence in the correctness of the verdict found by the automatic provers.
Best regards, Stephan On 31 Mar 2025, at 23:37, Calvin Loncaric <marvinx03@xxxxxxxxx> wrote:
One quick note:
Your formulation of NegDistrOverEq is not actually provable in TLA+, since Exp is unconstrained. Remember that (\neg p) is a "silly" _expression_ when (p \notin BOOLEAN). In other words, (\neg 1) could be TRUE or FALSE or "hello". Given only the axioms of TLA+, there is no way to prove which one it is.
TLAPS instantly proves this modified version, where p and q are constrained to be booleans:
THEOREM NegDistrOverEq2 == \A p,q \in BOOLEAN : (\neg (p = q)) = ((\neg p) = q) OBVIOUS
So, be extremely careful using AXIOM! As this example demonstrates, if TLAPS cannot prove a theorem you think is obvious, then it might be because you have misunderstood the TLA+ semantics of the theorem.
Also:
> Is there a way to print the actual proof a theorem prover found?
No, as far as I know.
...And I think the "actual proof" from the backend might be less useful than you're imagining, unfortunately. If you poke around the Isabelle formalization of TLA+ here:
then you'll see that it contains not just the axioms and definitions of TLA+ (like the definition of EXCEPT), but also many useful derived facts (like these ones about EXCEPT). Therefore, the "actual proof" from the backend is likely to use many lemmas that are opaque and inscrutable to us end-users.
-- Calvin
Dear all,
As a second reply to my 2nd question, it seems provers have associativity for '\equiv' built-in but not for '='.
Moreover, almost all propositional calculus theorems from Chap. 3 of Gries and Schneider (1994) are verified "obviously". However, sometimes what Gries and Schneider (1994) use as axioms times out on the provers but later succeed after other theorems are verified first ("obviously"), so I assume the provers use a different set of axioms than Gries and Schneider (1994).
Now, I am still wondering about how to visualize the proof found by the theorem prover(s).
Sorry for the monologue...
Best regards,
Erick
Dear all,
As a quick way to find which axioms and theorems are already known by the provers, I found that I can simply change 'AXIOM' for 'THEOREM' and test whether the latter can be "obviously" proven. So for example:
CONSTANT Exp THEOREM NeqDef == \A p,q \in Exp : (p # q) = (\neg (p = q)) (* Succeeds => Already built-in axiom/theorem *) OBVIOUS
THEOREM NegDistrOverEq == \A p,q \in Exp : (\neg (p = q)) = ((\neg p) = q) (* Fails => Can be supplied as AXIOM instead *) OBVIOUS Best regards,
Erick On Monday, March 31, 2025 at 6:53:14 PM UTC+2 Erick Lavoie wrote:
Dear TLA+ community,
I am currently learning how to use TLAPS. To get a better intuition about the capabilities and limitations of theorem provers, I am working my way through "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1994) and proving all theorems one by one, first by hand, then with TLAPS. The issue I am running into is that the theorem provers seem to have a fair amount of built-in knowledge but otherwise fail on seemingly simple examples, so it is hard to anticipate what needs or needs not be supplied.
Is there a way to print the actual proof a theorem prover found?
For example, given the following module:
-------------------------------- MODULE Test -------------------------------- CONSTANT Exp
AXIOM EqAssoc == \A p,q,r \in Exp : ((p = q) = r) = (p = (q = r)) THEOREM NeqEqInterch == \A p,q,r \in Exp : ((p # q) = r) = (p = (q # r)) BY EqAssoc
============================================= The Proof Manager successfully shows NeqEqInterch to be proved, even though I never supplied the properties for not equal (i.e. 'p # q'), negation (i.e. '\neg p') on Exp, nor gave any explicit membership information about Exp. However, when not supplying EqAssoc, the Proof Manager reports a timeout on all theorem provers. So somehow it seems that only associativity of equality is missing. But why is everything else already supplied but not associativity? Best, Erick
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/7ae642da-65f3-4faa-8427-72e1e7873a6dn%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAF6T5Kr73-aQuGSue7geMdigvtfT6dc3Rbps57t9N%2Boby7%2By1w%40mail.gmail.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABf5HMj7K-FzG_EtQoxxQ-F2iRSOK%2BCEVEF7UR9M4PY79xoVBw%40mail.gmail.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/B82A9FE6-BBC7-4DE7-AECF-91745AC774B1%40gmail.com.
|