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.
it seems like the number of swaps could be a sufficient termination metric?
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)
said otherwise, you can prove
∀ m, nSwaps x = m -> ∃ m, nSwaps (Nat.iter m f x) = 0 by (well-founded?) induction on
Last updated: Oct 04 2023 at 19:01 UTC