proof - 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)。我试过以非 pointsfree 风格编写 powApplyI，并使用 %elim 修饰符定义我自己的 ZZ(我不明白)，但这些都不起作用。为什么不通过检查 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

问题:根据 Idris 的说法，powApplyI 无法证明是完全的。 Idris 的完整性检查器依赖于能够将参数减少到结构上更小的形式，而对于原始 ZZ，这是行不通的。

答案是将递归委托(delegate)给普通的旧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 channel 的 Melvar。