More than 5 years have passed since last update.

@suharahiromichi(須原浩道)

SSReflectのViewとView Hintについてのメモ

Last updated at 2019-08-16Posted at 2014-10-26

SSReflectのViewとView Hintについてのメモ

2014_10_26 @suharahiromichi
2019_5_7 @suharahiromichi
2019_8_16 @suharahiromichi

この文書のコードは、以下にあります。
https://github.com/suharahiromichi/coq/blob/master/ssr/ssr_ais_view_hint.v

ProofCafe Nr.42 で、「An introduction to small scale reflection in Coq」
https://hal.inria.fr/inria-00515548/PDF/main-rr.pdf
の4章「4 Small scale reflection, first examples」の説明をしましたが、その補足（訂正を含む）を以下にまとめます。

ご注意：この文章では、説明を簡単にするために、セクションの中でVariableを宣言しています。そのため、「Viewを使わない例」が実際よりも単純にみえるかもしれません。
通常の証明をViewを使わないように書き直す場合など、機械的な書き直しでエラーになるでしょう。その場合、適宜に、述語の引数を補う必要があります（アンダースコア「_」でもよい場合がある）。そのあたりについては、上記の文献を参照してください。

FrommathcompRequireImportall_ssreflect.

View

CoqのSSReflct拡張では、move/V や apply/V のかたちで前提（スタックトップ）や、ゴールの書き換えができますが、このときのVをViewと呼びます。
実際は前提またはゴールに対する apply の略記であり、おなじことがStandard Coqでもできることがわかります。

SectionSample1.VariablePQ:bool->Prop.HypothesisP2Q:foralla,Pa->Qa.

仮定の書き換え：Interpreting assumptions

ゴール「△->○」のとき、△の部分（スタックトップ）を書き換えます。

Goalforalla,Pa->Qa.Proof.move=>a.move/P2Q.(* Q a -> Q a *)Undo1.move=>HPa;move:{HPa}(P2QaHPa).Undo1.move=>HPa;applyP2QinHPa;move:HPa.apply.Undo2.introHPa;applyP2QinHPa;applyHPa.(* Standard Coq風 *)Qed.

ゴールの書き換え：Interpreting goals

ゴール全体を書き換えます。ゴールが△->○の場合はその全体が対象になりますが、通常はintro(move=>)して○だけを対象にします。

Goalforalla,Pa->Qa.Proof.move=>aHPa.(* Goal : Q a *)apply/P2Q;applyHPa.(* 最初のapplyの後、HPa : P a |- P a *)Undo1.apply:(P2QaHPa).(* apply (P2Q a HPa) でもよい。 *)Undo1.applyP2Q;applyHPa.(* Standard Coq風、一番簡単？ *)Qed.EndSample1.

View Hint

View には、前節に加えてView Hintとして宣言された定理（補題）を自動的に補う機能があります。View Hint のひとつに、iffLR があります。

CheckiffLR:forallPQ:Prop,(P<->Q)->P->Q.

「P<->Q」のかたちをした述語をViewとして使った場合、iffLRが自動的に補われ、「P->Q」として適用されるわけです。

SectionSample2.VariablePQ:bool->Prop.HypothesisPQequiv:foralla,Pa<->Qa.

仮定の書き換え：Interpreting assumptions

Goalforalla,Pa->Qa.Proof.move=>a.move/PQequiv.(* Q a -> Q a *)Undo1.Check(iffLR(PQequiva)):Pa->Qa.move/(iffLR(PQequiva)).(* a は _ でもよい。 *)Undo1.move=>HPa;move:{HPa}(iffLR(PQequiva)HPa).Undo1.move=>HPa;apply(iffLR(PQequiva))inHPa;move:HPa.Undo1.(* 実は、Standard Coq のapplyは、iffLR と iffRL を補完できる。 *)move=>HPa;applyPQequivinHPa;move:HPa.apply.Qed.

ゴールの書き換え：Interpreting goals

Goalforalla,Pa->Qa.Proof.move=>aHPa.(* Goal : Q a *)apply/PQequiv;applyHPa.Undo1.Check(iffLR(PQequiva)):Pa->Qa.apply/(iffLR(PQequiva));applyHPa.Undo1.apply:(iffLR(PQequiva)HPa).Undo1.apply(iffLR(PQequiva));applyHPa.Undo1.(* 実は、Standard Coq のapplyは、iffLR と iffRL を補完できる。 *)applyPQequiv;applyHPa.Qed.EndSample2.

