根据定义,Idris证明

Question

我可以写这个功能

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

并且琐碎地证明:

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

到现在为止还挺好.现在,我尝试概括此函数以使用负指数.当然,必须提供反向:

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)

然后我试着证明一个类似的陈述:

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

但是,Idris拒绝评估应用程序powApplyI,将类型保留?powApplyIZero_rhs为powApplyI (Pos 0) i x = x(是,Z已更改为0).我尝试powApplyI用非pointfree样式编写,并ZZ使用%elim修饰符(我不明白)定义自己的样式,但这些都不起作用.为什么不通过检查第一个案件处理证明powApplyI？

Idris版本:0.9.15.1

---

以下是一些事情:

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

第一个证据很好,但?powApplyZFZero_rhs固执地保持这种类型powApplyZF (Pos 0) f x = x.显然,ZZ(或我使用它)存在一些问题.

Answer 1

powApplyI根据伊德里斯的说法,这个问题:完全不可证明.Idris的整体检查器依赖于能够将参数减少到结构上较小的形式,而使用原始ZZs,这不起作用.

答案是将递归委托给普通的powApply(已证明总计):

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

然后,一个案例分裂i,powApplyIZero被证明是平凡的.

感谢#idris IRC频道的Melvar.