An Idris proof about `mod`

Question

I was trying to write a proof in Idris regarding the following subtraction-based mod operator:

mod : (x, y : Nat) -> Not (y = Z) -> Nat
mod x Z p = void (p Refl)
mod x (S k) _ = if lt x (S k) then x else helper x (minus x (S k)) (S k)
  where total
        helper : Nat -> Nat -> Nat -> Nat
        helper Z x y = x
        helper (S k) x y = if lt x y then x else helper k (minus x y) y

The theorem I wanted to prove is that the remainder as produced by "mod" above is always smaller than the divider. Namely,

mod_prop : (x, y : Nat) -> (p : Not (y=0))-> LT (mod x y p) y

I constructed a proof but was stuck by a final hole. My full code is pasted below

    mod : (x, y : Nat) -> Not (y = Z) -> Nat
    mod x Z p = void (p Refl)
    mod x (S k) _ = if lt x (S k) then x else helper x (minus x (S k)) (S k)
      where total
            helper : Nat -> Nat -> Nat -> Nat
            helper Z x y = x
            helper (S k) x y = if lt x y then x else helper k (minus x y) y
    
    lteZK : LTE Z k
    lteZK {k = Z} = LTEZero
    lteZK {k = (S k)} = let ih = lteZK {k=k} in
                        lteSuccRight {n=Z} {m=k} ih 
    
    lte2LTE_True : True = lte a b -> LTE a b
    lte2LTE_True {a = Z} prf = lteZK
    lte2LTE_True {a = (S _)} {b = Z} Refl impossible
    lte2LTE_True {a = (S k)} {b = (S j)} prf = 
      let ih = lte2LTE_True {a=k} {b=j} prf in LTESucc ih

    
    lte2LTE_False : False = lte a b -> GT a b
    lte2LTE_False {a = Z} Refl impossible
    lte2LTE_False {a = (S k)} {b = Z} prf = LTESucc lteZK
    lte2LTE_False {a = (S k)} {b = (S j)} prf = 
      let ih = lte2LTE_False {a=k} {b=j} prf in (LTESucc ih)
    
    total
    mod_prop : (x, y : Nat) -> (p : Not (y=0))-> LT (mod x y p) y
    mod_prop x Z p = void (p Refl)
    mod_prop x (S k) p with (lte x k) proof lxk
      mod_prop x (S k) p | True  = LTESucc (lte2LTE_True lxk)
      mod_prop Z (S k) p | False = LTESucc lteZK 
      mod_prop (S x) (S k) p | False with (lte (minus x k) k)  proof lxk'
        mod_prop (S x) (S k) p | False | True = LTESucc (lte2LTE_True lxk')
        mod_prop (S x) (S Z) p | False | False  = LTESucc ?hole

Once I run the type checker, the hole is described as follows:

- + Main.hole [P]
 `--          x : Nat
              p : (1 = 0) -> Void
            lxk : False = lte (S x) 0
           lxk' : False = lte (minus x 0) 0
     --------------------------------------------------------------------------
      Main.hole : LTE (Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1) 0

I am not familiar with the syntax of Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1 given in the idris-holes window. I guess (S x) 0 p are the three parameters of "mod" while (minus (minus x 0) 1) 1 are the three parameters of the local "helper" function of "mod"?

It seems that it's time to leverage an induction hypothesis. But how can I finish up the proof using induction?

stop-cran stop-cran · Accepted Answer · 2018-10-08T09:47:39

(Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1)

can be read as

Main.mod, helper - a qualified name for helper function, which is defined in the where clause of the mod function (Main is a module name);
Arguments of mod which are also passed to helper - (S x), 0 and p (see docs):

Any names which are visible in the outer scope are also visible in the where clause (unless they have been redefined, such as xs here). A name which appears only in the type will be in scope in the where clause if it is a parameter to one of the types, i.e. it is fixed across the entire structure.

Arguments of helper itself - x, (minus (minus x 0) 1) and 1.

Also below is another implementation of mod which uses Fin n type for the remainder in division by n. It turns out to be easier to reason about, since any value of Fin n is always less than n:

import Data.Fin

%default total


mod' : (x, y : Nat) -> {auto ok: GT y Z} -> Fin y
mod' Z (S _) = FZ
mod' (S x) (S y) with (strengthen $ mod' x (S y))
    | Left _ = FZ
    | Right rem = FS rem

mod : (x, y : Nat) -> {auto ok: GT y Z} -> Nat
mod x y = finToNat $ mod' x y

finLessThanBound : (f : Fin n) -> LT (finToNat f) n
finLessThanBound FZ = LTESucc LTEZero
finLessThanBound (FS f) = LTESucc (finLessThanBound f)

mod_prop : (x, y : Nat) -> {auto ok: GT y Z} -> LT (mod x y) y
mod_prop x y = finLessThanBound (mod' x y)

Here for convenience I used auto implicits for proofs that y > 0.

An Idris proof about `mod`

1 Answers