3
votes

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).

2
That's because you also pattern-match on i, which is not in weak head normal form. Try to replace pattern-matching on i with a case-expression. Or you can rewrite your signature as powApplyIZero : (f : _) -> (g : _) -> (eq : _) -> (x : _) -> powApplyI (Pos Z) (MkInvertible f g eq) x = x.user3237465
@user3237465, thanks, but neither of those suggestions worked. By the way, why do you suggest a case expression? I thought that pattern matching/with was the canonical way in proofs. (I tried both the case expression and pattern matching on the left hand side.)mudri
I suggested to use a case-expression (or an auxiliary function), because sometimes it's useful to delay forcing an argument to be in whnf, but yes, that's unrelated to your question. I added an answer.user3237465

2 Answers

5
votes

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.

1
votes

powApplyI (Pos Z) i x doesn't reduce further because i is not in weak head normal form.

I don't have an Idris compiler, so I rewrote your code in Agda. It's pretty similar:

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Integer

data Invertible : Set -> Set -> Set where
  MkInvertible : {a b : Set} (f : a -> b) -> (g : b -> a) ->
                 (∀ x -> g (f x) ≡ x) -> Invertible a b

powApplyI : {a : Set} -> ℤ -> Invertible a a -> a -> a
powApplyI  ( + 0     ) (MkInvertible f g x) = id
powApplyI  ( + suc k ) (MkInvertible f g x) = f ∘ powApplyI  ( + k ) (MkInvertible f g x)
powApplyI -[1+ 0     ] (MkInvertible f g x) = g
powApplyI -[1+ suc k ] (MkInvertible f g x) = g ∘ powApplyI -[1+ k ] (MkInvertible f g x)

Now you can define your powApplyIZero as

powApplyIZero : {a : Set} (i : Invertible a a) -> ∀ x -> powApplyI (+ 0) i x ≡ x
powApplyIZero (MkInvertible _ _ _) _ = refl

Pattern-matching on i induces unification and powApplyI (+ 0) i x becomes replaced with powApplyI (+ 0) i (MkInvertible _ _ _), so powApplyI can proceed further.

Or you could write this explicitly:

powApplyIZero : {a : Set} (f : a -> a) (g : a -> a) (p : ∀ x -> g (f x) ≡ x)
              -> ∀ x -> powApplyI (+ 0) (MkInvertible f g p) x ≡ x
powApplyIZero _ _ _ _ = refl