Zenn
Open10

Coqに入門してみる

coq
SphendamiSphendami

ここを使う：
https://softwarefoundations.cis.upenn.edu/
和訳版もあったけど微妙に古かった。

Coq自体はopam on WSL2でインストールした。
IDEはEmacs上のProof GeneralとスタンドアロンのCoqIDE（Coq付属）が書かれていたが、慣れ親しんだVSCode（+拡張機能vscoq）でやってみる。

SphendamiSphendami

Basics

  • Inductive day : Type := の Type は何だろ（無くても推論されるっぽい）
    • ⇒ 多相型は Inductive list (X:Type) : Type := みたいに定義。依存型もできそう
    • ⇒ 帰納的な命題も Inductive を使って定義（e.g. Inductive ev : nat -> Prop := ... ）。（IndProp参照）
  • 呪文のように出てくる Proof. simpl. reflexivity. Qed.
    • ⇒ simplは両辺の計算を進める（無くても reflexivity がやってくれる）。reflexivityは両辺が等価かチェックする（反射律）。
  • Example hoge := でなく Example hoge : 。 = が付いていてもExample自体はエラー出ない（Proofでエラー出る）
    • ⇒ 定理名はその定理の証明（proof object）を参照しており、言明自体は定理名の型である。なので(?)、 := でなく :。カリー・ハワード対応。（ProofObjects参照）
    • Theorem hoge := などExample以外での := はエラー。Exampleは真でなくてもいいから？
  • Notationはマクロではない？
  • (b0 b1 b2 b3 : bit)
    • ⇒ (b0 : bit) (b1 : bit) (b2 : bit) (b3 : bit) の略記
  • True はPropで true はbool
    • ⇒ Logic#Propositions vs. Booleansとその次で違い・利点欠点の説明有り
  • forall n に対して intros m でもいいのは先頭から埋めてくから？
    • ⇒ そうっぽい。名づけをしている感じ（仮定 H はその後の証明で「 H 」で参照できる）
  • 含意の左辺（仮定）がFalseだった場合に直接含意をTrueに判定できるtacticありそう
    • ⇒ discriminate tacticが使える。（Tactics#The injection and dicsriminate Tactics参照）
    • ⇒ H: False に対して destruct H で、サブゴールが0になるのでQED.（Logic#Falsehood and Nagation参照）
  • 組み込みの比較演算子は？
    • ⇒ From Coq Require Import Arith.Arith. すれば <=? などが使える
SphendamiSphendami

Indcution

  • Exercise mul_comm ちょっと詰まった。サブ定理で量化するか否かの違いだった
    • ⇒ Tactics#Varying the Induction Hypothesisでそれに近いことが解説されてる
  • 定義済みの定理一覧欲しい
    • ⇒ Search (_ + _ = _ + _). などで定理検索可（List#Search参照）
  • 関数の中身見たい
    • ⇒ Compute <関数名> で見れる（再帰がfix使ってたり関数が展開されてたりはする）
    • ⇒ それよりも Print <関数名> で正に中身を見れる。
SphendamiSphendami

Lists

  • 任意長のリストもNotationできるの面白い
  • n + 1 を S n に書き換えるのは、可換（add_comm）を示せば rewrite add_comm. simpl. でいける（加算の定義は左辺でmatchingしてるので具体的な項を左辺に持ってくればsimplificationできる）
SphendamiSphendami

Poly

  • Inductive list' {X:Type} : Type := としたときの問題
    • ⇒ X が具体的に判明していようがいまいが list' で表示される
      • cons' 1 nil' : list'
      • (nil' : @list' nat) : list'
      • nil' : list'
      • c.f. nil: list ?X, (nil : list nat) : list nat
  • 扱いの違い
    • Compute nil. → = nil : list ?X
    • Check nil. → nil : list ?X where ?X : [ |- Type]
    • Definition mynil := nil. → The following term ...
SphendamiSphendami

Tactics

  • generalize dependent x の dependent は何？
    • ⇒ x に依存するものも移動させるらしい
