VOOZH about

URL: https://qiita.com/suharahiromichi/items/723896ebfbc332f9d3dd

⇱ 「The Little Prover」のCoqでの実現---「定理証明手習い」の「公理」をCoqで証明してみた #lisp - Qiita

👁 Image
6

Go to list of users who liked

9

Share on X(Twitter)

Share on Facebook

Add to Hatena Bookmark

More than 5 years have passed since last update.

@suharahiromichi(須原 浩道)

「The Little Prover」のCoqでの実現---「定理証明手習い」の「公理」をCoqで証明してみた

6
Last updated at Posted at 2017-08-01

「The Little Prover」のCoqでの実現

2017/08/02

2017/08/07 シンボルをstringを使うようにした。
2017/08/09 case: eqP を使うようにした。
2017/08/11 prove_nil タクティクを完成した。
2017/10/21 「定理証明手習い」発刊記念。
2019/07/24 Stringの定義をマージした。

@suharahiromichi
この文書のソースコードは以下にあります。

はじめに

「The Little Prover」（以下 TLP）[1] を読んで、Coqの上でそれを実現しようとした話です。
TLPで証明しているプログラムをGallinaに移植して証明することは簡単です[2]。
しかし、これからやろうとするのは、TLPの対象言語であるLispの「意味」をCoqで実現しようと思います。
それによって、

  1. Coqはinductiveに定義したデータ型はinductionができることを原理としています。
    これに対して、TLPはinductionはハードコードされています。
    結果として、帰納法の公理からすべての定理を導くことができず、多くの「公理」を導入しています。
    帰納法の公理を使って、TLPの「公理」を証明することで、TLPの正しさが検証できるでしょう。

  2. TLPはLispのプログラム（当然S式を返す）がnilでないことを証明する。
    これをもって、そのプログラムの意味する論理式が真であるとします。
    Coqは論理式（Prop型）でなければ証明できないので、
    これをLispのプログラムをCoqの論理式に埋め込むことで実現します。

CoqのMathcomp/SSReflect拡張を使用しているので、それについては[3]を参照してください。また、見ただけでは解らないようなタクティカル（"by case=> -> ->" など) の使用は避けています。

FrommathcompRequireImportall_ssreflect.RequireImportString.SetImplicitArguments.UnsetStrictImplicit.UnsetPrintingImplicitDefensive.SetPrintAll.

文字列の定義

バニラCoqの定義を使用し、eqTypeのインスタンスにすることで、「==」が使えるようになります。

Definitionstring_eqMixin:=@EqMixinstringString.eqbString.eqb_spec.Canonicalstring_eqType:=@EqTypestringstring_eqMixin.OpenScopestring_scope.Check"aaa"="aaa":Prop.Check"aaa"=="aaa":bool.Check"aaa"=="aaa":Prop.SectionTLP.

S式の定義

S式をInductiveなデータ型として定義します。ここでは、S式にことをTLPにあわせて Star型と呼ぶことにします。

Atomic

アトムどうしのbooleanの等式を定義したうえで、それが、論理式(ライプニッツの等式、Propの等式)と同値であることを証明することで、boolとPropの間での行き来ができるようになります。つまり、「==」と「=」の両方を使うことができるようになります。これをリフレクションといいます[4]。
アトムとしては、シンボルの他に自然数もとれるようにします。

Inductiveatomic:Type:=|ATOM_NAT(n:nat)|ATOM_SYM(s:string).DefinitioneqAtom(ab:atomic):bool:=match(a,b)with|(ATOM_NATn,ATOM_NATm)=>n==m|(ATOM_SYMs,ATOM_SYMt)=>s==t(* eqString *)|_=>falseend.Lemmaatomic_eqP:forall(xy:atomic),reflect(x=y)(eqAtomxy).Proof.move=>xy.apply:(iffPidP).-case:x;case:y;rewrite/eqAtom=>xy;move/eqP=>H;by[rewriteH|||rewriteH].-move=>H;rewriteH.case:yH=>nH1;byrewrite/eqAtom.Qed.Definitionatomic_eqMixin:=@EqMixinatomiceqAtomatomic_eqP.Canonicalatomic_eqType:=@EqTypeatomicatomic_eqMixin.

List型 (L-EXP)

