こわくない Idris (6)

表明から証明へ (3)

headを証明する

HaskellのPrelude.headとは異なり、IdrisのPrelude.List.headは、引数にコンスセルである証明をとるので、全域函数になっている。Idrisのシステムでは次のように、%assert_total宣言によって、全域函数であることが「表明」されている。

%assert_total
head : (l : List a) -> (isCons l = True) -> a
head (x::xs) p = x

ここでは、自分でhead函数が全域函数であることを「証明」をしてみよう。

%default total

namespace MyHead
  head : (l : List a) -> (isCons l = True) -> a
  head Nil prf = FalseElim (replace {P=P} prf ())
    where
      P : Bool -> Type
      P False = ()
      P True = _|_
  head (x :: xs) _ = x

head函数の第1引数はList a型なので、Nilのケースと(x :: xs)のケースとがある。NilのケースではBuiltins.idrで定義されている次の函数を使っている。

FalseElim : _|_ -> a
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

対話型証明をしたかった

Idrisで対話型証明する話を書こうとしたけどIdrisのtacticがCoqと比べて非常に貧弱な感じだし、おとなしくCoq使えばいいと思います……また今度詳しく書きます。