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?
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
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
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.
I have an alternative approach that's more efficient. Would you like to hear it?
Well, let me write some C++. I hope you can translate to Coq easily. The definition doesn't require well founded recursion
#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);
}
Fun exercise: prove its correctness
I guess to make it structural you'll want to recurse on n - index
? And && n / 2 >= close
appears redundant (by transitivity of >=
)
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.
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