Hatena::Groupcoq

mzpの日記

2010-06-26

Ex 3.1

Inductive truth := Yes | No | Maybe.

Definition not (t : truth) :=
  match t with
    | Yes => No
    | No  => Yes
    | Maybe => Maybe
  end.

Definition and (t1 t2 : truth) :=
  match (t1,t2) with
    | (Yes,Yes) => Yes
    | (No,No) => No
    | _   => Maybe
  end.

Definition or (t1 t2 : truth) :=
  match (t1,t2) with
    | (Yes,_)  => Yes
    | (_,Yes)  => Yes
    | (No,No)  => No
    | _ => Maybe
  end.

Lemma and_comm : forall (t1 t2 t3 : truth),
  and t1 (and t2 t3) = and (and t1 t2) t3.
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Lemma or_dist_r : forall (t1 t2 t3 : truth),
  and t1 (or t2 t3) = or (and t1 t2) (and t1 t3).
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Lemma or_dist_l : forall (t1 t2 t3 : truth),
  and (or t1 t2) t3 = or (and t1 t3) (and t2 t3).
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Ex 3.2

Inductive binop : Set :=
| Plus
| Times.

Definition var := nat.

Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp
| Var   : var   -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (assign : var -> nat) (e : exp) : nat :=
  match e with
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote assign e1) (expDenote assign e2)
    |  Var v  => assign v
  end.

Fixpoint const_fold (e : exp) : exp :=
  match e with
    | Binop b e1 e2 =>
      match (const_fold e1, const_fold e2) with
        | (Const x, Const y) => Const ((binopDenote b) x y)
        | (x,y) => Binop b x y
      end
    | _ => e
  end.

Theorem preserve : forall e assign,
  expDenote assign e = expDenote assign (const_fold e).
Proof.
intros.
induction e; simpl; try tauto.
rewrite IHe1, IHe2.
destruct (const_fold e1); destruct (const_fold e2); reflexivity.
Qed.

DannyApenoDannyApeno2017/06/20 22:43Attention Required! | Cloudflare
<a href=http://acheterdufrance.com/>Show more>>></a>

TimothyTeNTimothyTeN2017/07/01 23:47301 Moved Permanently
<a href=https://www.viagrapascherfr.com/>Click here>>></a>

GuestWayncGuestWaync2017/12/22 00:44guest test post
<a href=" http://kioppoerk.com/ ">bbcode</a>
<a href="http://kioppoerk.com/">html</a>
http://kioppoerk.com/ simple

JerdulkJerdulk2018/01/28 01:59Homeopathic Amoxicillin For Pets <a href=http://tadalafbuy.com>cialis</a> Achat Kamagra Voir Le Profil Amoxicillin Tablets

KirhauhKirhauh2018/04/16 04:14Achat De Viagra En Belgique <a href=http://cialviag.com>canadian cialis</a> Overnight Meds Online

utalethzdsutalethzds2018/08/01 07:18<a href="http://rabbitinahat.com">cheap cialis pills online</a> buy cialis http://rabbitinahat.com

staletpzbrstaletpzbr2018/08/02 06:31<a href="http://rabbitinahat.com">order cialis australia</a> cheap cialis black http://rabbitinahat.com

ltaletgqykltaletgqyk2018/08/03 03:36<a href="http://gigawatt6.com">how to order cialis from canada</a> ordering cialis online http://gigawatt6.com

utaletbxmiutaletbxmi2018/08/04 04:04<a href="http://motechautomotive.com">buy cialis non prescription</a> best place to buy generic cialis http://motechautomotive.com

gtaletpnecgtaletpnec2018/08/05 11:09<a href="http://istanbulexpressonline.com">cheap viagra</a> buy viagra usa http://istanbulexpressonline.com

ctalettzmgctalettzmg2018/08/07 23:03<a href="http://psychologytweets.com">generic cialis 20mg</a> canadian pharmacy online cialis http://psychologytweets.com

jtaletzduljtaletzdul2018/08/09 12:52<a href="http://mphasset.com">best place to buy generic viagra online</a> buy viagra los angeles http://mphasset.com

btaletplcnbtaletplcn2018/08/18 07:05<a href="http://mphasset.com">viagra 100mg side effects</a> is taking viagra bad for you http://mphasset.com

