Re: [tlaplus] TLA and TLAPIS

On Friday, April 26, 2024 at 4:55:24 AM UTC+12 Stephan Merz wrote:

On 25 Apr 2024, at 18:34, marta zhango <marta...@xxxxxxxxx> wrote:

I am getting very confused. About (1) an easy outline of a proof and (2) the complete code for a proof system to check it.

The complete code for checking a proof can be enormously complicated, especially when one has to declare a significant
number of functions and constructs.

Consider "Appendix A: Formal Proof" ( https://lamport.azurewebsites.net/pubs/proof.pdf ) containing a TLA+ formalization
of Spivak’s proof. That is not the actual complete code for a proof system to check it, am I right ?

That paper was written before TLAPS was developed, and we never tried to port the example to the prover. For one thing, we do not currently have support for reasoning about real numbers (but this may change, see Gunasekera et al. [1]). As you say, the effort of a machine-checked proof depends a lot on the operations that are involved in the statement. More complex proofs will require a library of definitions and lemmas that establish basic facts of the respective domain. Of course, you can always fake that to a certain extent and just state unproved lemmas (effectively axioms) that you consider to be obvious — as Lamport does in the proof in the paper that you refer to.

Now, about comment regarding the proof in Cantor10.tla. Is that the actual complete code for a proof system to check the
correctness of the proof ? Or is it a description of the proof.

That is the entire input needed for TLAPS for checking the theorem. Of course, Cantor’s theorem is stated in elementary set theory, so most of the proof is automated. You can look at other examples within the TLAPS distribution to get an idea of what other proofs look like. And there are similar collections for Coq, Isabelle or Lean etc.

I want to write some proofs from signal processing that are more formal than the standard way of showing a proof in a
textbook, but not as complicated as the complete code required by a proof system. What would you suggest ?

As said above, you’ll have to start building up a collection of elementary facts in order to prove anything meaningful. I cannot tell you whether TLAPS is appropriate or not for what you have in mind. I suggest starting small with one or two proof assistants before deciding if it’s worth the effort. If you do not have any experience with machine-checked proofs, be warned that it can be both super-addictive and involve a steep learning curve.

Stephan

[1] https://conf.researchr.org/program/nfm-2024/program-nfm-2024/

On Friday, April 26, 2024 at 3:46:36 AM UTC+12 Stephan Merz wrote:
The proof appearing at the beginning of appendix B of the paper you point to is checked by TLAPS, cf. also [1] that has 10 different versions of the proof that are all checked by TLAPS. The proof in Cantor10.tla is even more succinct than the one appearing in the paper.

Stephan

[1] https://github.com/tlaplus/tlapm/tree/main/examples/cantor

On 25 Apr 2024, at 16:58, marta zhango <marta...@xxxxxxxxx> wrote:

For instance, consider the TLA+2 Proof of Cantor’s Theorem ( see first theorem of appendix B in
https://lamport.azurewebsites.net/pubs/keappa08-web.pdf ) as a proof in a mathematics textbook.
That would be more suitable than a TLAPS version of it. TLAPS is a translation of a TLA+2 Proof
for checking the proof. In such a description correct ?

As you say, a detailed proof written in a way that enables it to be checked by an automated system
requires substantial effortfrom the user.

For a textbook, an outline of the proof using TLA+2 could be the formal proof. Which can then be
checked out by coding the corresponding instructions for a proof checker.

On Friday, April 26, 2024 at 2:20:42 AM UTC+12 Stephan Merz wrote:
Could you elaborate on what you mean by referring to TLA as a way to outline a proof? TLA stands for Temporal Logic of Actions, so it is a logic rather than a proof system – although the TLA paper [1] includes proof rules that can be (mainly) used in paper-and-pencil proofs.

Like Coq and Lean, TLAPS is a mechanical proof assistant that allows you to write a detailed proof and have it checked by the system. These tools indeed require substantial effort from the user, but unlike model checkers such as TLC they can (in principle) verify correctness properties for arbitrary specifications, not only finite-state systems.

Stephan

[1] https://lamport.azurewebsites.net/pubs/pubs.html#lamport-actions

On 25 Apr 2024, at 14:38, marta zhango <marta...@xxxxxxxxx> wrote:

There seems to exist a big difference between TLA and TLAPIS. TLA is a way to outline a proof, whilst TLAPIS, Coq, Lean provide ways to check whether a proof is correct. With the
proof checkers being quite long and time consuming to construct.

In this correct ?

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9811f409-94b8-42d4-b56b-2ff4b2739886n%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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8bd4439d-7f5d-4e5d-b935-7c4d8b71b4ban%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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bdc5219c-0411-4355-91f6-af1ee5f218a3n%40googlegroups.com.