Stream: Coq users

Topic: Review regular bracket string proof


view this post on Zulip bubble sort now (deactivated) (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.

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 17 2023 at 12:07):

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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Jan 17 2023 at 14:32):

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


Last updated: Mar 29 2024 at 05:40 UTC