Расщепление дизъюнкций (\ /) в гипотезе 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 ... *)

А вот что говорит Кок:

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]..