如何简化finset中类型强制转换的列表投影函数定义？

我通过finset库定义了如下类型my_list，用于表示自然数与通用类型U子集元素的配对列表：

Definition my_list {U : finType} (E : {set U}) : Type := 
  let P u := mem u E in
  list (nat * {x | P x}).

我需要实现一个投影函数，提取属于E1的元素并将其类型转换为nat * {x : U | mem x E1}。当前我通过Program Fixpoint结合引理in_E1_pair实现：

Context {U : finType}.
Variable E1 E2 : {set U}.

Lemma in_E1_pair (x : nat*{x : U | mem x (E1 :|: E2)}) :
  (val (snd x)) \in E1 = true -> nat*{x : U | mem x E1}.
Proof.
  ...
Defined.

Program Fixpoint proj1_set (m_list : my_list (E1 :|: E2))
  : my_list E1 :=
  match my_list with
  | [] => []
  | x :: tl => 
      match ((val (snd x)) \in E1) with
      | true => (in_E1_pair x _) :: proj1_set tl
      | _ => proj1_set tl
      end
  end

该实现虽能满足需求，但使用Program或护航模式导致后续证明中函数难以使用。请问是否有更简便的定义方式，既能保持目标返回类型，又能降低后续证明的复杂度？比如借助filter配合类型强制引理，或重新定义my_list类型。

方案一：基于现有类型，用filter+类型强制简化定义 #

核心思路是用纯函数式的类型转换配合filter_map，替代Program Fixpoint的护航模式，让函数定义更简洁，同时保留原类型约束。

1. 定义类型转换函数 #

先实现一个判断元素是否属于E1并转换类型的函数，直接返回option类型结果：

Context {U : finType}.
Variables E1 E2 : {set U}.

Definition convert_to_E1 (x : nat * {x | mem x (E1 :|: E2)}) : option (nat * {x | mem x E1}) :=
  let (n, xu) := x in
  if mem (val xu) E1 then
    Some (n, exist (fun u => mem u E1) (val xu) (mem (val xu) E1))
  else
    None.

2. 用filter_map实现投影函数 #

借助Coq标准库的filter_map函数（自动过滤None结果并收集Some中的值），直接完成投影：

Definition proj1_set (m_list : my_list (E1 :|: E2)) : my_list E1 :=
  filter_map convert_to_E1 m_list.

这个定义完全是纯函数式的，没有依赖任何证明项或Program机制。后续证明时，可以直接复用filter_map的已有引理（如filter_map_nil、filter_map_cons），大幅降低证明难度。

方案二：重新设计my_list类型 #

如果允许调整原类型定义，可以弱化静态类型约束，改用谓词描述列表元素的子集属性：

1. 简化my_list定义 #

Definition my_list {U : finType} : Type := list (nat * U).

2. 定义子集谓词 #

用谓词描述列表中所有元素都属于某个子集：

Definition my_list_subset {U : finType} (E : {set U}) (l : my_list) : Prop :=
  forall (n : nat) (u : U), (n, u) ∈ l -> mem u E = true.

3. 实现投影函数 #

此时投影函数可以直接用标准filter定义：

Definition proj1_set (l : my_list) : my_list :=
  filter (fun p => mem (snd p) E1) l.

后续证明只需维护my_list_subset的性质即可，无需处理子集类型的强制转换，定义和证明都会更简洁。

方案对比 #

• 方案一：保留原my_list的强类型约束，同时避免Program带来的证明复杂度，适合需要严格静态类型保证的场景。
• 方案二：通过弱化类型约束换取定义和证明的简洁性，适合对类型灵活性要求更高的场景。

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