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

[Erick Lavoie <erick.lavoie@xxxxxxxxx>]

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/0bd409f9-864d-4aa4-84e1-c131367f228an%40googlegroups.com.