How can I write a filter function for sequences represented as functions in Coq?

Question

Given that we have the types T1, T2 and T_Union, as well as functions proj1 : T_Union -> option T1 and proj2 : T_Union -> option T2, and a sequence represented as nat -> T_Union, how can you write a filter function that will return a type nat -> T1 or nat -> T2? I'm representing the union of T1 and T2 in this way as I'm not looking for the disjoint union (T1 + T2), but perhaps there might be a better way of doing this.

As an example, if we have the function of type nat -> T_Union where 0 -> a, 1 -> aa, 2 -> aaa, 3 -> aaaa and we want to restrict it to even length strings, I would want something like 0 -> aa, 1 -> aaaa. So, I would like to 'cut out' the other mappings instead of having 'holes' in the function.

What I am starting with is this:

Definition p1 (seq : nat -> T_Union) : nat -> T1 := 
  fun n => match proj seq n with
         | Some e => e
         | None   => ...
         end.

Answer 1

If the sequence s contains only odd length strings (or, more generally a finite number of strings of even length), your filter function would loop forever (hence be partial). Thus, Coq would reject such a definition of filter, unless you assume that you can find an infinite number of i such that the i-th element of shas the right property.

(cf. Yves Bertot's paper https://hal.inria.fr/inria-00070658/document )

Just for instance, here is an attempt to realize a simplified version of your specification.

Definition seq (A:Type) := nat -> A.

Definition shift {A} (s : seq A) : seq A := fun n => s (S n).


Fixpoint filter {A} (s: seq (option A)) : seq A :=
fun i => match i, s i with
         | 0, Some x => x
         | i , None => filter (shift s) i
         | S i, Some _ => filter (shift s) i
         end.
(* Error: Cannot guess decreasing argument of fix. *)

Obviously, filter would loop when applied to the infinite sequence of None.