Coq repeating "destruct" for disjunctive hypothesis causing unwanted destruction in the end

Question

I need to prove a theorem involving 2 variables a and b, a hypothesis H specifying the possible values of a (a = v1 \/ a = v2 \/ ... \/ a = vn), and a hypothesis H0 specifying values of b (b = v1' \/ b = v2' \/ ... \/ b = vn'), and a hypothesis that a and b are not equal. I can't use repeat (destruct H0; xxx) because it would destruct the hypothesis H0: b = vn', and make the proof impossible to continue. Is there a way to do "repeat" only finite number of times? Or what are some other ways to solve the problem that I currently have?

My proof currently looks like this (xxx is a tactic I defined myself):

intros. subst.
destruct H.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
xxx.

destruct H.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
xxx.
...(just repeat the above)

Answer 1

It is best to include a minimal working example with your question. I tried to reconstruct your question as best I could, but without a full example, I had to guess in some places.

The following seems to work:

From Coq Require Import Utf8.
Parameter A : Type.
Parameter v1 v2 v3 v4 v5 v6 v7 v8 v1' v2' v3' v4' v5' v6' v7' v8' : A.

Goal ∀ a b : A, (a = v1 ∨ a = v2 ∨ a = v3 ∨ a = v4 ∨
                   a = v5 ∨ a = v6 ∨ a = v7 ∨ a = v8) →
                (b = v1' ∨ b = v2' ∨ b = v3' ∨ b = v4' ∨
                   b = v5' ∨ b = v6' ∨ b = v7' ∨ b = v8') → False.
Proof.
  intros a b H H0.
  (repeat destruct H as [ | ]); (repeat destruct H0 as [ | ]).

Answer 2

I am not sure it is a matter of number of times because an hypothesis of the form A \/ B \/ C has a tree structure where all branches do not have the same length.

You want to destruct only goals where the hypothesis has the shape of an disjunction, and keep the name of H0 for the next branch that is likely to be a disjunction.

There is a theorem for that: or_ind.

repeat (apply or_ind in H0; clear H0;[intros H0 | intros]).

should do the trick (I did not have time to test it, though).

Answer 3

Is there a way to do "repeat" only finite number of times?

Yes, it's called do. For example, do 3 (destruct H0; xxx) repeats destruct H0; xxx three times.

I'm not sure this solves your problem though, see the other answers.