如何在Coq中为函数表示的T_Union序列编写过滤函数？

核心需求 #

已知类型T1、T2、T_Union，以及投影函数proj1 : T_Union -> option T1、proj2 : T_Union -> option T2，还有以nat -> T_Union表示的序列。需要编写过滤函数，返回nat -> T1或nat -> T2类型的序列——要求直接移除不符合条件的映射，而非保留空缺（比如原序列0→a、1→aa、2→aaa、3→aaaa，过滤偶数长度后要得到0→aa、1→aaaa）。另外，当前用T_Union表示并集而非不相交并集T1 + T2，也可探讨更优实现方式。

问题分析 #

你当前的初始代码存在一个关键问题：nat -> T1要求对每个自然数n都返回一个T1值，但过滤后必然存在原序列中对应位置无法提取T1的情况，直接返回T1会出现无法填充的None分支。因此不能直接用nat -> T1作为返回类型，需要调整实现思路。

可行实现方案 #

方案1：用列表存储过滤结果（直观易实现） #

先把nat -> T_Union序列转换成有限列表（适用于序列会终止的场景），过滤出能提取T1的元素，再按需转换成nat -> T1（超出列表长度的位置可指定默认值）：

Definition filter_T1_list (seq : nat -> T_Union) : list T1 :=
  let rec aux n acc :=
    match proj1 (seq n) with
    | Some e => aux (S n) (e :: acc)
    | None => aux (S n) acc
    (* 需添加终止条件，比如假设序列到某个n后全为None，或手动指定遍历上限 *)
    end in
  rev (aux 0 nil).

(* 将列表转为nat -> T1，超出长度的位置用指定默认值填充 *)
Definition list_to_seq {A} (l : list A) (default : A) : nat -> A :=
  fun n => nth n l default.

Definition filter_T1_seq (seq : nat -> T_Union) (default_T1 : T1) : nat -> T1 :=
  list_to_seq (filter_T1_list seq) default_T1.

方案2：用索引类型保证类型安全（适合需严格证明的场景） #

如果要严格表示“仅对存在有效T1的自然数有定义”，可以定义索引类型来关联过滤后的位置与原序列的有效位置：

Inductive Filtered_T1 : nat -> Type :=
| Filtered_T1_step : forall n e k, proj1 (seq n) = Some e -> Filtered_T1 k -> Filtered_T1 (S k)
| Filtered_T1_base : Filtered_T1 0.

(* 从索引类型提取T1值 *)
Definition get_filtered_T1 {k} (ft : Filtered_T1 k) : T1 :=
  match ft with
  | Filtered_T1_step _ e _ _ => e
  | Filtered_T1_base => (* 需处理初始空情况，或调整归纳定义 *)
  end.

方案3：调整并集表示（更优的类型设计） #

如果T_Union的设计可以调整，建议用子集类型明确区分属于T1的元素，这样过滤后的序列类型更严谨：

(* 定义属于T1的T_Union子集 *)
Definition T1_subset : Type := {x : T_Union | proj1 x <> None}.

(* 从子集安全提取T1值（依赖子集的证明） *)
Definition proj1_subset (x : T1_subset) : T1 :=
  match proj1 (proj1 x) with
  | Some e => e
  | None => False_rect _ (proj2 x)
  end.

(* 过滤出所有属于T1_subset的元素 *)
Definition filter_T1 (seq : nat -> T_Union) : nat -> option T1_subset :=
  fun n => match proj1 (seq n) with
         | Some _ => Some (exist _ (seq n) _)
         | None => None
         end.

针对示例的具体实现 #

以字符串长度过滤为例，假设T_Union为字符串类型，proj1用于识别并返回偶数长度的字符串，实现如下：

(* 判断字符串长度是否为偶数 *)
Definition is_even_len (s : string) : bool :=
  even (length s).

(* 投影函数：仅返回偶数长度的字符串 *)
Definition proj1 (s : string) : option string :=
  if is_even_len s then Some s else None.

(* 过滤原序列，提取偶数长度字符串 *)
Definition filter_even_seq (seq : nat -> string) : list string :=
  let rec aux n acc :=
    match n with
    | 4 => rev acc (* 假设原序列到索引3为止 *)
    | _ => match proj1 (seq n) with
           | Some s => aux (S n) (s :: acc)
           | None => aux (S n) acc
           end
    end in
  aux 0 nil.

(* 测试场景：原seq 0→"a",1→"aa",2→"aaa",3→"aaaa"，filter_even_seq会返回["aa";"aaaa"] *)

内容的提问来源于stack exchange，提问作者Bas Laarakker