CoqIntroを読む

前回のつづき。POPL08チュートリアルのうちの基礎部分CoqIntro.vをやってみる。

CoqIntroはboolとnatからなる式言語を定義しているが、それが興味深い表現になっている。

言語定義

まず、構文定義

Inductive tm : Set :=
| tm_true : tm
| tm_false : tm
| tm_if : tm -> tm -> tm -> tm
| tm_zero : tm
| tm_succ : tm -> tm
| tm_pred : tm -> tm
| tm_iszero : tm -> tm.

ここはまあ普通のデータ型定義だ。面白くなるのは次。bool値をあらわすデータの定義

Inductive bvalue : tm -> Prop :=
| b_true : bvalue tm_true
| b_false : bvalue tm_false.

bvalueの型が関数型になっている。まず、普通ならtmと同様Setでやりたいところなので、ここで混乱する。
そこで、いろいろCheckしてみる。

  • Check bvalue
    • : tm -> Prop
  • Check bvalue tm_true
    • : Prop
  • Check bvalue tm_zero
    • : Prop
  • Check b_true tm_true
    • The expression "b_true" of type "bvalue tm_true" cannot be applied to the term "tm_true" : "tm"
  • Check b_true
    • : bvalue tm_true

b_true : bvalue tm_true : Propとなってる関係が見える。Propなので即真か偽かになるわけではなく、Propデータと見たほうがいいようだ。Prop->boolにする判定自体はどうするのかまだわからない。

bvalue tm_trueは何らかのデータで、b_trueはそのデータに属すというシンボルとして見てもいいのかな。(bvalue tm_true)を表現するオブジェクトがb_trueというふうに。

また、別の視点でbvalueという型のパラメータとしてtm_trueやtm_falseしか入らないと考えると、なんとなくGADTを思い出す(値そのものは型パラメータに使えなかったとは思うが):

data TrueT
data FalseT
class BoolT t ...
instance BoolT TrueT where ...
instance BoolT FalseT where ...

data Tm t where
  TmTrue :: Tm TrueT
  TmFalse :: Tm FalseT
  ...

data BValue t where
  BTrue :: BValue (Tm TrueT)
  BTrue :: BValue (Tm FalseT)

GADTでは、どこかでパラメータ型の値を取り出す関数が定義されるが、これはあまり考えにくいかも。


でつぎが数値のデータ定義

Inductive nvalue : tm -> Prop :=
| n_zero : nvalue tm_zero
| n_succ : forall t,
    nvalue t ->
    nvalue (tm_succ t).

bvalueに似ているが、n_succでforallが出てくる。ここでもCheck。

  • Check n_zero
    • : nvalue tm_zero
  • Check nvalue tm_zero
    • : Prop
  • Check nvalue tm_true
    • : Prop
  • Check n_succ
    • : forall t : tm, nvalue t -> nvalue (tm_succ t)
  • Check forall t : tm, nvalue t -> nvalue (tm_succ t)
    • Prop

forall t:tm, nvalue t -> nvalue (tm_succ t)がPropになるのは最後のnvalue (tm_succ t)がPropだからだろう。この式自体は任意のtm型のtに対して生成される型で、nvalue tつまりPropから、nvalue (tm_succ t)つまりPropを返す型を生成するという感じなのだろう。ということは、n_succはtm型の式を受け取ることができると予想できる。

  • Check n_succ tm_zero
    • : nvalue tm_zero -> nvalue (tm_succ tm_zero)
  • Check n_succ tm_zero n_zero
    • : nvalue (tm_succ tm_zero)
  • Check n_succ tm_true
    • : nvalue tm_true -> nvalue (tm_succ tm_true)
  • Check n_succ tm_true n_zero
    • Error: The term "n_zero" has type "nvalue tm_zero" while it is expected to have type "nvalue tm_true"

というように式として成り立てる。n_succ (tm_succ tm_zero)なども同様にできあがってるものとみなせるが、たぶんその第二引数に使える構造は(n_succ tm_zero n_zero)だけになる。
bvalueでつけたProp解釈でいうと、nvalue tにあたるPropを受け取ってnvalue (tm_succ t)にあたるPropを返す関数オブジェクトが(n_succ t)ということになる。

このnvalueを先のようにGADT風に考えるとどうなるかな。

data Zero = Zero
data Succ a = Succ a
class NatT t where ...
instance NatT Zero where ...
instance (Nat a) => NatT (Succ a) where ...

