如何解决如何在 Coq 中专门化嵌套假设?
我已经有了 Coq 中 specialize
的想法。
它与 specialize (H1 trm_int).
H1 : forall x,value x -> term x.
但是这个案子呢
H1 : forall x,value x -> forall y,value y -> sub x y.
它不适用于 specialize (H1 trm_int _trm_int)
。
编辑:
specialize (H1 trm_int _trm_int)
适用于
H1 : forall x y,value x -> value y -> sub x y.
注意 forall y
出现在第二个前提中。
解决方法
我不确定我是否理解您的问题。
specialize
会将您的假设应用于您给出的论点。它不限于 forall
量词。
说你有
h : nat -> bool
你也可以使用specialize (h 0)
,你会得到
h : bool
所以当你有
H1 : forall x,value x -> forall y,value y -> sub x y.
如果你专精,你必须使用 specialize (H1 some_x some_value_x some_y)
其中 some_x
是 x
的实例,some_value_x
是 value some_x
的证明,some_y
是 y
的实例。
请注意,还有一种使用 with
的替代方法,可以让您专门使用名称。请考虑以下示例
Lemma foo :
forall (h : forall x,x = 0 -> forall y,y = x -> x = y),True.
Proof.
intro h.
specialize h with (x := 0) (y := 0).
在这里你会结束
h: 0 = 0 -> 0 = 0 -> 0 = 0
但是你也可以直接用
specialize (h 0 eq_refl 0).
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。