Stream of non-empty lists to stream

Using Coq
1

I am trying to write a cofixpoint to create a stream from a generator function of lists.
Thus, I want to define

\text{concatLists} : \forall A.~(\mathbb{N}\to \text{ne_list}~A) \to \text{Stream}~A

ne_list is the type of non-empty lists:

Inductive ne_list (A:Type) : Type :=
| ne_single (a:A)
| ne_cons   (a:A) (xs:ne_list A)

One of my attempts is

CoFixpoint concat_list {A} (f:nat -> ne_list A) n :=
    (prependNeListStream (f n) (concat_list f (S n))).

prependNeListStream matches on the non-empty list and in each case applies the Cons constructor.
Here, coq does not see that the fixpoint ends in guarded expressions.

Therefore, I tried to make the guaranteed Cons application per call explicit:

CoFixpoint concat_list {A} (f:nat -> ne_list A) n :=
  Cons (ne_head (f n))
    (prependListStream (ne_tail (f n)) (concat_list f (S n))).

But this code results in the same error in the guardedness check for the prepend sub-expression.

Is it possible to define a function converting a stream of non-empty lists to a stream of elements
that is accepted by the guarded checker?

I could use TLC’s FixFunMod or Unset Guard Checking.
But I wondered whether it is possible without additional assumption.

My complete code:

Require Import ssreflect ssrbool ssrfun.
Require Import List.
Require Import Lists.Streams.
Import Nat ListNotations.

Inductive ne_list (A:Type) : Type :=
| ne_single (a:A)
| ne_cons   (a:A) (xs:ne_list A).
Arguments ne_single {A}.
Arguments ne_cons {A}.

Fixpoint prependListStream {A} (xs:list A) ys :=
    match xs with
    | [] => ys
    | x::xr => Cons x (prependListStream xr ys)
    end.

Fixpoint prependNeListStream {A} (xs:ne_list A) ys :=
    match xs with
    | ne_single x => Cons x ys
    | ne_cons x xr => Cons x (prependNeListStream xr ys)
    end.

Fixpoint neListToList {A} (xs:ne_list A) :=
    match xs with
    | ne_single x => [x]
    | ne_cons x xr => x::neListToList xr
    end.

Definition ne_head {A} (xs:ne_list A) :=
    match xs with
    | ne_single x | ne_cons x _ => x
    end.

Definition ne_tail {A} (xs:ne_list A) :=
    match xs with
    | ne_single _ => []
    | ne_cons _ xr => neListToList xr
    end.

Transparent prependNeListStream.

(* Sub-expression (prepend _ _) not in guarded form *)
Fail CoFixpoint concat_list {A} (f:nat -> ne_list A) n :=
    (prependNeListStream (f n) (concat_list f (S n))).

(* Sub-expression (prepend _ _) not in guarded form *)
Fail CoFixpoint concat_list {A} (f:nat -> ne_list A) n :=
  Cons (ne_head (f n))
    (prependListStream (ne_tail (f n)) (concat_list f (S n))).


Lemma ne_conv_prepend {X} (xs:ne_list X) ys:
(prependNeListStream xs ys) = (prependListStream (neListToList xs) ys).
Proof.
  elim xs => /= [x|x xr ->] //=.
Qed.

Lemma split_head {X} (xs:ne_list X) ys:
(prependNeListStream xs ys) = (Cons (ne_head xs) (prependListStream (ne_tail xs) ys)).
Proof.
  case : xs => [x|x xr] //=.
  rewrite ne_conv_prepend;done.
Qed.
2

Hello,

I think one way to do it is to force the inlining of prependNeListStream by generalizing your cofix to work over an additional accumulator:

Definition concat_list_aux {A} (f:nat -> ne_list A) : ne_list A -> nat -> Stream A :=
  cofix F acc n :=
    match acc with
    | ne_single a  => Cons a (F (f n) (S n))
    | ne_cons a tl => Cons a (F tl n)
    end.

Definition concat_list {A} (f: nat -> ne_list A) n := concat_list_aux f (f n) (S n).
2 Likes
3

Here’s a way to define prepend.

  1. Fixpoints and cofixpoints don’t mix.
  2. Remove arguments that remain constant from recursive calls.
Definition prependNeListStream {A} (xs:ne_list A) ys :=
  (cofix prepend (xs : ne_list A) :=
    match xs with
    | ne_single x => Cons x ys
    | ne_cons x xr => Cons x (prepend xr)
    end) xs.

CoFixpoint concat_list {A} (f:nat -> ne_list A) n :=
    (prependNeListStream (f n) (concat_list f (S n))).
2 Likes