Этот вопрос может показаться очень глупым, но я не могу доказать, что единственное натуральное число меньше 1 - 0. Я использую библиотеку mathcomp finType, и цель, которую я хочу доказать:
Lemma ord0_eq1 (a : ordinal 1) : a = ord0.
Проблема в том, что если я уничтожу a
и ord0
, я получу следующую цель:
∀ (m : nat) (i : (m < 1)%N), Ordinal i = Ordinal (ltn0Sn 0)
Теперь я могу использовать case
и получить абсурд, если m не равно 0. Но если m равно 0, я получаю:
∀ i : (0 < 1)%N, Ordinal i = Ordinal (ltn0Sn 0)
И единственный способ доказать это равенство - доказать, что forall i : 0 < 1, i = (ltn0Sn 0)
. Но я не знаю, как доказать равенство между двумя доказательствами одного и того же Prop
без использования ненужных доказательств, и я не хочу добавлять аксиому в мою теорию. Должен быть какой-то способ использовать возможности отражения Ssreflect для решения этой цели, но я ничего не нашел: я могу добраться до точки, где мне нужно доказать равенство между двумя доказательствами равенства, и я мог бы использовать UIP (уникальность доказательства личности), но это еще одна аксиома, и я не хочу ее использовать.
Я не могу поверить, что мне нужно добавить аксиому, чтобы доказать эту цель: отношение меньше чем может быть определено только вычислением. Должен быть способ доказать, что forall (m n : nat) (a b : m < n), a = b
без UIP или доказательства несоответствия.
Спасибо
EDIT : я использую библиотеку ssrnat
mathcomp, а не Coq * Модуль 1025 *. Запись "<"
связана с ltn
от ssrnat, а не lt
от Arith.