Destruct hypothesis: general case

Question

That's pretty clear what destruct H does if H contains conjunction or disjunction. But I can't figure out what it does in general case. It does something bizarre, especially if H: a -> b.

Some examples:

Lemma demo : forall (x y: nat), x=4 -> x=4.
Proof.
  intros. destruct H.

The hypothesis is just destroyed:

1 subgoal
x, y : nat
______________________________________(1/1)
x = x

Another one:

Lemma demo : forall (x y: nat), (x = 4 -> x=4) -> True.
Proof.
  intros. destruct H.

Now I have two branches:

1 subgoal
x, y : nat
______________________________________(1/1)
x = 4

1 subgoal
x, y : nat
______________________________________(1/1)
True

Third example. It's not provable but it still doesn't make sense to me:

Lemma demo : forall (x y: nat), (x = 4 -> x = 4) -> x = 4.
Proof.
  intros. destruct H.

Now I have to prove x = x in the second branch!

2 subgoals
x, y : nat
______________________________________(1/2)
x = 4
______________________________________(2/2)
x = x

So, I clearly don't understand what destruct H does.

Answer 1

The cases you are referring to fall in two categories. If H : A and A is inductively or coinductively defined (e.g., conjunction and disjunction), then destruct H generates one subgoal for each constructor in that type, with additional hypotheses determined by the arguments of that constructor. On the other hand, if H : A -> B, then destruct H generates one subgoal where you have to prove A, and then continues recursively as if H : B. This is roughly equivalent to the following calls:

assert (H' : A); [ |specialize (H H'); destruct H].

The missing piece of the puzzle is that equality itself is defined as an inductive type:

Inductive eq (A : Type) (a : A) : A -> Prop :=
| eq_refl : eq A a a

When you destruct something of type x = 4, Coq generates one case for each constructor of that type. But there is only one constructor in that type: eq_refl. When considering that case, Coq also automatically replaces occurrences of the RHS of destructed equality by the LHS (since both sides are equal for that constructor). In your first and third examples, this leads to replacing 4 in the goal with x.

Most of the time, you do not want to destruct an equality hypothesis, since this replacement behavior is not very useful. It is usually better to use the rewrite tactic, since it allows you to rewrite from rightto-left or left-to-right.