On proving lists infinite

Posted on October 26, 2021

It’s obvious what an infinite list is. But when formalizing things, we must be picky about definitions to not get tangled up in a messy web of concepts. This post will present some ways of saying that “a list is infinite” formally in Coq.¹

Coinductive lists

Imports and options

From Coq Require Import Arith Lia.

Set Primitive Projections.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Contextual Implicit.

First, define the type of lists. Lists are made of Cons (::) and Nil. As it is a recursive type, we also have to decide whether to make it inductive, so that only finite lists can be constructed, or coinductive, so that lists might also be infinite sequences of Cons. We start by introducing the type’s base functor ColistF a _, presenting the two list constructors without recursion. We obtain the coinductive type Colist a as a fixed point of ColistF a : Type -> Type.

Inductive ColistF (a : Type) (x : Type) :=
| Nil : ColistF a x
| Cons : a -> x -> ColistF a x
.

CoInductive Colist (a : Type) : Type :=
  Delay { force : ColistF a (Colist a) }.

Thus the type Colist a has a destructor force : Colist a -> ColistF a (Colist a) (the final coalgebra of ColistF a) and a constructor Delay : ColistF a (Colist a) -> Colist a. This ceremony may look all mysterious if you’re new to this; after living with coinductive types for a while, you will assimilate their philosophy of “destructors first”—unlike inductive types’ “constructors first”.

Notation prep

Add Printing Constructor Colist.

Declare Scope colist_scope.
Delimit Scope colist_scope with colist.
Local Open Scope colist_scope.

Some familiar notations, [] for Nil and :: for Cons.

Notation "'[' ']'" := Nil : colist_scope.
Notation "x :: xs" := (Cons x xs) : colist_scope.

Some simple definitions

Recursive definitions involving lists mostly look as you would expect in Coq as in any functional programming language, but every output list is wrapped in an explicit Delay, and every input list of a match is wrapped in a force. It’s as if you were handling lazy data structures in an eagerly evaluated programming language. Coq is a pure and total language, so evaluation order doesn’t matter as much as in partial languages, but the operational semantics is still careful to not reduce coinductive definitions unless they are forced.

Here is the map function that any self-respecting type of list must provide.

CoFixpoint map {a b} (f : a -> b) (xs : Colist a) : Colist b := Delay
  match force xs with
  | [] => []
  | x :: xs => f x :: map f xs
  end.

Another example is the list nats of all natural numbers. It relies on the more general definition of lists of numbers greater than an arbitrary natural number n.

CoFixpoint nats_from (n : nat) : Colist nat := Delay
  (n :: nats_from (S n)).

Definition nats := nats_from 0.

Let’s put that aside for now. We will be needing map and nats later.

Never-ending lists

We will now say “infinite lists” in an informal you-know-what-I-mean sense, as we explore different ways of making it more formal, which will have their own names.

A list is infinite when it never ends with a Nil. But in constructive mathematics we never say never—it’s not even obvious how you could even say it in this instance. A list is infinite when it, and its tails, always evaluate to a Cons.

A more “incremental” rephrasing of the above is that a list xs is infinite when xs evaluates to a Cons, and its tail is also infinite. That definition of infinite lists is recursive, so that you can “unfold” it iteratively to establish that every tail evaluates to a Cons. But because it is recursive, it’s not a priori well-defined.

Let us forget about “is infinite” for a second, and talk more generally about properties P that somehow subscribe to that definition: if xs satisfies P, then xs evaluates to a Cons, and the tail of xs satisfies P. Let us call such a P a never-ending invariant.

Definition Neverending_invariant {a} (P : Colist a -> Prop) : Prop :=
  forall xs, P xs -> exists x xs', force xs = Cons x xs' /\ P xs'.

The intuition is that if xs satisfies any never-ending invariant P, then xs must be infinite. This leads to our first characterization of infinite lists, “never-ending” lists.

Never-ending: definition

A list is never-ending when it satisfies some never-ending invariant.

Definition Neverending {a} (xs : Colist a) : Prop :=
  exists (P : Colist a -> Prop),
    Neverending_invariant P /\ P xs.

The key property that makes the notion of never-ending lists useful is the following unfolding lemma: a never-ending list is a Cons, and its tail is never-ending.

Note: you can hover and click on the tactics in proof scripts (Proof. ... Qed.) to see the intermediate proof states.²

Lemma unfold_Neverending {a} (xs : Colist a)
  : Neverending xs ->
    exists x xs',
      force xs = Cons x xs' /\ Neverending xs'.a: Type