etaletdknxetaletdknx2018/08/18 09:38<a href="http://mphasset.com">what else is viagra used for</a> mixing cialis with viagra http://mphasset.com

ntaletvtgrntaletvtgr2018/08/18 12:26<a href="http://mphasset.com">food viagra</a> what happens if you take viagra and dont have sex http://mphasset.com

wtaletyrwhwtaletyrwh2018/08/18 14:41<a href="http://istanbulexpressonline.com">viagra after drinking alcohol</a> is cialis viagra http://istanbulexpressonline.com

utaletwpjiutaletwpji2018/08/18 16:51<a href="http://istanbulexpressonline.com">herbal viagra review</a> using viagra everyday http://istanbulexpressonline.com

qtaletxfhsqtaletxfhs2018/08/18 18:45<a href="http://mphasset.com">free sample viagra</a> is there a viagra generic http://mphasset.com

ktaletwrkuktaletwrku2018/08/18 20:34<a href="http://bullsac.com">compare viagra cialis levitra</a> viagra v levitra http://bullsac.com

staletkcnrstaletkcnr2018/08/18 22:20<a href="http://bakerssign.com">buy levitra 10mg</a> levitra cialis viagra price comparison http://bakerssign.com

qtaletmtdkqtaletmtdk2018/08/18 23:48<a href="http://rabbitinahat.com">cialis 20mg buy</a> cialis lower blood pressure http://rabbitinahat.com

ztaletvpbrztaletvpbr2018/08/19 01:32<a href="http://gigawatt6.com">free trial cialis online</a> where is cialis manufactured http://gigawatt6.com

ntalethsqmntalethsqm2018/08/19 03:02<a href="http://baymontelreno.com">what is cialis tadalafil used for</a> want to buy cialis http://baymontelreno.com

ttaletwwxmttaletwwxm2018/08/19 04:42<a href="http://baymontelreno.com">cialis what dosage</a> how often to take cialis http://baymontelreno.com

ltaletjngaltaletjnga2018/08/19 07:39<a href="http://psychologytweets.com">brand cialis online</a> cialis stories http://psychologytweets.com

btaletlxvbbtaletlxvb2018/08/19 08:59<a href="http://missreplicawatches.com">how much is cialis at walmart</a> cialis high blood pressure http://missreplicawatches.com

btaletqqpsbtaletqqps2018/08/19 10:28<a href="http://baymontelreno.com">cialis tadalafil</a> cialis canada http://baymontelreno.com

ttaletwlbhttaletwlbh2018/08/19 20:13<a href="http://bullsac.com">levitra wiki</a> over the counter levitra http://bullsac.com

vtaletoiievtaletoiie2018/08/19 21:47<a href="http://gigawatt6.com">discount coupons for cialis</a> what is the use of cialis tablets http://gigawatt6.com

otaletfwxmotaletfwxm2018/08/19 23:10<a href="http://missreplicawatches.com">what to do when cialis stops working</a> what is the use of cialis tablets http://missreplicawatches.com

xtaletcshkxtaletcshk2018/08/20 00:44<a href="http://missreplicawatches.com">low cost cialis canada</a> cialis 5mg side effects http://missreplicawatches.com

ataletfshvataletfshv2018/08/20 02:06<a href="http://missreplicawatches.com">generic cialis super active</a> buying cialis in mexico http://missreplicawatches.com

otaletflfvotaletflfv2018/08/20 05:08<a href="http://psychologytweets.com">cialis 5 mg online</a> cialis how fast http://psychologytweets.com

jtaletsfdsjtaletsfds2018/08/20 13:26<a href="http://bakerssign.com">levitra free samples</a> buy generic levitra online http://bakerssign.com

ftaletnkqvftaletnkqv2018/08/20 15:31<a href="http://bakerssign.com">levitra 20</a> levitra without a prescription http://bakerssign.com

htaletvqnhhtaletvqnh2018/09/11 09:17<a href="http://mphasset.com">can viagra be bought over the counter</a> where to buy viagra over the counter http://mphasset.com

ntaletdxvjntaletdxvj2018/09/11 12:54<a href="http://bakerssign.com">generic levitra online</a> levitra review http://bakerssign.com

ftaletwrljftaletwrlj2018/09/11 14:15<a href="http://istanbulexpressonline.com">how much viagra is too much</a> get viagra prescription online http://istanbulexpressonline.com

