Search code examples
coqprooftheorem-provingcoq-tactic

Using destruct instead of inversion

I understand the principle of explosion proof using the inversion tactic:

Theorem ex_falso_quodlibet : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  inversion contra.  Qed.

However, I don't understand the steps taken by Coq in order to do the same proof but using destruct instead of inversion:

Theorem ex_falso_quodlibet' : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  destruct contra.  Qed.

How is False inductive to be destructed? How does it affect to the goal and complete the proof?

Solution

  • False is an empty inductive data type, i.e. it has no possible values, see here. True is an inductive data type with a single value I

    When we destruct a value X of inductive data type we replace the current goal with multiple subgoals, one per each possible value of X. When we destruct False, we end up with zero subgoals to prove (as it has zero values), therefore proof is completed.

    Basically, destruct and inversion do more or less the same thing here.