Agda2で同値関係を表す

昨晩に、ikegamiさんがつくばにいらしてたので、soutaroさんと一緒にご飯を食べに。その時Agdaの過去話を色々聞いて、やっぱり色々だなーとか思っていました。

その場でdot-patternがちょっとみたいな事を言ったものの私が今実装してる言語では現時点でdot-patternもImplicit Parametersも実装してないので更に酷いよなぁみたいなそういう。

けどまぁそれらを回避しつつ幾つかのテクニックが詰まった方法として、Agda2上で同値関係を表すものを作って加算の可換性を証明してみる事にしたいと思います。

参考

型理論での形式的証明記述の技法について
http://www.nue.riec.tohoku.ac.jp/jssst2005/papers/05061.pdf

簡単な(?)定義

data Id (T : Set0) : T -> T -> Set0 where
  id : (t : T) -> Id T t t

例えばコレを使って

v : (n : Nat) -> Id (add n zero) (add zero n)
v = なんか

みたいな事を書けば、(n + 0) == (0 + n)みたいな事を言えた事に成ります。

二項関係において同値関係であるっていう時には、
1.反射律(reflexive) Id a aが成り立つ
2.推移律(transitive) Id a b かつ Id b cならば、Id a c
3.対称律(symmetric) Id a bならばId b a
みたいな3つを満たす時に言うそれなのですが、じゃあ取りあえず各々を書いてみましょう。

reflId : (T : Set0) -> (t1 : T) -> Id T t1 t1
reflId T t1 = id t1

transId : (T : Set0) -> (t1 t2 t3 : T) -> Id T t1 t2 -> Id T t2 t3 -> Id T t1 t3
transId T t1 .t1 .t1 (id .t1) (id .t1) = id t1

symId : (T : Set0) -> (t1 t2 : T) -> Id T t1 t2 -> Id T t2 t1
symId T t1 .t1 (id .t1) = id t1

みたいな事に成って、何じゃこりゃ！！と成ります。

これはImplicit Parametersを使って書かずに、dot-patternを使って尚かつAgda2の型チェッカがどう振る舞うかを少し想像しないと書けないのできびちい・・・。ちゅらいね・・・。

なのでImplicit Prametersを使って書き直してみます。

transId' : {T : Set0} -> {t1 t2 t3 : T} -> Id T t1 t2 -> Id T t2 t3 -> Id T t1 t3
transId' t1t2 (id t2) = t1t2

symId' : {T : Set0} -> {t1 t2 : T} -> Id T t1 t2 -> Id T t2 t1
symId' (id t1) = (id t1)

まぁsymId'は何とか良いとしても、transId'は直ぐぽんと書けるようなもんじゃ無いと思います。

簡単を組み合わせた定義

そこで、"Leibniz Equality"とか"Leibniz Identity"と呼ばれる方法をAgda2で書く事にしてみます。

これは、簡単に言うならば「X上の任意の述語P(x)に対してP(a)がP(b)を導く　その時に限りa≡b」と言うものです。

これ自体は

eq : (T : Set0) -> (x y : T) -> Set1
eq T x y = (P : T -> Set0) -> P x -> P y

leibnizEq : Nat -> Nat -> Set1
leibnizEq x y = (P : Nat -> Set0) -> P x -> P y

と書けます。今回はNatの事ばっかり考えたいので、下のleibnizEqを使う事にします。

さて、ここでも反射律、推移律、対称律を書きたいので書いてみましょう。実際にあると後の証明で凄く便利。

refl : (n : Nat) -> leibnizEq n n
refl _ = (\P -> (\px -> px))

refl自体の引数は、これはもう完全に型シグネチャに合わせているだけなので'_'を使って無視します。

sym : (x : Nat) -> (y : Nat) -> leibnizEq x y -> leibnizEq y x
sym x y xy = (\P -> (\py -> (xy (\z -> P z -> P x) (\px -> px) py)))
-- sym x y xy = (\P -> (\py -> ((xy (\z -> (P z -> P x))) (\px -> px)) py))

引数のxyは、xy ∈ leibnizEq xyを表している。
さて、xy (\z -> P z -> P x)はどうなるかというと、これは

xy (\z -> P z -> P x) ∈ (P x -> P x) -> (P y -> P x)

という事に成る。
従って

xy (\z -> P z -> P x) (\px -> px) ∈ (P y -> P x)

となる。
そこから

xy (\z -> P z -> P x) (\px -> px) py ∈ (P x)

