Here is the proof: https://pastebin.com/UtHpQFbN
There are two definitions of a regular bracket string:
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 strings
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.
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.
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/
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
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.
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
.
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).
(also I do use SSR + stdpp, so we probably don't really disagree)
Last updated: Oct 04 2023 at 20:01 UTC