如何通过 apply 创建新的假设？

Question

当我运行下面的 Coq 脚本时（原始脚本的简化版）：

Inductive w (g: nat): nat -> Prop:=
 | z: w g 0.

Lemma x:
  forall (i j: nat), w i j -> (forall k: nat, k <= k).
Proof.
Admitted.

Lemma y:
  forall (m n: nat),
  w m n -> w m n.
Proof.
  intros m n H. 
  apply x in H.

我在最后一行收到以下错误消息：

错误：无法找到变量 k 的实例。

任何人都可以向我解释为什么会发生这种情况以及我必须做什么才能将

forall k: nat, k <= k

作为上下文中的新假设吗？

提前致谢， 马库斯。

Answer 1

由于你的引理

x

包含一个内部通用量化（最后的

forall k

部分）， Coq 无法猜测您要使用哪个自然数。通过将

x

应用于

H

，您只需提供

i

和

j

。您有两种解决方案：

1. 使用

   k

   语法手动提供相关

   apply x with (k := foo) in H

2. 要求 Coq 使用

   eapply

   tactic

   引入一个“元变量”（将其视为稍后将填充的类型化孔）

希望对您有帮助， V.

Answer 2

您可以使用

apply x in H

，而不是

pose proof (x _ _ H)

。这将为您提供您正在寻找的假设。

来自 Coq 战术手册，

apply term in ident

尝试匹配结论

ident

的类型针对非依赖

term

类型的前提下，从右到左尝试它们。

我认为这里要注意的关键点是

apply

仅适用于非依赖前提，而您希望它匹配的前提

i=j

是依赖的。然而，Coq 返回的特定错误消息令人困惑。