xs: Colist a
Neverending xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
Proof.a: Type
xs: Colist a
Neverending xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  intros NE.a: Type
xs: Colist a
NE: Neverending xs
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  unfold Neverending in NE.a: Type
xs: Colist a
NE: exists P : Colist a -> Prop,
  Neverending_invariant P /\ P xs
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  destruct NE as [P [NE Hxs]].a: Type
xs: Colist a
P: Colist a -> Prop
NE: Neverending_invariant P
Hxs: P xs
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  unfold Neverending_invariant in NE.a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
Hxs: P xs
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  apply NE in Hxs.a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
Hxs: exists (x : a) (xs' : Colist a), force xs = x :: xs' /\ P xs'
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  destruct Hxs as [x [xs' [Hxs Hxs']]].a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
x: a
xs': Colist a
Hxs: force xs = x :: xs'
Hxs': P xs'
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
  exists x, xs'.a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
x: a
xs': Colist a
Hxs: force xs = x :: xs'
Hxs': P xs'
force xs = x :: xs' /\ Neverending xs'
  split; [assumption | ].a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
x: a
xs': Colist a
Hxs: force xs = x :: xs'
Hxs': P xs'
Neverending xs'
  unfold Neverending.a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
x: a
xs': Colist a
Hxs: force xs = x :: xs'
Hxs': P xs'
exists P : Colist a -> Prop,
  Neverending_invariant P /\ P xs'
  exists P.a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
x: a
xs': Colist a
Hxs: force xs = x :: xs'
Hxs': P xs'
Neverending_invariant P /\ P xs'
  split; [ | assumption ].a: Type
xs: Colist a
P: Colist a -> Prop
NE: forall xs : Colist a,
P xs ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ P xs'
x: a
xs': Colist a
Hxs: force xs = x :: xs'
Hxs': P xs'
Neverending_invariant P
  exact NE.
Qed.

Doesn’t that lemma’s statement remind you of Neverending_invariant above?

That lemma means exactly that the property of “being never-ending” is itself a never-ending invariant!

Lemma Neverending_invariant_Neverending {a}
  : Neverending_invariant (Neverending (a := a)).a: Type
Neverending_invariant Neverending
Proof.a: Type
Neverending_invariant Neverending
  unfold Neverending. (* This goal looks funny -> *)a: Type
Neverending_invariant
  (fun xs : Colist a =>
   exists P : Colist a -> Prop,
     Neverending_invariant P /\ P xs)
  exact (@unfold_Neverending a).
Qed.

The definition of Neverending makes it the weakest never-ending invariant: all never-ending invariants imply Neverending.

Lemma Neverending_weakest {a} (P : Colist a -> Prop) (xs : Colist a)
  : Neverending_invariant P -> P xs -> Neverending xs.a: Type
P: Colist a -> Prop
xs: Colist a
Neverending_invariant P -> P xs -> Neverending xs
Proof.a: Type
P: Colist a -> Prop
xs: Colist a
Neverending_invariant P -> P xs -> Neverending xs
  intros INV H.a: Type
P: Colist a -> Prop
xs: Colist a
INV: Neverending_invariant P
H: P xs
Neverending xs
  unfold Neverending.a: Type
P: Colist a -> Prop
xs: Colist a
INV: Neverending_invariant P
H: P xs
exists P : Colist a -> Prop,
  Neverending_invariant P /\ P xs
  exists P.a: Type
P: Colist a -> Prop
xs: Colist a
INV: Neverending_invariant P
H: P xs
Neverending_invariant P /\ P xs
  split; assumption.
Qed.

This is actually an instance of a pretty general way of defining recursive properties (and recursive types, by Curry-Howard) without using recursion. You introduce a class of “invariants” identified by the recursive definition, and then you pick the strongest or weakest one, depending on the situation (inductive or coinductive).³

Lists with too many elements

This next property is sufficient but not necessary: a list must be infinite if it contains infinitely many distinct elements. While this sounds circular, we care only about defining “infinite lists”, and for that we can leverage other “infinities” already lying around, like the natural numbers. Note that an infinite list may not satisfy that property by repeating the same finitely many elements (e.g., repeat 0).

One way to show that a set is infinite is to exhibit an injective function from the natural numbers (or any other infinite set): distinct elements are mapped to distinct elements, or conversely, every image element has a unique antecedent.

Definition injective {a b} (f : a -> b) : Prop :=
  forall x y, f x = f y -> x = y.

Now we need to tie those elements to a list, using the membership relation In. That relation is defined inductively: an element x is in a list xs if either x is the head of xs or x is in the tail of the list.

Snip

