Stream: Coq users

Topic: Flattening sequence of lists into a sequnece


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

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

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

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

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

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

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

view this post on Zulip Ali Caglayan (Oct 24 2021 at 14:18):

Nice! Thanks so much

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

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

view this post on Zulip Ali Caglayan (Oct 24 2021 at 14:34):

Thank you both for your help!


Last updated: Jan 31 2023 at 13:02 UTC