3

我可以写函数

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用非无点风格写作，并ZZ用%elim修饰符定义我自己的风格（我不明白），但这些都不起作用。为什么不通过检查第一个案例来处理证明powApplyI？

伊德里斯版本：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顽固地保留了 type powApplyZF (Pos 0) f x = x。显然，ZZ（或我对它的使用）存在一些问题。

4

2 回答 2

5

根据伊德里斯的说法，问题powApplyI是无法证明是完全的。Idris 的整体检查器依赖于能够将参数减少到结构上更小的形式，而对于 raw 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。

于 2015-01-03T23:10:22.660 回答
1

powApplyI (Pos Z) i x不会进一步减少，因为i不是弱头正常形式。

我没有 Idris 编译器，所以我在 Agda 中重写了您的代码。它非常相似：

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)

现在你可以定义你powApplyIZero的

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

上的模式匹配i导致统一并被powApplyI (+ 0) i x替换为powApplyI (+ 0) i (MkInvertible _ _ _)，因此powApplyI可以进一步进行。

或者你可以明确地写这个：

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
于 2015-01-03T12:46:50.083 回答