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

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

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

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

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

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