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_rhsas powApplyI (Pos 0) i x = x(yes, Zis changed to 0) のままにします。ポイントフリーではないスタイルで書き、モディファイアを使用しpowApplyIて独自のスタイルを定義しようとしましたが（これはわかりません）、どちらも機能しませんでした。の最初のケースを調べて証明を処理しないのはなぜですか?ZZ%elimpowApplyI

イドリスのバージョン: 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（または私の使い方に）問題があります。

4

2 に答える 2

1

powApplyI (Pos Z) i xi頭が弱い通常の形ではないため、これ以上減少しません。

私は 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 に答える