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

Re: [tlaplus] Proving properties of recursive function

Dear Stephan,

again many thanks. I will try to go on with what you provided me.
This is actually really difficult with bags ... there are so many things to consider.

Kind regards

Stephan Merz schrieb am Montag, 5. Dezember 2022 um 21:16:10 UTC+1:
Hi Andreas,

recursive definitions are really hard!

What you try to achieve is too much for me to do in a single go, so I tried something simpler and proved the analogous properties for the function that adds up all elements of a finite set of integers. The result is attached. You'll observe that I strictly followed the sequence of definitions and lemmas from module WellFoundedInduction.

I believe that in order to obtain what you want to achieve one can first do a similar development for bags of integers by iterating over the domain of the bag (which is a set of integers) and add the domain element times its multiplicity. Then extend to bags of pairs of integers by first summing the pair.

Of course I agree that it would be good to have generic lemmas over fold operators, and I will do that when I find some time.

Hope this helps,


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/6e92405e-75c3-406d-86a5-1a42793cf459n%40googlegroups.com.