Stream: Coq users

Topic: Enumerating Dyck words


view this post on Zulip 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?

view this post on Zulip 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 nseq 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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);
}

view this post on Zulip Huỳnh Trần Khanh (Mar 08 2023 at 23:36):

Fun exercise: prove its correctness

view this post on Zulip 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 >=)

view this post on Zulip 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.

view this post on Zulip 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 13 2024 at 01:02 UTC