Pourquoi l'identité de gauche sur "Addition" est une preuve triviale, mais l'identité de droite ne l'est pas?

Question

Je suis en train d'apprendre l'Agda, mais je ne comprends pas que lorsque j'essaie de prouver l'Identité plutôt que l'Addition, je vois que l'Identité de gauche est une preuve triviale.

left+identity : ∀ n -> (zero + n) ≡ n 
left+identity n = refl 

Mais cela n'est pas vrai pour l'identité correcte.

right+identity : ∀ n -> (n + zero) ≡ n 
right+identity zero = refl 
right+identity (suc n) = cong suc (right+identity n) 

Je ne peux pas comprendre la raison. S'il vous plaît, expliquez. Merci.

Answer 1

Le problème est de savoir comment les théories typées dépendantes traitent l'égalité. Habituellement, la définition de l'addition est:

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

Notez que l'équation 1 implique l'identité gauche. Lorsque vous avez:

forall n -> 0 + n = n 

Le vérificateur de type d'Agda peut utiliser l'équation (1) d'addition pour vérifier que l'égalité est vraie. Rappelez-vous, le constructeur de l'égalité propositionnelle (refl) a le type

refl : x == x 

Ainsi, lorsque vous utilisez refl comme une preuve de l'identité de gauche, Agda va essayer de réduire les deux côtés de l'égalité (les normaliser) et vérifier si elles sont en effet égaux. En utilisant la définition de l'addition, l'identité de gauche est immédiate, par l'équation (1).

Mais pour la bonne identité, cela ne tient pas par définition. Notez que lorsque nous avons

n + 0 == n 

vérificateur de type de Agda ne peut pas utiliser des équations d'addition afin de vérifier que cette égalité en effet tenir. La seule façon de prouver cette égalité est d'utiliser l'induction (ou, si vous préférez, la récursivité).

Espérons que cela peut vous aider.