Why does `sym` need to be used in this case when using `rewriting`?

Question

Given the Peano definition of natural numbers:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

We can prove by different methods the property ∀ (m : ℕ) → zero + m ≡ m + zero.

For example:

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

And more compactly:

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) = cong suc (comm-+₀ n)

If we want, we can even use rewrite and forgo cong:

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) rewrite comm-+₀ n = refl

But wait! That doesn't work. Agda will tell us that the expression is wrong because it can't prove the following:

suc (n + 0) ≡ suc (n + 0 + 0)

If we present Agda the symmetrical rewrite of the property, sym (comm-+₀ n), it will type check without errors.

So, my question is: why do we need sym in this case? The proof worked perfectly fine without it with the other strategies. Does rewrite work on both sides simultaneously and not just the left side?

MrO MrO · Accepted Answer · 2020-02-11T00:19:05

In every cases, the goal when m is of the form suc n is:

suc n ≡ suc (n + 0)

To solve this goal by providing a correctly typed term, the right way is, as you noticed:

cong suc (comm-+₀ n)

However, when using rewrite with an equality a ≡ b you modify directly the goal by substituting all occurences of a by b In your case, using rewrite on the quantity comm-+₀ n whose type is n ≡ n + 0 leads to the replacing of every occurence of n by n + 0, thus transforming the goal from

suc n ≡ suc (n + 0)

to

suc (n + 0) ≡ suc (n + 0 + 0)

which is not what you want to do. Since rewriting replaces all occurences of the left side by the right side, reversing the equality using sym will instead replace the only occurence of n + 0 by n thus transforming the goal from

suc n ≡ suc (n + 0)

to

suc n ≡ suc n

which is your expected behaviour and let you conclude using refl direcly. This explains why you need to use sym.

To summarize :

rewrite interacts directly with the type of the goal.
rewrite rewrites from left to right.
rewrite rewrites all occurences it finds in the type of the goal.

Why does `sym` need to be used in this case when using `rewriting`?

1 Answers