日々の流転

λ. RHG読書会::東京 Revolution::ふつうのLinuxプログラミング 第八回

RHGは Ruby・Haskell・Gauche の略だそうです。

λ. length xs + length ys = length (xs ++ ys) の証明

RHG読書会の飲み会で即興で書いた証明。

--#include "Hedberg/SET.alfa"
--#include "Hedberg/Op/Nat.alfa"
open SET use Id, refId, mapId, Nat
open OpNat use zero, succ, (+)

(++) (|X::Set) (xs::List X) (ys::List X) :: List X
  = case xs of 
    (Nil    )-> ys
    (x : xs')-> x : (xs' ++ ys)

length (|X::Set) (xs::List X) :: Nat
  = case xs of 
    (Nil    )-> zero
    (x : xs')-> succ (length xs')

prop (|X::Set) (xs::List X) (ys::List X)
  :: Id (length xs + length ys) (length (xs ++ ys))
  = case xs of 
    (Nil    )-> refId (length ys)
    (x : xs')-> mapId succ (prop xs' ys)