Hatena::ブログ(Diary)

みずぴー日記

2011-12-05(月)

Show Scriptコマンドによる証明の整形

| Show Scriptコマンドによる証明の整形 - みずぴー日記 を含むブックマーク

(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)

Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。

そんなときは、Show Scriptコマンドで整形すると楽になります。

例: 読みにくい証明

例として次のようなリストに関する補題証明するときのことを考えてみます。

Require Import List.

Lemma rev_app_distr : forall A (x y:list A), 
  rev (x ++ y) = rev y ++ rev x.

Focusを使ってサブゴールを移動しながら証明したり、インデントなしで場合分けの証明したりすると、こんな感じの読みづらい証明になってしまいます。

Proof.
induction x as [| a l IHl].
destruct y as [| a l].
Focus 2.
simpl.
rewrite app_nil_r.
auto.
Show.
simpl.
auto.
intro y.
simpl.
rewrite (IHl y).
rewrite app_assoc.
trivial.
Qed.

Show Scriptコマンドによる証明の整形

そんなときは、Qedの直前にShow Scriptコマンドを使うと、次のような整形した証明を出力できます。

induction x as [| a l IHl].

 destruct y as [| a l].
  simpl.
  auto.
 
  simpl.
  rewrite app_nil_r.
  auto.
 
 intro y.
 simpl.
 rewrite (IHl y).
 rewrite app_assoc.
 trivial.

Focusによるサブゴールの入れ替えを元に戻して、場合分けごとにインデントしてくれます。

ただ、"現在の証明"に対してしか使えないのでQedする前でないと使えませんし、コメントはすべて消えてしまいます。

おまけ: そのほかのShow XXXコマンド

ちなみに、Show Script以外にも、証明木を表示するShow Treeコマンドもおもしろいです。

先ほどの証明をShow Treeすると、次のような証明木を出力できます。

 BY induction x as [| a l IHl]   
    A : Type
    ============================
     forall y : list A, rev (nil ++ y) = rev y ++ rev nil
 
   BY Evar change
     
      ============================
       forall y : list A, rev (nil ++ y) = rev y ++ rev nil
   
     BY destruct y as [| a l]
       
        ============================
         rev (nil ++ nil) = rev nil ++ rev nil
     
       BY Evar change
         
          ============================
           rev (nil ++ nil) = rev nil ++ rev nil

      ….

まとめ

Show Scriptコマンドで証明を整形すると、たのしいですよ。

2010-01-13(水)

Coqのモジュール間の依存関係を可視化するスクリプトを書いたよ

| Coqのモジュール間の依存関係を可視化するスクリプトを書いたよ - みずぴー日記 を含むブックマーク

f:id:mzp:20100113073200p:image

こんな感じの画像を生成してくれます。リファクタリングのお供にどうぞ。

何をやるの?

  • coqdepの出力をdotファイルに変換する
  • dotファイルをGraphvizで画像に変換する

使い方

$ coqdep -I . *.v | ruby depends.rb > depend.dot
$ dot -Tpng -o depend.png depend.dot

ソースコード

昔、OCamlモジュール間の依存関係を可視化したときのスクリプト(haXeのファイル間の依存関係 - Happy OCaml!! - ocaml-nagoyaグループ)の焼き直しです。

puts 'digraph depend{'

ARGF.read.gsub(/\\\n/,'').each do|line|
  file,depends = line.split ':',2
  if file =~ /\.v/
    depends.split.each do |x|
      puts "#{File.basename file,'.*'} -> #{File.basename x,'.*'}"
    end
  end
end

puts '}'

2010-01-08(金)

Coqで健全性と完全性の証明をしたよ

| Coqで健全性と完全性の証明をしたよ - みずぴー日記 を含むブックマーク

Coqでラムダ計算を証明してみた - みずぴー日記の続けて、単純型付きラムダ計算の型推論(Type reconstruction)に関する定理の証明をしてました。

そして、とうとう健全性と完全性の証明ができました! やったね!

ただ、完全性の証明が1000行を越えてしまったので、今がんばってリファクタリングしてます。似たような証明を何度もした気がするので、きっと短かくなります。

2009-11-30(月)

Coqを落すコード

| Coqを落すコード - みずぴー日記 を含むブックマーク

Coqを使っていたら、coqcを落すコードに出会ってしまいました。

コード

Require Import Sets.Ensembles.

Variable (P: Prop).
Variable (A: Type).

