Idris proof with simplification causing "type mismatch" error

Question

I am learning Idris by following along with this book: https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf

I kind of hit a snag when getting to the section on proof with simplification (yes it is right at the start). The small bit of code I am working on is:

namespace Numbers

  data Nat : Type where
    Zero : Numbers.Nat
    Successor : Numbers.Nat -> Numbers.Nat

  plus : Numbers.Nat -> Numbers.Nat -> Numbers.Nat
  plus Zero b = b
  plus (Successor a) b = Successor(plus a b)

These simpler proofs work okay:

One : Numbers.Nat
One = Successor Zero

Two : Numbers.Nat
Two = Successor One

Three : Numbers.Nat
Three = Successor Two

proofOnePlusZero : plus One Zero = One
proofOnePlusZero = Refl

proofOnePlusZero' : plus Zero One = One
proofOnePlusZero' = Refl

however as I tried to copy in the more complicated proof I get an error

-- works
plus_Z_n : (n : Numbers.Nat) -> plus Zero n = n
plus_Z_n n = Refl

-- breaks / errors
plus_Z_n' : (n : Numbers.Nat) -> plus n Zero = n
plus_Z_n' n = Refl

This is the error

When checking right hand side of plus_Z_n' with expected type
        plus n One = Successor n

Type mismatch between
        Successor n = Successor n (Type of Refl)
and
        plus n (Successor Zero) = Successor n (Expected type)

Specifically:
        Type mismatch between
                Successor n
        and
                plus n (Successor Zero)

this is the expected behavior - however the recommendation is that one is able to understand why. I am at a loss and looking for hints or how to conisder this.

xash xash · Accepted Answer · 2019-08-15T12:56:36

Here Idris just follows the definition (“proof of simplification”). So take plus Zero n = n. To simplify this type, the definition of plus helps: one branch defines plus Zero b = b. So we can replace plus Zero n with n to get to n = n, voilà. On the other hand, if trying to simplify plus n Zero = n, none of the branches in the definition of plus matches plus n Zero. So no replacement can be done and Idris is stuck with plus n Zero = n, until you help f.e. by case-splitting on n.

More precisely, if Idris tries to replace plus x Zero, it goes through all of the branches one by one and tries to match them, just as it would evaluate it. If it could be matched, it will stop. But only if the branch is equal to plus x Zero, it will be replaced. So given:

plus : Numbers.Nat -> Numbers.Nat -> Numbers.Nat
plus Zero b = b
plus a Zero = a
plus (Successor a) b = Successor(plus a b)

plus1 : plus n Zero = n
plus1 = Refl

This won't compile, because plus n Zero could be handled by plus Zero b = b, depending on what n is. But because n is not known, Idris already stops here, but does not replace it. So the second branch is not reached.

Idris proof with simplification causing "type mismatch" error

1 Answers