coq - 如何在证明过程中将单个统一变量转化为目标
问题描述
我想以交互方式构造一个存在变量。我不能使用Grab Existential Variables,因为我需要在完成目标之前填充存在变量。
最小的例子 这是一个最小的例子(因为它很简单,它有其他解决方案,但它说明了我的问题)
Context (A:Type).
Parameter P Q: A -> Prop.
Definition filter: forall {a}, P a -> A:= fun a Pa=> a.
Lemma my_lemma:
forall a b, Q b -> (Q b -> P a) ->
exists a (H: P a), P (filter H).
Proof.
intros ?? H H0.
do 2 eexists.
在这一点上,有两个解决方案不能回答我的问题:(1)我可以运行 ( eauto
) 然后做Grab Existential Variables
,但假设 eauto 在我实例化统一变量之前不会成功;(2) 我可以用instantiate(1:= H0 H)
(或什至instantiate(1:= ltac:(eauto))
)明确地传递证明项,但假设存在性的证明是乏味的,我们希望以交互方式进行。
我们还能做什么?我们可以尝试使用cut
or assert
,像这样:
match goal with
|[|- P (filter ?x)] =>
match type of x with
| ?T => assert (HH:T) by eauto
end
end.
但是 HH 不在统一变量的上下文中,所以不能实例化。
instantiate(1:=HH). (* Instance is not well-typed in the environment of ?H. *)
据我所知,解决这个问题的唯一方法是使用Show Existentials
,查看变量的类型,手动复制它,将证明回滚到引入统一之前并在那里构造变量。在示例中,它看起来像这样:
Lemma my_lemma:
forall a b, Q b -> (Q b -> P a) ->
exists a (H: P a), P (filter H).
Proof.
intros ?? H H0.
do 2 eexists.
Show Existentials.
Restart. (* This command restores the proof editing process to the original goal. *)
intros ?? H H0.
assert (HH:P a) by eauto.
eexists; exists HH.
auto.
Qed.
显然,我想避免这种工作流程。那么,无论如何要将存在变量变成子目标?
解决方案
您最好的选择可能是首先避免将存在变量创建为 evar。您不必手动构造变量来执行此操作;如果你能确定它是在哪里创建的,你可以用 包裹这个有问题的策略unshelve t
,这会将所有创建的 evast
变成目标。如果相关策略深入某些自动化并且难以识别或更改,这可能会很困难。
推荐阅读
- linux - IGMP:主机拒绝来自 src“0.0.0.0”的 igmp 查询
- php - 无法使用准备好的语句从表中找到特定值
- asp.net - Office 365 仍然可以实现 Office 服务器端自动化?
- asp.net-core - razor 页面 - 全局 onGet onPost - .net 核心
- arrays - VBA 函数中的元素数组操作
- java - Android 资源链接失败。它拒绝建造
- python-3.x - 如果它不属于训练数据集,我该如何设置错误消息?
- vue.js - 运行“npm run build”需要什么?
- node.js - 如何查看 nodejs 中 readline 模块的源代码?
- python - Tensorflow Callback:如何将最佳模型保存在内存而不是磁盘上