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 Nones

Paolo Giarrusso (Feb 03 2023 at 11:54):

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

Paolo Giarrusso (Feb 03 2023 at 12:20):

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: Oct 04 2023 at 21:01 UTC