In #Coq users > advancingIsAlwaysOk I already explained the problem statement. The crux of the proof is for an arbitrary balanced string, I can swap a ")" on the left and a "(" on the right to obtain another balanced string. This is proved in the canAlwaysSwapCloseAndOpen lemma. But I can't find a way to transform this lemma into canAlwaysSwapCloseAndOpenInWitness. I need this exact statement because this is the form that propertyPreservedAfterSorting expects.

Wow, I spent so many days just to solve this problem! And I wrote so many files! I hope that the correct proof for the only missing lemma is not very long.

You can help me by cloning the repo. The only dependency is coq-stdpp.

Wait, why doesn't `apply canAlwaysSwapCloseAndOpen; by destruct_and!`

work?

You're probably misreading the lemma statement

I'm aware I don't write idiomatic Coq. So here's a human friendly translation: withBlanks is a string with holes. s1 ++ ... ++ s2 ++ ... ++ s3 is the list of values to be filled into the holes. Holes are represented by `None`

s

checking it out

yep my bad, the hole is

```
count_occ optionBracketEqualityDecidable withBlanks None =
length (s1 ++ [BracketClose] ++ s2 ++ [BracketOpen] ++ s3) ->
isBalanced (fillLeftToRight withBlanks (s1 ++ [BracketClose] ++ s2 ++ [BracketOpen] ++ s3)) ->
isBalanced (fillLeftToRight withBlanks (s1 ++ [BracketOpen] ++ s2 ++ [BracketClose] ++ s3))
```

but `canAlwaysSwapCloseAndOpen`

only gives

```
isBalanced (s1 ++ [BracketClose] ++ s2 ++ [BracketOpen] ++ s3) →
isBalanced (s1 ++ [BracketOpen] ++ s2 ++ [BracketClose] ++ s3)
```

~~so you have to prove that ~~ EDIT: see below`fillLeftToRight`

's output has the right form

I’m trying a bit

okay, got a proof

https://github.com/huynhtrankhanh/CoqCP/pull/1

Huỳnh Trần Khanh has marked this topic as resolved.

Last updated: Jun 24 2024 at 01:01 UTC