coq - 在 Coq 中将临时列表转换为依赖类型列表
问题描述
我在 Coq 中有以下列表定义:
Variable A : Set.
Variable P : A -> Prop.
Hypothesis P_dec : forall x, {P x}+{~(P x)}.
Inductive plist : nat -> Set :=
pnil : plist O
| pcons : A -> forall n, plist n -> plist n
| pconsp : forall (a:A) n, plist n -> P a -> plist (S n)
.
A
它描述了“其中至少n
满足谓词的类型元素列表P
”。
我的任务是创建将临时列表转换为plist
(尽可能n
)的函数。我的尝试是首先计算所有匹配P
的元素,然后根据结果设置输出类型:
Fixpoint pcount (l : list A) : nat :=
match l with
| nil => O
| h::t => if P_dec h then S(pcount t) else pcount t
end.
Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
match l with
| nil => pnil
| h::t => match P_dec h with
| left proof => pconsp h _ (plistIn t) proof
| right _ => pcons h _ (plistIn t)
end
end.
但是,我收到一条错误消息left proof
:
Error:
In environment
A : Set
P : A -> Prop
P_dec : forall x : A, {P x} + {~ P x}
plistIn : forall l : list A, plist (pcount l)
l : list A
h : A
t : list A
proof : P h
The term "pconsp h (pcount t) (plistIn t) proof" has type
"plist (S (pcount t))" while it is expected to have type
"plist (pcount (h :: t))".
问题是 Coq 看不到那S (pcount t)
等于pcount (h :: t)
知道P h
,这已经被证明了。我不能让 Coq 知道这个真相。
如何正确定义这个函数?甚至有可能这样做吗?
解决方案
您可以使用依赖模式匹配,因为结果类型plist (pcount (h :: t))
取决于P_dec h
isleft
或right
.
下面,关键字as
引入了一个新变量p
,并return
告诉了整个match
表达式的类型,由 参数化p
。
Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
match l with
| nil => pnil
| h::t => match P_dec h as p return plist (if p then _ else _) with
| left proof => pconsp h (pcount t) (plistIn t) proof
| right _ => pcons h _ (plistIn t)
end
end.
替换时类型plist (if p then _ else _)
必须等于。然后在每个分支中,比如说,你需要产生(减少到左分支)。plist (pcount (h :: t))
p := P_dec h
left proof
plist (if left proof then _ else _)
Coq 可以在这里推断下划线中的内容有点神奇,但为了安全起见,您始终可以将其拼写出来:(if p then S (pcount t) else pcount t
这意味着与 的定义完全匹配pcount
)。
推荐阅读
- mysql - 如何使用对同一数据库表的查询结果更新 MYSQL 表中的字段?
- node.js - Mongoose `Promise.all()` 事务错误
- javascript - 如何从 JavaScript 中的两个二维数组中获取唯一值
- django - Django importError(无法导入名称“六”)
- javascript - 如何在不改变原始数组的情况下将数组传递给函数?
- android - Xamarin Android 如何正确声明 Intent Filter 以匹配自定义文件类型?
- javascript - Gulp 不是 comile sass 文件并重新加载页面
- mariadb - MySQL Workbench 无法转发工程,错误 1064
- c++ - preLaunch 'C/C++:gcc.exe build active file' 以退出代码 -1 终止
- android - `clearPackageData` 删除生成 JaCoCo 报告所需的文件(.exec 和 .ec):Android