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.
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.