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

Question

我有两个假设

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.

我应该使用哪种策略来实例化假设中的变量？

Answer 1

你的假设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类型的两个构造函数之一.

现在您可能必须明确传递BProp,除非可以通过统一在上下文中找出它.

以下是应该工作的事情:

(* 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你可以使用,但是根据你隐含/推断的内容,我很难告诉你它是哪一个.