代码之家 › 专栏 › 技术社区 › Bromind

使用依赖类型减少参数

termination dependent-type coq

Bromind · 技术社区 · 6 年前

当处理非依赖类型时,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}.

现在,假设我想要一个固定点递归地处理这样一个列表(这里的2个引理并不有趣)。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.

正如所料,它返回一个错误“无法猜测fix的递减参数”,因为严格地说,我们并没有递减参数。尽管如此,我们显然在减少 proj1_sig l (嵌入在 sig

这也许可以用 Program Fixpoint s、但是,由于减少依赖类型的投影肯定是一种非常常见的模式,我想知道管理这种情况的“正确”方法是什么。

1 回复 | 直到 6 年前

Anton Trunov 6 年前

你可以用我在 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.

推荐文章

Mei Zhang · 定义“依赖类型”模函子

6 年前

Jason Hu · 参见Ltac中的Hintbase

6 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

6 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

6 年前

user9335697 · 实例化参数以评估函数定义

6 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

6 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

6 年前

jmite · Coq:在校样脚本编写期间查看校样术语

6 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

6 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

6 年前