如何在Coq中利用不等假设简化match模式的证明？

我定义了一个包含match的函数，示例如下：

Definition five (n: nat): bool :=
match n with
| 5 => true
| _ => false
end.

我尝试证明如下定理：

Theorem fiveT: forall (n: nat),
n <> 5 -> five n = false.
Proof. intros. unfold five.

展开five的定义后，我不知道如何让Coq知晓因假设H: n <> 5，match的第一个分支不成立。当前证明状态如下：

1 goal
n : nat
H : n <> 5
______________________________________(1/1)
match n with
| 5 => true
| _ => false
end = false

注：我的实际问题更为复杂，请勿提供与当前思路完全不同的方法，感谢理解！

解决方案 #

你可以对自然数n进行分情况讨论，在n=5的分支里利用假设H导出矛盾，Coq会自动完成该分支的证明；其他分支直接验证等式即可。

分步实现（直观版） #

Theorem fiveT: forall (n: nat),
n <> 5 -> five n = false.
Proof.
  intros n H. unfold five.
  (* 对n分情况拆解 *)
  destruct n as [|n] eqn:E.
  - (* n=0 *) reflexivity.
  - destruct n as [|n] eqn:E.
    - (* n=1 *) reflexivity.
    - destruct n as [|n] eqn:E.
      - (* n=2 *) reflexivity.
      - destruct n as [|n] eqn:E.
        - (* n=3 *) reflexivity.
        - destruct n as [|n] eqn:E.
          - (* n=4 *) reflexivity.
          - destruct n as [|n] eqn:E.
            - (* n=5 *) contradiction H. (* 利用H导出矛盾，自动闭合分支 *)
            - (* n>5 *) reflexivity.
Qed.

简洁写法 #

手动拆到5太繁琐，用case命令可以简化步骤：

Theorem fiveT: forall (n: nat),
n <> 5 -> five n = false.
Proof.
  intros n H. unfold five.
  case n; case n; case n; case n; case n.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - contradiction H.
  - reflexivity.
Qed.

核心思路（适配复杂场景） #

如果你的实际问题涉及更复杂的归纳类型，核心逻辑不变：

1. 对match语句中的变量执行分情况归纳（destruct/case）；
2. 在与否定假设冲突的分支，用contradiction或discriminate导出矛盾，Coq会自动处理该分支；
3. 其他分支通过reflexivity或对应等式规则完成证明。

内容的提问来源于stack exchange，提问作者Leo G.