## Stream: Coq users

### Topic: Flattening sequence of lists into a sequnece

#### Ali Caglayan (Oct 24 2021 at 13:38):

Hi, I am having some trouble coming up with a way to flatten a sequence. I have a sequence of non-empty lists which I would like to concatenate into a big sequence. I couldn't find anything in the stdlib that does this.

I have a working example here, but I couldn't convince the guard checker that my definition was valid. Is there a cleverer way to do what I want or can I somehow convince the guard checker? Also is it possible to have a version of `nth` that doesn't have a default value? I should be able to guarantee that the index is valid.

``````From Coq Require Import List Nat PeanoNat.
Import ListNotations Nat.

#[bypass_check(guard)]
Fixpoint flatten_list_seq_index {A : Type} (a : nat -> list A)
(P : forall n, 0 < length (a n))
(n : nat) (off : nat) {struct n}
: nat * nat :=
let k := length (a off) in
if n <? k then
(off , n)
else
flatten_list_seq_index a P (n - k) (S off).

Definition flatten_list_seq {A : Type} (a0 : A) (a : nat -> list A)
(P : forall n, 0 < length (a n)) (n : nat) : A :=
let '(m, k) := flatten_list_seq_index a P n 0 in
nth k (a m) a0.

(** Silly example *)

Inductive A := a | b | start | finish.

Definition seq (n : nat) : list A :=
cons start (
(fix seq' (n : nat) {struct n} :=
match n with
| 0 => [finish]
| S k => if even k then
cons a (seq' k)
else
cons b (seq' k)
end) n).

Lemma bar : forall n, 0 < length (seq n).
Proof.

(** See the first 100 values of flattening *)
Eval cbv in (map (flatten_list_seq a seq bar) (Lists.List.seq 0 100)).
``````

#### Karl Palmskog (Oct 24 2021 at 13:40):

there are various forms of flattening here, may be useful for comparison: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v#L3091

#### Ali Caglayan (Oct 24 2021 at 13:49):

@Karl Palmskog those are not quite comparable here. When I say sequence I mean `nat -> A` but in mathcomp they mean list. I am asking how `nat -> list A` can be flattened to `nat -> A`.

#### Gaëtan Gilbert (Oct 24 2021 at 14:01):

you can do something like this

``````Fixpoint flatten_list_seq_index_popped {A : Type} (a : nat -> A * list A)
(n : nat) (off : nat) {struct n}
: nat * nat.
Proof.
pose (k := length (snd (a off))).
destruct (n <? S k) eqn:H.
- exact (off, n).
- destruct n as [|n].
+ cbv in H. abstract discriminate H.
+ exact (flatten_list_seq_index_popped A a (n - k) (S off)).
Defined.

Definition pop {A} (l:list A) (H:0 < length l) : A * list A.
Proof.
destruct l as [|x l].
- exfalso; abstract inversion H.
- split;assumption.
Defined.

Definition flatten_list_seq_index {A : Type} (a : nat -> list A)
(P : forall n, 0 < length (a n))
(n : nat) (off : nat)
: nat * nat :=
flatten_list_seq_index_popped (fun n => pop (a n) (P n)) n off.
``````

or use wf recursion to define flatten_list_seq_index directly

#### Li-yao (Oct 24 2021 at 14:07):

TIL (n-k) is structurally smaller than (or equal to) n. How sophisticated is the termination checker!?

#### Gaëtan Gilbert (Oct 24 2021 at 14:09):

``````Nat.sub =
fix sub (n m : nat) {struct n} : nat :=
match n return nat with
| O => n
| S k => match m return nat with
| O => n
| S l => sub k l
end
end
``````

it only works because it the 0 case it returns syntactically `n` instead of `0`

#### Ali Caglayan (Oct 24 2021 at 14:18):

Nice! Thanks so much

#### Li-yao (Oct 24 2021 at 14:20):

Another one, where you massage the sequence into a structure that you can iterate through step by step.

``````Definition pop {A : Type} (a : list A) (P : 0 < length a) : A * list A.
Proof.
destruct a; [ exfalso; inversion P | constructor; assumption ].
Defined.

Definition biglist (A : Type) : Type := A * list A * (nat -> A * list A).

Definition to_biglist {A : Type} (a : nat -> A * list A) : biglist A :=
let '(a0, a1) := a 0 in
(a0, a1, fun i => a (S i)).

Definition uncons {A : Type} (xs : biglist A) : A * biglist A :=
let '(x0, x1, xs') := xs in
(x0, match x1 with
| [] => to_biglist xs'
| x0' :: x1' => (x0', x1', xs')
end).

Fixpoint flatten_list_seq_ {A : Type} (xs : biglist A) (n : nat) : A :=
let '(x0, xs') := uncons xs in
match n with
| O => x0
| S n => flatten_list_seq_ xs' n
end.

Definition flatten_list_seq {A : Type} (a0 : A) (a : nat -> list A)
(P : forall n, 0 < length (a n)) (n : nat) : A :=
flatten_list_seq_ (to_biglist (fun n => pop (a n) (P n))) n.
``````

#### Ali Caglayan (Oct 24 2021 at 14:34):

This one is nice because I don't have to deal with getting elements out of lists.

#### Ali Caglayan (Oct 24 2021 at 14:34):

Thank you both for your help!

Last updated: Oct 03 2023 at 20:01 UTC