Huỳnh Trần Khanh (Jan 23 2023 at 16:26): 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.
Paolo Giarrusso (Jan 23 2023 at 19:55):it seems like the number of swaps could be a sufficient termination metric?
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)
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: Oct 04 2023 at 19:01 UTC