在 Coq 中归纳其他基本案例
Induction with other base case in Coq
我正在尝试证明 Coq 中的鸽巢问题。因此，我有以下要证明的引理：
Lemma pigeon_hole :
forall m n, m < n ->
forall f, (forall i, i < n -> f i < m) ->
exists i, i < n /\
exists j, j < n /\ i <> j /\ f i = f j.
我从老师那里得到提示，自动证明自然数之间的等式和不等式的一种有用策略是
omega.
但我怀疑这在这里是否相关。
我认为可以像 https://math.stackexchange.com/questions/910741/constructive-proof-of-pigeonhole-principle 那样用归纳法来完成。
如果我尝试对 n 进行归纳，我会得到 n=0 的基本情况。这里我先做'intros.'然后'induction n.'.
但我想要基本情况 n=2。 Coq 是否有可能做到这一点，还是我走错了路？
您链接到的问题的答案包含这条副手评论：
The case n=1 is impossible
这对人类数学家来说已经足够好了，但对 Coq 来说就不行了。你可以告诉 Coq 你只想证明 n >= 2 的情况，方法是将它添加到引理的前提中：
Lemma pigeon_hole :
forall m n,
n >= 2 -> (* added this *)
m < n ->
forall f,
(forall i, i < n -> f i < m) ->
exists i, i < n /\
exists j, j < n /\ i <> j /\ f i = f j.
现在这个说法应该是可以证明的了。要达到你的归纳从 n = 2 开始的状态，你可以在纸上这样争论：
按第 n 个案例
- n = 0: 前提条件 n >= 2 不可能。
- n = 1: 前提条件 n >= 2 不可能。
- n >= 2: 通过归纳...
你可以在 Coq 中使用 destruct on n 两次来做同样的事情：
Proof.
intros.
destruct n.
我们区分了 n = 0 和 n >= 0（即 n = S n' 对于某些 n'）。我们处于证明状态：
H : 0 >= 2
这个错误假设正是omega可以为你排泄的那种东西：
- omega.
在另一种情况下，我们知道 n >= 1。这更接近 n >= 2，但仍然不够，因此我们可以再次对 n 进行大小写区分，以摆脱 n = 1 的情况：
- destruct n.
+ omega.
+
证明状态现在是：
1 subgoal
m, n : nat
H : S (S n) >= 2
H0 : m < S (S n)
f : nat -> nat
H1 : forall i : nat, i < S (S n) -> f i < m
______________________________________(1/1)
exists i : nat,
i < S (S n) /\ (exists j : nat, j < S (S n) /\ i <> j /\ f i = f j)
因此 n 的所有原始用途已被 S (S n) 取代，即 >= 2 的值。
您应该可以使用 induction n 从此处继续。
基础是n = 0，但是你可以去掉这个。然后你有一个归纳案例，你在每个地方查看带有 S n 的公式。如果你做destruct n as [ | n]，那么有两种情况，第一种是针对1，并且可能再次摆脱那个，然后如果再次做destruct n as [ | n]，你将不得不采取处理案件 2。所以这将扮演你的基本案例的角色。现在，剩下的情况将是大致相同的公式，但是初始 n 被 S (S (S n)) 替换并且归纳假设是关于公式已经对 S (S n) 成立的。这将为您提供从基本案例 n = 2.
开始的归纳证明
但是 n = 0 和 n = 1 的说法仍然正确，你需要证明这些情况。
第二种可能性（适用于较高常数的基本情况）
或者，您可以通过证明 n 为 0 是不可能的来得到基本情况，然后在查看归纳情况时，您可以通过
开始证明
destruct (le_lt_dec 2 n).
这会给你两种情况：一种是 2 <= n，你必须证明 S n 的 属性，另一种是 n < 2。对于后者，你应该知道这是不可能的（我没有检查你是否应该将 2 或 1 作为测试边界）。
我正在尝试证明 Coq 中的鸽巢问题。因此，我有以下要证明的引理：
Lemma pigeon_hole :
forall m n, m < n ->
forall f, (forall i, i < n -> f i < m) ->
exists i, i < n /\
exists j, j < n /\ i <> j /\ f i = f j.
我从老师那里得到提示，自动证明自然数之间的等式和不等式的一种有用策略是
omega.
但我怀疑这在这里是否相关。
我认为可以像 https://math.stackexchange.com/questions/910741/constructive-proof-of-pigeonhole-principle 那样用归纳法来完成。
如果我尝试对 n 进行归纳，我会得到 n=0 的基本情况。这里我先做'intros.'然后'induction n.'.
但我想要基本情况 n=2。 Coq 是否有可能做到这一点，还是我走错了路？
您链接到的问题的答案包含这条副手评论：
The case n=1 is impossible
这对人类数学家来说已经足够好了，但对 Coq 来说就不行了。你可以告诉 Coq 你只想证明 n >= 2 的情况，方法是将它添加到引理的前提中：
Lemma pigeon_hole :
forall m n,
n >= 2 -> (* added this *)
m < n ->
forall f,
(forall i, i < n -> f i < m) ->
exists i, i < n /\
exists j, j < n /\ i <> j /\ f i = f j.
现在这个说法应该是可以证明的了。要达到你的归纳从 n = 2 开始的状态，你可以在纸上这样争论：
按第 n 个案例
- n = 0: 前提条件 n >= 2 不可能。
- n = 1: 前提条件 n >= 2 不可能。
- n >= 2: 通过归纳...
你可以在 Coq 中使用 destruct on n 两次来做同样的事情：
Proof.
intros.
destruct n.
我们区分了 n = 0 和 n >= 0（即 n = S n' 对于某些 n'）。我们处于证明状态：
H : 0 >= 2
这个错误假设正是omega可以为你排泄的那种东西：
- omega.
在另一种情况下，我们知道 n >= 1。这更接近 n >= 2，但仍然不够，因此我们可以再次对 n 进行大小写区分，以摆脱 n = 1 的情况：
- destruct n.
+ omega.
+
证明状态现在是：
1 subgoal
m, n : nat
H : S (S n) >= 2
H0 : m < S (S n)
f : nat -> nat
H1 : forall i : nat, i < S (S n) -> f i < m
______________________________________(1/1)
exists i : nat,
i < S (S n) /\ (exists j : nat, j < S (S n) /\ i <> j /\ f i = f j)
因此 n 的所有原始用途已被 S (S n) 取代，即 >= 2 的值。
您应该可以使用 induction n 从此处继续。
基础是n = 0，但是你可以去掉这个。然后你有一个归纳案例，你在每个地方查看带有 S n 的公式。如果你做destruct n as [ | n]，那么有两种情况，第一种是针对1，并且可能再次摆脱那个，然后如果再次做destruct n as [ | n]，你将不得不采取处理案件 2。所以这将扮演你的基本案例的角色。现在，剩下的情况将是大致相同的公式，但是初始 n 被 S (S (S n)) 替换并且归纳假设是关于公式已经对 S (S n) 成立的。这将为您提供从基本案例 n = 2.
但是 n = 0 和 n = 1 的说法仍然正确，你需要证明这些情况。
第二种可能性（适用于较高常数的基本情况）
或者，您可以通过证明 n 为 0 是不可能的来得到基本情况，然后在查看归纳情况时，您可以通过
开始证明destruct (le_lt_dec 2 n).
这会给你两种情况：一种是 2 <= n，你必须证明 S n 的 属性，另一种是 n < 2。对于后者，你应该知道这是不可能的（我没有检查你是否应该将 2 或 1 作为测试边界）。