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

Posted 2023-03-28

【中文标题】在 Coq 假设中拆分析取 (\\/)

【英文标题】：Splitting disjunctions (\/) in Coq hypothesis在 Coq 假设中拆分析取 (\/)

【发布时间】：2019-03-24 06:38:31

【问题描述】：

我试图在 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.

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

【参考方案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].。