Coq：使用不动点和归纳法证明简单定理

Question

我现在正在学习使用 Coq，我偶然发现了一个我似乎无法证明的定理。下面是定理和我目前的尝试。

  Fixpoint nateq (n m : nat) : bool :=
    match n with
      | O => match m with
              | O => true
              | S _ => false
            end
      | S n' => match m with
                 | O => false
                 | S m' => nateq n' m'
                end
    end.

  Theorem nateq_is_eq : ∀ n m : nat, nateq n m = true → n = m.
  Proof.
     admit.
  Admitted.

我的尝试

  Theorem nateq_is_eq : ∀ n m : nat, nateq n m = true → n = m.
  Proof.
    intros n m H.
    induction n as [| n' IHn'].
    - induction m as [| m' IHm'].
      + reflexivity.
      + inversion H.
    - induction m as [| m' IHm'].
      + inversion H.
      + 
  Admitted.

我的问题在最后的归纳步骤。我的子目标的当前状态如下：

1 subgoal
n', m' : nat
H : nateq (S n') (S m') = true
IHn' : nateq n' (S m') = true → n' = S m'
IHm' : nateq (S n') m' = true → (nateq n' m' = true → n' = m') → S n' = m'
______________________________________(1/1)
S n' = S m'

这一切似乎有点令人费解。我真的很感激任何正确方向的建议。

Answer 1

您对 n' 的归纳假设不够普遍：要获得通过的证明，它需要适用于任意 m。 generalize dependent 策略可以用来解决这个问题：

Require Import Coq.Unicode.Utf8.

Fixpoint nateq (n m : nat) : bool :=
    match n with
      | O => match m with
              | O => true
              | S _ => false
            end
      | S n' => match m with
                 | O => false
                 | S m' => nateq n' m'
                end
    end.

Theorem nateq_is_eq : ∀ n m : nat, nateq n m = true → n = m.
Proof.
intros n m H.
generalize dependent m.
induction n as [|n IH].
- destruct m; easy.
- destruct m as [|m]; try easy.
  simpl. intros H. specialize (IH _ H). congruence.
Qed.

在这种情况下，只需在上下文中保留 m 即可完全避免该问题：

Theorem nateq_is_eq' : ∀ n m : nat, nateq n m = true → n = m.
Proof.
intros n. induction n as [|n IH].
- destruct m; easy.
- destruct m as [|m]; try easy.
  simpl. intros H. specialize (IH _ H). congruence.
Qed.

Software Foundations 书中对 generalize dependent 策略有更详细的解释。

Coq：使用不动点和归纳法证明简单定理

Coq: Proving simple theorem using Fixpoints and Induction

coq

proof

coq-tactic