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

On Tuesday, July 27, 2021 at 6:21:45 PM UTC+2 k.petr...@xxxxxxxxx wrote:

Tried to check this proof as well. But I'm getting the following error
when using tlapm from the updated_enabled_cdot branch.
As I understand, this branch is going to be the basis for the next
release, thus I hope this report will be useful.

(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/home/karolis/CODE/pub/tlapm/tmp/lib/tlaps/TLAPS.tla", line 1,
character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
tlapm ending abnormally with Invalid_argument("List.combine")
Raised at file "stdlib.ml", line 30, characters 20-45
Called from file "list.ml", line 263, characters 36-49
Called from file "e_levels.ml", line 228, characters 28-55
Called from file "e_levels.ml", line 234, characters 27-55
Called from file "e_levels.ml", line 413, characters 21-30
Called from file "e_levels.ml", line 934, characters 21-30
Called from file "e_levels.ml", line 992, characters 26-35
Called from file "e_visit.ml", line 222, characters 23-31
Called from file "e_visit.ml", line 223, characters 24-33
...
Called from file "e_visit.ml", line 223, characters 24-33
Called from file "e_visit.ml", line 146, characters 22-31
Called from file "e_levels.ml", line 560, characters 27-39
Called from file "prep.ml", line 1373, characters 12-42
Called from file "prep.ml", line 1458, characters 51-70
Called from file "camlinternalLazy.ml", line 29, characters 17-27
Re-raised at file "camlinternalLazy.ml", line 36, characters 4-11
Called from file "schedule.ml", line 83, characters 17-24
Called from file "schedule.ml", line 141, characters 37-62
Called from file "schedule.ml", line 181, characters 4-14
Called from file "tlapm.ml", line 208, characters 4-42
Called from file "tlapm.ml", line 408, characters 12-77
Called from file "tlapm.ml", line 503, characters 23-43
Called from file "list.ml", line 121, characters 24-34
Called from file "tlapm.ml", line 506, characters 13-40
Called from file "tlapm.ml", line 518, characters 8-33

On Tue, Jul 27, 2021 at 12:21 PM cf Shi. <shichun...@xxxxxxxxx> wrote:
>
> Hi Stephan,
> Thanks for your reply and help! I think that maybe I can learn how to use the tlaps by other simple one firstly. It's very kind of you! Hope I will finish the proof soon.
>
> Regards,
> Shi
>
> 在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.
>>
>>
> --
> 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/84f326ac-a2f8-4966-a8c5-fa33a3d6c3c4n%40googlegroups.com.