Agda allows for incorrect proofs?

Question

I was playing around a bit with proofs in Agda following PLFA, specifically the monus operator.

-- Monus
_∸_ : ℕ → ℕ → ℕ
m ∸ zero = m
zero ∸ suc (m) = zero
suc (n) ∸ suc(m) = n ∸ m

And the problem I found is that I can make incorrect "proofs" that compile:

_ : 3 ∸ 5 ≡ 0
_ =
  begin
      3 ∸ 5
    ≡⟨⟩
      2 ∸ 4
    ≡⟨⟩
      1 ∸ 3
    ≡⟨⟩
      0 ∸ 3
    ≡⟨⟩
      0
    ∎

While it is true that 3 ∸ 5 ≡ 0, in the rules for the monus there is no rule that indicates that 1 ∸ 3 ≡⟨⟩ 0 ∸ 3. The correct application of rule 3 would yield 1 ∸ 3 ≡⟨⟩ 0 ∸ 2. How can I be sure that I only apply correct rules in each step of the proof, and reject this kind of proofs? Thank you.

Answer 1

What @Naïm Favier says in the comments is correct.

You're asking to mirror a particular computation, step-by-step, and Agda doesn't do that, it computes all the way. So it sees 0 all the way down.

If you want to reason about derivations, then you should create the monus relation that has two rules; from that relation, you can 'extract' the function, since it is a functional relation. But now that you have a proof-relevant relation, derivations are tangible, and you won't be able to write down an incorrect one.