## Stream: Coq users

### Topic: Enumerating Dyck words

#### Stefan Haan (Mar 08 2023 at 14:57):

I want to enumerate all Dyck words: words of parentheses of length 2*n, which are well formed, for example `((()(())))`. I came up with following function, but I have trouble convincing Coq that `k` is indeed structurally smaller than `S n`.

``````Require Import FunInd Recdef.

Function dycks (n: nat) {struct n}: list (list bool) :=
match n with
| 0 => [ nil ]
| S n =>
flat_map
(fun k =>
map (fun ww => true::(fst ww)++false::(snd ww))
(combine (dycks k) (dycks (n-k))))
(seq 0 (S n))
end.
``````

I also tried `{wf lt n}` instead of `{struct n}` however this also leads to an error:

``````Abstracting over the term "k" leads to a term
fun k0 : nat =>
1 < k0 ->
forall def : nat -> list word,
iter (nat -> list word) k0 dycks_F def (S n0) =
flat_map
(fun k1 : nat =>
map
(fun ww : list bool * list bool =>
true :: fst ww ++ false :: snd ww)
(combine (dycks k1) (dycks (n0 - k1)))) (seq 0 (S n0))
which is ill-typed.
``````

Is defining this function possible?

#### Paolo Giarrusso (Mar 08 2023 at 15:16):

I don't know if it can be defined with `Function`, but I'm sure it's possible with `Equations` and maybe some tweaking.
Since you also call `dycks (n - k)`, it's pretty likely you'll need well-founded recursion...

It's not clear whether you'll be able to prove that `k < S n``seq 0 (S n)` gives a `list nat` and the information might be lost. _However_ having a list of `{ m | m < S n }` should work; alternatively, it might be easier to do a nested recursion on `S n` instead of mapping over `seq`

#### Laurent Théry (Mar 08 2023 at 15:17):

A standard trick is to add an extra argument to control the recursion depth and call the function with enough fuel.
In your example it may look like

#### Laurent Théry (Mar 08 2023 at 15:17):

``````Function dycks_aux v (n: nat) {struct v}: list (list bool) :=
match v with
0 => [ nil ]
|S v1 =>
match n with
| 0 => [ nil ]
| S n =>
flat_map
(fun k =>
map (fun ww => true::(fst ww)++false::(snd ww))
(combine (dycks_aux v1 k) (dycks_aux v1 (n-k))))
(seq 0 (S n))
end
end.

Definition dycks n := dycks_aux n n.
``````

#### Huỳnh Trần Khanh (Mar 08 2023 at 23:18):

I have an alternative approach that's more efficient. Would you like to hear it?

#### Huỳnh Trần Khanh (Mar 08 2023 at 23:20):

Well, let me write some C++. I hope you can translate to Coq easily. The definition doesn't require well founded recursion

#### Huỳnh Trần Khanh (Mar 08 2023 at 23:36):

``````#include <bits/stdc++.h>
using namespace std;
int n;
string s;
bool check(int index, int open, int close)
{
return n / 2 >= open && n / 2 >= close && open >= close;
}
void enumerate(int index, int open, int close)
{
if (index == n)
{
cout << s << "\n";
return;
}

if (check(index + 1, open + 1, close))
{
s += '(';
enumerate(index + 1, open + 1, close);
s.pop_back();
}

if (check(index + 1, open, close + 1))
{
s += ')';
enumerate(index + 1, open, close + 1);
s.pop_back();
}
}
int main()
{
n = 6;
enumerate(0, 0, 0);
}
``````

#### Huỳnh Trần Khanh (Mar 08 2023 at 23:36):

Fun exercise: prove its correctness

#### Paolo Giarrusso (Mar 08 2023 at 23:47):

I guess to make it structural you'll want to recurse on `n - index`? And `&& n / 2 >= close` appears redundant (by transitivity of `>=`)

#### Li-yao (Mar 09 2023 at 23:00):

Instead of top-down you can work bottom-up, where you accumulate a list of enumerations for smaller lengths while you compute the next one.
You can also use a nested fixpoint to make the n recursive calls, get the list of results, and zip it with its reverse:

``````Require Import List.
Import ListNotations.

(* foldi_nat f x n = f n (f (n-1) .. (f 0 x) ..) *)
Definition foldi_nat {A : Type} (f : nat -> A -> A) (x : A) : nat -> A :=
fix foldi (n : nat) :=
f n (match n with
| O => x
| S n => foldi n
end).

Notation "a >>= k" := (concat (map k a)) (at level 40).

Fixpoint dyck (n : nat) : list (list bool) :=
match n with
| O => [ [] ]
| S n =>
let prev := foldi_nat (fun k etc => dyck k :: etc) [] n in
combine prev (rev prev) >>= fun '(dyck_k, dyck_n_k) =>
list_prod dyck_k dyck_n_k >>= fun '(xs, ys) =>
[true :: xs ++ false :: ys]
end.

Compute dyck 4.
``````

#### Stefan Haan (Mar 11 2023 at 17:15):

Laurent Théry said:

A standard trick is to add an extra argument to control the recursion depth and call the function with enough fuel.
In your example it may look like

Thanks, this trick works! I could define the function like this (one need `list_prod` instead of `combine`) and I believe it's correct:

``````Fixpoint dycks_aux fuel (n: nat) {struct fuel}: list word :=
match fuel with
| 0 => [ nil ]
| S fuel =>
match n with
| 0 => [ nil ]
| S n =>
flat_map
(fun k =>
map (fun '(v,w) => (true::v++[false])++w)
(list_prod (dycks_aux fuel k) (dycks_aux fuel (n-k))))
(seq 0 (S n))
end
end.

Definition dycks n := dycks_aux n n.
``````

However the `fuel` seems to complicate induction proofs, it's likely I have to use @Li-yao 's approach here.

Last updated: Oct 04 2023 at 19:01 UTC