代码之家 › 专栏 › 技术社区 › Jeremy Salwen

将具体假设应用于存在目标的Coq策略

ltac coq

Jeremy Salwen · 技术社区 · 7 年前

考虑下面的例子:

Theorem example: forall (P: nat->Prop), P (1+2+3) -> (exists x, P x).
Proof.
intros. 
apply H

apply H

Unable to unify "P (1 + 2 + 3)" with "exists x : nat, P x".

所以我知道我可以用这个策略 exists 1+2+3 申请在这里工作,或者 this other stackoverflow question 有一种更复杂的方法来使用正向推理 H 把它变成存在的形式。

1 回复 | 直到 7 年前

Tej Chajed 7 年前

你不需要推理,你只需要评估:

Theorem example: forall (P: nat->Prop), P (1+2+3) -> (exists x, P x).
Proof.
intros.
eexists.
apply H.

推荐文章

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

8 年前

Jason Hu · 参见Ltac中的Hintbase

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前