Library CT.Language.Dyck

Dyck Language

This module is just a lightweight toy implementation of the Dyck language, just for messing around. It isn't per-se related to category theory, although later on we can formalize some things in relation to the bicyclic semigroup and the Dyck syntactic monoid, if we get that far.

https://en.wikipedia.org/wiki/Dyck_language

Require Import Coq.Lists.List.
Import ListNotations.

Inductive paren := l | r.

Definition word := list paren.

Inductive Dyck : word → Prop :=
| dEpsilon : Dyck nil
| dInd : ∀ w x, Dyck w → Dyck x → Dyck ([l ] ++ w ++ [r ] ++ x).

Example l_r_ex : Dyck ([l ; r ]).
Proof.
  apply (dInd [] []).
  apply dEpsilon.
  apply dEpsilon.
Qed.

Theorem dyck_must_start_l : ∀ w,
    Dyck w →
      match w with
      | nil ⇒ True
      | cons c _ ⇒ c = l
      end.
Proof.
  intros.
  induction H.
  trivial.
  simpl.
  trivial.
Qed.