`agda`: how to specify that a step in equational reasoning is by definition of a function?

Question

I'm new to agda. How can I specify, when I do equational reasoning, that a specific step is by definition of a function?

For example, take the following definition of natural numbers:

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

add : Nat -> Nat -> Nat
add zero    x = x
add (suc x) y = suc (add x y)

I can now prove that 2 + 3 is 5:

_ : add 2 3 ≡ 5
_ =
  begin
     add 2 3
     
  ≡⟨⟩  -- replace notation
     add (suc (suc zero)) (suc (suc (suc zero)))
     
  ≡⟨⟩  -- inductive case of add
     suc (add (suc zero) (suc (suc (suc zero))))
     
  ≡⟨⟩  -- inductive case of add
     suc (suc (add zero (suc (suc (suc zero)))))
     
  ≡⟨⟩  -- base case of add
     suc (suc (suc (suc (suc zero))))
     
  ≡⟨⟩  -- replace notation
     5
  ∎

Agda is perfectly happy with this, but I'd like to make it also check that my reasoning in some steps is correct. Is there a way for me to replace:

     suc (suc (add zero (suc (suc (suc zero)))))

  ≡⟨⟩  -- base case of add
     suc (suc (suc (suc (suc zero))))

with:

     suc (suc (add zero (suc (suc (suc zero)))))

  ≡⟨ ?put something here? ⟩
     suc (suc (suc (suc (suc zero))))

where the "?put something here?" but refers specifically to the base case in the definition of add, so that agda can check that it is precisely by applying add that one can reduce the expression as I say?

Answer 1

(Excluding rewrite rules), the only way Agda can ever reduce an expression is by appealing to the definition. Therefore it's not terribly meaningful to try and make Agda "check that it is precisely by applying add that one can reduce the expression". It's the only way Agda can do it!

If you really want to make explicit the fact that you're using the base case you could prove the lemma:

rightIdentity : forall x -> 0 + x ≡ x
rightIdentity x = refl

and then write:

suc (suc (add zero (suc (suc (suc zero)))))

  ≡⟨ cong (\a -> suc (suc a)) (rightIdentity (suc (suc (suc zero)))) ⟩

suc (suc (suc (suc (suc zero))))