otaletlgdfotaletlgdf2018/09/11 14:27<a href="http://istanbulexpressonline.com">side effects of viagra on females</a> free samples of viagra http://istanbulexpressonline.com

xtaletignbxtaletignb2018/09/11 17:04<a href="http://missreplicawatches.com">cialis 5</a> cialis 40 mg reviews http://missreplicawatches.com

staletltxkstaletltxk2018/09/11 22:00<a href="http://missreplicawatches.com">cialis interactions</a> cialis benefits and side effects http://missreplicawatches.com

ltaletpkqnltaletpkqn2018/09/11 23:46<a href="http://baymontelreno.com">cialis side effects lower back pain</a> cialis maximum daily dosage http://baymontelreno.com

btaletrxujbtaletrxuj2018/09/12 03:16<a href="http://top-monterey-salinas-dentists.com">levitra mexico</a> cialis and levitra taken together http://top-monterey-salinas-dentists.com

otaletnbdsotaletnbds2018/09/12 06:12<a href="http://bullsac.com">viagra vs levitra dosage</a> levitra online canadian pharmacy http://bullsac.com

qtaletxwmiqtaletxwmi2018/09/12 07:22<a href="http://missreplicawatches.com">order cialis in canada</a> cialis generic best price http://missreplicawatches.com

utaletynitutaletynit2018/09/12 12:02<a href="http://baymontelreno.com">order discount cialis online</a> cialis canada mail order http://baymontelreno.com

ktaletvbvaktaletvbva2018/09/12 16:26<a href="http://baymontelreno.com">order cialis paypal</a> cialis 5mg http://baymontelreno.com

ktaletovpektaletovpe2018/09/12 18:33<a href="http://gigawatt6.com">generic cialis usa</a> how to order cialis http://gigawatt6.com

ftaletufpeftaletufpe2018/09/12 19:46<a href="http://gigawatt6.com">order 5mg cialis online</a> buy cialis 5mg online http://gigawatt6.com

btaletummgbtaletummg2018/09/12 23:43<a href="http://bullsac.com">generic levitra online</a> what is levitra used for http://bullsac.com

utaletilgoutaletilgo2018/09/13 02:17<a href="http://top-monterey-salinas-dentists.com">levitra professional</a> staxyn vs levitra http://top-monterey-salinas-dentists.com

ytaletrraaytaletrraa2018/09/13 06:48<a href="http://h-m-j.com">cheap viagra</a> viagra pills http://h-m-j.com

gtaletnwvmgtaletnwvm2018/09/13 08:07<a href="http://top-monterey-salinas-dentists.com">levitra cost walmart</a> how to take levitra http://top-monterey-salinas-dentists.com

btaletnabdbtaletnabd2018/09/13 11:31<a href="http://bullsac.com">levitra 20 mg cost</a> canada levitra online http://bullsac.com

ptaletsxysptaletsxys2018/09/13 12:57<a href="http://vico4me.com">order cheap female viagra</a> buy viagra online canada http://vico4me.com

rtaletqemwrtaletqemw2018/09/13 17:01<a href="http://h-m-j.com">generic viagra canada pharmacy</a> generic viagra soft http://h-m-j.com

vtaletndedvtaletnded2018/09/13 17:59<a href="http://vico4me.com">buy viagra with paypal</a> cheap viagra online canadian pharmacy http://vico4me.com

otaletszgpotaletszgp2018/09/13 19:41<a href="http://canadian-pharmabuy.com">buy real viagra online cheap</a> generic viagra online canada http://canadian-pharmabuy.com

etaletogruetaletogru2018/09/13 20:49<a href="http://canadian-pharmaonline.com">order viagra pills</a> order viagra onlines http://canadian-pharmaonline.com

etaletbrxtetaletbrxt2018/09/14 00:46<a href="http://canadian-pharmaonline.com">order pfizer viagra</a> cheap female viagra http://canadian-pharmaonline.com

ataletrgdvataletrgdv2018/09/14 01:20<a href="http://vico4me.com">generic viagra pills</a> viagra canada http://vico4me.com

dtaletxbmzdtaletxbmz2018/09/14 01:32<a href="http://canadian-pharmabuy.com">cheap viagra pills online</a> viagra usa http://canadian-pharmabuy.com

