Inductive relations: Explicit proof that inverse relation is refl

Question

In PLFA they define the inverse relation:

inv-z≤n :   ∀ {m : ℕ} 
            → m ≤ zero 
        ----------------------
            → m ≡ zero

And then assert that:

inv-z≤n z≤n = refl

My question is, how could I give an explicit proof of m ≡ zero? I'm looking something that looks like this:

inv-z≤n {m} (z≤n) = 
    begin
        m
    ≡⟨⟩
        .....
    ≡⟨⟩
        zero
    ∎

but completing the intermediate steps with something. Of course simply writing

inv-z≤n {m} (z≤n) = 
    begin
        m
    ≡⟨⟩
        zero
    ∎

compiles, but I don't find it satisfying. I want to know why m ≡ zero instead of just writing that refl is a proof.

Answer 1

@Matematiflo's answer is pretty comprehensive (and the gist of my more long-winded account below is already present in their first line of explanation), but intuitively/informally one can gain confidence in the unimpeachable formality of the Agda by thinking out loud as follows (and learning to do so whenever faced with a formal proof that seems hard to understand: leave the machine behind and 'reckon it out' in your own mind):

• if m ≤ zero holds (by hypothesis), then how could that be?
• _≤_ is inductively defined, so there are two possibilities, corresponding to the 'base' and 'step' cases of that inductive definition:
  • in the first, m is/must be definitionally equal to zero (via the z≤n constructor, with its argument n then also equal to zero);
  • in the second, the s≤s constructor expects the RHS term to be of the form suc n, but that's impossible, because zero is not of that form... so there is no case to answer.
• so we must be in the first case... and now we are done, because the problem statement is (definitionally equal to) zero ≡ zero, which has refl as a proof of it.

In terms of your Agda fragment

inv-z≤n {m} (z≤n) = 
    begin
        m
    ≡⟨⟩
        zero
    ∎

what 'is going on' is that the pattern (z≤n) is actually forcing the prior binding {m} in fact to be of the form {m@zero} or {m = zero}... in the Good Old Days, such 'forced' bindings were marked with a dot (and interactively such bindings, and marks on bindings, would be inserted by the typechecker), so that the following would typecheck

inv-z≤n {.zero} (z≤n) = 
    begin
        zero
    ≡⟨⟩
        zero
    ∎

but the @-pattern or telescopic {m = ...} forms work just as well. But just because the typechecker accepts it doesn't really answer the question as to why?, does it?

There's maybe the additional meta-level why? as to "why is such reasoning sound in the first place?" which touches on our willingness to accept proof by induction on complicated inductive definitions, and the justification of dependently-typed pattern-matching as a mechanism to instrument such reasoning (and unification along with it as the means by which we can say what form(s) m must take in the course of such reasoning)... but

• that (perhaps) takes us too philosophically far off-topic, but is always part of the justification for type theory, and how we come to have confidence in such arguments, as well as the distinguished role played by definitional equality 'in the background';
• we are already working in an implementation of type theory, so such niceties might already be considered to be 'taken as read' as part of our presupposed epistemological commitment to using Agda in the first place... ;-)