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