Почему Coq не допускает инверсии, разрушения и т. д. когда цель-это тип?

Когда refineразрабатывал программу, я пытался закончить доказательство inversion на гипотезе False, Когда целью было Type. Вот сокращенная версия доказательства, которое я пытался сделать.

Lemma strange1: forall T:Type, 0>0 -> T.
  intros T H.
  inversion H.  (* Coq refuses inversion on 'H : 0 > 0' *)

Кок пожаловался 

Error: Inversion would require case analysis on sort 
Type which is not allowed for inductive definition le

Однако, поскольку я ничего не делаю с T, это не должно иметь значения, ... или ...

Я избавился от T Вот так, и доказательство прошло: 

Lemma ex_falso: forall T:Type, False -> T.
  inversion 1.
Qed.  

Lemma strange2: forall T:Type, 0>0 -> T.
  intros T H.
  apply ex_falso.  (* this changes the goal to 'False' *)
  inversion H.
Qed.

По какой причине Кок жаловался? Это просто недостаток inversion, destruct, и т. д. ?

1 6
coq proof

1 ответ:

Я никогда не видел эту проблему раньше, но это имеет смысл, хотя можно, вероятно, утверждать, что это ошибка в inversion.

Эта задача обусловлена тем, что inversion реализуется методом case analysis. В логике Coq нельзя Вообще проводить анализ случая на логической гипотезе (т. е. что-то, чей тип является Prop), если результат является чем-то вычислительным (т. е. если тип возвращаемой вещи является Type). Одна причина дело в том, что разработчики Coq хотели сделать возможным удаление аргументов доказательства из программ при извлечении их в код разумным способом: таким образом, можно только сделать анализ случая на гипотезе, чтобы произвести что-то вычислительное, если разрушаемая вещь не может изменить результат. Это включает в себя:

    Предложения без конструкторов, такие как False.
  1. предложения только с одним конструктором, если этот конструктор не принимает аргументов вычислительного характера. Это включает в себя True, Acc (предикат доступности, используемый для выполнения хорошо обоснованной рекурсии), но исключает экзистенциальный Квантор ex.
Однако, как вы заметили, можно обойти это правило, преобразовав некоторое предложение, которое вы хотите использовать для получения вашего результата, в другое, которое вы можете непосредственно проанализировать. Таким образом, если у вас есть противоречивое предположение, как в вашем случае, вы можете сначала использовать его для доказательства False (что допускается, так как False является Prop), и , то устраняя False, чтобы получить свой результат (что разрешено вышеприведенными правилами).

В вашем примере inversion слишком консервативен, отказываясь только потому, что он не может выполнить анализ случая на что-то типа 0 < 0 в этом контексте. Это правда, что он не может сделать анализ случая на нем непосредственно по правилам логики, как объяснено выше; однако можно было бы подумать о создании немного более умной реализации inversion, которая признает, что мы устранение противоречивой гипотезы и добавление False в качестве промежуточного шага, как и вы. К сожалению, кажется, что мы должны сделать этот трюк вручную, чтобы заставить его работать.

7