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

Coq正向推理:应用多个假设

ltac coq

Jeremy Salwen · 技术社区 · 7 年前

我有两个假设,我想用正向推理来应用一个定理,这两个定理都用到了。

我的具体情况是我有假设

H0 : a + b = c + d
H1 : e + f = g + h

我想应用标准库中的定理:

f_equal2_mult
     : forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2

现在我知道我可以手动给出x1,y1,x2,y2的值,但是我希望Coq在与 H0 H1

eapply f_equal2_mult in H0; try exact H1.

但这感觉像一个黑客,打破了对称性和 try apply f_equals2_mult in H0, H1 或者类似的清晰。有这样的方法吗?

1 回复 | 直到 7 年前

Li-yao Xia 7 年前

你可以用 pose proof specialize 将其应用于其他假设。

Lemma f (a b c d : nat) : a = b -> c = d -> False.
intros H1 H2.
pose proof f_equal2_mult as pp.
specialize pp with (1 := H1).
specialize pp with (1 := H2).

(* or *)
specialize pp with (1 := H1) (2 := H2).

推荐文章

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 年前