Re: [tlaplus] Resources for learning TLA+ proofs

[mohan radhakrishnan <radhakrishnan.mohan@xxxxxxxxx>]

Hello,

>5. you can look into the documentation of

the Isabelle hol prover. There are some 

constructs you can copy and paste.

I've started to dabble in Coq and Pluscal. Not Isabelle. 

Are there common constructs?

Thanks

Mohan

On Wednesday, March 29, 2023, 'Andreas Recke' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

Dear Andrew,

I’ve been struggling since a while to get into

TLA+ proofs. There is some stuff out there

about temporal proofs, and these PTL rules.

Then there is the theorem library in the 

TLA+ folders which is quite helpful.

Concerning the syntax: this is relatively 

simple. Like with TLA+ itself. But because it is

so immensely expressive, the semantics is difficult.

I found these principles as a good 

orientation:

1. you often have to show that an A is \in B.

The rest is easy for the prover backends.

I found this most important when doing

arithmetic proofs: you have to show for

each component of your formula that

it is in Nat or Int or Real.

2. you can split your proof into pieces and

leave the proof as „omitted“ to see what 

components you need.

3. if you use BY-proofs, then you need to

„collect“ assumptions and preconditions.

You find these in the theorem library.

4. Proofs with recursive functions are extremely

hard.

5. you can look into the documentation of

the Isabelle hol prover. There are some 

constructs you can copy and paste.

6. The HAVE and TAKE proofs are mainly 

reformulations for the SUFFICES construct. 

7. In any case, you have to be aware what facts

are visible at a certain proof step. The TLA+ toolbox 

shows the expanded proof when proving, so

you can check what facts are taken.

8. Do not overload the prover with complex

constructs… better simplify and prove layer

by layer. The HIDE statement does a good job here.

Kind regards 

Andreas

Am 29.03.2023 um 08:22 schrieb Andrew Helwer <andrew.helwer@xxxxxxxxx>:

 Achtung, externe Mail!

Hah! Thanks Calvin. Actually I've been looking at my own tree-sitter grammar I wrote to figure out the proof syntax: https://github.com/tlaplus-community/tree-sitter-tlaplus/blob/main/grammar.js

Ironic, I can parse the proof language but I cannot write one myself (yet!)

Like most proof languages, the TLA+ proof language is sort of a mirror version of the TLA+ language itself. Each TLA+ language construct has its corresponding proof language element that is used to "destructure" that construct in proofs. For example here's a (probably not yet correct) mental model I'm building about how to handle every TLA+ language construct when it's in either the P or Q spot of a P => Q we are trying to prove:

TLA+ Language Construct	Antecedent or Consequent (P => Q)?	Destructuring Element
e1 /\ e2	Antecedent (P)	Prove e1 => Q \/ e2 => Q
e1 /\ e2	Consequent (Q)	Prove P => e1 /\ P => e2
e1 \/ e2	Antecedent (P)	Prove e1 => Q /\ e2 => Q
e1 \/ e2	Consequent (Q)	Prove P => e1 \/ P => e2
IF e1 THEN e2 ELSE e3	Antecedent (P)	???
IF e1 THEN e2 ELSE e3	Consequent (Q)	Prove CASE e1 => e2 /\ CASE ~e1 => e3
\E e \in S : f(e)	Antecedent (P)	Prove (PICK e \in S : f(e)) => Q
\E e \in S : f(e)	Consequent (Q)	Prove (WITNESS e \in S) => f(e)
\A e \in S : f(e)	Antecedent (P)	Prove (PICK e \in S : f(e)) => Q
\A e \in S : f(e)	Consequent (Q)	Prove (TAKE e \in S) => f(e)

Andrew

On Tue, Mar 28, 2023 at 10:49 AM Calvin Loncaric <c.a.loncaric@xxxxxxxxx> wrote:

When I was first learning TLAPS back in 2019 I had a lot of trouble understanding the syntax. There are lots of awe-inspiring examples, but no clear reference for the actual structure of a proof. In particular, I couldn't seem to figure out how to begin a new proof for something I cared about without copying the structure of a similar proof from somewhere else. And when I did manage to find a similar proof, I was never sure what kinds of changes to the proof steps were syntactically valid.

I wrote myself the kind of reference I wish I'd had:

https://github.com/Calvin-L/util/blob/master/wisdom/Proofs.tla

