Stream: Coq users

Topic: A wild exchange argument just landed!


view this post on Zulip Huỳnh Trần Khanh (Jan 23 2023 at 16:26):

Hello folks! In the #Coq users > advancingIsAlwaysOk thread I already explained the problem statement. I've implemented your suggestions to simplify the problem statement in Coq. Also, I've coded the main part of the exchange argument I outlined in the thread. https://github.com/huynhtrankhanh/coqcp/blob/0921fc77bc557a0fc8c6896a9197c95144141359/theories/FillInTheBlanks.v

Now, I'm about to turn off my computer. Maybe I can figure out the solution myself tomorrow when I sit in front of the computer again, and continue to formalize the argument. But anyway, here's the deal. I proved that for an arbitrary balanced string, I can find two arbitrary symbols, the left one being the ) symbol, and the right one being the ( symbol, and when I swap the two symbols, I still obtain a balanced string. To a human being, it's obvious that when I keep swapping like this, I'll end up with the string that I provided in the possibleToFillBool function. But... how can I formalize? To Coq, it's not obvious that the process of swapping the symbols will eventually terminate. So do you have any tips? I just want to do some sort of induction, and in the inductive step I'll keep swapping the symbols and as I already proved that the string is still balanced after swapping, I will eventually prove that the string in possibleToFillBool is balanced.

What is an exchange argument? When formalizing an algorithm, you often want to prove something along the lines of if a solution exists, then my construction is a solution. An exchange argument is a way to prove that. You provide a way to transform an arbitrary solution into your construction and prove that while transforming the solution is still valid.

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:55):

it seems like the number of swaps could be a sufficient termination metric?

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 19:59):

up to typos, if nSwaps : T -> nat and 0 < nSwaps x -> nSwaps (f x) < nSwaps x then nSwaps (Nat.iter (nSwaps x) f x) = 0 (EDITed)

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 20:02):

said otherwise, you can prove ∀ m, nSwaps x = m -> ∃ m, nSwaps (Nat.iter m f x) = 0 by (well-founded?) induction on m


Last updated: Jun 18 2024 at 08:01 UTC