Hypothesis the_hypo :
  forall x, exists xs, In A xs x -> P.

Theorem some_theorem :
  P -> P.
Proof.
intros.
apply the_hypo in H.
(* Anomaly: uncaught exception Not_found. Please report. *)

症状

これをコンパイルしようとすると、コンパイラが落ちます。

$ coqc bug.v
File "./bug.v", line 13, characters 0-19:
Anomaly: uncaught exception Not_found. Please report.

動作環境

ちなみにCoqはSnowLeopardで動いてます。

$ coqc -v
The Coq Proof Assistant, version 8.2pl1 (October 2009)
compiled on Oct 31 2009 09:59:41 with OCaml 3.11.1

わかってること

apply the_hypo in H.はダメだけど、apply the_hypo in |- *.は平気です。

2009-11-23(月)

Coqでラムダ計算を証明してみた

| Coqでラムダ計算を証明してみた - みずぴー日記 を含むブックマーク

f:id:mzp:20091122200215j:image

前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。

動機

  • let多相の実装はしたから、次は証明だろ
  • 最近、流行っているCoqを覚えたい

扱えるラムダ式

型は、Bool型と関数型のみ。

Inductive type : Set :=
  | BoolT : type
  | FunT  : type -> type -> type.

式は、変数参照、真偽値、ラムダ(関数抽象)、関数適用、if式。

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term
  | If      : term -> term -> term -> term.

証明した定理

型が付くなら、それは値か評価できるかのどちらか。

Theorem Progress : forall t r,
  Typed t empty_env r -> Value t \/ (exists t', Eval t t').

評価しても型は代わらない。

Theorem preservation: forall t t' tenv T,
  Typed t tenv T -> Eval t t' -> Typed t' tenv T.

あと、これを証明するのに必要な補題を何個か証明しています。

ソースコード

詳しい証明のついたソースコードはgithubにあります。

http://github.com/mzp/lambda/tree/simple-typed

参考文献

Types and Programming Languages (The MIT Press)

Types and Programming Languages (The MIT Press)

元ネタ。

Coqの本。Coqの中の話がメインらしいですが、ボクはタクティクスの利用例集としてぐらいしか、使えていません。

プログラミング言語の基礎理論 (情報数学講座)

プログラミング言語の基礎理論 (情報数学講座)

TAPLで納得できないところは、こっちで確認してました。特に、変数束縛が発生する場合のsubstitutionの定義でお世話になりました。

日本語なのにTAPLより難しく感じました。

絶版していて手にいれれなかったので、図書館で借りてコピーしました。

感想

  • straightforwardはやめてください。難しいよ、その証明(><)
  • 一発で正しい定義はなかなかできない。(Coqのおかげで見つけれたバグ - みずぴー日記)
  • さらっと「変数は重複して登場しないものとする」って書かないで! 難しいよ、その証明(><)

2009-10-28(水)

今日のCoq: InductiveなProp

| 今日のCoq: InductiveなProp - みずぴー日記 を含むブックマーク

定理の中で使うProp(命題)は、関数的に定義するよりも、Inductiveに定義したほうが証明が楽らしいですよ。

要約

  • Inductiveに定義したPropのほうが使いやすいらしい
  • Inductiveに定義したPropの各名前は、applyできる
  • Inductive Xを定義するとX_indが自動で定義される

前提

こんな簡単なラムダ式があると思ってください。

Inductive type : Set :=
    BoolT : type
  | FunT  : type -> type -> type.

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term
  | If      : term -> term -> term -> term.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  | If _ _ _ =>
      false
  end.

ダメなPropの例

true/falseを返すかわりに、True/Falseを返すだけのやつ。

Definition value (t : term) : Prop :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      True
  | Apply _ _  | If _ _ _ =>
      False
  end.

イイPropの例

値とは何かを、帰納的(Inductive)に定義している。

Inductive Value  : term -> Prop :=
  | ValVar    : forall s : string, Value (Var s)
  | ValBool   : forall b : bool,   Value (Bool b)
  | ValLambda : forall (x : string) (ty : type) (body : term), Value (Lambda x ty body).

ここで与えたValVarとかいう名前は証明するときに使うので、覚えやすいのにするといいでしょう。

じゃあ、これを使って証明してみよう!(その1)

試しに、こんなんを証明してみましょう。

Theorem is_value_is_Value :
  forall t : term, is_value t = true -> Value t.

