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 存在问题（或者是我使用它的问题）。

- mudri

---

这是因为你也在i上进行了模式匹配，但它不是处于弱头标准形式。尝试用case表达式替换对i的模式匹配。或者你可以将签名重写为powApplyIZero: (f : _) -> (g : _) -> (eq : _) -> (x : _) -> powApplyI (Pos Z) (MkInvertible f g eq) x = x。 - effectfully

@user3237465，谢谢您的建议，但这些建议都没有起作用。顺便问一下，为什么您建议使用case表达式？我认为模式匹配/with是证明中的规范方式。（我在左侧尝试了case表达式和模式匹配。） - mudri

我建议使用case表达式（或辅助函数），因为有时候延迟强制参数进入whnf是很有用的，但是这与你的问题无关。我添加了一个答案。 - effectfully

Answer 1

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

答案是将递归委托给已被证明为完全的普通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。

- mudri

Answer 2

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

- effectfully

---

问题似乎是特定于Idris的。它拒绝缩减powApplyI（Pos 0）（MkInvertible f g p）x = x（无论元变量的类型是什么，逐字逐句）。 - mudri

@James Wood，powApplyIZero 的第一个定义也无法通过类型检查吗？ - effectfully

当我尝试使用“Refl”填充空洞时，它每次都会给出相同的类型，即“无法将x = x与powApplyI（Pos 0）（MkInvertible f g p）x = x统一”。 - mudri

@James Wood，看起来是一个 bug。你尝试过在不细化洞的情况下编写 Refl 吗？据我所知，Idris 没有 Agda 中那样深度融合的元变量概念，因此可能是洞的问题。 - effectfully

我进行了更多的测试，所以我会编辑问题。简而言之，问题出在ZZ上。 - mudri