Inductivelist:Type:=|L_ATOMofatomic|L_CONSofatomic&list.

Star型 (S-EXP)

「Star型は、アトム、または、Star型のふたつ要素を連結(Cons)したもの」と再帰的に定義できます。これがinductiveなデータ型です。

Inductivestar:Type:=|S_ATOMofatomic|S_CONSofstar&star.

Coqはinductiveなデータ型に対して、inductionできるようになります。そのために、star_ind という公理が自動的に定義されます。これは、TLPの第7賞で説明されている "star induction" と同じものです。
Coqによる証明でも、この公理を直接使用することはなく、star型のデータに対して、inductionタクティクまたはelimタクティクを使用すると、この公理が適用されます。

Checkstar_ind:forallP:star->Prop,(foralla:atomic,P(S_ATOMa))->(forallx:star,Px->forally:star,Py->P(S_CONSxy))->foralls:star,Ps.

Star型についても、booleanの等号を定義して、論理式の等号にリフレクションできるようにします。

FixpointeqStar(xy:star):bool:=match(x,y)with|(S_ATOMa,S_ATOMb)=>a==b(* eqAtom *)|(S_CONSx1y1,S_CONSx2y2)=>eqStarx1x2&&eqStary1y2|_=>falseend.LemmaeqConsxyx'y':(x=x'/\y=y')->S_CONSxy=S_CONSx'y'.Proof.case=>HxHy.byrewriteHxHy.Qed.Lemmastar_eqP_1:forall(xy:star),eqStarxy->x=y.Proof.elim.-move=>a.elim=>b.+move/eqP=>H.(* ATOM どうし *)byrewriteH.+done.(* ATOM と CONS *)-move=>xHxyHy.elim.+done.(* CONS と ATOM *)+move=>x'IHxy'IHy.(* CONS と CONS *)move/andP.case=>Hxx'Hyy'.apply:eqCons.split.*byapply:(Hxx').*byapply:(Hyy').Qed.Lemmastar_eqP_2:forall(xy:star),x=y->eqStarxy.Proof.move=>xyH;rewrite-H{H}.elim:x.-bymove=>a/=.-move=>xHxy'Hy/=.byapply/andP;split.Qed.Lemmastar_eqP:forall(xy:star),reflect(x=y)(eqStarxy).Proof.move=>xy.apply:(iffPidP).-byapply:star_eqP_1.-byapply:star_eqP_2.Qed.Definitionstar_eqMixin:=@EqMixinstareqStarstar_eqP.Canonicalstar_eqType:=@EqTypestarstar_eqMixin.

Star型のboolの等式について、反射律と対称律が成立することを証明ておきます。リフレクションを使用してPropの等式に変換することで、簡単に証明できます。
この補題はあとで使用します。

Lemmarefl_eqStar(x:star):(x==x).Proof.byapply/eqP.Qed.Lemmasymm_eqStar(xy:star):(x==y)=(y==x).Proof.byapply/idP/idP;move/eqP=>H;rewriteH.Qed.

シンボルをS式の中に書くときに簡単になるような略記法を導入します。「'T」などと書くことができるので、quoted literal のように見えますが、「'」は記法(notation)の一部であることに注意してください。

Definitions_quote(s:string):star:=(S_ATOM(ATOM_SYMs)).Notation"\' s":=(S_ATOM(ATOM_SYMs))(atlevel60).Notation"'T":=(S_ATOM(ATOM_SYM"T")).Notation"'NIL":=(S_ATOM(ATOM_SYM"NIL")).Notation"'FOO":=(S_ATOM(ATOM_SYM"FOO")).Notation"'BAR":=(S_ATOM(ATOM_SYM"BAR")).Notation"'BAZ":=(S_ATOM(ATOM_SYM"BAZ")).Notation"'?":=(S_ATOM(ATOM_SYM"?")).Check'NIL:star.Check\'"aaa":star.Check\'"FOO":star.Check'FOO:star.Compute\'"FOO"=='FOO.(* true *)

自然数については、（S式の）アトムとの相互変換をする関数を用意します。

Definitions2n(x:star):nat:=matchxwith|S_ATOM(ATOM_NATn)=>n|_=>0end.Definitionn2s(n:nat):star:=S_ATOM(ATOM_NATn).

組込関数の定義

