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

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

coq

MikkelBybjerg · 技术社区 · 6 年前

我有一个声明,两个lambda是相同的:

G : (fun s' : S => x = s') = (fun s' : S => y = s')

我想用这个来证明 x=y 。我的想法很简单,用 (fun s' : S => x = s') y 使用 G 要将一个lambda替换为另一个,请将 y=y 利润我的问题是在第一步中,我找不到任何方法来设置一个包含一个lambda应用程序的语句,而Coq不会立即将其缩减为 x=y 。我想让未申请的lambda“呆一会儿”,这样我就有机会申请了 G 。

这看起来应该很容易,只是想不出来。

2 回复 | 直到 6 年前

eponier 6 年前

的确 replace (x=y) with (fun s' : S => x = s') y 没有给出任何有用的结论,因为结论被简化了。但事实并非如此 change (x=y) with (fun s' : S => x = s') y 你可以在这里做你想做的事。

然而,最简单的方法可能是 pattern y 直接将结论转换为适当的形式。

Qinshi Wang 2 年前

我会使用 pose proof (equal_f G y) 获取 (x = y) = (y = y) 。 equal_f 来自 Coq.Logic.FunctionalExtensionality 。

equal_f : forall {A B : Type} {f g : A -> B}, f = g -> forall x : A, f x = g x

equal_f is not universe polymorphic
Arguments equal_f {A B}%type_scope {f g}%function_scope _ _
equal_f is opaque
Expands to: Constant Coq.Logic.FunctionalExtensionality.equal_f

推荐文章

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中导入它们

7 年前