如何在 Coq 的假设中实例化 forall 的变量？
How to instantiate a variable of forall in a hypothesis in Coq?
我有两个假设
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 道具，除非它可以通过统一在上下文中计算出来。
以下是应该起作用的东西：
(* 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 您可以使用，但是根据您的 implicit/inferred 是什么，我很难告诉您它是哪个。
我有两个假设
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 道具，除非它可以通过统一在上下文中计算出来。
以下是应该起作用的东西：
(* 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 您可以使用，但是根据您的 implicit/inferred 是什么，我很难告诉您它是哪个。