Я только изучаю Агду, но я не понимаю, что, когда я пытаюсь доказать Тождество над Сложением, я вижу, что Левое Тождество является тривиальным доказательством.
left+identity : ∀ n -> (zero + n) ≡ n
left+identity n = refl
Но это не верно для правильной идентичности.
right+identity : ∀ n -> (n + zero) ≡ n
right+identity zero = refl
right+identity (suc n) = cong suc (right+identity n)
Я не могу понять причину. Пожалуйста, объясни. Спасибо.
Проблема заключается в том, как зависимые типизированные теории работают с равенством. Обычно определение сложения выглядит так:
_+_ : Nat -> Nat -> Nat
zero + m = m -- (1)
(suc n) + m = suc (n + m) -- (2)
Обратите внимание, что уравнение один подразумевает левое тождество. Когда у тебя есть:
forall n -> 0 + n = n
Средство проверки типов Agda может использовать уравнение сложения (1) для проверки выполнения равенства. Помните, конструктор пропозиционального равенства (refl) имеет тип
refl : x == x
Итак, когда вы используете refl в качестве доказательства левого тождества, Agda попытается уменьшить обе стороны равенства (нормализовать их) и проверить, действительно ли они равны. Используя определение сложения, левое тождество является непосредственным по уравнению (1).
Но для правильного тождества это неверно по определению. Обратите внимание, что когда у нас есть
n + 0 == n
Средство проверки типов Agda не может использовать уравнения сложения для проверки того, что это равенство действительно выполняется. Единственный способ доказать это равенство — использовать индукцию (или, если хотите, рекурсию).
Надеюсь, что это может помочь вам.
