[Coq] How to Find Unreachable Nodes

不正な状態遷移を見つけるアルゴリズム @ kencobaの日記経由。

答えを出すだけならこんなのでもOK?　元の問題の規模が判らないが、この程度に小さな問題なら auto で探索出来る。

Axiom O A B C D E F G H I:Prop.
Axiom OA : O -> A.
Axiom AB : A -> B.
Axiom BC : B -> C.
Axiom CB : C -> B.
Axiom CA : C -> A.
Axiom DB : D -> B.
Axiom DH : D -> H.
Axiom HD : D -> H.
Axiom EF : E -> F.
Axiom FG : F -> G.
Axiom GF : G -> F.
Axiom GE : G -> E.
Axiom II : I -> I.

Hint Resolve OA AB BC CB CA DB DH HD EF FG GF GE II.

Goal O -> A. info auto. Qed.
Goal O -> B. info auto. Qed.
Goal O -> C. info auto. Qed.

Goal O -> D.などはauto.で証明出来ないので、path が無いと判る。