data Tm t where
  TmZero :: Tm Zero
  TmSucc :: Tm a -> Tm (Succ a)
  ...

data NValue t where
  NZero :: NValue (Tm Zero)
  NSucc :: (Nat aT) => (Tm a) -> NValue (Tm a) -> NValue (Tm (Succ a))

NSuccの引数はTmなのでそろそろくるしいか。

次はvalueの定義。

Definition value (t : tm) : Prop :=
  bvalue t \/ nvalue t.

これはあまり不思議ではないが、\/はboolの計算ではなくPropの連結で、結果は連結したPropデータ。value tが式かどうかを判定するデータ。bvalueとnvalueでパターン的に無理そうな気もするが

つぎはeval。これも最終的にPropを作るInductiveで定義している。

Inductive eval : tm -> tm -> Prop :=
| e_iftrue : forall t2 t3,
    eval (tm_if tm_true t2 t3) t2
| e_iffalse : forall t2 t3,
    eval (tm_if tm_false t2 t3) t3
| e_if : forall t1 t1' t2 t3,
    eval t1 t1' ->
    eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)
| e_succ : forall t t',
    eval t t' ->
    eval (tm_succ t) (tm_succ t')
| e_predzero :
    eval (tm_pred tm_zero) tm_zero
| e_predsucc : forall t,
    nvalue t ->
    eval (tm_pred (tm_succ t)) t
| e_pred : forall t t',
    eval t t' ->
    eval (tm_pred t) (tm_pred t')
| e_iszerozero :
    eval (tm_iszero tm_zero) tm_true
| e_iszerosucc : forall t,
    nvalue t ->
    eval (tm_iszero (tm_succ t)) tm_false
| e_iszero : forall t t',
    eval t t' ->
    eval (tm_iszero t) (tm_iszero t').

定義自体には、eval a bがパターンaならbに評価するルールとみなせ、簡約っぽい雰囲気がある。証明としては命題にあたる部分は型におくのはわかってはいるが、直感的に納得しにくいのは、チェックのためのパターンマッチだけでしか使わないというふうにはわりきらず、プログラムのデータ値としてどうなるのか想像しようとしてできにくいところだったりする。

とりあえずCheck.

  • Check: eval tm_true tm_zero
    • : Prop
  • Check e_iftrue tm_zero tm_false
    • : eval (tm_if tm_true tm_zero tm_false) tm_zero
  • Check eval (tm_if tm_true tm_zero tm_false) tm_zero
    • : Prop

bvalue,nvalueと同じような違和感があるが、まあいいか。ここまでくるとGADT風にはもう書けないな。

eval_manyもうよくわからない。

Inductive eval_many : tm -> tm -> Prop :=
| m_refl : forall t,
    eval_many t t
| m_step : forall t t' u,
    eval t t' ->
    eval_many t' u ->
    eval_many t u.
  • Check m_refl tm_true
    • : eval_many tm_true tm_true
  • Check m_step tm_zero tm_true tm_false
    • : eval tm_zero tm_true -> eval_many tm_true tm_false -> eval_many tm_zero tm_false

帰納的定義ではあるが、もう理解不能。

簡約不能をあらわす正規形になってるかどうかの判定normal_form

Definition normal_form (t : tm) : Prop :=
  ~ exists t', eval t t'.

evalの右側に相当するものが無いと正規形。

証明

定義の後半はよくわからない状態になったけど、証明に進む。

補題1. 

Lemma e_succ_pred_succ : forall t,
  nvalue t ->
  eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t).

これは簡単だが、前日と違い、autoでは解決しない。

intro t.
intro H.
apply e_succ.
apply e_predsucc.
exact H.

coqtopログ

Coq < Lemma e_succ_pred_succ : forall t,
  nvalue t ->
  eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t).
1 subgoal

  ============================
   forall t : tm,
   nvalue t -> eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

e_succ_pred_succ < intro t.
1 subgoal

  t : tm
  ============================
   nvalue t -> eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

e_succ_pred_succ < intro H.
1 subgoal

  t : tm
  H : nvalue t
  ============================
   eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

e_succ_pred_succ < apply e_succ.
1 subgoal

  t : tm
  H : nvalue t
  ============================
   eval (tm_pred (tm_succ t)) t

e_succ_pred_succ < apply e_predsucc.
1 subgoal

  t : tm
  H : nvalue t
  ============================
   nvalue t

e_succ_pred_succ < exact H.
Proof completed.

e_succ_pred_succ < Qed.
intro t.
intro H.
apply e_succ.
apply e_predsucc.
exact H.
e_succ_pred_succ is defined

e_succ_pred_succ <

apply e_succは、明示的に引数を指定すると、

apply e_succ with (t := (tm_pred (tm_succ t))) (t' := t)

ということになる。こうすると、

eval (tm_pred (tm_succ t)) t -> eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

に変換されるので、->の右辺の現証明対象が成り立つには->の左辺の仮定側が成り立っていればよいことになり、証明対象は仮定側の

eval (tm_pred (tm_succ t)) t

に入れ替わる。


補題2.

Coq < Lemma m_succ_pred_succ : forall t,
  nvalue t ->
  eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).
1 subgoal

  ============================
   forall t : tm,
   nvalue t -> eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

m_succ_pred_succ <

証明。これもautoではむり。

m_succ_pred_succ < intro t.
1 subgoal

  t : tm
  ============================
   nvalue t -> eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

m_succ_pred_succ < intro H.
1 subgoal

  t : tm
  H : nvalue t
  ============================
   eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

m_succ_pred_succ <

intro二回でforallと->が消え、次にパターン的にapply m_stepになるのはわかる。が、m_stepは3引数

| m_step : forall t t' u,
    eval t t' ->
    eval_many t' u ->
    eval_many t u.

であり、t := (tm_succ (tm_pred (tm_succ t))), u := (tm_succ t)はすぐわかるが、t'はパターン内には直接埋まっていないため、明示的にt'を与える必要がある。つまり、eval (tm_succ (tm_pred (tm_succ t))) t'さらにパターンで分解できるようなt'を探す。これは先の補題1 e_succ_pred_succの->の右辺が、eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t) であることを覚えていれば、t' := tm_succ tを与えればいいことがわかる。

