Stream: Coq users

Topic: ✔ Balanced bracket strings

Huỳnh Trần Khanh (Sep 20 2022 at 03:32):

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.

Huỳnh Trần Khanh (Sep 20 2022 at 03:33):

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?

Huỳnh Trần Khanh (Sep 20 2022 at 03:41):

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

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?

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.

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: Sep 23 2023 at 15:01 UTC