Convince Idris about recursive call totality

Question

I have written the following type to encode all possible rational numbers in it:

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number
    Ratio : Number -> Number -> Number

Note that PosN Z actually encodes number 1, while NegN Z encodes -1. I prefer such a symmetric definition to that given by Data.ZZ module. Now I've got a problem with convincing Idris that addition of such numbers is total:

mul : Number -> Number -> Number
mul Zero _ = Zero
mul _ Zero = Zero
mul (PosN k) (PosN j) = PosN (S k * S j - 1)
mul (PosN k) (NegN j) = NegN (S k * S j - 1)
mul (NegN k) (PosN j) = NegN (S k * S j - 1)
mul (NegN k) (NegN j) = PosN (S k * S j - 1)
mul (Ratio a b) (Ratio c d) = Ratio (a `mul` b) (c `mul` d)
mul (Ratio a b) c = Ratio (a `mul` c) b
mul a (Ratio b c) = Ratio (a `mul` b) c

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = subtractNat k j
plus (NegN k) (PosN j) = subtractNat j k
plus (Ratio a b) (Ratio c d) =
    let a' = assert_smaller (Ratio a b) a in
    let b' = assert_smaller (Ratio a b) b in
    let c' = assert_smaller (Ratio c d) c in
    let d' = assert_smaller (Ratio c d) d in
    Ratio ((mul a' d') `plus` (mul b' c')) (mul b' d')
plus (Ratio a b) c =
    let a' = assert_smaller (Ratio a b) a in
    let b' = assert_smaller (Ratio a b) b in
    Ratio (a' `plus` (mul b' c)) c
plus a (Ratio b c) =
    let b' = assert_smaller (Ratio b c) b in
    let c' = assert_smaller (Ratio b c) c in
    Ratio ((mul a c') `plus` b') (mul a c')

Interestingly when I press Alt-Ctrl-R in Atom editor it's all fine (even with %default total directive). However, when I load this into the REPL it warns me that plus is possibly not total:

   |
29 |     plus Zero y = y
   |     ~~~~~~~~~~~~~~~
Data.Number.NumType.plus is possibly not total due to recursive path 
Data.Number.NumType.plus --> Data.Number.NumType.plus

From the message I understand that it's worried about these recursive calls to plus in patterns handling ratios. I thought that asserting that a is smaller than Ratio a b etc. would solve the problem, but it didn't, so probably Idris sees that, but has trouble with something else. I cannot figure out what it could be, though.

xash xash · Accepted Answer · 2019-02-16T17:52:58

assert_smaller (Ratio a b) a is already known to Idris (a is an argument to the "bigger" Ratio a b type after all). What you need to prove (or assert), is that the result of mul is structurally smaller than the arguments to plus.

So it should work with

plus (Ratio a b) (Ratio c d) =
    let x = assert_smaller (Ratio a b) (mul a d) in
    let y = assert_smaller (Ratio a b) (mul b c) in
    Ratio (x `plus` y) (mul b d)
plus (Ratio a b) c =
    let y = assert_smaller (Ratio a b) (mul b c) in
    Ratio (a `plus` y) c
plus a (Ratio b c) =
    let x = assert_smaller (Ratio b c) (mul a c) in
    Ratio (x `plus` b) (mul a c)

Convince Idris about recursive call totality

1 Answers