Ali Caglayan (Oct 24 2021 at 13:38): 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)).
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.
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