Использование разрушения вместо инверсии

Question

Я понимаю принцип взрывозащищенности, используя тактику inversion:

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

Однако я не понимаю шагов, предпринятых Coq для того же доказательства, но с использованием destructвместо inversion:

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

Как разрушить индуктивную False?Как это влияет на цель и завершить доказательство?

Answer 1

False - это пустой индуктивный тип данных, т. Е. Он не имеет возможных значений, см. здесь .True - это индуктивный тип данных с одним значением I

Когда мы destruct значение X индуктивного типа данных, мы заменяем текущую цель несколькими подцелями, по одному на каждое возможное значениеX.Когда мы уничтожаем False, мы получаем нулевые подцели для доказательства (поскольку оно имеет нулевые значения), поэтому доказательство завершено.

В основном destruct и inversion делают более или менее одно и то жездесь.