ようするに、is_value関数が正しく定義されているか証明したいわけです。

まずは、tについて場合分けします。Inductiveに定義されたデータ型は、inductionを使うよりdestructを使って場合分けしたほうがいいらしいです。

is_value_is_Value < destruct t.
5 subgoals

  s : string
  ============================
   is_value (Var s) = true -> Value (Var s)

subgoal 2 is:
 is_value (Bool b) = true -> Value (Bool b)
subgoal 3 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 4 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 5 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

Value (Var s)が登場するまで、適当にintroを使ってやります。

is_value_is_Value < Show 1.

  s : string
  ============================
   is_value (Var s) = true -> Value (Var s)

is_value_is_Value < intro.
5 subgoals

  s : string
  H : is_value (Var s) = true
  ============================
   Value (Var s)

subgoal 2 is:
 is_value (Bool b) = true -> Value (Bool b)
subgoal 3 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 4 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 5 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

ここで、さっき定義したValVarが使えます。

is_value_is_Value < Check ValVar.
ValVar
     : forall s : string, Value (Var s)

というわけで、これをapplyすれば証明が完了します。

is_value_is_Value < apply ValVar.
4 subgoals

  b : bool
  ============================
   is_value (Bool b) = true -> Value (Bool b)

subgoal 2 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 3 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 4 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

あとは、BoolとLambdaについても同様に証明できます。

is_value_is_Value < intro; apply ValBool.
3 subgoals

  s : string
  t : type
  t0 : term
  ============================
   is_value (Lambda s t t0) = true -> Value (Lambda s t t0)

subgoal 2 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 3 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < intro; apply ValLambda.
2 subgoals

  t1 : term
  t2 : term
  ============================
   is_value (Apply t1 t2) = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

ApplyとIfについては、simplで簡約すると前提がFalseになります。これをintroで仮定に移動させて、discriminateを使ってやれば証明できます。

is_value_is_Value < Show.
2 subgoals

  t1 : term
  t2 : term
  ============================
   is_value (Apply t1 t2) = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < simpl.
2 subgoals

  t1 : term
  t2 : term
  ============================
   false = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < intro.
2 subgoals

  t1 : term
  t2 : term
  H : false = true
  ============================
   Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < discriminate.
1 subgoal

  t1 : term
  t2 : term
  t3 : term
  ============================
   is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < simpl;intro; discriminate.
Proof completed.

じゃあ、これを使って証明してみよう!(その2)

じゃあ、逆向きも証明してみましょう。

Theorem Value_is_value :
  forall t : term, Value t -> is_value t = true.

で、これをtについて場合分けしても全然ハッピーになりません。

Inductiveで何かを定義した場合には、xxx_indが自動で定義されます。

Value_is_value < Check Value_ind.
Value_ind
     : forall P : term -> Prop,
       (forall s : string, P (Var s)) ->
       (forall b : bool, P (Bool b)) ->
       (forall (x : string) (ty : type) (body : term), P (Lambda x ty body)) ->
       forall t : term, Value t -> P t

これをapplyすると、いい感じのsubgoalがでてきます。あとはreflexivityだけで証明でいます。

Value_is_value < apply Value_ind.
3 subgoals

  ============================
   forall s : string, is_value (Var s) = true

subgoal 2 is:
 forall b : bool, is_value (Bool b) = true
subgoal 3 is:
 forall (x : string) (ty : type) (body : term),
 is_value (Lambda x ty body) = true
Value_is_value < reflexivity.
2 subgoals

  ============================
   forall b : bool, is_value (Bool b) = true

subgoal 2 is:
 forall (x : string) (ty : type) (body : term),
 is_value (Lambda x ty body) = true

Value_is_value < reflexivity.
1 subgoal

  ============================
   forall (x : string) (ty : type) (body : term),
   is_value (Lambda x ty body) = true

Value_is_value < reflexivity.
Proof completed.

2009-10-26(月)

今日のCoq: Inversion of the typing relation補題とUniqueness of types定理

| 今日のCoq: Inversion of the typing relation補題とUniqueness of types定理 - みずぴー日記 を含むブックマーク

今日もTypes and Programming Languages (The MIT Press)に載っている定理の証明です。

type_dec

補題を定義する際に、以下のような定義が必要になりました。

Definition type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}.

で、これを証明するために、2時間ほどがんばってました。

