coq - 如何在 Coq 的假设中实例化 forall 的变量？

我有两个假设

IHl: forall (lr : list nat) (d x : nat), d = x \/ In x l' -> (something else)
Head : d = x

我想在 apply IHl 上使用 Head，因为它满足 IHl 的 d = x \/ In x l。我尝试了 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/