How do I prove the string is not balanced?

```
Require Import List.
Import ListNotations.
Inductive bracket_t :=
| left
| right.
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).
Definition very_balanced :
balanced [
left; left; right; left; left; right; right; right
] :=
wrap _ (join _ _
(wrap _ empty) (wrap _ (wrap _ empty))).
Lemma not_balanced_at_all :
~ balanced [left; left; right; right; right].
Admitted.
```

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?

The very_balanced lemma proves that (()(())) is balanced. The not_balanced_at_all lemma proves that (())) is not balanced.

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

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

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.

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: Jun 18 2024 at 09:02 UTC