Что означает Ошибка: несогласованность Вселенной в Coq?

В Coq у всего есть тип. Type не является исключением: если вы спросите Coq с командой Check, он скажет вам, что его тип ... Type!

На самом деле это немного неправда. Если вы запросите более подробную информацию, выполнив директиву Set Printing Universes., Coq сообщит вам, что этот Type не такой же, как первый, а более крупный. Формально с каждым Type связан индекс, называемый его уровнем юниверса. Этот индекс обычно не отображается при печати выражений. Таким образом, правильный ответ на этот вопрос состоит в том, что Type_i имеет тип Type_j для любого индекса j > i. Это необходимо для обеспечения непротиворечивости теории Кока: если бы был только один Type, можно было бы показать противоречие, подобно тому, как можно получить противоречие в теории множеств, если предположить, что существует множество всех множеств.

Чтобы упростить работу с индексами типов, Coq дает вам некоторую гибкость: на самом деле ни один тип не имеет связанного с ним фиксированного индекса. Вместо этого Coq генерирует одну новую индексную переменную каждый раз, когда вы пишете Type, и отслеживает внутренние ограничения, чтобы гарантировать, что они могут быть созданы с конкретными значениями, которые удовлетворяют ограничениям, требуемым теорией.

Сообщение об ошибке, которое вы видели, означает, что решатель ограничений Coq для уровней юниверса говорит, что не может быть решения для системы ограничений, которую вы просили. Проблема в том, что forall в определении nat количественно превышает Type_i, но логика Coq заставляет nat быть самим собой типа Type_j с j > i. С другой стороны, приложение n nat требует этого j <= i, что приводит к невыполнимому набору ограничений индекса.