## Stream: Coq users

### Topic: ✔ One final lemma

#### Huỳnh Trần Khanh (Feb 03 2023 at 07:56):

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.

#### Paolo Giarrusso (Feb 03 2023 at 10:30):

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

#### Huỳnh Trần Khanh (Feb 03 2023 at 11:23):

You're probably misreading the lemma statement

#### Huỳnh Trần Khanh (Feb 03 2023 at 11:26):

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

#### Paolo Giarrusso (Feb 03 2023 at 12:04):

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 `fillLeftToRight`'s output has the right form EDIT: see below

I’m trying a bit

#### Paolo Giarrusso (Feb 03 2023 at 13:45):

okay, got a proof

#### Paolo Giarrusso (Feb 03 2023 at 13:48):

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

#### Notification Bot (Feb 03 2023 at 13:57):

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

Last updated: Jun 24 2024 at 01:01 UTC