Re: [tlaplus] Re: Obtaining Actual Proof Found when using TLAPS? Why is associativity not built-in?

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:

https://github.com/tlaplus/tlapm/tree/main/isabelle

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

On Mon, Mar 31, 2025 at 1:32 PM Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:

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

On Mon, Mar 31, 2025 at 7:24 PM Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:
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.