使用依赖类型减少参数

Question

在处理非依赖类型时，Coq（通常）会推断出哪个参数在固定点中递减。但是，依赖类型并非如此。

例如，考虑以下示例，其中我有一个类型 A_list，它确保属性 P 对列表中的所有元素（类型 A）都成立：

Require Import Coq.Lists.List.

Variable A: Type.
Variable P: A -> Prop.

Definition A_list := {a: list A | Forall P a}.

现在，假设我想让一个固定点递归地处理这样一个列表（这两个引理在这里并不有趣。dummy_arg 用于模拟处理多个参数。）：

Lemma Forall_tl: forall P (h: A) t, Forall P (h::t) -> Forall P t.
Admitted.
Lemma aux: forall (l1: list A) l2 P, l1 = l2 -> Forall P l1 -> Forall P l2.
Admitted.

Fixpoint my_fixpoint (l: A_list) (dummy_arg: A) :=
match (proj1_sig l) as x return proj1_sig l = x -> bool with
| nil => fun _ => true
| hd::tl =>
    fun h =>
      my_fixpoint (exist (Forall P) tl (Forall_tl P hd tl (aux _ _ _ h (proj2_sig l)))) dummy_arg
end eq_refl.

正如预期的那样，返回错误“无法猜测修复的递减参数”。因为，严格来说，我们并没有减少论点。尽管如此，我们明显减少了proj1_sig l（嵌入在sig 中的列表）。

这可能可以使用Program Fixpoints 解决，但由于在依赖类型的投影上减少一定是一种非常常见的模式，我想知道管理此类情况的“正确”方法是什么。

Answer 1

您可以使用我在this answer 中提到的一种方法来解决这个问题，包括Program。 如果您将列表和证明解耦，则可以使用普通递归来完成：

Fixpoint my_fixpoint (l: list A) (pf : Forall P l) (dummy_arg: A) : bool :=
match l as x return Forall P x -> bool with
| nil => fun _ => true
| hd::tl => fun h => my_fixpoint tl (Forall_tl P hd tl h) dummy_arg
end pf.