SphendamiSphendami

Logic

  • H: ~ P をdestructすると、現在のゴールを無視して P というサブゴールだけになる
    • ⇒ P がTrueであることを示せれば、 H はFalseすなわちcontradiction。
  • apply H1. apply H2. apply H3 を apply H1 H2 H3 みたいに書けないか（ rewrite も）
    • ⇒ apply H1, H2, H3 でいけた
  • /\ と \/ は右結合、なぜ？
    • ⇒ splitで左から1つずつはがせる
    • ⇒ 証明の自動化の際に利便性がわかりやすい。左から1つずつleftを試して剥がしていける（Imp#Coq Automation参照）
  • tr_rev_correct少し詰まった。 tr_rev l （すなわち rev_append l [] ）は特殊な形なので、より一般的な形にした言明を示してそれを適用する。
  • excluded_middle_irrefutableは本当に試行錯誤。
    • 必要なassertionは複雑なものではなくとてもシンプルなもの。
    • H: P \/ ~P -> False はassertionの証明にも使うし、assertionを証明した後にももう一回使う。
  • classical_axiomsも試行錯誤。
    • 含意のループを作れとヒントがあるけど、それでさえループの候補は 5!/5 = 24 通りもある。結局、とりあえず成り立ちそうな含意を片っ端から示していくのがよい。
    • A -> B を示したいときに「仮定に A だけじゃなくて C もあればいけるのにな」となったら、とりあえず A /\ C -> B を示して、そのあと別に A -> C も示せれば、両者から A -> B が示せる。
SphendamiSphendami

IndProp

  • 仮定 H: S n <= S m をinductionしたときの第1ケースで仮定 n = m （ないしは S n = S m ）は生成されないが、inversionすれば n = m は生成される
    • ⇒ S n と S m をrememberすればinductionでもいける（IndProp#The remember Tactic参照）
  • subseq_trans、試行錯誤を経て何とか解けた。何で？
  • H1: P と H2: P -> Q があるときに apply H2 in H1 すると H1 が消えてしまう。（backwardでやればいいのでは？ ⇒ Q が exists x, ... の形の場合 x を文脈に持ってくるためにはforwardでないとだめそう。）仮定を複製する組み込みtacticない？（assertしたり自前で P -> P /\ P を用意すればいけるけど）
    • ⇒ apply H2 in H1 as H1' でいいじゃん
  • 証明中に脈絡なく thm: P \/ Q を使って場合分けしたい場合は destruct thm すればよい
    • ⇒ 一般に、脈絡なく thm: P を仮定に持ってきたいときはassertすればよい
  • inversionすると名づけられない等式が生成されることがある
    • ⇒ 等式らは [EQ1 EQ2] のようにまとめてあげることで名づけられる
  • 鳩の巣原理の問題中のrepeatsは問題説明が良くない気がする。「要素がrepeatしている」はその要素が連続している印象があるけど、ここでは連続している必要はない。どちらかと言えばduplicates。
  • asciiのbool比較は eqb 、そのPropへの反映は eqb_spec （調べた）。これ使わなくても行けるのか...？
  • x <> y にsymmetryを使いたい
SphendamiSphendami

Maps / ProofObjects / IndPrinciples / Rel

特になし

Imp

  • Set Printing Implicit. とは

Auto

  • Hint Transparent とは

ImpCEvalFun / ImpParser / Extraction

特になし

SphendamiSphendami

Volume 1 読了。

  • ある程度Coqを扱えるようになった。
  • 上のコメント量の差の通り、IndPropsまでは時折立ち止まることが多かった一方それ以降はスムーズに進められた。
  • 関数型言語に触れたことのある人にとっては、序盤は関数型言語一般の話も割とあるのでやや冗長ぎみ。
  • ProofObjectsとIndPrinciplesは、Recommended pathには入ってないけど読んでおいた方がいい気がする。
  • 主だった概念の紹介はImp前までで、Imp以降は応用・自動化の話。