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,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