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
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))
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
Huỳnh Trần Khanh has marked this topic as resolved.
Last updated: Oct 04 2023 at 21:01 UTC