在 Coq 假设中拆分析取 (\/)

Question

我试图在 Coq 中证明一个简单的引理，其中 假设是析取。我知道如何在目标中出现split析取， 但是当它们出现在假设中时无法将它们分开。这是我的例子：

Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
  ((n < 5) \/ (n > 8)) -> ((n > 7) \/ (n < 6)).
Proof.
  intros n H1.
  split H1. (** this doesn't work ... *)

这是 Coq 所说的：

1 subgoal
n : nat
H1 : n < 5 \/ n > 8
______________________________________(1/1)
n > 7 \/ n < 6

有错误：

Error: Illegal tactic application.

我显然错过了一些简单的东西。 非常感谢任何帮助，谢谢！

Answer 1

你想要的策略是destruct。

Theorem splitting_disjunctions_in_hypotheses : forall (n : nat),
  ((n < 5) \/ (n > 8)) -> ((n > 7) \/ (n < 6)).
Proof.
  intros n H1.
  destruct H1.

如果你想命名得到的假设，你可以destruct H1 as [name1 | name2].。