標準のView Hint の例 (iffLR, iffRL, iffLRn, iffRLn)

SSReflectのソースコードを見ると、theories/ssreflect.v の最後に四つのView Hintが宣言されています。

CheckiffLR:forallPQ:Prop,(P<->Q)->P->Q.CheckiffRL:forallPQ:Prop,(P<->Q)->Q->P.CheckiffLRn:forallPQ:Prop,(P<->Q)->~P->~Q.CheckiffRLn:forallPQ:Prop,(P<->Q)->~Q->~P.SectionSample3.VariablePQ:bool->Prop.Variablea:bool.HypothesisPQequiv:Pa<->Qa.CheckiffLRPQequiv:Pa->Qa.CheckiffRLPQequiv:Qa->Pa.CheckiffLRnPQequiv:~Pa->~Qa.CheckiffRLnPQequiv:~Qa->~Pa.

仮定の書き換え：Interpreting assumptions

端折った言い方をすると、move/PQequiv は、move/(iffLR PQequiv) または move/(iffRL PQequiv) または move/(iffLRn PQequiv) または move/(iffRLn PQequiv)のどれかが選ばれて使われるので、以下の4種類のゴールがすべて、move/PQequiv をつかって証明できます。

GoalPa->Qa.move/PQequiv.byapply.Qed.(* Q a -> Q a *)GoalQa->Pa.move/PQequiv.byapply.Qed.(* P a -> P a *)Goal~Pa->~Qa.move/PQequiv.byapply.Qed.(* ~ Q a -> ~ Q a *)Goal~Qa->~Pa.move/PQequiv.byapply.Qed.(* ~ P a -> ~ P a *)

ゴールの書き換え：Interpreting goals

同様に、apply/PQequiv は、apply/(iffLR PQequiv) または apply/(iffRL PQequiv) または apply/(iffLRn PQequiv) または apply/(iffRLn PQequiv)のどれかが選ばれて使われるので、以下の4種類のゴールがすべて、apply/PQequiv をつかって証明できます。

GoalPa->Qa.move=>H;apply/PQequiv.byapplyH.Qed.(* H : P a |- P a *)GoalQa->Pa.move=>H;apply/PQequiv.byapplyH.Qed.(* H : Q a |- Q a *)Goal~Pa->~Qa.move=>H;apply/PQequiv.byapplyH.Qed.(* H : ~ P a -> ~ P a *)Goal~Qa->~Pa.move=>H;apply/PQequiv.byapplyH.Qed.(* H : ~ Q a -> ~ Q a *)EndSample3.

reflect述語を使用可能にするView Hint

より重要なView Hintに elimT と intorT があります。このView Hintのおがけで、andPやorPのような「reclect P b」のかたちのreflect述語をViewに書くことができます。

CheckelimT:forall(P:Prop)(b:bool),reflectPb->b->P.CheckintroT:forall(P:Prop)(b:bool),reflectPb->P->b.SectionSample4.Variableab:bool.

仮定の書き換え：Interpreting assumptions

HypothesisandP:reflect(a/\b)(a&&b).CheckelimTandP:a&&b->a/\b.Goala&&b->a.Proof.move/andP.(* a /\ b -> a /\ b *)Undo1.move/(elimTandP).Undo1.move=>Hab;move:{Hab}(elimTandPHab).Undo1.move=>Hab;apply(elimTandP)inHab;move:Hab.case;by[].Qed.

ゴールの書き換え：Interpreting goals

HypothesisorP:reflect(a\/b)(a||b).CheckintroTorP:a\/b->a||b.Goala->a||b.Proof.move=>Ha.apply/orP.(* Hab : a |- a || b *)Undo1.apply/(introTorP).Undo1.apply:(introTorP).left;by[].Qed.(* 次はゴール「a&&b->a/\b」に対して、「a&&b->a/\b」を適用している。
「△->○」全体を対象にしているので一般的な例になっていない。要補足 *)Goala&&b->a/\b.Proof.apply/andP.Undo1.apply/(elimTandP).Qed.EndSample4.