DefinitionCONS(xy:star):=S_CONSxy.DefinitionCAR(x:star):star:=matchxwith|S_ATOM_=>'NIL|S_CONSx_=>xend.DefinitionCDR(x:star):star:=matchxwith|S_ATOM_=>'NIL|S_CONS_y=>yend.DefinitionATOM(x:star):star:=matchxwith|S_ATOM_=>'T|S_CONS__=>'NILend.

IFとEQUALは、booleanの等式で判定します。
「IF」というラベルが使えないようなので、「_IF」とします。

Definition_IF(qae:star):star:=ifq=='NILtheneelsea.DefinitionEQUAL(xy:star):star:=ifx==ythen'Telse'NIL.Fixpoints_size(x:star):nat:=matchxwith|S_CONSab=>s_sizea+s_sizeb+1|_=>0end.DefinitionSIZE(x:star):star:=S_ATOM(ATOM_NAT(s_sizex)).EvalcomputeinSIZE(S_CONS'T(S_CONS'T'T)).(* S_ATOM (ATOM_NAT 2) *)DefinitionLT(xy:star):star:=ifs2nx<s2nythen'Telse'NIL.EvalcomputeinLT(n2s2)(n2s3).(* 'T *)DefinitionPLUS(xy:star):star:=n2s(s2nx+s2ny).EvalcomputeinPLUS(n2s2)(n2s3).(* S_ATOM (ATOM_NAT 5) *)

埋め込み

S式を論理式(Prop)に埋め込めるようにします。このとき、Lispの真偽の定義から、
「真」 iff 「'NILでないS式」
としなければいけません。実際には、S式からbooleanの等式 (x != 'NIL) へのコアーションを定義します。これは、一旦boolを経由することで、論理式(Prop)の否定も扱えるようにするためです。

Coercionis_not_nil(x:star):bool:=x!='NIL.(* ~~ eqStar x 'NIL *)Check(ATOM'T):star.Check(ATOM'T):Prop.Check~(ATOM'T):Prop.Check(ATOM(CONS'T'T)):star.Check(ATOM(CONS'T'T)):Prop.Check~(ATOM(CONS'T'T)):Prop.

Set Printing Coercions.を使うと、コアーションがどのように使われているか分かります。

Checkis_true(is_not_nil(ATOM'T)):Prop.Check~is_true(is_not_nil(ATOM'T)):Prop.

のちの証明で便利なように、'NILに関する補題を証明しておきます。

_ != _ は ~~(_ == _) の略記なので、次はis_not_nil と同じことです。が、忘れがちなので定義しておきます。

Lemmanot_nil_Eq:~~(q=='NIL)=q.Proof.done.Qed.

二重否定を解消するための補題です。

Lemmanot_not_nil__nil_Eq:~~(q!='NIL)=(q=='NIL).Proof.bycase:(q=='NIL).Qed.Lemmanot_q__q_nil_E(q:star):~q<->q='NIL.Proof.split.-rewrite/is_not_nil=>/negP.byrewritenot_not_nil__nil_E=>/eqP.-bymove=>Hq;rewriteHq.Qed.Lemmaq__q_not_nil_E(q:star):q<->q<>'NIL.Proof.rewrite/is_not_nil.split.-move=>H.byapply/eqP.-bymove/eqP.Qed.

タクティク

case_if (不使用)

_IFやEQUALを分解するためのタクティクを定義します。このなかではコアーションが機能しないことに注意してください。
ほとんどの場合、case: eqP または case: ifP で置き換えることができるので、使用していない。

Ltaccase_if:=matchgoalwith|[|-is_true(is_not_nil(if?Xthen_else_))]=>caseHq:X=>//end.

prove_nil

ゴールおよび前提の NIL に関する命題を q=NIL または q<>NIL に変換するものです。前提とゴールが同じでなくても、前提に q=NILとq<>NILの両方があるなら、矛盾からdoneで証明が終わることができます。
なお、~~(q==NIL) は q!=NIL と同じなので、条件としてあらわれません。

Ltacprove_nil:=repeatmatchgoalwith|[H:is_true(?q!='NIL)|-_]=>move/eqPinH|[H:is_true(is_not_nil?q)|-_]=>move/q__q_not_nil_EinH|[H:is_true(?q=='NIL)|-_]=>move/eqPinH|[H:~is_true(is_not_nil?q)|-_]=>move/not_q__q_nil_EinH|[|-is_true(?q!='NIL)]=>apply/eqP|[|-is_true(is_not_nil?q)]=>apply/q__q_not_nil_E|[|-is_true(?q=='NIL)]=>apply/eqP|[|-~is_true(is_not_nil?q)]=>apply/not_q__q_nil_Eend.

IFとEQUALの補題

TLPの定理は、(EQUAL X Y) または (IF Q 'T (EQUAL X Y)) または (IF Q (EQUAL X Y) 'T)のかたちをしているので、それをCoqの等式と同値であることを証明しておきます。これらは、TLPの定理の証明や、その定理を使うときに使用します。

Lemmaequal_eq{xy:star}:(EQUALxy)->x=y.Proof.rewrite/EQUAL.bycase:eqP.Qed.LemmaifAP{qxy:star}:(_IFq(EQUALxy)'T)<->(q->x=y).Proof.split.-rewrite/_IF/EQUAL.case:eqP=>Hq_nil.+move=>_Hq.byprove_nil.+bycase:eqP.-move=>H.rewrite/_IF;case:eqP=>//Hnot_nil_q.(* q <> NIL *)rewrite/EQUAL;case:ifP=>//=>Hx_ne_y.(* x <> y) *)exfalso.applynegbTinHx_ne_y.move/negPinHx_ne_y.apply:Hx_ne_y.apply/eqP.apply:H.move/eqPinHnot_nil_q.byprove_nil.Qed.LemmaifEP{qxy:star}:(_IFq'T(EQUALxy))<->(~q->x=y).Proof.split.-rewrite/_IF/EQUAL.case:eqP=>Hq_nil.+bycase:eqP.+move=>_Hnq.byprove_nil.-move=>H.rewrite/_IF;case:eqP=>//Hq_nil.(* q = NIL *)rewrite/EQUAL;case:eqP=>//=>Hx_ne_y.(* x <> y) *)exfalso.apply:Hx_ne_y.apply:H.byprove_nil.Qed.(*
 Set Printing Coercions.
 *)

J-Bobの「公理」の証明

ここまでに用意した道具を使って、証明をおこないます。

Theoremequal_same(x:star):(EQUALxx).Proof.rewrite/EQUAL.byrewriterefl_eqStar.Qed.Theorematom_cons(xy:star):(EQUAL(ATOM(CONSxy))'NIL).Proof.done.Qed.Theoremcar_cons(xy:star):(EQUAL(CAR(CONSxy))x).Proof.rewrite/EQUAL.bycase:eqP.Qed.Theoremcdr_cons(xy:star):(EQUAL(CDR(CONSxy))y).Proof.rewrite/EQUAL.bycase:eqP.Qed.Theoremequal_swap(xy:star):(EQUAL(EQUALxy)(EQUALyx)).Proof.rewrite{2}/EQUAL{2}/EQUAL.rewrite{1}symm_eqStar.byrewriteequal_same.Qed.Theoremequal_if(xy:star):(_IF(EQUALxy)(EQUALxy)'T).Proof.byrewrite/_IF;case:eqP;move/eqP.Qed.Theoremif_true(xy:star):(EQUAL(_IF'Txy)x).Proof.byrewrite/EQUAL;case:eqP.Qed.Theoremif_false(xy:star):(EQUAL(_IF'NILxy)y).Proof.byrewrite/EQUAL;case:eqP.Qed.Lemmal_if_same(xy:star):(_IFxyy)=y.Proof.case:x.-case.+done.(* NAT *)+rewrite/_IF=>s.bycase:eqP.(* SYM *)-done.(* CONS *)Qed.Theoremif_same(xy:star):(EQUAL(_IFxyy)y).Proof.rewritel_if_same.byrewriteequal_same.Qed.Theoremif_nest_A(xyz:star):(_IFx(EQUAL(_IFxyz)y)'T).Proof.rewrite/_IF;case:eqP=>//.byrewriteequal_same.Qed.Theoremif_nest_E(xyz:star):(_IFx'T(EQUAL(_IFxyz)z)).Proof.rewrite/_IF;case:eqP=>//.byrewriteequal_same.Qed.Lemmal_cons_car_cdr(x:star):(ATOMx)='NIL->(CONS(CARx)(CDRx))=x.Proof.move=>Hn.caseHc:x;rewrite/CONS=>//.byrewriteHcinHn.(* 前提の矛盾 *)Qed.Theoremcons_car_cdr(x:star):(_IF(ATOMx)'T(EQUAL(CONS(CARx)(CDRx))x)).Proof.rewrite/_IF;case:eqP=>Hq//.rewritel_cons_car_cdr//.byrewriteequal_same.Qed.Lemmal_size_car(x:star):ATOMx='NIL->s_size(CARx)<s_sizex.Proof.elim:x.-bymove=>aHc//.-move=>xHxyHyHc/=.(* s_size x < s_size x + s_size y + 1 *)byrewriteaddn1ltnSleq_addr.Qed.Lemmal_size_cdr(x:star):ATOMx='NIL->s_size(CDRx)<s_sizex.Proof.elim:x.-bymove=>aHc//.-move=>xHxyHyHc/=.(* s_size y < s_size x + s_size y + 1 *)rewrite[s_sizex+s_sizey]addnC.byrewriteaddn1ltnSleq_addr.Qed.Theoremsize_car(x:star):(_IF(ATOMx)'T(EQUAL(LT(SIZE(CARx))(SIZEx))'T)).Proof.apply/ifEP=>Hq.rewrite/LT/=l_size_car.-by[].-byapply/not_q__q_nil_E.Qed.Theoremsize_cdr(x:star):(_IF(ATOMx)'T(EQUAL(LT(SIZE(CDRx))(SIZEx))'T)).Proof.apply/ifEP=>Hq.rewrite/LT/=l_size_cdr.-by[].-byapply/not_q__q_nil_E.Qed.

「公理」を書換規則として使う

TLPでは、以上の「公理」を問題プログラムの 書換 に使用します。Coqの場合、書換 は、X = Y または Q -> (X = Y) のかたちでなければなりません。後者の場合、書換えにともなって、新しいゴールとしてQが追加されます。

「公理」の書換への変換

EQUALのかたちをした「公理」を等式に変換するには、equal_eq を使います。

SectionTLP_REWRITE_CHECK.Variablesqxy:star.SectionTLP_REWRITE_CHECK_0.Variablee:(EQUALxy).Checkequal_eqe:x=y.EndTLP_REWRITE_CHECK_0.

_IF式かたちをした「公理」を等式に変換するには、(iffLR ifAP) または (iffLR ifEP) を使います。

SectionTLP_REWRITE_CHECK_1.(** (_IF Q (EQUAL X Y) 'T) の場合。 *)Variableifa:(_IFq(EQUALxy)'T).CheckiffLRifAPifa:q->x=y.EndTLP_REWRITE_CHECK_1.SectionTLP_REWRITE_CHECK_2.(** (_IF Q 'T (EQUAL X Y)) の場合。 *)Variableife:(_IFq'T(EQUALxy)).CheckiffLRifEPife:~q->x=y.EndTLP_REWRITE_CHECK_2.EndTLP_REWRITE_CHECK.

書換の例

SectionTLP_REWRITE_SAMPLE.Variablesxyz:star.Checkequal_eq(equal_samex):x=x.CheckiffLRifAP(if_nest_Axyz):x->(_IFxyz)=y.CheckiffLRifEP(size_cdrx):~ATOMx->(LT(SIZE(CDRx))(SIZEx))='T.EndTLP_REWRITE_SAMPLE.EndTLP.

参考文献

[1] Daniel P. Friedman, Carl Eastlund, "The Little Prover", MIT Press, 2015.
https://mitpress.mit.edu/books/little-prover
中野圭介監訳、「定理証明手習い」、ラムダノート、2017。
https://www.lambdanote.com/collections/littleprover

[2] 「The Little Prover の memb?/remb をCoqで解いてみる（サブリスト改訂版）」
https://github.com/suharahiromichi/coq/blob/master/prog/coq_membp_remb_3.v

[3] Mathematical Components resources
http://ssr.msr-inria.inria.fr/

[4] 「リフレクションのしくみをつくる」
http://qiita.com/suharahiromichi/items/9cd109386278b4a22a63

6

Go to list of users who liked

9
0

Go to list of comments

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
6

Go to list of users who liked

9