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

On 3 Apr 2025, at 22:18, Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:

I have found the Peano natural numbers definition in the TLA+ examples. I also found the Isabelle equivalent, including the comment mentioning that: "the existence of such [a set of naturals] is assumed, but not proven in the [Specifying Systems] book". Are there fundamental limitations of TLA+ that prevent a proof of the existence of a Peano set to be written in TLA+?

Erick

On Thu, Apr 3, 2025 at 5:38 PM Erick Lavoie <erick.lavoie@xxxxxxxxx> wrote:

Thanks both to @Calvin and @Stephen for your detailed answers. That was really useful.

I also stumbled upon "Encoding TLA+ into unsorted and many-sorted first-order logic" (https://doi.org/10.1016/j.scico.2017.09.004) from Stephen, with Section 3.1. on the liberal interpretation of Boolification of TLAPS that helped me understand why I could use propositional logic operators on variables whose possible values are elements of an unconstrained set.

My end goal is to use TLAPS for proving properties of distributed algorithms. I do understand that I should avoid using custom axioms when doing so, for it could unintentionally hide errors. However, my background knowledge on formal mathematics and logic is somewhat lacking, so I am ramping up with the same tools I intend to use later, to validate my reasoning, practice the proof format advocated by Lamport, and learn the limitations of the tools.

I am impressed that all interesting theorems of propositional calculus from Gries and Schneider (1993) could be obviously proven with TLAPS, except for Leibniz substition (which I could not find how to express). That defeats my goal of verifying my hand proofs however because the Proof Manager succeeds at them regardless of which facts I am supplying to justify intermediate steps (so I cannot catch errors in mis-selecting relevant facts). I understand this is intentional: working engineers should not have to reprove basics of propositional calculus.

So in the last days, I have been experimenting with using the axioms given by Gries and Schneider (1993) with custom syntax / operators except for equivalence, in order to force the provers to work by re-writing. TLAPS successfully verifies the followings theorems from the book this way:

CONSTANT Form

True == <<"T">>
False == <<"F">>
Neg(f) == <<"neg", f>>
a ## b == Neg(a \equiv b)

AXIOM EqAssoc == \A p,q,r \in Form : ((p \equiv q) \equiv r) \equiv (p \equiv (q \equiv r))
AXIOM EqSym == \A p,q \in Form : (p \equiv q) \equiv (q \equiv p)
AXIOM EqIden == \A p \in Form : (True \equiv (p \equiv p))

THEOREM Thm3_4 ==
ASSUME NEW p \in Form
PROVE True
<1>1 True \equiv (True \equiv True)
  BY EqIden
<1>2 (True \equiv True) \equiv (True \equiv (p \equiv p))
  BY EqIden (* By replacing 2nd True with (p \equiv p) *)
<1>3 (True \equiv (p \equiv p))
  BY EqIden (* Axiom *)
<1>z QED
  BY <1>1,<1>2,<1>3

AXIOM NegDistrOverEq == \A p,q \in Form : Neg(p \equiv q) \equiv (Neg(p) \equiv q)

THEOREM Thm3_11 ==
ASSUME NEW p \in Form,
NEW q \in Form
PROVE (Neg(p) \equiv q) \equiv (p \equiv Neg(q))
<1>1 (Neg(p) \equiv q) \equiv Neg(p \equiv q)
  BY NegDistrOverEq
<1>2 (p \equiv Neg(q)) \equiv Neg(p \equiv q)
  <2>1 (p \equiv Neg(q)) \equiv (Neg(q) \equiv p)
  BY EqSym
  <2>2 (Neg(q) \equiv p) \equiv Neg(q \equiv p)
  BY NegDistrOverEq
  <2>3 Neg(q \equiv p) \equiv Neg(p \equiv q)
  BY EqSym
  <2>4 (Neg(p) \equiv q) \equiv Neg(p \equiv q)
  BY NegDistrOverEq
  <2>5 QED
  BY <2>1, <2>2, <2>3, <2>4
<1>z QED
  BY <1>1, <1>2, EqSym

However, I did not manage to restrict the "Form" set to only contain valid formulas (rather than being an unconstrained set). The various ways I have tried to define the infinite set of valid formulas seem to run into limitations of TLAPS.

I understand this is possible since Integers and Sequences are infinite sets themselves, but as far as I can tell they are defined in Isabelle rather TLA+. So is what I am trying possible?

Thanks again for your previous help, that was really useful.

Best regards,

Erick

On Thu, Apr 3, 2025 at 3:34 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n \div 2 = 0

fails

Well, fortunately TLAPS fails to prove this ... I meant to write

LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n % 2 = 0

which is indeed proved by OBVIOUS. Still, there are many intuitively obvious facts that TLAPS fails to prove: for example, it will not prove essentially any assertion involving the Cardinality operator.

Stephan

--
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/e7535dbc-0eeb-49a4-ba50-aac7a35bc9dfn%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/CAF6T5KrfvpboULwBuoZTEy6jNygV8GBiLXmOG40Ayywc68qgAw%40mail.gmail.com.