我有两个假设
IHl: forall (lr : list nat) (d x : nat), d = x \/ In x l' -> (something else)
Head : d = x
我要
apply IHl
在 Head
因为它满足d = x \/ In x l
IHl。我试过 apply with
以简单提示失败的策略 Error: Unable to unify
.我应该使用哪种策略来实例化假设中的变量?
最佳答案
您的假设 IHl
接受 4 个参数:lr : list nat
, d : nat
, x : nat
, 和 _ : d = x \/ In x l'
.
您的假设 Head : d = x
没有正确的类型作为第四个参数传递。您需要将其从平等证明转变为析取证明。幸运的是,您可以使用:
or_introl
: forall A B : Prop, A -> A \/ B
这是
or
的两个构造函数之一类型。现在您可能必须明确传递
B
Prop,除非它可以通过统一在上下文中弄清楚。以下是应该起作用的事情:
(* To keep IHl but use its result, given lr : list nat *)
pose proof (IHl lr _ _ (or_introl Head)).
(* To transform IHl into its result, given lr : list nat *)
specialize (IHl lr _ _ (or_introl Head)).
可能有一个
apply
您可以使用,但取决于对您隐含/推断的内容,我很难告诉您它是哪一个。
关于coq - 如何在 Coq 的假设中实例化 forall 的变量?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/31515009/