Unset Elimination Schemes. (* Don't generate induction principles for us. *)

Inductive In {a : Type} (x : a) (xs : Colist a) : Prop :=
| In_split y ys : force xs = Cons y ys -> x = y \/ In x ys -> In x xs
.

Snip

Lemma In_ind (a : Type) (x : a) (P : Colist a -> Prop)
    (H : forall xs (y : a) (ys : Colist a),
         force xs = y :: ys -> x = y \/ (In x ys /\ P ys) -> P xs)
  : forall xs, In x xs -> P xs.a: Type
x: a
P: Colist a -> Prop
H: forall (xs : Colist a) (y : a) (ys : Colist a),
force xs = y :: ys ->
x = y \/ In x ys /\ P ys -> P xs
forall xs : Colist a, In x xs -> P xs
Proof.a: Type
x: a
P: Colist a -> Prop
H: forall (xs : Colist a) (y : a) (ys : Colist a),
force xs = y :: ys ->
x = y \/ In x ys /\ P ys -> P xs
forall xs : Colist a, In x xs -> P xs
  fix SELF 2; intros xs [].a: Type
x: a
P: Colist a -> Prop
H: forall (xs : Colist a) (y : a) (ys : Colist a),
force xs = y :: ys ->
x = y \/ In x ys /\ P ys -> P xs
SELF: forall xs : Colist a, In x xs -> P xs
xs: Colist a
y: a
ys: Colist a
H0: force xs = y :: ys
H1: x = y \/ In x ys
P xs
  eapply H; eauto.a: Type
x: a
P: Colist a -> Prop
H: forall (xs : Colist a) (y : a) (ys : Colist a),
force xs = y :: ys ->
x = y \/ In x ys /\ P ys -> P xs
SELF: forall xs : Colist a, In x xs -> P xs
xs: Colist a
y: a
ys: Colist a
H0: force xs = y :: ys
H1: x = y \/ In x ys
x = y \/ In x ys /\ P ys
  destruct H1; [ left | right ]; auto.
Qed.

Lemma not_In_Nil {a} (x : a) xs : force xs = [] -> In x xs -> False.a: Type
x: a
xs: Colist a
force xs = [ ] -> In x xs -> False
Proof.a: Type
x: a
xs: Colist a
force xs = [ ] -> In x xs -> False
  intros ? []; congruence.
Qed.
#[global] Hint Resolve not_In_Nil : core.

Naturally, an element cannot be in an empty list. Two distinct elements cannot be in a list of length one. And so on. So if we can prove that infinitely many elements are in a list, then the list must be infinite. Let us call this property “surnumerable”, since it means that we can enumerate a subset of its elements.

Surnumerability: definition

A list xs is surnumerable if there is some injective function f : nat -> a such that f i is in xs for all i.

Definition Surnumerable {a} (xs : Colist a) : Prop :=
  exists f : nat -> a,
    injective f /\ forall i, In (f i) xs.

`Surnumerable` implies `Neverending`

A simple approach is to prove that Surnumerable is a never-ending invariant, but that requires decidable equality on a. A more general solution considers the invariant satisfied by lists xs such that Surnumerable (ys ++ xs) for some finite ys. The pigeonhole reasoning for that proof seems challenging, so I haven’t done it myself.

Theorem Surnumerable_Neverending {a} (xs : Colist a)
  : Surnumerable xs -> Neverending xs.a: Type
xs: Colist a
Surnumerable xs -> Neverending xs
Proof.a: Type
xs: Colist a
Surnumerable xs -> Neverending xs
  (* Exercise for the reader. *)
Abort.

Injectivity is not very “constructive”, you have to use a lot of tricks to recover useful information from it. In a proof that surnumerability implies never-ending-ness, a big part of it is to prove that surnumerability of a list Cons x xs implies (more or less) surnumerability of its tail xs. In other words, given f which describes an infinite set of elements in Cons x xs, and we must construct a new f2 which describes an infinite set of elements all in xs. The challenge is thus to “remove” the head x from the given injective function—if x occurs at all in f. This would be easier if we had a pseudo-inverse function to point to its antecedent by f. The existence of a pseudo-inverse is equivalent to injectivity classically, but it is stronger constructively. In category theory, a function f with a pseudo-inverse is called a split mono(morphism).

Definition splitmono {a b} (f : a -> b) : Prop :=
  exists g : b -> a, forall x, g (f x) = x.

We obtain a variant of Surnumerable using splitmono instead of injective.

Definition SplitSurnumerable {a} (xs : Colist a) : Prop :=
  exists (f : nat -> a),
    splitmono f /\ forall i, In (f i) xs.

The pseudo-inverse makes the proof of never-ending-ness much simpler.

Theorem SplitSurnumerable_Neverending {a} (xs : Colist a)
  : SplitSurnumerable xs -> Neverending xs.a: Type
xs: Colist a
SplitSurnumerable xs -> Neverending xs
Proof.a: Type
xs: Colist a
SplitSurnumerable xs -> Neverending xs
  intros PN.a: Type
xs: Colist a
PN: SplitSurnumerable xs
Neverending xs unfold SplitSurnumerable in PN.a: Type
xs: Colist a
PN: exists f : nat -> a,
  splitmono f /\ (forall i : nat, In (f i) xs)
Neverending xs
  destruct PN as (f & Hf & Hincl).a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
Neverending xs
  unfold Neverending.a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
exists P : Colist a -> Prop,
  Neverending_invariant P /\ P xs
  (* Here is the never-ending invariant. *)
  exists (fun xs => exists n, forall i, n <= i -> In (f i) xs).a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
Neverending_invariant
  (fun xs : Colist a =>
   exists n : nat,
     forall i : nat, n <= i -> In (f i) xs) /\
(exists n : nat, forall i : nat, n <= i -> In (f i) xs)
  split.a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
Neverending_invariant
  (fun xs : Colist a =>
   exists n : nat,
     forall i : nat, n <= i -> In (f i) xs)
a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
exists n : nat, forall i : nat, n <= i -> In (f i) xs
  -a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
Neverending_invariant
  (fun xs : Colist a =>
   exists n : nat,
     forall i : nat, n <= i -> In (f i) xs) unfold Neverending_invariant.a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
forall xs : Colist a,
(exists n : nat, forall i : nat, n <= i -> In (f i) xs) ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\
  (exists n : nat,
     forall i : nat, n <= i -> In (f i) xs')
    intros xs_ [n Hn].a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
exists (x : a) (xs' : Colist a),
  force xs_ = x :: xs' /\
  (exists n : nat,
     forall i : nat, n <= i -> In (f i) xs')
    destruct (force xs_) as [ | x xs'] eqn:Hforce.a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
Hforce: force xs_ = [ ]
exists (x : a) (xs' : Colist a),
  [ ] = x :: xs' /\
  (exists n : nat,
     forall i : nat, n <= i -> In (f i) xs')
a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
exists (x0 : a) (xs'0 : Colist a),
  x :: xs' = x0 :: xs'0 /\
  (exists n : nat,
     forall i : nat, n <= i -> In (f i) xs'0)
    +a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
Hforce: force xs_ = [ ]
exists (x : a) (xs' : Colist a),
  [ ] = x :: xs' /\
  (exists n : nat,
     forall i : nat, n <= i -> In (f i) xs') exfalso.a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
Hforce: force xs_ = [ ]
False eauto using not_In_Nil.
    +a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
exists (x0 : a) (xs'0 : Colist a),
  x :: xs' = x0 :: xs'0 /\
  (exists n : nat,
     forall i : nat, n <= i -> In (f i) xs'0) exists x, xs'; split; [ auto | ].a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
exists n : nat, forall i : nat, n <= i -> In (f i) xs'
      destruct Hf as [g Hf].a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
exists n : nat, forall i : nat, n <= i -> In (f i) xs'
      exists (max n (S (g x))).a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
forall i : nat,
Init.Nat.max n (S (g x)) <= i -> In (f i) xs'
      intros i Hi.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n: nat
Hn: forall i : nat, n <= i -> In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
i: nat
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs'
      specialize (Hn i (Nat.max_lub_l _ _ _ Hi)).a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
Hn: In (f i) xs_
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs'
      destruct Hn.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
y: a
ys: Colist a
H: force xs_ = y :: ys
H0: f i = y \/ In (f i) ys
x: a
xs': Colist a
Hforce: force xs_ = x :: xs'
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs'
      rewrite H in Hforce; inversion Hforce; subst; clear Hforce.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: f i = x \/ In (f i) xs'
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs'
      destruct H0.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: f i = x
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs'
a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: In (f i) xs'
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs'
      *a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: f i = x
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs' exfalso.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: f i = x
Hi: Init.Nat.max n (S (g x)) <= i
False rewrite <- H0 in Hi.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: f i = x
Hi: Init.Nat.max n (S (g (f i))) <= i
False rewrite Hf in Hi.a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: f i = x
Hi: Init.Nat.max n (S i) <= i
False lia.
      *a: Type
xs: Colist a
f: nat -> a
g: a -> nat
Hf: forall x : nat, g (f x) = x
Hincl: forall i : nat, In (f i) xs
xs_: Colist a
n, i: nat
x: a
xs': Colist a
H: force xs_ = x :: xs'
H0: In (f i) xs'
Hi: Init.Nat.max n (S (g x)) <= i
In (f i) xs' assumption.
  -a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
exists n : nat, forall i : nat, n <= i -> In (f i) xs exists 0.a: Type
xs: Colist a
f: nat -> a
Hf: splitmono f
Hincl: forall i : nat, In (f i) xs
forall i : nat, 0 <= i -> In (f i) xs auto.
Qed.

Surnumerability may be easier to prove than never-ending-ness in some situations. A proof that a list is never-ending essentially “walks through” the evaluation of the list, but in certain situations the list might be too abstract to inspect, for example when reasoning by parametricity,⁴ and we can only prove the membership of individual elements one by one.

Enumerability

Our last idea is that infinite lists (with element type a) are in bijection with functions nat -> a. So we can show that a list is infinite by proving that it corresponds to a function nat -> a via such a bijection. We shall use the obvious bijection that sends f to map f nats—and conversely sends an infinite list xs to a function index xs : nat -> a. We will thus say that a list xs is enumerable if it can be written as map f nats for some f.

Equality of colists

Before we can state the equation xs = map f nats, we must choose a notion of equality. One can be readily obtained via the following coinductive relation, which corresponds to the relational interpretation of the type Colist à la Reynolds.⁵ It interprets the type constructor Colist : Type -> Type as a relation transformer RColist : (a -> b -> Prop) -> (Colist a -> Colist b -> Prop), which can be specialized to an equivalence relation RColist eq; we will write it in infix notation as == in the rest of the post.

Inductive RColistF {a b} (r : a -> b -> Prop) xa xb (rx : xa -> xb -> Prop)
  : ColistF a xa -> ColistF b xb -> Prop :=
| RNil : RColistF r rx [] []
| RCons x xs y ys : r x y -> rx xs ys -> RColistF r rx (Cons x xs) (Cons y ys)
.

CoInductive RColist {a b} (r : a -> b -> Prop) (xs : Colist a) (ys : Colist b) : Prop :=
  RDelay { Rforce : RColistF r (RColist r) (force xs) (force ys) }.

Notation "x == y" := (RColist eq x y) (at level 70) : colist_scope.

Enumerability: definition

We can now say formally that xs is enumerable by f if xs == map f nats.

Definition Enumerable_by {a} (f : nat -> a) (xs : Colist a) : Prop :=
  xs == map f nats.

Definition Enumerable {a} (xs : Colist a) : Prop :=
  exists f, Enumerable_by f xs.

As mentioned earlier, the equation xs == map f nats exercises one half of the bijection between infinite lists and functions on nat. Formalizing the other half takes more work, and it will actually let us prove that Neverending implies Enumerable.

`Neverending` implies `Enumerable`

Essentially, we need to define an indexing function index : Colist a -> nat -> a. However, this is only well-defined for infinite lists. A better type will be a dependent type index : forall (xs : Colist a), Neverending xs -> nat -> a, where the input list xs must be never-ending.

Start with a naive definition having the simpler type, which handles partiality with a default value:

Fixpoint index_def {a} (def : a) (xs : Colist a) (i : nat) : a :=
  match force xs, i with
  | Cons x _, O => x
  | Cons _ xs, S i => index_def def xs i
  | Nil, _ => def
  end.

Given a never-ending list, we are able to extract an arbitrary value as a default—which will be passed to index_def but never actually be used. It takes a bit of dependently typed programming, which we dispatch with tactics. And since we don’t actually care about the result we can keep the definition opaque with Qed (instead of Defined).

Definition head_NE {a} (xs : Colist a) (NE : Neverending xs) : a.a: Type
xs: Colist a
NE: Neverending xs
a
Proof.a: Type
xs: Colist a
NE: Neverending xs
a
  destruct (force xs) as [ | x xs' ] eqn:Hxs.a: Type
xs: Colist a
NE: Neverending xs
Hxs: force xs = [ ]
a
a: Type
xs: Colist a
NE: Neverending xs
x: a
xs': Colist a
Hxs: force xs = x :: xs'
a
  -a: Type
xs: Colist a
NE: Neverending xs
Hxs: force xs = [ ]
a exfalso.a: Type
xs: Colist a
NE: Neverending xs
Hxs: force xs = [ ]
False apply unfold_Neverending in NE.a: Type
xs: Colist a
NE: exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
Hxs: force xs = [ ]
False destruct NE as [? [? []]].a: Type
xs: Colist a
x: a
x0: Colist a
H: force xs = x :: x0
H0: Neverending x0
Hxs: force xs = [ ]
False congruence.
  -a: Type
xs: Colist a
NE: Neverending xs
x: a
xs': Colist a
Hxs: force xs = x :: xs'
a exact x.
Qed.

Combining index_def and head_NE, we obtain our index function.

Definition index {a} (xs : Colist a) (NE : Neverending xs) (i : nat) : a :=
  index_def (head_NE NE) xs i.

The remaining code in this post proves that a never-ending list xs is enumerated by index xs.

This first easy lemma says that index_def doesn’t depend on the default value if the list is never-ending.

Lemma index_def_Neverending {a} (def def' : a) (xs : Colist a) (i : nat)
  : Neverending xs -> index_def def xs i = index_def def' xs i.a: Type
def, def': a
xs: Colist a
i: nat
Neverending xs ->
index_def def xs i = index_def def' xs i
Proof.a: Type
def, def': a
xs: Colist a
i: nat
Neverending xs ->
index_def def xs i = index_def def' xs i
  revert xs; induction i; intros * NE; cbn.a: Type
def, def': a
xs: Colist a
NE: Neverending xs
match force xs with
| [ ] => def
| x :: _ => x
end =
match force xs with
| [ ] => def'
| x :: _ => x
end
a: Type
def, def': a
i: nat
IHi: forall xs : Colist a,
Neverending xs ->
index_def def xs i = index_def def' xs i
xs: Colist a
NE: Neverending xs
match force xs with
| [ ] => def
| _ :: xs => index_def def xs i
end =
match force xs with
| [ ] => def'
| _ :: xs => index_def def' xs i
end
  all: apply unfold_Neverending in NE.a: Type
def, def': a
xs: Colist a
NE: exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
match force xs with
| [ ] => def
| x :: _ => x
end =
match force xs with
| [ ] => def'
| x :: _ => x
end
a: Type
def, def': a
i: nat
IHi: forall xs : Colist a,
Neverending xs ->
index_def def xs i = index_def def' xs i
xs: Colist a
NE: exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
match force xs with
| [ ] => def
| _ :: xs => index_def def xs i
end =
match force xs with
| [ ] => def'
| _ :: xs => index_def def' xs i
end
  all: destruct NE as [x [xs' [Hxs NE]]].a: Type
def, def': a
xs: Colist a
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE: Neverending xs'
match force xs with
| [ ] => def
| x :: _ => x
end =
match force xs with
| [ ] => def'
| x :: _ => x
end
a: Type
def, def': a
i: nat
IHi: forall xs : Colist a,
Neverending xs ->
index_def def xs i = index_def def' xs i
xs: Colist a
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE: Neverending xs'
match force xs with
| [ ] => def
| _ :: xs => index_def def xs i
end =
match force xs with
| [ ] => def'
| _ :: xs => index_def def' xs i
end 
  all: rewrite Hxs.a: Type
def, def': a
xs: Colist a
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE: Neverending xs'
x = x
a: Type
def, def': a
i: nat
IHi: forall xs : Colist a,
Neverending xs ->
index_def def xs i = index_def def' xs i
xs: Colist a
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE: Neverending xs'
index_def def xs' i = index_def def' xs' i
  all: auto.
Qed.

The next lemma does the heavy lifting, constructing an “equality invariant” (or “bisimulation”) that must hold between all respective tails of xs and map (index xs) nats, which then implies ==.

Note that instead of index xs, we actually write index NE where NE is a proof of Neverending xs, since index requires that argument, and xs can be deduced from NE’s type.

Lemma Neverending_Enumerable_ {a} (xs : Colist a) (NE : Neverending xs)
    (f : nat -> a) (n : nat)
  : (forall i, f (n+i) = index NE i) ->
    xs == map f (nats_from n).a: Type
xs: Colist a
NE: Neverending xs
f: nat -> a
n: nat
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
Proof.a: Type
xs: Colist a
NE: Neverending xs
f: nat -> a
n: nat
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
  revert xs NE n; cofix SELF; intros * Hf.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
xs == map f (nats_from n)
  constructor.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
RColistF eq (RColist eq) 
  (force xs) (force (map f (nats_from n)))
  assert (NE' := NE).a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
NE': Neverending xs
RColistF eq (RColist eq) 
  (force xs) (force (map f (nats_from n)))
  apply unfold_Neverending in NE'.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
NE': exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\ Neverending xs'
RColistF eq (RColist eq) 
  (force xs) (force (map f (nats_from n)))
  destruct NE' as [x [xs' [Hxs NE']]].a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
RColistF eq (RColist eq) 
  (force xs) (force (map f (nats_from n)))
  rewrite Hxs; cbn.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
RColistF eq (RColist eq) 
  (x :: xs') (f n :: map f (nats_from (S n)))
  constructor.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
x = f n
a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
xs' == map f (nats_from (S n))
  -a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
x = f n specialize (Hf 0).a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: f (n + 0) = index NE 0
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
x = f n
    cbn in Hf.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: f (n + 0) =
match force xs with
| [ ] => head_NE NE
| x :: _ => x
end
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
x = f n rewrite Nat.add_0_r, Hxs in Hf.a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
x: a
Hf: f n = x
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
x = f n auto.
  -a: Type
f: nat -> a
SELF: forall (xs : Colist a) (NE : Neverending xs)
  (n : nat),
(forall i : nat, f (n + i) = index NE i) ->
xs == map f (nats_from n)
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
xs' == map f (nats_from (S n)) apply SELF with (NE := NE'); clear SELF.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
forall i : nat, f (S n + i) = index NE' i
    intros i.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n: nat
Hf: forall i : nat, f (n + i) = index NE i
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
i: nat
f (S n + i) = index NE' i specialize (Hf (S i)).a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n, i: nat
Hf: f (n + S i) = index NE (S i)
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
f (S n + i) = index NE' i
    cbn in Hf.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n, i: nat
Hf: f (n + S i) =
match force xs with
| [ ] => head_NE NE
| _ :: xs0 => index_def (head_NE NE) xs0 i
end
x: a
xs': Colist a
Hxs: force xs = x :: xs'
NE': Neverending xs'
f (S n + i) = index NE' i rewrite Nat.add_succ_r, Hxs in Hf.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n, i: nat
xs': Colist a
Hf: f (S (n + i)) = index_def (head_NE NE) xs' i
x: a
Hxs: force xs = x :: xs'
NE': Neverending xs'
f (S n + i) = index NE' i
    cbn; rewrite Hf.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n, i: nat
xs': Colist a
Hf: f (S (n + i)) = index_def (head_NE NE) xs' i
x: a
Hxs: force xs = x :: xs'
NE': Neverending xs'
index_def (head_NE NE) xs' i = index NE' i unfold index.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n, i: nat
xs': Colist a
Hf: f (S (n + i)) = index_def (head_NE NE) xs' i
x: a
Hxs: force xs = x :: xs'
NE': Neverending xs'
index_def (head_NE NE) xs' i =
index_def (head_NE NE') xs' i
    apply index_def_Neverending.a: Type
f: nat -> a
xs: Colist a
NE: Neverending xs
n, i: nat
xs': Colist a
Hf: f (S (n + i)) = index_def (head_NE NE) xs' i
x: a
Hxs: force xs = x :: xs'
NE': Neverending xs'
Neverending xs' auto.
Qed.

Here’s the final result. A never-ending list xs is enumerated by index xs.

Theorem Neverending_Enumerable_by {a} (xs : Colist a) (NE : Neverending xs)
  : Enumerable_by (index NE) xs.a: Type
xs: Colist a
NE: Neverending xs
Enumerable_by (index NE) xs
Proof.a: Type
xs: Colist a
NE: Neverending xs
Enumerable_by (index NE) xs
  unfold Enumerable_by, nats.a: Type
xs: Colist a
NE: Neverending xs
xs == map (index NE) (nats_from 0)
  apply Neverending_Enumerable_ with (NE := NE) (n := 0).a: Type
xs: Colist a
NE: Neverending xs
forall i : nat, index NE (0 + i) = index NE i
  reflexivity.
Qed.

We can repackage the theorem to hide the enumeration function, more closely matching the English sentence “never-ending-ness implies enumerability”.

Corollary Neverending_Enumerable {a} (xs : Colist a)
  : Neverending xs -> Enumerable xs.a: Type
xs: Colist a
Neverending xs -> Enumerable xs
Proof.a: Type
xs: Colist a
Neverending xs -> Enumerable xs
  intros NE; eexists; apply (Neverending_Enumerable_by (NE := NE)).
Qed.

The converse holds this time. The main insight behind the proof is that the property “xs == map f (nats_from n) for some n” is a never-ending invariant.

Theorem Enumerable_Neverending {a} (xs : Colist a)
  : Enumerable xs -> Neverending xs.a: Type
xs: Colist a
Enumerable xs -> Neverending xs
Proof.a: Type
xs: Colist a
Enumerable xs -> Neverending xs
  unfold Enumerable, Enumerable_by.a: Type
xs: Colist a
(exists f : nat -> a, xs == map f nats) ->
Neverending xs intros [f EB].a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
Neverending xs
  unfold Neverending.a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
exists P : Colist a -> Prop,
  Neverending_invariant P /\ P xs
  exists (fun xs => exists n, xs == map f (nats_from n)).a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
Neverending_invariant
  (fun xs : Colist a =>
   exists n : nat, xs == map f (nats_from n)) /\
(exists n : nat, xs == map f (nats_from n))
  split.a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
Neverending_invariant
  (fun xs : Colist a =>
   exists n : nat, xs == map f (nats_from n))
a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
exists n : nat, xs == map f (nats_from n)
  -a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
Neverending_invariant
  (fun xs : Colist a =>
   exists n : nat, xs == map f (nats_from n)) unfold Neverending_invariant.a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
forall xs : Colist a,
(exists n : nat, xs == map f (nats_from n)) ->
exists (x : a) (xs' : Colist a),
  force xs = x :: xs' /\
  (exists n : nat, xs' == map f (nats_from n)) intros xs_ [n EB_].a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: xs_ == map f (nats_from n)
exists (x : a) (xs' : Colist a),
  force xs_ = x :: xs' /\
  (exists n : nat, xs' == map f (nats_from n))
    destruct EB_ as [EB_].a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: RColistF eq (RColist eq) (force xs_) (force (map f (nats_from n)))
exists (x : a) (xs' : Colist a),
  force xs_ = x :: xs' /\
  (exists n : nat, xs' == map f (nats_from n)) cbn in EB_.a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: RColistF eq (RColist eq) (force xs_) (f n :: map f (nats_from (S n)))
exists (x : a) (xs' : Colist a),
  force xs_ = x :: xs' /\
  (exists n : nat, xs' == map f (nats_from n)) inversion EB_; subst.a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: RColistF eq (RColist eq) (force xs_) (f n :: map f (nats_from (S n)))
xs0: Colist a
H3: xs0 == map f (nats_from (S n))
H: f n :: xs0 = force xs_
exists (x : a) (xs' : Colist a),
  f n :: xs0 = x :: xs' /\
  (exists n : nat, xs' == map f (nats_from n))
    exists (f n), xs0.a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: RColistF eq (RColist eq) (force xs_) (f n :: map f (nats_from (S n)))
xs0: Colist a
H3: xs0 == map f (nats_from (S n))
H: f n :: xs0 = force xs_
f n :: xs0 = f n :: xs0 /\
(exists n : nat, xs0 == map f (nats_from n)) split; [ auto | ].a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: RColistF eq (RColist eq) (force xs_) (f n :: map f (nats_from (S n)))
xs0: Colist a
H3: xs0 == map f (nats_from (S n))
H: f n :: xs0 = force xs_
exists n : nat, xs0 == map f (nats_from n)
    exists (S n).a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
xs_: Colist a
n: nat
EB_: RColistF eq (RColist eq) (force xs_) (f n :: map f (nats_from (S n)))
xs0: Colist a
H3: xs0 == map f (nats_from (S n))
H: f n :: xs0 = force xs_
xs0 == map f (nats_from (S n)) assumption.
  -a: Type
xs: Colist a
f: nat -> a
EB: xs == map f nats
exists n : nat, xs == map f (nats_from n) exists 0; assumption.
Qed.

Reasoning with enumerability

I think Neverending is the most intuitive characterization of infinite lists, but Enumerable can be easier to use. To illustrate the point, let us examine a minimized version of my use case.

Consider an arbitrary function from lists of lists to lists: join : Colist (Colist a) -> Colist a.

Try to formalize the statement

When join is applied to a square matrix, i.e., a list of lists all of the same length, it computes the diagonal.

(NB: An infinite list of infinite lists is considered a square.)

The literal approach is to introduce two functions length (in the extended naturals) and diagonal, so we can translate the above sentence as follows:

forall (xs : Colist (Colist a)),
  (forall row, In row xs -> length row = length xs) ->
  join xs == diagonal xs.

However, this is unwieldly because the definition of diagonal is not completely trivial. One will have to prove quite a few propositions about diagonal in order to effectively reason about it.

A more parsimonious solution relies on the idea that the “diagonal” is simple to define on functions f : b -> b -> a, as diagonal f := fun x => f x x. That leads to the following translation:

forall (f : b -> b -> a) (xs : Colist b),
  join (map (fun x => map (f x) xs) xs) = map (fun x => f x x) xs

It takes a bit of squinting to recognize the original idea, but the upside is that this is now a purely equational fact, without side conditions.

Rather than constrain a general list of lists to be a square, we generate squares from a binary function f : b -> b -> a and a list xs : Colist b representing the “sides” of the square, containing “coordinates” along one axis. In particular, we can use xs := nats as the side of an “infinite square”, and nats arises readily from Enumerable lists. Any square can be extensionally rewritten in that way. This theorem requires no ad-hoc definition like a separate diagonal function, and instead we can immediately use general facts about map both to prove and to use such a theorem.

Surnumerable: the list contains infinitely many distinct elements (two versions, based on classical injections and split monos).
Never-ending: the list never terminates with Nil—always evaluates to Cons.
Enumerable: the list identifies with some function on nat.

Print SplitSurnumerable.SplitSurnumerable = 
fun (a : Type) (xs : Colist a) =>
exists f : nat -> a,
  splitmono f /\ (forall i : nat, In (f i) xs)
     : forall a : Type, Colist a -> Prop

Arguments SplitSurnumerable {a}%type_scope xs
(*      ⇓      *)
Print Surnumerable.Surnumerable = 
fun (a : Type) (xs : Colist a) =>
exists f : nat -> a,
  injective f /\ (forall i : nat, In (f i) xs)
     : forall a : Type, Colist a -> Prop

Arguments Surnumerable {a}%type_scope xs
(*      ⇓      *)
Print Neverending.Neverending = 
fun (a : Type) (xs : Colist a) =>
exists P : Colist a -> Prop,
  Neverending_invariant P /\ P xs
     : forall a : Type, Colist a -> Prop

Arguments Neverending {a}%type_scope xs
(*      ⇕      *)
Print Enumerable.Enumerable = 
fun (a : Type) (xs : Colist a) =>
exists f : nat -> a, Enumerable_by f xs
     : forall a : Type, Colist a -> Prop

Arguments Enumerable {a}%type_scope xs

Can you think of other characterizations of infinite lists?