proving not (iff a (not a)) with basic tactics

My experience proving contradictory things in Coq is very limited and I can't find an explicit way to prove the following theorem with basic tactics:

Theorem thrm : forall a, not (iff a (not a)).

I can prove it immediately with firstorder or intuition, but these tactics are like magic to me, my impression is that they involve some sophisticated automation. What would be a more explicit way to prove this theorem with simple explicit tactics such as rewrite, destruct, apply, assert?

Solution

In order to prove a negated proposition not something, one can use the intros tactic to add the expectedly-wrong assumption to the context and then prove that the context indeed is inconsistent. This is due to the fact not something is an abbreviation for something -> False. You can notice this by typing Print not. or during a proof, unfold not. to substitute the goal accordingly.

Then, to discharge the goal so obtained, several tactics may be used depending on the context, for example:

tactics intros, apply, exact and assumption for minimal propositional logic;
tactics such as destruct, inversion, discriminate or injection in the presence of inductive types;
etc., see the Coq reference manual

In your example, intros, destruct, apply and assumption are enough:

Theorem thrm : forall a, not (iff a (not a)).
Proof.
intros a Hiff; destruct Hiff as [H1 H2].
apply H1; apply H2; intros Ha; apply H1; assumption.
Qed.

Note that the proof can also be shortened to this equivalent version:

Theorem thrm : forall a, not (iff a (not a)).
Proof. now intros a [H1 H2]; apply H1; apply H2; intros Ha; apply H1. Qed.

where now something is a notation for something; easy (cf. the doc).

Hoping this helps