应用策略有效，但目标和假设中的变量不同

Question

使用 IndProp 的 leb_complete 定理，我发现了以下奇怪之处：

Theorem leb_complete : forall n m,
  n <=? m = true -> n <= m.
Proof.
  induction n as [|n'].
  - intros. apply O_le_n.
  - induction m as [| m'] eqn:Em.
    + intros H. discriminate H.
    + intros H. apply n_le_m__Sn_le_Sm.

它产生以下内容：

1 subgoal (ID 155)

n' : nat
IHn' : forall m : nat, (n' <=? m) = true -> n' <= m
m, m' : nat
Em : m = S m'
IHm' : m = m' -> (S n' <=? m') = true -> S n' <= m'
H : (S n' <=? S m') = true
============================
n' <= m'

一切都很好。现在，当我运行 apply IHn'. 它工作并产生以下内容时：

(n' <=? m') = true

为什么有效？在 IHn' 我们有

n' <= m - in IHn'
n' <= m' - in the goal

变量m和m'不一样，但还是可以的。当我尝试

`rewrite -> Em in IHn'.

报错：

Found no subterm matching "m" in IHn'.

但是IHn'里面有变量"m"！我很困惑，请解释这里发生了什么。

Answer 1

IHn'中的m只是一个虚拟变量。 IHn' 量化所有自然数：forall m : nat, [...]。特别地，m' 是一个 nat，因此假设适用 m 替换为 m'。

IHn' 中的 m 与您上下文中的不同（特别是与 Em : m = S m' 中的 m 不同）。他们只是碰巧有相同的名字。

应用策略有效，但目标和假设中的变量不同

apply tactics works, but the variables in goal and hypothesis are different

coq

logical-foundations