Stream: Coq users

Topic: Review regular bracket string proof

Huỳnh Trần Khanh (Jan 17 2023 at 06:41):

Here is the proof: https://pastebin.com/UtHpQFbN
There are two definitions of a regular bracket string:

1. An empty string is a regular bracket string. If s is a regular bracket string, "(" + s + ")" is also a regular bracket string. If s1 and s2 are regular bracket strings, s1 + s2 is also a regular bracket string
2. s is a regular bracket string if number of ( characters is equal to number of ) characters and for every prefix, the number of ( characters is greater than or equal to the number of ) characters.

The proof proves that the two definitions are equivalent. I'm looking for code style feedback and other tips to make the proof shorter.

Also there's a little decision procedure (isBalancedBool). How can I assign this bool function to the isBalanced inductive predicate, so I can do something like bool_decide (isBalanced ...)? I'm using coq-stdpp.

Karl Palmskog (Jan 17 2023 at 07:32):

if you want to follow Stdpp conventions, you'd define an instance of the Decision typeclass for the isBalanced predicate. Then, you can get a boolean function and its correctness proof via bool_decide and friends.

Karl Palmskog (Jan 17 2023 at 11:28):

perhaps this wasn't obvious in my response, but in the Stdpp typeclass methodology, using booleans at all inside Coq is not the best idea, with the general argument being boolean blindness: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/

Paolo Giarrusso (Jan 17 2023 at 12:00):

should you be arguing for (if) decide against (if) bool_decide — that works has uses but https://gitlab.mpi-sws.org/iris/stdpp/-/issues/168 shows ways in which bool_decide can be easier to reason about

Paolo Giarrusso (Jan 17 2023 at 12:07):

• stylistically: I think in Coq it's common to avoid + 1 on nat, and use 1 + or S instead. Then countOpenConsOpen and countCloseConsClose would be easier to prove instead of requiring lia. That differs from what we do on paper, but saves work. (Mathcomp even has notations to make this look nicer).

• simpl would do those simplifications if you add:

Global Arguments countOpen !_ /.
Global Arguments countClose !_ /.

that instructs simpl and cbn to unfold those functions when their (lone) argument starts with a constructor; that happens automatically for count_occ since it's a fixpoint.

Karl Palmskog (Jan 17 2023 at 14:13):

The argument in https://gitlab.mpi-sws.org/iris/stdpp/-/issues/168 against decide is essentially all about Coq implementation quirks...

Unless you want to use SSR+Stdpp, I'd still go with decide.

Paolo Giarrusso (Jan 17 2023 at 14:29):

YMMV, but it's not just implementation quirks: (P ↔ Q) → decide P = decide Q is ill-typed, but the analogue for bool_decide is much nicer (and ditto for other lemmas):

Lemma bool_decide_ext (P Q : Prop) `{Decision P, Decision Q} :
  (P ↔ Q) → bool_decide P = bool_decide Q.
Lemma decide_ext {A} P Q `{Decision P, Decision Q} (x y : A) :
  (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).

Paolo Giarrusso (Jan 17 2023 at 14:32):

(also I do use SSR + stdpp, so we probably don't really disagree)

Last updated: Oct 04 2023 at 20:01 UTC