よってsymの右辺は
(\(P : Nat -> Set0) -> (\(py : P y) -> (xy (\z -> P z -> P x) (\px -> px) py : P x)))
となり型が(Nat -> Set0) -> P y -> P xとなり正しい。

trans : (x : Nat) -> (y : Nat) -> (z : Nat) -> leibnizEq x y -> leibnizEq y z -> leibnizEq x z
trans x y z xy yz = (\P -> (\px -> yz P (xy P px)))

xy P px ∈ P yとなる。これをpyと置く。
yz P py ∈ P zとなる。これをpzと置く。
(\P -> (\px -> pz)) これは (P -> P x -> P z)

揃った

ので証明してみる。

data Nat : Set0 where
  ０ : Nat -- これは全角の０です。
  1+ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
_+_ ０ y = y
_+_ (1+ x) y = 1+ (x + y)

eq : (T : Set0) -> (x y : T) -> Set1
eq T x y = (P : T -> Set0) -> P x -> P y

leibnizEq : Nat -> Nat -> Set1
leibnizEq x y = (P : Nat -> Set0) -> P x -> P y

refl : (n : Nat) -> leibnizEq n n
refl _ = (\P -> (\px -> px))

sym : (x : Nat) -> (y : Nat) -> leibnizEq x y -> leibnizEq y x
sym x y xy = (\P -> (\py -> (xy (\z -> P z -> P x) (\px -> px) py)))

trans : (x : Nat) -> (y : Nat) -> (z : Nat) -> leibnizEq x y -> leibnizEq y z -> leibnizEq x z
trans x y z xy yz = (\P -> (\px -> yz P (xy P px)))

mapEq : (x : Nat) -> (y : Nat) -> (f : Nat -> Nat) -> leibnizEq x y -> leibnizEq (f x) (f y)
mapEq x y f xy = (\P -> xy (\z -> P (f z)))

-- 加算の定義から明らか
lemma1 : (n : Nat) -> (m : Nat) -> leibnizEq ((1+ n) + m) (1+ (n + m))
lemma1 n m = (\P -> (\px -> px))

-- (0 + x) = (x + 0)
lemma2 : (x : Nat) -> leibnizEq x (x + ０)
lemma2 ０ = (\P -> (\px -> px))
lemma2 (1+ n) with lemma2 n
... | r = mapEq n (n + ０) 1+ r

lemma3 : (n : Nat) -> (m : Nat) -> leibnizEq (n + (1+ m)) (1+ (n + m))
lemma3 ０ m = refl (1+ m)
lemma3 (1+ n) m = v5
  where
    v1 : leibnizEq (1+ (n + m)) ((1+ n) + m)
    v1 = lemma1 n m

    v2 : leibnizEq (n + (1+ m)) ((1+ n) + m)
    v2 = lemma3 n m

    v3 : leibnizEq (n + (1+ m)) (1+ (n + m))
    v3 = v2

    v4 : leibnizEq (1+ (n + (1+ m))) (1+ (1+ (n + m)))
    v4 = mapEq (n + (1+ m)) (1+ (n + m)) 1+ v3

    v5 : leibnizEq ((1+ n) + (1+ m)) (1+ ((1+ n) + m))
    v5 = v4

theorem : (n : Nat) -> (m : Nat) -> leibnizEq (n + m) (m + n)
theorem ０ y = lemma2 y
theorem (1+ x) y = v4
  where
    v1 : leibnizEq (x + y) (y + x)
    v1 = theorem x y

    v2 : leibnizEq ((1+ x) + y) (1+ (y + x))
    v2 = mapEq (x + y) (y + x) 1+ v1

    v3 : leibnizEq (1+ (y + x)) (y + (1+ x))
    v3 = sym (y + (1+ x)) (1+ (y + x)) (lemma3 y x)

    v4 : leibnizEq ((1+ x) + y) (y + (1+ x)) -- leibnizEq (n + m) (m + n)
    v4 = trans ((1+ x) + y) (1+ (y + x)) (y + (1+ x)) v2 v3

途中にmapEqというものを定義していますが、これは x = yならば、ある関数fを持って来て f(x) = f(y)になるよねというものです。

symとtransの定義テクニックが分かれば別段問題無いソレだと思うので省略。

他には

Setoidを使ったものなどがあるらしいですが、まぁ取りあえず個人的にはImplicit Parameterは欲しいよーっていう感じにやっぱりなります。

至る所で欲しいです。

のでなんとか日月で実装したい。