Difference between computation in proposition proof and definitional computation?

Question

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as definitional equality (at least in type theory).

But then if we consider $p$ in $p:Id_\mathbb{N}(a+b, b+a)$ as computation steps taking $a+b$ to $b+a$ then what is the difference between computation steps in $p$ and computation steps in above mentioned computational equality which prevents $p$ to be considered sort of a definitional equality? Are they of different computation level/form?

Or in other words, if I have got it correctly, what is the difference between $p$ in $p:Id_\mathbb{N}(a+b, b+a)$ and $p'$ in $p':Id_\mathbb{N}(s(s(0))+s(0), s(s(s(0)))) $ so that one can be considered almost the same thing as definitional equality but not the other one?

As an example following are the Agda codes in proving above mentioned reactions from Programming language foundations in Agda: Natural Numbers and [Programming language foundations in Agda: Proof by induction][3]correspondingly:

_ : 2 + 3 ≡ 5
  =
-
  begin
    2+3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    5
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

In my understanding both thing are computational steps that take you from left hand side to the right hand side!

Would you please answer it both intuitively and technically?

P.S. I found the following piece in Homotopy Type Theory(§1.1 p.22) which I thought might be the answer to part of my own question:

Whether or not two expressions are equal by definition is just a matter of expanding out the definitions; in particular, it is algorithmically decidable (though the algorithm is necessarily meta-theoretic, not internal to the theory).

I guess the above paragraph is talking about $\alpha$ and $\beta$ expansions. But if that is true then it raises the question that: What does a proof of a proposition has in addition to function application that makes it a different equality? Is it that beside application we do have function definitions as well in a proof definition?!

Answer 1

What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $a$ and $b$, it normalizes both of them (based on judgemental equalities, such as $\beta$-reduction) and compares the normalized values for syntactic equalities. There is a theorem which says that $a$ and $b$ are judgementally equal if, and only if, they have syntactically equal normal forms.

When judgemental equality has the property that things are equal preciely when they have syntactically equal normal forms, then people sometimes call it computational equality because it "computes" by computing normal forms. There is a lot of confusion in terminology.

To test judgmental equality in Agda, we can use refl to show that two things are judgmentally equal (because the rule for refl states that refl a has type b ≡ c if, and only if, b and c are both judgmentally equal to a). Here are some examples:

 open import Relation.Binary.PropositionalEquality
 open import Data.Nat

 -- this works, the normal form of 2 + 3 is 5
 p : 2 + 3 ≡ 5
 p = refl

 -- this works, the normal form of 0 + m is m
 q : ∀ m → 0 + m ≡ m
 q _ = refl

 -- this does not work, because the normal form of m + 0 is m + 0
 -- r : ∀ m → m + 0 ≡ m
 -- r _ = refl

You can also show that $2 + 3 = 5$ by providing an element p' of 2 + 3 ≡ 5 which is not refl, such as the one you posted in the question. In the text you read, they were just trying to demonstrate the normalization steps by making them explicit as elements of an identity type (without saying so explicitly, probably). The thing to remember is that in Agda you will never see "a proof of judgemental equality", as that always happens in the background.