## Stream: Coq users

### Topic: A wild exchange argument just landed!

#### 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: Jun 18 2024 at 08:01 UTC