Coq: working with inequalities (<>)

I'm trying to understand the logic about working with inequalities in Coq.

When <> is present in the goal, doing intros contra. changes the goal to False and moves the goal to an hypothesis but with <> switched to =. I think I understand how it is sound. If I have as goal a <> b, then a = b as hypothesis would generate a contradiction.

However, I can't do the opposite in Coq. If I have as goal a = b, I can't intros contra. in order to have False as goal and a <> b as hypothesis. Would this intros be logically sound? Is it not supported just because it is never needed to complete a proof?
When <> is in an hypothesis H, doing destruct H. will remove the hypothesis (I can't do destruct (H) eqn:H.) and it will switch any goal to the same that H but with <> switched for =. I don't understand the logic here. If I have an hypothesis which is an inequality, I don't see how not having it is the same as having the equality as goal.

How an inequality is inductive to be used by destruct?

If I have a contradictory hypothesis G 0 <> 0, in order to complete the proof and tell it is a contradiction, I need to do destruct G. (* now the goal is 0 = 0 *). reflexivity. Why is it not possible to just do something like inversion G., as you would do with an hypothesis S n = 0?.

So I have, in fact, 4 related questions marked in bold.

Solution

Would this intros [on a goal a = b] be logically sound?

If I understand your question, you want to know if it would be possible to have a goal a = b, call intros contra, and transform that into the goal H : a <> b |- False. This would be sound, but not derivable in Coq's basic constructive logic for a and b of arbitrary type: it asserts that the proposition a = b supports double-negation elimination (~ (~ a = b) -> a = b). Coq does not support this because it would mean working in a different logical formalism.

How an inequality is inductive to be used by destruct?

As yeputons remarked, a <> b is defined as a = b -> False, and falsity is inductively defined as the proposition with no constructors; thus, destructing something of type False simply completes the proof. Furthermore, calling destruct on something of type A -> B has roughly the effect of generating a goal of type A, feeding that proof into the implication to obtain a proof of B, and then calling destruct on that proof of B. In your case, this means doing exactly what you described.

Why is it not possible to just do something like inversion G., as you would do with an hypothesis S n = 0?

My guess is that inversion is not as lenient as destruct, and is not extended to work on implications as I explained above.