ゴールがequivalence（「=」）であるときに、reflect述語を使用可能にするView Hint

ゴールが「=」のときは、とりあえず「apply/idP/idP」と、覚えておいてもよいですが、このとき、左の/idPにはintroTFが、右の/idPにはequivPifが、View Hintとして使われます。

CheckintroTF:forall(P:Prop)(bc:bool),reflectPb->(ifcthenPelse~P)->b=c.CheckequivPif:forall(PQ:Prop)(b:bool),reflectPb->(Q->P)->(P->Q)->ifbthenQelse~Q.SectionSample4_5.Variableab:bool.HypothesisidP:forallb:bool,reflectbb.Goala||b=b||a.Proof.apply/idP/idP.Undo1.CheckintroTF(idP(a||b)).apply(introTF(idP(a||b))).CheckequivPif(idP(b||a)).apply(equivPif(idP(b||a))).(* 説明のため、冗長に書いています。 *)-move/orP=>H;apply/orP;case:H;by[right|left].-move/orP=>H;apply/orP;case:H;by[right|left].Qed.

View Hint以前の話題ですが、次のようにも書けます。

Goala||b=b||a.Proof.apply/orP/orP;case;by[right|left].Qed.EndSample4_5.

補足

View Hint の elimT と introT で、eqP などのreflect述語によって、Prop型と bool型を相互変換できると考えてまちがいではありませんが、
ゴールないし仮定がbool型である場合は（コアーションの）b = true を含めてView Hint が探されるため、elimTF と introTF が使われるようです。
これは、b = false である場合にも適用されます。否定を含めて考えると、Prop型と bool型との相互変換より以上のことができるます。
たとえば、以下のすべてが、move/eqP または apply/eqP で変換可能です。

SectionSample4_6.Variablen:nat.Check(@elimT(n=42)(n==42)eqP):n==42->n=42.Check(@elimN(n=42)(n==42)eqP):n!=42->n<>42.Check(@elimTF(n=42)(n==42)trueeqP):(n==42)=true->n=42.Check(@elimNTF(n=42)(n==42)trueeqP):(n!=42)=true->n<>42.Check(@elimTF(n=42)(n==42)falseeqP):(n==42)=false->n<>42.Check(@elimNTF(n=42)(n==42)falseeqP):(n!=42)=false->n=42.Check(@introT(n=42)(n==42)eqP):n=42->(n==42).Check(@introN(n=42)(n==42)eqP):n<>42->n!=42.Check(@introTF(n=42)(n==42)trueeqP):n=42->(n==42)=true.Check(@introNTF(n=42)(n==42)trueeqP):n<>42->(n!=42)=true.Check(@introTF(n=42)(n==42)falseeqP):n<>42->(n==42)=false.Check(@introNTF(n=42)(n==42)falseeqP):n=42->(n!=42)=false.EndSample4_6.

まだ説明できていない事項

move/とapply/のView Hintの区別がある理由。
独自にView Hintを定義する方法。
上記以外のssrboolにふくまれるView Hint。
Standard Coqと比較や、それへの書き換え。

のこりのView Hint

標準定義のView Hintの一覧