結局、decide equalityタクティクスで一発でした。ちぇー。

Proof.
  decide equality.
Qed.

Inversion of the typing relation補題

昨日の続きです。

補題の直感的な意味は「ある項tが型を持つなら、そのsubtermも型を持つ」で、その証明は「Immediate from the definithion」らしいです。

証明する戦略は、

  • 条件分岐が登場したらcaseタクティクスで場合分け
  • 仮定が真ならintroで取り出して、inversionを適用し、reflexivityで証明する
  • 仮定が偽ならintroで取り出して、discriminateで証明する

です。

Lemma VarRel :
  forall (tenv : list (string * type)) (x : string) (r : type),
  Some r = typing (Var x) tenv -> In (x,r) tenv.

Lemma LambdaRel :
  forall (x : string)
         (t r1 : type)
      	 (body : term)
         (tenv : list (string * type)),
  Some r1 = typing (Lambda x t body) tenv ->
      exists r2 : type,
      Some r2 = typing body ((x,t)::tenv) /\
      r1 = FunT t r2.

Lemma ApplyRel:
  forall (r : type)
      	 (f x : term)
         (tenv : list (string * type)),
    Some r = typing (Apply f x) tenv ->
      exists t : type,
      Some (FunT t r) = typing f tenv /\
      Some t = typing x tenv.

Lemma TrueRel:
  forall (tenv : list (string * type)) (r : type),
  Some r = typing (Bool true) tenv -> r = BoolT.

Lemma FalseRel:
  forall (tenv : list (string * type)) (r : type),
  Some r = typing (Bool false) tenv -> r = BoolT.

Lemma IfRel:
  forall (tenv : list (string * type)) (r : type) (t1 t2 t3 : term),
  Some r = typing (If t1 t2 t3) tenv ->
  Some BoolT = typing t1 tenv /\  Some r = typing t2 tenv /\  Some r = typing t3 tenv.

no title

Uniqueness of types定理

初の定理(Theorem)です。

直感的な意味は「ある項tが型を持つらなら、その型は唯一(unique)である」で、その証明は「Exercise」らしいです。

簡単に見えるけれども、けっこう大変でした。tについて場合分けをし、それぞれについてひたすら証明しました。

Theorem type_uniq :
  forall (tenv : list (string * type)) (r1 r2 : type) (t : term),
    Some r1 = typing t tenv /\ Some r2 = typing t tenv ->
      r1 = r2.

no title

ソースコード

okagawaokagawa 2009/10/31 21:30 ご存知かもしれませんが、Programming in Haskellのシーザー暗号を思い出しました。
暗号化/復号化だけでなく文字の出現頻度を測ってcrackするコードまで入ってます。(笑)

http://www.cs.nott.ac.uk/~gmh/cipher.lhs

mzpmzp 2009/11/01 14:26 おお、ありがとうございます。恥しいことに、Programming in Haskellという本がでてることも知りませんでした。
クラックするコードまではいってるのはすごいですね。

2009-10-25(日)

今日のCoq: Inversion of the typing relation補題

| 今日のCoq: Inversion of the typing relation補題 - みずぴー日記 を含むブックマーク

前回までで作った型付け規則を元に、Types and Programming Languages (The MIT Press)に載っている「Inversion of the typing relation補題」の証明にチャレンジしました。

Inversion of the typing relation補題

Lemma LambdaRel :
  forall (x : string)
         (t r1 : type)
      	 (body : term)
         (tenv : list (string * type)),
  Some r1 = typing (Lambda x t body) tenv ->
      exists r2 : type,
      Some r2 = typing body ((x,t)::tenv) /\
      r1 = FunT t r2.

のようなやつです。直感的な意味は「あるtermが型を持つなら、そのsubtermも型を持つ」です。ちなみに、Types and Programming Languages (The MIT Press)によると「Immediate from the definithion」らしいですよ。

このような形をした補題が、VarとかBoolとかの各コンストラクタごとに定義されています。今回は、VarとLambdaのやつだけを証明しました。続きはまた明日です。

わかったこと

  • 場合分けはcaseタクティクスで行なう
  • existsはexistsタクティクスで具体的な値を与えるか、eapply ex_introで仮定を導入する

ソースコード

今回からGithubに置くようにしました。

http://github.com/mzp/lambda

2009-10-22(木)

今日のCoq: 型づけ規則とそれに関する補題

