Re: [tlaplus] How to prove RealInv' in the example "BubbleSort" ?

在2021年7月26日星期一 UTC+8 下午4:14:01<Stephan Merz> 写道：

Hello,

that example is not an easy one for learning how to use the TLAPS proof assistant. I haven't tried to finish the proof, but I'll give you some hints on how to proceed.

The level-2 proof starts with

  <2> SUFFICES ASSUME Inv, Lbl_1 \/ Lbl_2 \* Next
   PROVE Inv'

This indicates that the case distinction should be as follows:

  <3>1. CASE Lbl_1
<3>2. CASE Lbl_2

Note that the actions such as Lbl_1 give you stronger hypotheses than just assuming, say, pc = "Lbl_1", which is but one conjunct of the definition of Lbl_1.

Indeed, we can then finish the proof by

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

Of course, the real work is in proving steps <3>1 and <3>2. I would not expect these proofs to work by brute force (BY expanding definitions and invoking utility lemmas), but probably you want to decompose them along the definitions of the actions. For Lbl_1, this suggests writing

  <4>1. CASE i < N
<4>2. CASE ~(i < N)
<4>. QED BY <4>1, <4>2

For step <4>1, we can now gather information on the effect of the action:

  <5>1. /\ pc = "Lbl_1"
/\ j' = i+1
/\ pc' = "Lbl_2"
/\ UNCHANGED << A, A0, i >>
BY <3>1, <4>1 DEF Lbl_1

In particular, this tells us that we only need to worry about the conjunct of RealInv' that talks about what is expected when pc = Lbl_2. And now think about why the predicate holds true and guide the prover towards proving it. (As you observed, just adding all available facts and expanding all relevant definitions rarely works when proofs become a bit more complicated.) Steps <4>2 and <3>2 will be handled similarly. When the proof is done, you may be able to shorten it by compressing some proof steps into larger leaf proofs, but this is just cosmetics: I usually find that decomposing the proof helps me discover what is actually needed.

Note in particular that I used the case assumptions <3>1 and <4>1 in the proof of step <5>1: as a user you may find this unnecessary but TLAPS requires all necessary facts to be invoked explicitly.

Hope this helps (and if you finish the proof we'd love to add it to the collection of examples),

Stephan

On 26 Jul 2021, at 04:29, cf Shi. <shichun...@xxxxxxxxx> wrote:

Hello,
I'm new in tlaps and trying to finish the example BubbleSort.tla[1]. But the attempt was invalid.
I have no idea on it, and whether I handled it in a disorderly way? How to prove RealInv' in the example "BubbleSort" ?

My approach to this is as follows: (of course, this is predictably not working)

<2>2. RealInv'
    <3>1. CASE pc = "Lbl_1"
       BY DEF TypeOK, RealInv, Lbl_1,
              Lbl_2, IsSortedTo,IsSorted,IsSortedFromTo, IsPermOf, Perms, **
    <3>2. CASE pc = "Lbl_2"
    <3>3. CASE pc = "Done"
        BY IsPermOfExchange DEF TypeOK, RealInv, Lbl_1, Lbl_2,IsSortedTo,
                 IsSorted,IsSortedFromTo, IsPermOf, Perms, **
    <3>4. QED
        BY <3>1,<3>2,<3>3 DEF TypeOK, RealInv, Lbl_1, Lbl_2

-------------------------------------------------------------------------

[1] https://github.com/tlaplus/tlapm/blob/master/examples/BubbleSort.tla

--
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/ee395ae0-b749-4f4e-9da0-611f91564424n%40googlegroups.com.