Arantium Maestum

プログラミング、囲碁、読書の話題

Logical Foundationsの2章まで読んだ＆Coqこと始め雑感

Coq Software Foundations

Coqでソフトウェア工学の基礎をいろいろ証明するよという趣旨（多分？）のSoftware Foundationsというウェブ上で読める教科書シリーズがある。

softwarefoundations.cis.upenn.edu

第1巻Logical FoundationsはそのままCoqの教科書になっている。これを読み進めていきたい。

とりあえず最初の2章までできたので（ただし最後の問題はいったん飛ばした・・・）、復習がてら雑感をメモ。

Fixpoint

再帰的な関数をFixpointで定義できる。例えばペアノ数として定義されているcoqの自然数の足し算：

Fixpoint add (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => add n' (S m)
  end.

coqでは停止性が自明な関数しか書けない。その自明性もかなり粗いチェックになっていて、再帰のたびに必ず構造的に小さくなっていく引数が必要になる。上記のadd関数では停止するまで第一引数が必ず小さくなっていく（Sが一つずつ外されていく）。

こういう関数すら許容されない：

Fixpoint one (n : nat) : nat :=
  match n with
  | O => one (S n)
  | _ => S O
  end.

one (S n)と引数が大きくなるような再帰は（人間の目からは自明に停止する関数でも）弾かれてしまう。

この制約でどううまく記述していくかはまだ慣れが必要（第2章最後の演習問題がそこで詰まっている・・・）

tactics

Fixpointを含むプログラミング構文で記述した関数などについての命題をtacticsを組み合わせて証明していくのがCoqの主眼。

第２章までで出てくるtactics：

  • intros
  • simpl
  • reflexivity
  • rewrite
  • destruct
  • induction
  • assert
  • replace

今のところ出てきたtacticsだと、contextにH : c = trueが入っていてgoalもc = trueだとrewrite -> H. reflexivityとやってgoalをtrue = trueに変換してから自明に左右が同値だと指摘しないといけないのだけど、非常に冗長。多分contextとgoalが同じだと指摘するtacticsがあるはず・・・　

assertとreplaceの使い分けがまだよくわかっていない。

assertは同じ証明の中で複数回使いたいような（でも完全に別の証明に分けるほどではない）補題のためにあるのかな。

Logical Foundationsではassertの方が先に出てくるので演習などでそっちを使いまくっていて、その後replaceを知って書き直して少し簡潔になったケースが多かった。

ただ、

こう書いたとおり、assertを使うとその場で導入した補題をsubgoalとして証明するのに対して、replaceだとその正当性を証明するのは当面のsubgoalの後になるので、証明の流れがわかりにくい気がする。

spacemacs develop branch

Clojureの関係でspacemacsのdevelop branchに切り替えたらそれまで不安定だったcompany-coqの補完機能の問題が全部解決した（以前は行末をm.で終わらせると自動的にmatch ....に補完されるなど非常にめんどくさかった・・・）

practicalli.github.io

多分この記事：

zehnpaard.hatenablog.com

に書いた手動でいじらないといけない部分も全部解決しているっぽい。spacemacsはdevelop branchを使うのがかなりベターなようだ。

和、積の法則の証明

演習問題に出てきた、自然数の和と積に関して交換則、結合則、分配則などの証明：

Coq proofs for addition/multiplication laws based on Software Foundations · GitHub

ゲーム性が高くて非常に楽しい。