Search code examples
coq

Splitting disjunctions (\/) in Coq hypothesis

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!

Solution

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