| 今日のCoq: 型づけ規則とそれに関する補題 - みずぴー日記 を含むブックマーク

とうとう、型づけ規則の定義ができました。

というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。

証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediate from the definitionらしいです。

(*
  typing t tenvは、型環境tenvにおいてtが型づけ可能ならSome type、型がつかないならNoneを返す。
*)
Lemma InvTypeRelVar :
  forall (tenv : list (string * type)) (x : string) (r : type),
  Some r = typing (Var x) tenv -> In (x,r) tenv.

というわけで証明にチャレンジします。

まずは、forallを仮定に移します。

InvTypeRelVar < Proof.
InvTypeRelVar < intros until r.
1 subgoal

  tenv : list (string * type)
  x : string
  r : type
  ============================
   Some r = typing (Var x) tenv -> In (x, r) tenv

そして、tenvに関する帰納法を用います。

InvTypeRelVar < induction tenv.
2 subgoals

  x : string
  r : type
  ============================
   Some r = typing (Var x) nil -> In (x, r) nil

subgoal 2 is:
 Some r = typing (Var x) (a :: tenv) -> In (x, r) (a :: tenv)

tenvがnilのときの証明は簡単です。

InvTypeRelVar < simpl.
2 subgoals

  x : string
  r : type
  ============================
   Some r = None -> False

subgoal 2 is:
 Some r = typing (Var x) (a :: tenv) -> In (x, r) (a :: tenv)

InvTypeRelVar < discriminate.
1 subgoal

  a : string * type
  tenv : list (string * type)
  x : string
  r : type
  IHtenv : Some r = typing (Var x) tenv -> In (x, r) tenv
  ============================
   Some r = typing (Var x) (a :: tenv) -> In (x, r) (a :: tenv)

で、問題は再帰ステップのほうです。とりあえず、simplで簡約します。

InvTypeRelVar < simpl.
1 subgoal

  a : string * type
  tenv : list (string * type)
  x : string
  r : type
  IHtenv : Some r = typing (Var x) tenv -> In (x, r) tenv
  ============================
   Some r =
   (let (key, v) := a in if string_dec x key then Some v else assoc x tenv) ->
   a = (x, r) \/ In (x, r) tenv

で、ここから先に進めない。string_dec x keyが成立する場合と成立しない場合の2つのsubgoalに分けれればいけそうなんだけど・・・。

ソースコード

(* simple typed lambda calculus *)
Require Import Arith.EqNat.
Require Import Arith.
Require Import Recdef.
Require Import List.
Require Import String.
Require Import Bool.DecBool.

(* simple type *)
Inductive type : Set :=
    BoolT : type
  | FunT  : type -> type -> type.

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term.

(* Eval *)
Fixpoint subst (t : term) (old : string) (new : term) :=
  match t with
  | Bool _ =>
      t
  | Var x =>
      if string_dec x old then
      	new
      else
      	t
  | Lambda x type body =>
      if string_dec x old then
      	t
      else
        Lambda x type (subst body old new)
  | Apply t1 t2 =>
      Apply (subst t1 old new) (subst t2 old new)
  end.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  =>
      false
  end.