xtaletmqjmxtaletmqjm2018/09/14 03:26<a href="http://motechautomotive.com">buy cialis now</a> cheap cialis black http://motechautomotive.com

jtaletmxexjtaletmxex2018/09/14 04:32<a href="http://missreplicawatches.com">order cialis overnight delivery</a> cheap cialis 10mg http://missreplicawatches.com

ptaletknmkptaletknmk2018/09/14 11:27<a href="http://vico4me.com">cheap viagra europe</a> best mail order viagra http://vico4me.com

ptalethnohptalethnoh2018/09/14 12:11<a href="http://canadian-pharmasale.com">can you order cialis online for canada</a> cheap generic cialis http://canadian-pharmasale.com

wtaletlznfwtaletlznf2018/09/14 21:06<a href="http://bullsac.com">cost levitra</a> how long is levitra effective http://bullsac.com

ktaletbbwuktaletbbwu2018/09/14 21:27<a href="http://vico4me.com">order viagra softtabs</a> generic viagra online http://vico4me.com

htaletreuyhtaletreuy2018/09/14 21:28<a href="http://timsbmw.com">how long does levitra 10mg last</a> how long does 10mg levitra last http://timsbmw.com

jtaletwwqmjtaletwwqm2018/09/15 05:41<a href="http://valladium.com">order cialis from india</a> how to order cialis http://valladium.com

ytaletcodjytaletcodj2018/09/15 06:11<a href="http://buycialisonlineglka.com">order cialis online cheap</a> buy cialis no prescription http://buycialisonlineglka.com

htaletrxzrhtaletrxzr2018/09/15 07:30<a href="http://vico4me.com">women viagra</a> how to buy viagra http://vico4me.com

italetprujitaletpruj2018/09/15 07:37<a href="http://istanbulexpressonline.com">buy viagra uk</a> cheap viagra 100mg http://istanbulexpressonline.com

staletynmzstaletynmz2018/09/15 09:44<a href="http://vico4me.com">buy viagra brand</a> order viagra http://vico4me.com

htaletncwchtaletncwc2018/09/15 16:57<a href="http://timsbmw.com">levitra vs sildenafil</a> levitra vs cialis vs viagra http://timsbmw.com

staletykmfstaletykmf2018/09/15 17:17<a href="http://buycialisonlineglka.com">buy cialis online canada</a> buy cialis online pharmacy http://buycialisonlineglka.com

italetpegeitaletpege2018/09/15 18:12<a href="http://baymontelreno.com">cheap cialis 20mg</a> order cialis pills http://baymontelreno.com

dtaletdalzdtaletdalz2018/09/15 18:21<a href="http://h-m-j.com">order generic viagra online</a> buy viagra brand http://h-m-j.com

ntaletzjwlntaletzjwl2018/09/16 01:15<a href="http://buycialisonl1ne.us">cialis 5mg</a> buy cheap cialis generic http://buycialisonl1ne.us

ptalethsqoptalethsqo2018/09/16 01:52<a href="http://canadian-pharmaonline.com">best place to buy viagra</a> viagra usa http://canadian-pharmaonline.com

btaletbubqbtaletbubq2018/09/16 03:18<a href="http://h-m-j.com">best online pharmacy viagra</a> buy viagra cheaply http://h-m-j.com

jtaletaghqjtaletaghq2018/09/16 12:30<a href="http://rabbitinahat.com">buy cialis now</a> cialis coupons online http://rabbitinahat.com

ztaletclyeztaletclye2018/09/16 19:56<a href="http://viciolatino.com">cheap generic viagra online</a> cheapest generic viagra http://viciolatino.com

ytaletxdslytaletxdsl2018/09/16 20:44<a href="http://buycialisonl1ne.us">best place to buy cialis</a> buy cialis online pharmacy http://buycialisonl1ne.us

btaletrbxxbtaletrbxx2018/09/16 21:15<a href="http://usedrestaurantequipmentaz.com">buy generic cialis online with mastercard</a> cheap cialis generic canada http://usedrestaurantequipmentaz.com

utaletjzqautaletjzqa2018/09/17 04:27<a href="http://buyviagraonl1ne.us">order viagra today</a> order viagra 100mg http://buyviagraonl1ne.us

