Почему левая идентичность над «добавлением» является тривиальным доказательством, но правильной идентичности нет?

Question

Я просто изучаю Агда, но я не понимаю, что когда я пытаюсь доказать Идентичность над добавлением, я вижу, что Левая Идентичность является тривиальным доказательством.

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) 

Не могу понять причину. Пожалуйста, объясни. Благодарю.

Answer 1

Проблема в том, как зависимые типизированные теории имеют дело с равенством. Обычно определение добавления:

_+_ : Nat -> Nat -> Nat 
zero + m = m    -- (1) 
(suc n) + m = suc (n + m) -- (2) 

Обратите внимание, что уравнение 1 подразумевает левую идентификацию. Когда у вас есть:

forall n -> 0 + n = n 

Контроллер типа Agda может использовать уравнение (1) для подтверждения того, что это равенство. Помните, что конструктор пропозициональная равенства (refl) имеет тип

refl : x == x 

Таким образом, при использовании refl в качестве доказательства для левой идентичности, Agda будет пытаться свести обе части равенства (нормализуют их), и если они проверяют действительно равны. Используя определение сложения, левое тождество немедленно, по уравнению (1).

Но для правильного удостоверения это не выполняется по определению. Обратите внимание, что, когда мы имеем

n + 0 == n 

типа проверки Agda не могут использовать сложение уравнений для того, чтобы проверить, что это равенство действительно имеет место. Единственный способ доказать это равенство - использовать индукцию (или, если хотите, рекурсию).

Надеюсь, что это может вам помочь.