Coq: a vicious circle with two identical subgoals

Question

Sorry for overcomplicated example. I have

Lemma test : forall x y z : Prop,
 (
     (((x → (y ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
   ∧ (((y → (x ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
   ∧  ((y → (x ∨ z)) → (x ∨ (x → (y ∨ z))))
   ∧  ((x → (y ∨ z)) → (y ∨ (y → (x ∨ z))))
  )  → ((x → (y ∨ z)) → (y ∨ z)).

Doing

Proof.
  intros.
  destruct H.
  destruct H1.
  destruct H2.
  pose proof (H3 H0).

gives

1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y ∨ (y → x ∨ z)
______________________________________(1/1)
y ∨ z

I then do destruct H4. and this gives

2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y ∨ z
______________________________________(2/2)
y ∨ z

which I already don't understand: why two identical goals?? I then do left. and obtain

2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y
______________________________________(2/2)
y ∨ z

and then assumption. gives

1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y → x ∨ z
______________________________________(1/1)
y ∨ z

Then doing

pose proof (H3 H0).
destruct H5.
left.
assumption.

introduces two identical goals again, and brings me to

1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4, H5 : y → x ∨ z
______________________________________(1/1)
y ∨ z

which is identical to a previous state except that I now have two identical premises y → x ∨ z.

I am stuck. Obviously I am doing something wrong, but what?

Answer 1

This is not only an issue about tactics or understanding how Coq works: your goal is false, as the following demonstrates.

Lemma test : ~ forall x y z : Prop,
 (
     (((x -> (y \/ z)) -> (x \/ y)) <-> (x \/ y))
   /\ (((y -> (x \/ z)) -> (x \/ y)) <-> (x \/ y))
   /\  ((y -> (x \/ z)) -> (x \/ (x -> (y \/ z))))
   /\  ((x -> (y \/ z)) -> (y \/ (y -> (x \/ z))))
  )  -> ((x -> (y \/ z)) -> (y \/ z)).
Proof.
  intros H.
  specialize (H False False False).
  firstorder.
Qed.

In other words, if x, y and z are taken to be False, then all premises to your lemma are valid, but its conclusion does not.

[Edit: How I discovered this] I first tried the firstorder tactic (a decision procedure for such first-order goals) and found that it was not terminating, which got me suspicious. Then I turned to the corresponding goal boolean (using the ssreflect/ssrbool packages), where I could use case splits on x, y and z + computation to check whether the lemma held. Finding out that when the three of them were false the goal reduced to false, I had my counter-example, and then simply turned that back into a propositional counter-example.

Answer 2

Let us start with your first question. Actually, the two goals that were generated after destruct are not the same. Their conclusions are indeed both y \/ z, but their premises differ: the first one has H4 : y, while the second one has H4 : y -> x \/ z. More generally, if you have a goal of the form

(* ... *)
H : A \/ B
------------
 C

and you do destruct H as [H1 | H2]., you generate the subgoals

(* ... *)
H1 : A
-----------
  C

and

(* ... *)
H2 : B
------------
  C

with identical conclusions.

As for your second question, the issue is probably that you calling pose proof (H3 H0) twice. If you go through your script, you will notice that the hypotheses introduced by that tactic are the same on both calls: y \/ (y -> x \/ z). I suspect that you should have H2 H4 on the second call instead of H3 H0, though I haven't checked.

A final comment: you should letting Coq pick up the names of hypotheses for you, as this leads to unmaintainable proof scripts (see here). Whenever possible, you should use forms such as destruct H as [H1 | H2] instead of destruct H.