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... ;-)

Answer 2

The way I think of why this is true is as follows: the only inequality of the form m ≤ zero in the definition of the the relation ≤ is zero ≤ zero, or equivalently z≤n {0}. So, if we assume m ≤ zero, we "must" have m ≡ 0.

data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} → zero ≤ n
  s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc n 

And if you start writing your proof like this

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

Then C-c C-l transforms it into

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

with goal

?0 : m ≤ zero → m ≡ zero

Then C-c C-, gives you the goal and context:

m ≤ zero → m ≡ zero
m : ℕ   (not in scope)

So this confirms that you have to define a function m ≤ zero → m ≡ zero. And indeed C-c C-r

will produce

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n = λ x → {!   !}

with goal and context

m ≡ zero
x : m ≤ zero
m : ℕ   (not in scope)

At this stage, the best I can suggest is to change your definition to

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n x = ?

(which may on fact be a more natural starting point than the one I initially suggested) and do C-c C-l and C-c C-, again. Then you get:

inv-z≤n : {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n x = {!   !}

with goal and context

m ≡ zero
x : m ≤ zero
m : ℕ   (not in scope)

Now the trick is to recall that m ≤ zero is an inductive type, so you can use C-c C-c and case split on xto distinguish between possible cases (this could not be done when x was only a local variable). And then you get only one possible case, namely z≤n, for the reasons explained at the beginning of this post. Now your definition looks like this:

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

with goal and context (after doing C-c C-, again)

zero ≡ zero

and then it is clear that refl will close this goal. And indeed C-c C-r gives you:

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

with goal and context

*All Done*

I don't know any way to make the proof of m ≤ zero → m ≡ zero explicit besides the case split / pattern matching described above.