m_succ_pred_succ < apply m_step with (t' := (tm_succ t)).
2 subgoals

  t : tm
  H : nvalue t
  ============================
   eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)

subgoal 2 is:
 eval_many (tm_succ t) (tm_succ t)

m_succ_pred_succ <

m_stepには->が二つあるので満たさなくてはいけない仮定であるsubgoalは二つできる。

また、applyはパターンとしても書けて、

apply (m_step (tm_succ (tm_pred (tm_succ t))) (tm_succ t) (tm_succ t)) .

でもいい。


あとはそのまま、

m_succ_pred_succ < apply e_succ_pred_succ.
2 subgoals

  t : tm
  H : nvalue t
  ============================
   nvalue t

subgoal 2 is:
 eval_many (tm_succ t) (tm_succ t)

m_succ_pred_succ < exact H.
1 subgoal

  t : tm
  H : nvalue t
  ============================
   eval_many (tm_succ t) (tm_succ t)

m_succ_pred_succ < apply m_refl.
Proof completed.

m_succ_pred_succ < Qed.
auto.
intro t.
intro H.
apply m_step with (t' := tm_succ t).
 apply e_succ_pred_succ.
   exact H.
apply m_refl.
m_succ_pred_succ is defined

Coq <
練習用補題

証明戦略としては

  • introできるまでintro
  • その後は定義や補題からゴールの形になっているパターンを探してapplyしていく
    • applyする場合で引数が必要なときは、次のパターン展開できそうなパターンを探して使う
  • ゴールと同じものが仮定中にあれば、exact
Coq < Lemma m_one : forall t1 t2,
  eval t1 t2 ->
  eval_many t1 t2.
1 subgoal

  ============================
   forall t1 t2 : tm, eval t1 t2 -> eval_many t1 t2

m_one < intros t1 t2 H.
1 subgoal

  t1 : tm
  t2 : tm
  H : eval t1 t2
  ============================
   eval_many t1 t2

m_one < auto.
1 subgoal

  t1 : tm
  t2 : tm
  H : eval t1 t2
  ============================
   eval_many t1 t2

m_one < apply (m_step t1 t2 t2).
2 subgoals

  t1 : tm
  t2 : tm
  H : eval t1 t2
  ============================
   eval t1 t2

subgoal 2 is:
 eval_many t2 t2

m_one < exact H.
1 subgoal

  t1 : tm
  t2 : tm
  H : eval t1 t2
  ============================
   eval_many t2 t2

m_one < apply (m_refl t2).
Proof completed.

m_one < Qed.
intros t1 t2 H.
auto.
apply (m_step t1 t2 t2).
 exact H.
apply (m_refl t2).
m_one is defined

Coq <

Coq < Lemma m_two : forall t1 t2 t3,
  eval t1 t2 ->
  eval t2 t3 ->
  eval_many t1 t3.
1 subgoal

  ============================
   forall t1 t2 t3 : tm, eval t1 t2 -> eval t2 t3 -> eval_many t1 t3

m_two < intros t1 t2 t3 H H1.
1 subgoal

  t1 : tm
  t2 : tm
  t3 : tm
  H : eval t1 t2
  H1 : eval t2 t3
  ============================
   eval_many t1 t3

m_two < apply (m_step t1 t2 t3).
2 subgoals

  t1 : tm
  t2 : tm
  t3 : tm
  H : eval t1 t2
  H1 : eval t2 t3
  ============================
   eval t1 t2

subgoal 2 is:
 eval_many t2 t3

m_two < exact H.
1 subgoal

  t1 : tm
  t2 : tm
  t3 : tm
  H : eval t1 t2
  H1 : eval t2 t3
  ============================
   eval_many t2 t3

m_two < apply (m_step t2 t3 t3).
2 subgoals

  t1 : tm
  t2 : tm
  t3 : tm
  H : eval t1 t2
  H1 : eval t2 t3
  ============================
   eval t2 t3

subgoal 2 is:
 eval_many t3 t3

m_two < exact H1.
1 subgoal

  t1 : tm
  t2 : tm
  t3 : tm
  H : eval t1 t2
  H1 : eval t2 t3
  ============================
   eval_many t3 t3

m_two < apply (m_refl t3).
Proof completed.

m_two < Qed.
intros t1 t2 t3 H H1.
apply (m_step t1 t2 t3).
 exact H.
apply (m_step t2 t3 t3).
 exact H1.
apply (m_refl t3).
m_two is defined

Coq <

Coq < Lemma m_iftrue_step : forall t t1 t2 u,
  eval t tm_true ->
  eval_many t1 u ->
  eval_many (tm_if t t1 t2) u.
1 subgoal

  ============================
   forall t t1 t2 u : tm,
   eval t tm_true -> eval_many t1 u -> eval_many (tm_if t t1 t2) u

m_iftrue_step < intros t t1 t2 u H H1.
1 subgoal

  t : tm
  t1 : tm
  t2 : tm
  u : tm
  H : eval t tm_true
  H1 : eval_many t1 u
  ============================
   eval_many (tm_if t t1 t2) u

m_iftrue_step < apply (m_step (tm_if t t1 t2) (tm_if tm_true t1 t2) u).
2 subgoals

  t : tm
  t1 : tm
  t2 : tm
  u : tm
  H : eval t tm_true
  H1 : eval_many t1 u
  ============================
   eval (tm_if t t1 t2) (tm_if tm_true t1 t2)

subgoal 2 is:
 eval_many (tm_if tm_true t1 t2) u

m_iftrue_step < apply e_if.
2 subgoals

  t : tm
  t1 : tm
  t2 : tm
  u : tm
  H : eval t tm_true
  H1 : eval_many t1 u
  ============================
   eval t tm_true

subgoal 2 is:
 eval_many (tm_if tm_true t1 t2) u

m_iftrue_step < exact H.
1 subgoal

  t : tm
  t1 : tm
  t2 : tm
  u : tm
  H : eval t tm_true
  H1 : eval_many t1 u
  ============================
   eval_many (tm_if tm_true t1 t2) u

m_iftrue_step < apply (m_step (tm_if tm_true t1 t2) t1 u).
2 subgoals

  t : tm
  t1 : tm
  t2 : tm
  u : tm
  H : eval t tm_true
  H1 : eval_many t1 u
  ============================
   eval (tm_if tm_true t1 t2) t1

subgoal 2 is:
 eval_many t1 u

m_iftrue_step < apply e_iftrue.
1 subgoal

  t : tm
  t1 : tm
  t2 : tm
  u : tm
  H : eval t tm_true
  H1 : eval_many t1 u
  ============================
   eval_many t1 u

m_iftrue_step < exact H1.
Proof completed.

m_iftrue_step < Qed.
intros t t1 t2 u H H1.
apply (m_step (tm_if t t1 t2) (tm_if tm_true t1 t2) u).
 apply e_if.
   exact H.
apply (m_step (tm_if tm_true t1 t2) t1 u).
 apply e_iftrue.
exact H1.
m_iftrue_step is defined

Coq <

ちなみにcoqtopでのアンドゥはUndo.になる。

今日は、ここまで。