Looking at it now I think it's a bit sparse, and I wouldn't recommend it as the first thing to look at when learning. Still, I hope it helps fill in gaps for you and others.

--

Calvin

On Fri, Mar 24, 2023 at 10:26 PM JosEdu Solsona <josedusolsona@xxxxxxxxx> wrote:

Some other resources i found useful are:

• Proving Safety Properties (lamport.azurewebsites.net)
  
• Auxiliary Variables in TLA+ (lamport.azurewebsites.net)
  
• tlaps: The [+] Proof System (mpg.de)
  

Specifying Systems is not really about proofs. (In fact, in the introduction we have: "However, this book is about specification; it says almost nothing about proofs." )  

On Saturday, March 25, 2023 at 1:38:14 AM UTC-3 Daniel Craig wrote:

There is also Specifying Systems by Dr Lamport

On Mar 24, 2023, at 5:56 PM, Andrew Helwer <andrew...@xxxxxxxxx> wrote:



What resources exist? I know of:

• The TLA+ hyperbook (unfinished?)
  
• Documentation on the TLAPS INRIA website
• Specs with proofs in the tlaplus/examples repo

Any others? Those of you who have written TLA+ proofs, how did you learn?

Andrew

--
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/beeb5b25-d80a-4847-a38e-687dfc604263n%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@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3d12ece6-2868-43c4-8456-8aeb8f6535f1n%40googlegroups.com.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/utkJxZ0mkxw/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABf5HMiSF-sW%3DTD6Hn3y3-sqOqmLz2Ae63wt9bxer5GS62eODQ%40mail.gmail.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@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWfRNUq42A0L%3DCrSRKE2cbfFEU_cHff9GNo97nwChvJdw%40mail.gmail.com.

UKSH hilft Ukraine: Wir machen weiter. Helfen Sie uns, zu helfen!
Unterstützung für die Menschen in und aus der Ukraine.

UKSH-Gutes tun!-Spendenkonto zur Aktion
Empfänger: UKSH WsG e.V.
IBAN: DE75 2105 0170 1400 1352 22 | BIC: NOLADE21KIE
Angabe bei Ihrer Überweisung im Verwendungszweck:
FW14042: UKSH hilft Ukraine

Spenden via PayPal: Spenden per PayPal
Alle Infos: www.uksh.de/ukrainehilfe

Universitätsklinikum Schleswig-Holstein

Rechtsfähige Anstalt des öffentlichen Rechts der Christian-Albrechts-Universität zu Kiel und der Universität zu Lübeck

 

Vorstandsmitglieder: Prof. Dr. Dr. h.c. mult. Jens Scholz (Vorsitzender/CEO), Peter Pansegrau (CFO), Corinna Jendges (COO), Prof. Dr. Thomas Münte, Prof. Dr. Joachim Thiery

Vorsitzender des Aufsichtsrates: Guido Wendt

Bankverbindungen:
Förde Sparkasse IBAN: DE14 2105 0170 0000 1002 06 SWIFT/BIC: NOLA DE 21 KIE
Commerzbank AG IBAN: DE17 2308 0040 0300 0412 00 SWIFT/BIC: DRES DE FF 230

Gemeinsam Gutes tun! Spenden: Alle UKSH-Spendenmöglichkeiten unter www.uksh.de/gutestun
Spendenkonto: Förde Sparkasse IBAN: DE75 2105 0170 1400 1352 22 | BIC: NOLADE21KIE | Empfänger: UKSH WsG e.V.

Diese E-Mail enthält vertrauliche Informationen und ist nur für die Personen bestimmt, an welche sie gerichtet ist.
Sollten Sie nicht der bestimmungsgemäße Empfänger sein, bitten wir Sie, uns hiervon unverzüglich zu unterrichten und die E-Mail zu vernichten.

Wir weisen darauf hin, dass der Gebrauch und die Weiterleitung einer nicht bestimmungsgemäß empfangenen E-Mail und ihres Inhalts gesetzlich verboten sind und ggf. Schadensersatzansprüche auslösen können.

--
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@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4DACC6DB-C397-4D05-AE94-069E8B394B5F%40uksh.de.

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/CAOoXFP8_zrVepGoZgYG16%2ByRC5CAP9mNEmEw7e-ag%3DiPBDk1zQ%40mail.gmail.com.