[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [SOCIAL NETWORK] Re: [tlaplus] Resources for learning TLA+ proofs

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:

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:
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@xxxxxxxxxxxxxxxx.
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@xxxxxxxxxxxxxxxx.
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@xxxxxxxxxxxxxxxx.
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


UKSH logo


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