Error about negative Nat

[tony mailer]

Hi,

I'm trying to implement this fibonacci funtion:

fib : Nat -> Nat
fib = fst . fib2
  where
    fib2 : Nat -> (Nat, Nat)
    fib2 Z = (1, 1)
    fib2 (S Z) = (1, 2)
    fib2 n@(S k) =
      let (a,b) = fib2 ((n `div` 2) - 1)
          c     = a + b in
          if isEven n then (a*a + b*b, c*c - a*a) else (c*c - a*a, b*b + c*c)

but Idris2 is complaining that ((n `div` 2) - 1) could be negative:

Error: While processing right hand side of fib2. Can't find an implementation for Neg Nat.

Shouldn't Idris figure out that given any n in this case, that expression can't be negative?

Or is there any way to let it know?

Thanks

tony

[Denis Buzdalov]

Hi,

but Idris2 is complaining that ((n `div` 2) - 1) could be negative:

Error: While processing right hand side of fib2. Can't find an implementation for Neg Nat.

This error does not mean that Idris is complaining that this expression can't be negative. It is complaining that `Nat` type does not have an implementation for the interface called `Neg` which contains function `(-)`. Function `(-)` from interface `Neg a` has signature `a -> a -> a` and is meant to be reverse of the function `(+)` from interface `Num`. Also, interface `Neg` contains `negate` function. Neither can be implemented for `Nat`.

You can see the interface declaration here: https://github.com/idris-lang/Idris2/blob/f016a81e37c538229d6a661fbcade0aadff29130/libs/prelude/Prelude/Num.idr#L27

But anyway, there is a kind of safe negation function for `Nat`s, called `minus` which has signature `Nat -> Nat -> Nat` and which returns `0` if the second argument is more than the first. Maybe, it will work for you, i.e. write ``((n `div` 2) `minus` 1)``.

[tony mailer]

Ah, gotcha. Thanks for the detailed explanation.