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).
i
, which is not in weak head normal form. Try to replace pattern-matching oni
with a case-expression. Or you can rewrite your signature aspowApplyIZero : (f : _) -> (g : _) -> (eq : _) -> (x : _) -> powApplyI (Pos Z) (MkInvertible f g eq) x = x
. – user3237465case
expression? I thought that pattern matching/with
was the canonical way in proofs. (I tried both thecase
expression and pattern matching on the left hand side.) – mudri