Stream: Coq users

Topic: ✔ Balanced bracket strings


view this post on Zulip Malcolm Sharpe (Sep 20 2022 at 04:15):

I'd guess that generally you might want to write a function of type list bracket_t -> bool that checks whether the brackets are balanced, then prove that function correct. (This might be considered reflection? I don't know what that term means precisely.)

For this specific case, though, it's enough to prove a lemma that the number of left and right brackets must be equal.

Lemma bracket_t_eq_dec : forall x y : bracket_t, {x = y} + {x <> y}.
Proof. destruct x, y; constructor; easy. Defined.

Require Import Lia.

Lemma balanced_count : forall x,
    balanced x ->
    count_occ bracket_t_eq_dec x left = count_occ bracket_t_eq_dec x right.
Proof.
  induction 1.
  - easy.
  - rewrite 4 count_occ_app. simpl. lia.
  - rewrite 2 count_occ_app. lia.
Qed.

Lemma not_balanced_at_all :
  ~ balanced [left; left; right; right; right].
Proof.
  intro H.
  apply balanced_count in H.
  easy.
Qed.

view this post on Zulip Notification Bot (Sep 20 2022 at 04:31):

Huỳnh Trần Khanh has marked this topic as resolved.

view this post on Zulip James Wood (Sep 20 2022 at 06:57):

Huỳnh Trần Khanh said:

Also, writing a lot of _ in the very_balanced lemma can be tiring. Is there a way I can change the definition of the inductive predicate so the bracket string list bracket_t can be inferred automatically?

Adding

Arguments wrap {_}.
Arguments join {_ _}.

before the Definition is the quickest fix, and you can also use curly braces rather than round brackets around arguments in the Inductive to achieve the same effect.

view this post on Zulip John Wiegley (Sep 20 2022 at 06:59):

James Wood said:

Huỳnh Trần Khanh said:

Also, writing a lot of _ in the very_balanced lemma can be tiring. Is there a way I can change the definition of the inductive predicate so the bracket string list bracket_t can be inferred automatically?

Adding

Arguments wrap {_}.
Arguments join {_ _}.

before the Definition is the quickest fix, and you can also use curly braces rather than round brackets around arguments in the Inductive to achieve the same effect.

Another way would be to write the implicits into the definition:

Inductive balanced : list bracket_t -> Prop :=
  | empty: balanced []
  | wrap {x : list bracket_t} : balanced x ->
    balanced ([left] ++ x ++ [right])
  | join {x y : list bracket_t} : balanced x ->
    balanced y -> balanced (x ++ y).

Last updated: Jan 29 2023 at 06:02 UTC