Splitting disjunctions (\/) in Coq hypothesis

Question

I'm trying to prove a simple lemma in Coq where the hypothesis is a disjunction. I know how to split disjunctions when they occur in the goal, but can't manage to split them when they appear in the hypothesis. Here is my example:

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 ... *)

And here is what Coq says:

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

With error:

Error: Illegal tactic application.

I'm clearly missing something simple. Any help is very much appreciated, thanks!

SCappella SCappella · Accepted Answer · 2019-03-24T07:30:05

The tactic you want is destruct.

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

If you want to name the resulting hypotheses you can do destruct H1 as [name1 | name2]..

Splitting disjunctions (\/) in Coq hypothesis

1 Answers