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

[Erick Lavoie]

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

[Erick Lavoie]

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

[Erick Lavoie]

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

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/7ae642da-65f3-4faa-8427-72e1e7873a6dn%40googlegroups.com.

[Calvin Loncaric]

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

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAF6T5Kr73-aQuGSue7geMdigvtfT6dc3Rbps57t9N%2Boby7%2By1w%40mail.gmail.com.

[Stephan Merz]

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

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABf5HMj7K-FzG_EtQoxxQ-F2iRSOK%2BCEVEF7UR9M4PY79xoVBw%40mail.gmail.com.

[Stephan Merz]

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

[Erick Lavoie]

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

--

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+u...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/e7535dbc-0eeb-49a4-ba50-aac7a35bc9dfn%40googlegroups.com.

[Erick Lavoie]

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 

 

[Stephan Merz]

If I understand correctly what you mean, Leibniz substitution can be expressed as

LEMMA

  ASSUME NEW F(_), NEW x, NEW y, x = y

  PROVE  F(x) = F(y)

which is proved by OBVIOUS.

For the rest, it looks to me that you are thinking about what is called a deep embedding of (propositional) logic in TLA+. This first requires defining a (set corresponding to the) inductive data type of formulas. There is no good support (yet) for such definitions in the TLAPS libraries, so you would probably have to inductively define a set of formulas of "size n", and then take their union, as in

makeForm(op, args) == [op |-> op, args |-> args]

True == makeForm("T", << >>)

Neg(f) == makeForm("neg", <<f>>)

Equiv(f,g) == makeForm("equiv", <<f,g>>)

Form[n \in Nat] ==

  IF n = 0 THEN {True}

  ELSE Form[n-1]

            \union { Neg(arg) : arg \in Form[n-1] }

            \union { Equiv(args[1], args[2]) : args \in Form[n-1] \X Form[n-1] }

Formula == UNION { Form[n] : n \in Nat }

You would then prove that formulas are closed under the application of operators:

LEMMA TrueFormula == True \in Formula

LEMMA NegFormula == 

  ASSUME NEW f \in Formula

  PROVE  Neg(f) \in Formula

LEMMA EquivFormula ==

  ASSUME NEW f \in Formula, NEW g \in Formula

  PROVE  Equiv(f,g) \in Formula