Fixpoint step (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        subst body x t2
      else
      	Apply t1 (step t2)
  | Apply t1 t2 =>
      Apply (step t1) t2
  end.

Fixpoint term_length (t : term) :=
  match t with
    Bool _ | Var _  =>
      1
  | Lambda _ _ body =>
      1 + term_length body
  | Apply t1 t2 =>
      1 + term_length t1 + term_length t2
  end.

(* typing *)
Fixpoint assoc {A : Type} (x : string) (xs : list (string * A)) :=
  match xs with
  | nil =>
      None
  | (key, v) :: ys =>
      if string_dec x key then
        Some v
      else
      	assoc x ys
  end.

Fixpoint beq_type (t1 : type) (t2 : type) :=
  match (t1,t2) with
    (BoolT,BoolT) => true
  | (FunT t1 t2, FunT t3 t4) => andb (beq_type t1 t3) (beq_type t2 t4)
  | _ => false
  end.

Fixpoint typing (t : term) (tenv : list (string * type)) :=
  match t with
    Bool _ =>
    Some BoolT
  | Var x =>
    assoc x tenv
  | Lambda x ty1 body =>
    match typing body ((x,ty1)::tenv) with
      None => None
    | Some ty2 => Some (FunT ty1 ty2)
   end
  | Apply t1 t2 =>
    match (typing t1 tenv, typing t2 tenv) with
       (Some (FunT ty11 ty12),Some ty13) =>
        if beq_type ty11 ty13 then
          Some ty12
      	else
	  None
      | _ => None
    end
  end.

(* theorem *)
Definition value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      True
  | Apply _ _  =>
      False
  end.

Lemma NoneSome :
  forall (A : Type) (t : A), None = Some t -> False.
Proof.
  intros A t.
  discriminate.
Qed.

(* Inversion of the typing relation *)
Lemma InvTypeRelVar :
  forall (tenv : list (string * type)) (x : string) (r : type),
  Some r = typing (Var x) tenv -> In (x,r) tenv.

(*
Lemma CanonicalForms_Bool :
  forall (v : term),
  (value v /\ typing v nil = Some BoolT) -> (v = Bool true \/ v = Bool false).
*)

yoshihiro503yoshihiro503 2009/10/23 08:36 string_decの項に対してcaseタクティックを使えばうまくいきます。

Lemma InvTypeRelVar :
 forall (tenv : list (string * type)) (x : string) (r : type),
 Some r = typing (Var x) tenv -> In (x,r) tenv.
Proof.
simpl in |- *.
intro tenv; induction tenv.
 intros.
 discriminate H.

 intros x r.
 simpl in |- *.
 destruct a.
 case (string_dec x s).
  intros; left.
  rewrite e in |- *.
  inversion H.
  reflexivity.

  intros neq H; right.
  apply (IHtenv x r H).
Qed.

mzpmzp 2009/10/23 08:57 うおお、ありがとうございます!
知らないタクティクスがいくつかあるので、調べてみます。

2009-10-21(水)

今日のCoq: eval

| 今日のCoq: eval - みずぴー日記 を含むブックマーク

前回作ったラムダ式の上に、evalを定義しました。

覚えたこと

全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。

  • 再帰関数の定義は、かなり厳しい制約があるっぽい

よく分からないこと

最初、termを与えると値になるまで評価するevalを書いてみました。

....

Function eval (t :term) {measure term_length t} : term :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        eval (subst body x t2)
      else
      	eval (Apply t1 (eval t2))
  | Apply t1 t2 =>
      eval (Apply (eval t1) t2)
  end.

そしたら、evalがないよ、と言われてしまった。

coqc lambda.v
File "./lambda.v", line 66, characters 0-319:
Error: No such section variable or assumption: eval.

いろいろ書き換えて試したところ

eval (Apply (eval t1) t2)

みたいな、evalを二回呼び出しているところがダメらしい。

回避方法

どっちにしろ、上記のようなevalだと停止しないことがありそうだったので、1ステップだけ簡約するstepという関数を定義しました。

...
Fixpoint step (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        subst body x t2
      else
      	Apply t1 (step t2)
  | Apply t1 t2 =>
      Apply (step t1) t2
  end.

ソースコード

(* simple typed lambda calculus *)
Require Import Arith.EqNat.

(* simple type *)
Inductive type : Set :=
    BoolT : type
  | FunT  : type -> type -> type.

Inductive term : Set :=
    Var     : nat -> term
  | Bool    : bool   -> term
  | Lambda  : nat -> type -> term -> term
  | Apply   : term  -> term -> term.

(* Eval *)
Fixpoint subst (t : term) (old : nat) (new : term) :=
  match t with
  | Bool _ =>
      t
  | Var x =>
      if beq_nat x old then
      	new
      else
      	t
  | Lambda x type body =>
      if beq_nat x old then
      	t
      else
        Lambda x type (subst body old new)
  | Apply t1 t2 =>
      Apply (subst t1 old new) (subst t2 old new)
  end.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  =>
      false
  end.

Fixpoint step (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        subst body x t2
      else
      	Apply t1 (step t2)
  | Apply t1 t2 =>
      Apply (step t1) t2
  end.

(*
Function eval (t :term) {measure term_length t} : term :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        eval (subst body x t2)
      else
      	eval (Apply t1 (eval t2))
  | Apply t1 t2 =>
      eval (Apply (eval t1) t2)
  end.*)

shiroshiro 2009/10/22 01:02 定番のツッコミですが、named letの初期化式のスコープにnameは入らないです。
(let + ((p +)) (p 1 2)) => 3 にならないとだめっす。

mzpmzp 2009/10/22 21:20 うう、定番なんですね・・。