ptaletbpllptaletbpll2018/09/17 05:48<a href="http://baymontelreno.com">cheap cialis canada</a> cialis pill http://baymontelreno.com

ctaletrtvrctaletrtvr2018/09/17 06:52<a href="http://unishade.com">cialis for sale cheap</a> buy generic cialis 20 mg http://unishade.com

ttaletrvxfttaletrvxf2018/09/17 08:32<a href="http://top-monterey-salinas-dentists.com">levitra generic date</a> best price on levitra http://top-monterey-salinas-dentists.com

ftaletsiofftaletsiof2018/09/17 12:55<a href="http://waltzweekend.com">order viagra using paypal</a> buy online order viagra http://waltzweekend.com

ntaletryafntaletryaf2018/09/17 16:53<a href="http://top-monterey-salinas-dentists.com">recommended dosage of levitra</a> levitra cost http://top-monterey-salinas-dentists.com

ptalethgkxptalethgkx2018/09/17 22:46<a href="http://canadian-pharmaonline.com">get viagra prescription online</a> cheap herbal viagra http://canadian-pharmaonline.com

vtaletlrfavtaletlrfa2018/09/18 00:23<a href="http://usedrestaurantequipmentaz.com">cheap cialis 20mg pills</a> ordering cialis online http://usedrestaurantequipmentaz.com

btaletfssjbtaletfssj2018/09/18 01:36<a href="http://h-m-j.com">best place to buy viagra online</a> viagra from canada http://h-m-j.com

ltaletwcrzltaletwcrz2018/09/18 10:07<a href="http://bullsac.com">cheap levitra professional</a> free levitra http://bullsac.com

otaletgtbeotaletgtbe2018/09/18 13:19<a href="http://timsbmw.com">levitra generic us</a> levitra generic name http://timsbmw.com

vtaletrmgmvtaletrmgm2018/09/18 14:07<a href="http://gigawatt6.com">generic cialis canada</a> cheap generic cialis canadian pharmacy http://gigawatt6.com

utaletzsbzutaletzsbz2018/09/18 21:17<a href="http://viciolatino.com">buy viagra las vegas</a> buy viagra no prescription http://viciolatino.com

ltaletkbnhltaletkbnh2018/09/18 23:37<a href="http://bullsac.com">price of levitra</a> cost of levitra vs viagra http://bullsac.com

ctaletmntbctaletmntb2018/09/19 00:26<a href="http://motechautomotive.com">order cialis with paypal</a> very cheap cialis http://motechautomotive.com

otaletcwwgotaletcwwg2018/09/19 02:25<a href="http://viciolatino.com">viagra pill</a> viagra online bestellen http://viciolatino.com

ptaletjoseptaletjose2018/09/19 06:19<a href="http://top-monterey-salinas-dentists.com">levitra and alcohol</a> buy levitra online cheap http://top-monterey-salinas-dentists.com

jtaletgwtejtaletgwte2018/09/19 09:24<a href="http://canadian-pharmabuy.com">buy viagra los angeles</a> cheap indian viagra http://canadian-pharmabuy.com

2009-12-05

Coq + omake =さいきょう

coqcで複数ファイルをコンパイルするのって面倒ですよね。依存関係も考慮しないといけないし。

そんなときは、omakeですね!

というわけで、Coqのソースコードをコンパイルするのに必要なルールをいくつか書きました。

A.v、B.v、C.vからなる証明をコンパイルしたいときは

.DEFAULT: $(Proof A B C)

とするだけでOKです。ちゃんとA.v、B.v、C.vの間の依存関係も解析してます。

あと、omakeなので当然omake -Pで継続ビルドもできちゃいます。

ソースコード

s# ------------------------------------------------------------
# ルール部
# ------------------------------------------------------------
# コンパイル
%.vo %.glob: %.v
	coqc $<

# 依存関係の解析
# パスは適宜変更してください
.SCANNER: %.vo: %.v
	coqdep -w -coqlib /opt/local/lib/coq/ -I . $<

# 便利関数
public.Proof(files) =
	vo=$(addsuffix .vo,$(files))
	value $(vo)

# ------------------------------------------------------------
# 利用例:
# A.v B.v C.vをコンパイルしたい場合
# ------------------------------------------------------------
FILES[] =
	A
	B
	C

.DEFAULT: $(Proof $(FILES))