(* move/で使用： *)CheckelimTF:forall(P:Prop)(bc:bool),reflectPb->b=c->ifcthenPelse~P.CheckelimNTF:forall(P:Prop)(bc:bool),reflectPb->~~b=c->ifcthen~PelseP.CheckelimTFn:forall(P:Prop)(bc:bool),reflectP(~~b)->b=c->ifcthen~PelseP.(* apply/で使用： *)CheckelimT:forall(P:Prop)(b:bool),reflectPb->b->P.CheckelimTn:forall(P:Prop)(b':bool),reflectP(~~b')->b'->~P.CheckelimN:forall(P:Prop)(b:bool),reflectPb->~~b->~P.(* apply//で使用： *)CheckequivPif:forall(PQ:Prop)(b:bool),reflectPb->(Q->P)->(P->Q)->ifbthenQelse~Q.CheckequivPifn:forall(PQ:Prop)(b:bool),reflectP(~~b)->(Q->P)->(P->Q)->ifbthen~QelseQ.(* move/で使用： *)CheckintroTF:forall(P:Prop)(bc:bool),reflectPb->(ifcthenPelse~P)->b=c.CheckintroNTF:forall(P:Prop)(bc:bool),reflectPb->(ifcthen~PelseP)->~~b=c.CheckintroTFn:forall(P:Prop)(bc:bool),reflectP(~~b)->(ifcthen~PelseP)->b=c.(* apply/で使用： *)CheckintroT:forall(P:Prop)(b:bool),reflectPb->P->b.CheckintroTn:forall(P:Prop)(b':bool),reflectP(~~b')->~P->b'.CheckintroN:forall(P:Prop)(b:bool),reflectPb->~P->~~b.(* apply//で使用： *)CheckxorPif:forall(PQ:Prop)(b:bool),reflectPb->Q\/P->~(Q/\P)->ifbthen~QelseQ.CheckxorPifn:forall(PQ:Prop)(b:bool),reflectP(~~b)->Q\/P->~(Q/\P)->ifbthenQelse~Q.SectionSample5.Variableab:bool.HypothesisandP:reflect(a/\b)(a&&b).HypothesisnandP:reflect(~~a\/~~b)(~~(a&&b)).HypothesisidP:reflectbb.Variablemn:nat.HypothesiseqP:reflect(m=n)(m==n).HypothesisnegP:reflect(~b)(~~b).HypothesisnegPn:reflectb(~~~~b).

andPまたはnandP を使う例

Variablec:bool.VariableQ:Prop.(* move/で使用： *)CheckelimTFandP(c:=c):a&&b=c->ifcthena/\belse~(a/\b).CheckelimNTFandP:~~(a&&b)=c->ifcthen~(a/\b)elsea/\b.CheckelimTFnnandP:a&&b=c->ifcthen~(~~a\/~~b)else~~a\/~~b.(* apply/で使用： *)CheckelimTandP:a&&b->a/\b.CheckelimTnnandP:a&&b->~(~~a\/~~b).CheckelimNandP:~~(a&&b)->~(a/\b).(* apply//で使用： *)CheckequivPifandP(Q:=Q):(Q->a/\b)->(a/\b->Q)->ifa&&bthenQelse~Q.CheckequivPifnnandP:(Q->~~a\/~~b)->(~~a\/~~b->Q)->ifa&&bthen~QelseQ.(* move/で使用： *)CheckintroTFandP:(ifcthena/\belse~(a/\b))->a&&b=c.CheckintroNTFandP:(ifcthen~(a/\b)elsea/\b)->~~(a&&b)=c.CheckintroTFnnandP:(ifcthen~(~~a\/~~b)else~~a\/~~b)->a&&b=c.(* apply/で使用： *)CheckintroTandP:a/\b->a&&b.CheckintroTnnandP:~(~~a\/~~b)->a&&b.CheckintroNandP:~(a/\b)->~~(a&&b).(* apply//で使用： *)CheckxorPifandP(Q:=Q):Q\/a/\b->~(Q/\a/\b)->ifa&&bthen~QelseQ.CheckxorPifnnandP:Q\/~~a\/~~b->~(Q/\(~~a\/~~b))->ifa&&bthenQelse~Q.

idPまたはidPn を使う例

(* move/で使用： *)CheckelimTFidP(c:=c).(* : b = c -> if c then b else ~ b *)CheckelimNTFidP:~~b=c->ifcthen~belseb.CheckelimTFnidPn:b=c->ifcthen~~~belse~~b.(* apply/で使用 ： *)CheckelimTidP:b->b.CheckelimTnidPn:b->~~~b.CheckelimNidP:~~b->~b.(* apply//で使用： *)CheckequivPifidP(Q:=Q):(Q->b)->(b->Q)->ifbthenQelse~Q.CheckequivPifnidPn:(c->~~b)->(~~b->c)->ifbthen~celsec.(* move/で使用： *)CheckintroTFidP(c:=c).(* (if c then b else ~ b) -> b = c *)CheckintroNTFidP:(ifcthen~belseb)->~~b=c.CheckintroTFnidPn:(ifcthen~~~belse~~b)->b=c.(* apply/で使用： *)CheckintroTidP:b->b.CheckintroTnidPn:~~~b->b.CheckintroNidP:~b->~~b.(* apply//で使用： *)CheckxorPifidP(Q:=Q):Q\/b->~(Q/\b)->ifbthen~QelseQ.CheckxorPifnidPn(Q:=Q)(b:=b):Q\/~~b->~(Q/\~~b)->ifbthenQelse~Q.

eqP を使う例

(* move/で使用： *)CheckelimTFeqP(c:=c):(m==n)=c->ifcthenm=nelsem<>n.CheckelimNTFeqP(c:=c):(m!=n)=c->ifcthenm<>nelsem=n.(* apply/で使用 ： *)CheckelimTeqP:m==n->m=n.CheckelimNeqP:m!=n->m<>n.(* apply//で使用： *)CheckequivPifeqP(Q:=Q):(Q->m=n)->(m=n->Q)->ifm==nthenQelse~Q.(* move/で使用： *)CheckintroTFeqP(c:=c):(ifcthenm=nelsem<>n)->(m==n)=c.CheckintroNTFeqP(c:=c):(ifcthenm<>nelsem=n)->(m!=n)=c.(* apply/で使用： *)CheckintroTeqP:m=n->m==n.CheckintroNeqP:m<>n->m!=n.(* apply//で使用： *)CheckxorPifeqP(Q:=Q):Q\/m=n->~(Q/\m=n)->ifm==nthen~QelseQ.

negPまたはnegPn を使う例

(* move/で使用： *)CheckelimTFnegP(c:=c):~~b=c->ifcthen~belse~~b.CheckelimTFnegPn(c:=c).(* : ~~ ~~ b = c -> if c then b else ~ b *)CheckelimNTFnegP(c:=c):~~~~b=c->ifcthen~~belse~b.CheckelimNTFnegPn(c:=c):~~~~~~b=c->ifcthen~belseb.CheckelimTFnnegP(c:=c):b=c->ifcthen~~belse~b.CheckelimTFnnegPn(c:=c):~~b=c->ifcthen~belseb.(* apply/で使用 ： *)CheckelimTnegP:~~b->~b.CheckelimTnegPn:~~~~b->b.CheckelimTnnegP:b->~~b.CheckelimTnnegPn:~~b->~b.CheckelimNnegP:~~~~b->~~b.CheckelimNnegPn:~~~~~~b->~b.(* apply//で使用： *)CheckequivPifnegP(Q:=Q):(Q->~b)->(~b->Q)->if~~bthenQelse~Q.CheckequivPifnegPn(Q:=Q):(Q->b)->(b->Q)->if~~~~bthenQelse~Q.CheckequivPifnnegP(Q:=Q):(Q->~b)->(~b->Q)->ifbthen~QelseQ.CheckequivPifnnegPn(Q:=Q):(Q->b)->(b->Q)->if~~bthen~QelseQ.(* move/で使用： *)CheckintroTFnegP(c:=c):(ifcthen~belse~~b)->~~b=c.CheckintroTFnegPn(c:=c).(* (if c then b else ~ b) -> ~~ ~~ b = c. *)CheckintroNTFnegP(c:=c):(ifcthen~~belse~b)->~~~~b=c.CheckintroNTFnegPn(c:=c):(ifcthen~belseb)->~~~~~~b=c.CheckintroTFnnegP(c:=c):(ifcthen~~belse~b)->b=c.CheckintroTFnnegPn(c:=c):(ifcthen~belseb)->~~b=c.(* apply/で使用： *)CheckintroTnegP:~b->~~b.CheckintroTnegPn:b->~~~~b.CheckintroTnnegP:~~b->b.CheckintroTnnegPn:~b->~~b.CheckintroNnegP:~~b->~~~~b.CheckintroNnegPn:~b->~~~~~~b.(* apply//で使用： *)CheckxorPifnegP(Q:=Q):Q\/~b->~(Q/\~b)->if~~bthen~QelseQ.CheckxorPifnegPn(Q:=Q):Q\/b->~(Q/\b)->if~~~~bthen~QelseQ.CheckxorPifnnegP(Q:=Q)(b:=b):Q\/~b->~(Q/\~b)->ifbthenQelse~Q.EndSample5.

Go to list of users who liked

Go to list of comments

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

URL: https://qiita.com/suharahiromichi/items/02c7f42809f2d20ba11a