Coqで命題論理の標準形 - にわとり小屋でのプログラミング

この記事はTppMark11の問題をCoqでやってみたという内容である。

問題はこちら:

docs.google.com

命題論理式と同値であることの定義

命題論理式の定義

Inductive Term :=
| Var(v : Var.T)
| Neg(t : Term)
| And(t1: Term)(t2: Term)
| Or(t1: Term)(t2: Term)
| Impl(t1: Term)(t2: Term)
| TRUE | FALSE
.

同値であることの定義

変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。

Fixpoint eval ctx t : bool :=
  match t with
  | Var v => ctx v
  | Neg t => negb (eval ctx t)
  | And t1 t2 => andb (eval ctx t1) (eval ctx t2)
  | Or t1 t2 => orb (eval ctx t1) (eval ctx t2)
  | Impl t1 t2 => implb (eval ctx t1)(eval ctx t2)
  | TRUE => true
  | FALSE => false
  end.

2つの命題の同値性はevalを使って次のように定義。

Definition Equiv (P Q: Term) := forall context,
  eval context P = eval context Q.

ここまではごく自然で素直な定義だと思う。

標準形の形式化と検証

問題は3.2の性質で、これを満たす標準形は私はこれまであまりみたことがなかった。

3.2 PとQが同値であれば、nf(P)とnf(Q)は形が全く等しい命題論理式である。
TPPmark-11th.docx - Google ドキュメント

例えば命題式 (P /\ P) と P は同値になるが、両者ともに連言標準形(Conjunctive normal form)であり形は等しくない。また、(P /\ Q) \/ (¬P /\ Q) と Q のように変数の数が違う命題式が同値になることもある。

これを解くために、命題論理式を真偽表へ落としこんでから復元するというアプローチを考えてみた。

真偽表への変換と正しさの証明

Definition toTable (t:Term) : TruthTable.T.
  refine ({|
    TruthTable.vars := toVars t
    ; TruthTable.map := toMap t
  |}).
  ...

Definition ofTable (table : TruthTable.T) : Term :=
  Map.elements table.(TruthTable.map)
  |> List.filter snd
  |> List.map fst
  |> List.map (fun bs => List.map2 literal table.(TruthTable.vars) bs)
  |> List.map (List.fold_right (And) TRUE)
  |> List.fold_right (Or) FALSE.

変換が正しく定義されていることを示すために次を証明した。

Lemma safe_toTable : forall context term,
  Some (eval context term) = TruthTable.eval context (toTable term).

Lemma safe_ofTable : forall context table,
  TruthTable.eval context table = Some (eval context (ofTable table)).

真偽表の最小化と一意性

以上でオッケーかと最初は考えていたけれど、実は無駄な変数があった場合、同値であっても真偽表が一意に定まらない。この問題を解決するために真偽値に影響を与えない変数を削除するという処理(elimVars)を導入した。

Definition elimVars (tbl : T) : T

そして、elimVarsの健全性(意味を変えないこと)と、一意性を証明した。

Theorem soundness : forall (x : T),
  sameSemantics x (elimVars x).
Theorem uniqueness : forall (x y: T),
  sameSemantics x y -> elimVars x == elimVars y.

標準形の定義と問題となっていた3.1, 3.2の証明

ここまでできればあとは簡単。問題にあったnfを定義と証明は以下の通り。

(** * 標準形にする関数の定義 *)
Definition nf (t : Term) : Term :=
  toTable t
  |> TruthTable.elimVars
  |> ofTable.

(** * 3.1の証明 *)
Theorem soundness_nf : forall t, Equiv t (nf t).
Proof.
 intros t. unfold Equiv. intros ctx. unfold nf, revapply.
 assert (Some (eval ctx t) = Some (eval ctx (ofTable (TruthTable.elimVars (toTable t))))).
 - rewrite <- safe_ofTable. rewrite <- TruthTable.soundness.
   now apply safe_toTable.
 - now injection H.
Qed.

(** * 3.2の証明 *)
Theorem main : forall P Q: Term, Equiv P Q -> nf P = nf Q.
Proof.
 intros. unfold nf, revapply.
 apply lem_ofTable.
 apply (TruthTable.uniqueness (toTable P) (toTable Q)).
 intro context. do 2 rewrite <- safe_toTable.
 unfold Equiv in H. now rewrite H.
Qed.

雑感

謝辞：chiguriさんに証明を一部手伝ってもらった。大変感謝。
まだ一部の小さな補題がAdmittedだけれどやればできると思っている
3日くらいでできるかと思ったけれど思ったより時間がかかった
Proof Summit で定義をいくらでもちょろまかせば簡単になると言われたけれど、ちょっといい例が思いつかない。他の人の解答に期待

Coqのコード全体はこちらから参照可能:github.com