.PHONY: clean
clean:
	rm -f *.vo *.glob *~ *.omc .omakedb .omakedb.lock *.html

参考

The OMake build system

2009-11-26

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はやめてください。難しいよ、その証明(><)
  • 一発で正しい定義はなかなかできない。(id:mzp:20091124)
  • さらっと「変数は重複して登場しないものとする」って書かないで! 難しいよ、その証明(><)

2009-11-25

Coqのおかげで見つけれたバグ

最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。

で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直してみると、そもそもsubstitutionの定義が間違っていました。このバグはなかなか根が深くて、前に作ったトイ・コンパイラ(scalet)でも同じ間違いをしてました。

というわけで、これはCoqのおかげで見つけれたバグだし、人手は見付けづらいバグと言えないこともないので記録しておきます。

バグを含んだSubstitution

まずはバグを含んだSubstitutionです。どこが間違っているか分かりますか? ボクは分かりませんでした。

(* subst *)
Inductive Subst : term -> term -> string -> term -> Prop :=
  | SVar1    : forall (s x : string) (t : term),
      x = s  -> Subst (Var x) t s t
  | SVar2    : forall (s x : string) (t : term),
      x <> s -> Subst (Var x) (Var x) s t
  | SBool    : forall (s : string) (b : bool) (t : term),
      Subst (Bool b) (Bool b) s t
  | SLambda1 : forall (x s : string) (body1 body2 t : term) (ty : type),
      x <> s -> Subst body1 body2 s t ->
      	Subst (Lambda x ty body1) (Lambda x ty body2) s t
  | SLambda2 : forall (x s : string) (body t : term) (ty : type),
      x = s  -> Subst (Lambda x ty body) (Lambda x ty body) s t
  | SApply   : forall (t1 t2 s1 s2 t : term) (x : string),
      Subst t1 s1 x t -> Subst t2 s2 x t -> Subst (Apply t1 t2) (Apply s1 s2) x t
  | SIf      : forall (t1 t2 t3 s1 s2 s3 t : term) (x : string),
      Subst t1 s1 x t -> Subst t2 s2 x t -> Subst t3 s3 x t ->
      	Subst (If t1 t2 t3) (If s1 s2 s3) x t.

正しい定義

そして、こちらがTAPL(asin:0262162091)に載っている正しい定義です。

f:id:mzp:20091104203722p:image

間違っていたところ

で、どこが間違っていたかと言うとFV(s)に関する条件が抜けていました。これのせいで、substitutionが不正になって、結果としてSubstitution lemmaの証明ができませんでした。これが無いと、weaking Lemmaを適用できないんだよね。

f:id:mzp:20091104203904p:image

そのときのTwitterのログ

みずぴー
@mzp
えー、substitution lemma無理だって。これ成り立たねーよ(2009-11-03 19:00:54) link
みずぴー
@mzp
どう考えてもsubstitution lemmaの証明、無理だって。きっと"変数が重複しない"という約束のおかげで、暗黙の前提があるに違いない(2009-11-03 20:54:36) link
みずぴー
@mzp
一晩一晩考えたけsubstitution lemmaが成立しない、ってのはウソな気がしてきた(←当然)。でも、証明ができないってのは依然とそのまま(2009-11-4 08:00:48) link
みずぴー
@mzp
そろそろでかける時間だけど、もうちょっとTAPLの証明を追いかけたいし、iPhoneの同期も終ってないので、まだ家にいる(2009-11-4 08:02:22) link
みずぴー
@mzp
あーーーー、証明できない理由がわかった。substitutionの定義が間違ってるんだ!!(2009-11-4 08:10:17) link
みずぴー
@mzp
TAPLだと「λx.t」のxは常にユニークである、という約束のおかげで、substitutionの定義が簡単になってるのか(2009-11-4 08:11:07) link
みずぴー
@mzp
ん?そんなこともないか。単にボクの実装ミスだ > substitutionの定義(2009-11-4 08:15:16) link
みずぴー
@mzp
今のボクの状態: substitution lemmaの証明ができない-> よく見たらsubstitutionの定義が間違っていた -> ちゃんとsubstitutionを定義するのが難しい! http://github.com/mzp/lambda(2009-11-04 09:51:20) link

ちなみに

書いているCoqのコードはGitHubにあります。

http://github.com/mzp/lambda

2009-11-24

今日の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.