Search code examples
proofidris

Proof a Natural (n) is Zero

I am trying to learn the idris paradigm and still struggling. Here i have a function isZero that takes some natural Nat and returns True or False.

My issue is with the non-relexive case.

namespace Numbers

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

  isZero: Numbers.Nat -> Prelude.Bool.Bool
  isZero Zero = True
  isZero _ = False

  isNotZero: Numbers.Nat -> Prelude.Bool.Bool
  isNotZero Zero = False
  isNotZero _ = True

  proofNIsZero : (n : Numbers.Nat) -> isZero n = Bool.True
  proofNIsZero Zero = Refl
  proofNIsZero (Successor _) = ?rhs

It seems obvious to reason that some Successor to any Nat cannot be Zero. But my struggle is in the proof. The Type of the ?rhs hole is

--------------------------------------
rhs : False = True

Trying to navigate what I think should be (and will one day be) simple has led to uninhabited, Void, absurd and impossible. None of which I can disambiguate.

Perhaps those are the keys - but I cannot decipher!

Solution

  • I am answering as I think I relaized that perphaps the proof above wasn't stated correctly. I added the statement that asserted n = Zero, which allow for the isZero n = Bool.True to have meaning. the n = Zero carries forward as prf and allows me to declare absurd prf as isZero n = Bool.True cannot hold true if n is Successor to some Nat.

      Uninhabited (Successor _ = Zero) where
    uninhabited Refl impossible

  proofNIsZero : (n : Numbers.Nat) -> n = Zero -> isZero n = Bool.True
  proofNIsZero Zero prf = Refl
  proofNIsZero (Successor _) prf = absurd prf

    Is there another approach or way to think of defining these as to not get caught in a pitfall?