【番外編】定理証明手習いをAgdaで

定理証明手習い

番外編ということで、定理証明手習いをAgdaでやってみた。
最初は、組み込み関数を普通に定義して、公理をpostulateで定義した。
そしたら問題が発生。

以下を考える。

data Star : Set where
  NIL : Star
  TRU : Star
  N   : Nat → Star
  S   : String → Star
  C   : Star → Star → Star

ATOM : Star → Star
ATOM (C _ _) = NIL
ATOM _ = TRU

ATOMを使った証明にxs:Starを引数とすると、
xsをコンストラクタでばらせないから、ATOMが計算できず、エラーになる。
引数にC x yとか渡さないといけない。これはやりたくない。

• Reasoningを使った証明もしんどかった。

長いSchemeの定理を何度も書かないといけない。
congの位置合わせも手間だった。

というわけで全部postulateにした。
証明もrewriteを使うようにした。
これなら書けるかもしれない。

rewriteで証明ステップが5つくらい一気に進んだのは謎。

ソースはこちらです。
TLP01.agdaボツネタ
TLP02.agda