(Proving this will first require showing that Form is well-defined and also that Form[i] \subseteq Form[j] whenever i ≤ j._

You can then define the semantics of formulas

Interp[n \in Nat, f] ==

  IF n = 0 THEN f = True   \* assign TRUE to True, FALSE to everything else

  ELSE IF \in Form[n-1] THEN Interp[n-1, f]

  ELSE IF \E arg \in Form[n-1] : f = Neg(arg) THEN ~ Interp[n-1, arg]

  ELSE IF \E args \in Form[n-1] \X Form[n-1] : f = Equiv(args[1], args[2]) THEN Interp[n-1, args[1]] <=> Interp[n-1, args[2]]

  ELSE FALSE \* arbitrary

Interpretation(f) == 

  LET n == CHOOSE n \in Nat : f \in Form[n]

  IN  Interp[n, f]

and show that this is again well-behaved:

LEMMA

  ASSUME NEW f \in Formula 

  PROVE  Interpretation(f) \in BOOLEAN

LEMMA InterpTrue == Interpretation(True)

LEMMA InterpNeg ==

  ASSUME NEW f \in Formula

  PROVE  Interpretation(Neg(f)) = (~ Interpretation(f))

LEMMA InterpEquiv ==

  ASSUME NEW f \in Formula, NEW g \in Formula

  PROVE  Interpretation(Equiv(f,g)) = (Interpretation(f) <=> Interpretation(g))

After all this preparatory work, you will be able to prove the axioms, stated over interpretations of formulas: indeed there is no reason to expect, say,

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

to hold, since elements of set Form are not Booleans.

However, this will be a lot of effort, and it is not clear to me if this effort is really well worth it?

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAF6T5KoX_vLw_prW3LEzfE6tN0339FoxVE54KfOy0ByEbN0NiQ%40mail.gmail.com.

[Stephan Merz]

Specifying Systems shows the definitions of the standard modules, including natural numbers. In particular, a set is chosen that satisfies the Peano axioms. Since the book adopts a semantic approach, it does not provide a logical justification for the existence of such a set – after all, we know that the standard set of natural numbers satisfies the Peano axioms.

A proof of existence, analogous to the one written in Isabelle, could very well be given in TLA+, but it requires some preliminary work, including the definition of fixed-point operators and corresponding lemmas in order to justify the underlying inductive definition. Additional TLA+ theorems about natural numbers are given in [1], and if you look at the proofs, you’ll see that the standard induction rule for Nat is justified using the corresponding rule proved in Isabelle.

Stephan

[1] https://github.com/tlaplus/tlapm/blob/main/library/NaturalsInduction.tla, with proofs appearing in https://github.com/tlaplus/tlapm/blob/main/library/NaturalsInduction_proofs.tla

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAF6T5KrfvpboULwBuoZTEy6jNygV8GBiLXmOG40Ayywc68qgAw%40mail.gmail.com.

[Erick Lavoie]

Thanks again @Stephen for your comprehensive answer. This is much more detailed than I had expected. Thank you for your guidance regarding defining a closed (infinite) set of formulas, I will try it later.

I come from a (dynamically-typed) programming language implementation background and the closest analogy to what I am trying to do is a "meta-circular implementation" of propositional logic on top of TLA+. In other words, I am trying to make explicit some of the logic while avoid a complete reimplementation by reusing existing operators. This way I can force the provers to require explicit fact and definition declarations so that the required proofs of basic theorems of propositional logic closely follow what I wrote by hand. In particular, a proof step will fail if I make simple mistakes, such as using the wrong facts or failing to explicit the targets of substitution. But I would like to still obtain a mostly declarative format for the proof, as usual for TLAPS and the proof style advocated by Lamport, and not have to completely redefine and prove a propositional logic.

I think this is possible because the textbook I am using ("A logical approach to discrete mathematics" by Gries and Schneider (1993)), uses a syntactic approach to proving theorems based on sequences of equivalences and substitutions, until the formula is equivalent to one of the axioms. They do this so that you need very little conceptual background to start proving theorem and the proof steps mostly follow the intuition students already have from algebra. So I think I can get away with not having to define and prove a semantics (i.e. interpretation) for the formulas, at the cost of a little more work when defining the axioms and assumptions to supply how equivalence maps to them.

Concretely, here is the current version I have. I re-use:
1. the TLA+ '\equiv'
2. the TLA+ '=' to define variables that corresponds to sub-formulas
3. explicitly mention that substitution is possible between the left-hand side and right-hand side of '\equiv' by asserting that both sides are equal  when equivalent, otherwise the provers don't use the equivalence relationship for substitution.

  EquivImpliesEq == \A f1,f2 \in F : f1 \equiv f2 => f1 = f2

where F is the set of formulas.

Everything else is redefined with different syntactic operators and a representation based on sequences, so the provers cannot use their knowledge of propositional logic to implicitly perform the proof steps. Any feedback is welcome to help simplify things or maybe correct

some misunderstanding I may have!

------------------------ MODULE PropositionalLogic2 ------------------------
EXTENDS Sequences

(* Syntactic redefinition of basic operators of propositional       *)
(* logic to hide them from the provers. Proofs then require         *)
(* explicit facts, otherwise facts we supply that are inconsistent  *)
(* with the proof step do not matter since the provers already know *)
(* all of propositional logic.                                      *)

True   == <<"T">>
False  == <<"F">>
Neg(f) == <<"neg", f>>

Equiv(s) == <<"equiv">> \circ s
a \doteq b == Equiv(<<a,b>>)
a ## b  == Neg(a \doteq b)

(* We define the set of valid formulas by an unconstrained set       *)
(* on which we later assert some properties. This side-steps a few   *)
(* bugs we ran into while using recursive operators or functions.    *)
(* This set is however not closed so cannot be relied on to determine*)
(* when a syntactic formula is incorrect. I will try the approach    *)
(* suggested by Stephen next.                                        *)
CONSTANT F

Formula(f) ==
  \/ Len(f) = 1 /\ Head(f) = Head(True)
  \/ Len(f) = 1 /\ Head(f) = Head(False)
  \/ /\ Head(f) = "neg"
     /\ Len(f) = 2
     /\ \E f2 \in F :
       /\ f=Neg(f2)
  \/ /\ Head(f) = "equiv"
     /\ Len(f) = 3
     /\ \E f1,f2 \in F :
       /\ f=(f1 \doteq f2)

(* The FOK assumptions seemed useful in previous tests     *)
(* but are not necessary for the first two theorems below. *)
FOK ==
/\ \A f : Formula(f) \equiv f \in F
/\ { True, False } \subseteq F
/\ \A f \in F : Neg(f) \in F
/\ \A f1,f2 \in F : (f1 \doteq f2) \in F
/\ \A f1,f2 \in F : (f1 ## f2) \in F

(* Tells the prover to allow substitutions
   between f1 and f2 when they are asserted to be equivalent. *)
EquivImpliesEq == \A f1,f2 \in F : f1 \equiv f2 => f1 = f2

(* These global assumptions are only for the reader: *)
(* they are ignored by the proof manager so we need  *)
(* to repeat them for every theorem when necessary.  *)
ASSUME FOK
ASSUME EquivImpliesEq

(* Axioms are given, first with their strictly syntactic version,  *)
(* then with a subset of corresponding equivalences that we used   *)
(* in proofs.*)
AXIOM EqAssoc == \A p,q,r \in F :
  /\ ((p \doteq q) \doteq r) \doteq (p \doteq (q \doteq r))
  /\ ((p \doteq q) \doteq r) \equiv (p \doteq (q \doteq r))
AXIOM EqSym   == \A p,q   \in F :
  /\ (p \doteq q) \doteq (q \doteq p)
  /\ (p \doteq q) \equiv (q \doteq p)
AXIOM EqIden  == \A p     \in F :
  /\ True \doteq (p \doteq p)
  /\ True \equiv (p \doteq p)
  /\ (True \doteq p) \equiv p

(* Following Gries and Schneider (1993), proofs are   *)
(* written with sequences of equivalences until the   *)
(* theorem reduces to one of the (purely syntactic)   *)
(* axioms.                                            *)
(* Equalities mentioned in proof steps are redundant, *)
(* since they are already part of the assumptions,    *)
(* but they make the substitution explicit for the    *)
(* reader.                                            *)
THEOREM Thm3_4 ==
ASSUME EquivImpliesEq,
       NEW p \in F,
       NEW q \in F, q = True,
       NEW r \in F, r = (p \doteq p)
PROVE True
<1>1 True \equiv (q \doteq q)
  BY EqIden  
<1>2 (q \doteq q) \equiv (q \doteq r)
  BY EqIden, q = True, r = (p \doteq p)  
<1>3 (True \doteq (p \doteq p))
  BY EqIden (* Syntactic Axiom, done *)

<1>z QED
  BY <1>1,<1>2,<1>3
 

THEOREM EqRefl ==
ASSUME EquivImpliesEq,
       NEW p \in F,
       NEW r \in F, r = True,
       NEW s \in F, s = (p \doteq p),
       NEW t \in F, t = p,
       NEW u \in F, u = (p \doteq True),
       \A f1,f2 \in F : f1 \equiv f2 => f1 = f2
PROVE p \doteq p
<1>1 (p \doteq p) \equiv (p \doteq (p \doteq True))
  BY EqIden, t = p, u = (p \doteq True)
<1>2 (p \doteq (p \doteq True)) \equiv ((p \doteq p) \doteq True)
  BY EqAssoc, r = True
<1>3 (True \doteq (p \doteq p)) \equiv ((p \doteq p) \doteq True)
  BY EqSym, r = True, s = (p \doteq p)
<1>4 (True \doteq (p \doteq p))
  BY EqIden (* Syntactic Axiom, done *)
<1>5 QED
  BY <1>1, <1>2, <1>3, <1>4
 
=============================================================================

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0577B216-F066-4DEB-84B4-D2EDFC3AB903%40gmail.com.