## Stream: Coq users

### Topic: ✔ Balanced bracket strings

#### 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.
``````

#### Notification Bot (Sep 20 2022 at 04:31):

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

#### 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?

``````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.

#### 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?

``````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