Search code examples
proofidris

Idris proof by definition

I can write the function

powApply : Nat -> (a -> a) -> a -> a
powApply Z f = id
powApply (S k) f = f . powApply k f

and prove trivially:

powApplyZero : (f : _) -> (x : _) -> powApp Z f x = x
powApplyZero f x = Refl

So far, so good. Now, I try to generalize this function to work with negative exponents. Of course, an inverse must be provided:

import Data.ZZ

-- Two functions, f and g, with a proof that g is an inverse of f
data Invertible : Type -> Type -> Type where
  MkInvertible : (f : a -> b) -> (g : b -> a) ->
                 ((x : _) -> g (f x) = x) -> Invertible a b

powApplyI : ZZ -> Invertible a a -> a -> a
powApplyI (Pos Z) (MkInvertible f g x) = id
powApplyI (Pos (S k)) (MkInvertible f g x) =
  f . powApplyI (Pos k) (MkInvertible f g x)
powApplyI (NegS Z) (MkInvertible f g x) = g
powApplyI (NegS (S k)) (MkInvertible f g x) =
  g . powApplyI (NegS k) (MkInvertible f g x)

I then try to prove a similar statement:

powApplyIZero : (i : _) -> (x : _) -> powApplyI (Pos Z) i x = x
powApplyIZero i x = ?powApplyIZero_rhs

However, Idris refuses to evaluate the application of powApplyI, leaving the type of ?powApplyIZero_rhs as powApplyI (Pos 0) i x = x (yes, Z is changed to 0). I've tried writing powApplyI in a non-pointsfree style, and defining my own ZZ with the %elim modifier (which I don't understand), but neither of these worked. Why isn't the proof handled by inspecting the first case of powApplyI?

Idris version: 0.9.15.1

Here are some things:

powApplyNI : Nat -> Invertible a a -> a -> a
powApplyNI Z (MkInvertible f g x) = id
powApplyNI (S k) (MkInvertible f g x) = f . powApplyNI k (MkInvertible f g x)

powApplyNIZero : (i : _) -> (x : _) -> powApplyNI 0 i x = x
powApplyNIZero (MkInvertible f g y) x = Refl

powApplyZF : ZZ -> (a -> a) -> a -> a
powApplyZF (Pos Z) f = id
powApplyZF (Pos (S k)) f = f . powApplyZF (Pos k) f
powApplyZF (NegS Z) f = f
powApplyZF (NegS (S k)) f = f . powApplyZF (NegS k) f

powApplyZFZero : (f : _) -> (x : _) -> powApplyZF 0 f x = x
powApplyZFZero f x = ?powApplyZFZero_rhs

The first proof went fine, but ?powApplyZFZero_rhs stubbornly keeps the type powApplyZF (Pos 0) f x = x. Clearly, there's some problem with ZZ (or my use of it).

Solution

  • The problem: powApplyI was not provably total, according to Idris. Idris' totality checker relies on being able to reduce parameters to structurally smaller forms, and with raw ZZs, this doesn't work.

    The answer is to delegate the recursion to plain old powApply (which is proven total):

    total
powApplyI : ZZ -> a <~ a -> a -> a
powApplyI (Pos k) (MkInvertible f g x) = powApply k f
powApplyI (NegS k) (MkInvertible f g x) = powApply (S k) g

    Then, with a case split on i, powApplyIZero is proven trivially.

    Thanks to Melvar from the #idris IRC channel.