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.
Admitted.
(** See the first 100 values of flattening *)
Eval cbv in (map (flatten_list_seq a seq bar) (Lists.List.seq 0 100)).
```

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

@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`

.

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

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

```
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`

Nice! Thanks so much

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.
```

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

Thank you both for your help!

Last updated: Oct 13 2024 at 01:02 UTC