ちょっと証明

gistfile1.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

-- 参考:
--     https://hackage.haskell.org/package/type-natural-0.2.3.2
--     http://yosh.hateblo.jp/entry/20091023/p2

module Proof where

import Data.Type.Equality

-- ペアノ数
data N = Z | S N

-- シングルトン
data SN :: N -> * where
    SZ :: SN 'Z
    SS :: SN a -> SN ('S a)

-- ペアノ数の足し算
type family a + b where
  'Z   + b = b
  'S a + b = 'S (a + b)

-- シングルトンの足し算
(.+) :: SN a -> SN b -> SN (a + b)
SZ   .+ b = b
SS a .+ b = SS (a .+ b)

infixl 6 .+

-- 特に必要ないけれど、一応明記しておく
reflS :: 'S :~: 'S
reflS = Refl

-- まずは結合法則
-- 特に考える事はない
plusAssoc :: SN a -> SN b -> SN c -> (a + b) + c :~: a + (b + c)
plusAssoc  SZ    _ _ = Refl
plusAssoc (SS a) b c = apply reflS (plusAssoc a b c)

-- 交換法則のための補題
plusSy :: SN a -> SN b -> a + 'S b :~: 'S (a + b)
plusSy  SZ    _ = Refl
plusSy (SS a) b = apply reflS (plusSy a b)

addL :: SN a -> x :~: y -> a + x :~: a + y
addL _ Refl = Refl

addR :: x :~: y -> SN a -> x + a :~: y + a
addR Refl _ = Refl

-- 交換法則
plusComm :: SN a -> SN b -> a + b :~: b + a
plusComm  SZ    SZ    = Refl
plusComm  SZ   (SS b) = apply reflS (plusComm SZ b)

-- ここまでは考える事は無い

-- type holeを使用してここで証明すべき型を聞くと、

-- plusComm (SS a) b = (undefined :: _)
--
-- a.hs|56 col 34 error| Found hole ‘_’ with type: 'S (a1 + b) :~: (b + 'S a1)
-- || Where: ‘b’ is a rigid type variable bound by
-- ||            the type signature for
-- ||              plusComm :: SN a -> SN b -> (a + b) :~: (b + a)
-- ||            at a.hs:50:13
-- ||        ‘a1’ is a rigid type variable bound by
-- ||             a pattern with constructor
-- ||               SS :: forall (a :: N). SN a -> SN ('S a),
-- ||             in an equation for ‘plusComm’

-- なので、ここで証明したいのは (a ~ 'S a') => 'S (a' + b) :~: (b + 'S a')

-- 適当にギャップを埋めていくと、
--
-- 'S (a' + b)
-- :~: 'S (b + a') -- plusComm
-- :~: (b + 'S a') -- plusSy
--
-- で証明できそう。
--
-- plusCommを使ってもう1度型を見てみる
--
-- plusComm (SS a) b   =
--     apply reflS (plusComm a b)
--     `trans` (undefined :: _)
--
--  a.hs|91 col 27 error| Found hole ‘_’ with type: 'S (b + a1) :~: (b + 'S a1)
--
--  なので、holeの部分にsym (plusSy b a)を入れるとギャップが埋まる
--
-- plusComm (SS a) b     =
--     apply reflS (plusComm a b)
--     `trans` sym (plusSy b a)
--     `trans` (undefined :: _)
--
-- a.hs|97 col 27 error| Found hole ‘_’ with type: (b + 'S a1) :~: (b + 'S a1)
--
-- 両辺が同じになったので`trans` (undefined :: _)を消して証明終了

plusComm (SS a) b     =
    apply reflS (plusComm a b)
    `trans` sym (plusSy b a)

type family a * b where
  'Z   * b = 'Z
  'S a * b = b + (a * b)

(.*) :: SN a -> SN b -> SN (a * b)
SZ   .* _ = SZ
SS a .* b = b .+ (a .* b)

infixl 7 .*

multL :: SN k -> x :~: y -> k * x :~: k * y
multL _ Refl = Refl

-- (a + b) + (k * (a + b))
-- (a + b) + (k * a + k * b) distr
--  a + (b + (k * a + k * b)) assoc
--  a + (b + (k * b + k * a)) comm
--  a + ((b + k * b) + k * a) assoc
--  a + (k * a + (b + k * b)) comm
-- (a + (k * a)) + (b + (k * b)) assoc

-- 分配法則
distrL :: SN k -> SN a -> SN b -> k * (a + b) :~: (k * a) + (k * b)
distrL  SZ    _  _ = Refl
distrL (SS k) a b  =
    addL (a .+ b) (distrL k a b)
    `trans` plusAssoc a b (k .* a .+ k .* b)
    `trans` addL a (addL b $ plusComm (k .* a) (k .* b))
    `trans` addL a (sym $ plusAssoc b (k .* b) (k .* a))
    `trans` addL a (plusComm (b .+ k .* b) (k .* a))
    `trans` sym (plusAssoc a (k .* a) (b .+ k .* b))

multZR :: SN a -> a * 'Z :~: 'Z
multZR  SZ    = Refl
multZR (SS a) = multZR a

-- S (b + (a * S b))
-- :~: S (b + (a + (a * b))) multSy
-- :~: S ((b + a) + (a * b)) plusAssoc
-- :~: S ((a + b) + (a * b)) plusComm
-- :~: S (a + (b + (a * b))) plusAssoc
multSy :: SN a -> SN b -> a * 'S b :~: a + (a * b)
multSy SZ     _ = Refl
multSy (SS a) b =
    apply reflS (addL b $ multSy a b)
    `trans` apply reflS (sym $ plusAssoc b a (a .* b))
    `trans` apply reflS (plusComm b a `addR` (a .* b))
    `trans` apply reflS (plusAssoc a b (a .* b))

-- (b + (a * b))
-- (b + (b * a)) multComm
-- :~: (b * S a) multSy
multComm :: SN a -> SN b -> a * b :~: b * a
multComm  SZ    b = sym $ multZR b
multComm (SS a) b =
    addL b (multComm a b)
    `trans` sym (multSy b a)

-- (a + b) * k
-- k * (a + b) multComm
-- (k * a) + (k * b) distrL
-- (a * k) + (k * b) multComm
-- :~: (a * k) + (b * k) multComm
distrR :: SN a -> SN b -> SN k -> (a + b) * k :~: (a * k) + (b * k)
distrR a b k =
    multComm (a .+ b) k
    `trans` distrL k a b
    `trans` (multComm k a `addR` (k .* b))
    `trans` ((a .* k) `addL` multComm k b)