31 March, 2012

[Coq] Specification of rev

そもそもの動機は(普通に再帰で書かれた) rev 関数の正しさを保証する最小の Unit Test ケースは何だろうみたいな話で、リストを逆転する rev 関数についての性質を話していて。

A:Type とし、f : list A -> list A な関数とするとき、

  • f (x::nil) = x::nil
  • f (xs ++ ys) = f ys ++ f xs

が成り立てば f = rev と言えるか?

については下記の様に肯定的に示せる。

Require Import FunctionalExtensionality.
Require Import List.
Require Import Omega.

Goal forall (A:Type)(f:list A->list A),
 (forall xs ys, f (xs++ys) = f ys ++ f xs) ->
 (forall x, f (x::nil) = x::nil) ->
 f = (@rev A).
Proof.
intros.
assert(f nil = nil).
 specialize(app_length (f nil) (f nil)). intro.
 rewrite <- (H nil nil) in H1. simpl in H1.
 assert(length (f nil) = 0).
  omega.
 induction (f nil).
  auto.
 simpl in H2. discriminate H2.
assert(forall x xs, f (x::xs) = f xs ++ (x::nil)).
 intros.
 replace (x::xs) with ((x::nil) ++ xs).
  rewrite H. rewrite H0. auto.
 simpl. auto.
extensionality l.
induction l.
 simpl. auto.
simpl. rewrite H2. rewrite IHl. auto.
Qed.

27 March, 2012

[Coq] Epistemic Logic

先日のFormal Methods Forum勉強会で話した話。

Epistemic Logicというのは「誰々は◯◯を知っている」「誰々は◯◯を知っていることは常識である」みたいな知識に関する事柄を扱う論理です。通常の命題 $P$ に対して、「$\alpha$は$P$を知っている」を表す $K_{\alpha} P$ や、「$P$は皆の常識である」を表す$C P$といった様相記号 $K_{\alpha}$ や  $C$ を用いた様相論理になります --- ということは、"Metareasoning for multi-agent epistemic logics" という論文 (PDF) に載っています。

酒井さんのヒビルテの「Alloyで知識論理を使って論理パズルを解く」という記事に載っている問題が上記の論文にも載っていて、その論文に従い Coq で定式化してみました。

Coq のコードは github の https://github.com/tmiya/coq/blob/master/epistemic/modal.v に上げてあります。

大雑把な解説をすると、論文に載っていた epistemic logic の公理系を Coq で下記の様に記述します。

Inductive theorem : (Ensemble prop) -> prop -> Prop :=
| intro_and : forall G p q, (G |-- p) -> (G |-- q) -> (G |-- (p && q))
| elim_and_l : forall G p q, (G |-- (p && q)) -> (G |-- p)
| elim_and_r : forall G p q, (G |-- (p && q)) -> (G |-- q)
| intro_or_l : forall G p q, (G |-- p) -> (G |-- (p || q))
| intro_or_r : forall G p q, (G |-- q) -> (G |-- (p || q))
| elim_or : forall G p1 p2 q, 
   (G |-- (p1 || p2)) -> ((p1::G) |-- q) -> ((p2::G) |-- q) -> (G |-- q)
| intro_imp : forall G p q, ((p::G) |-- q) -> (G |-- (p --> q))
| elim_imp : forall G p q, (G |-- (p --> q)) -> (G |-- p) -> (G |-- q)
| elim_not : forall G p, (G |-- !(!p)) -> (G |-- p)
| intro_not : forall G p, ((p::G) |-- F) -> (G |-- !p)
| reflex : forall G p, (p::G) |-- p
| dilution : forall G G' p, (G |-- p) -> ((G _+_ G') |-- p)
| intro_false : forall G p, (G |-- (p && (!p))) -> (G |-- F)
| intro_true : forall G, G |-- T
| rule_K : forall G a p q, G |-- ((K a (p --> q)) --> (K a p --> K a q))
| rule_T : forall G a p, G |-- (K a p --> p)
| intro_C : forall G p, (O |-- p) -> (G |-- (C p))
| elim_C : forall G a p, G |-- (C p --> K a p)
| rule_C_K : forall G p q, G |-- ((C (p --> q)) --> (C p --> C q))
| rule_R : forall G a p, G |-- (C p --> C (K a p))
where "G |-- p" := (theorem G p).

これを使って今回示したい定理は、
(* A1 may wear red hat (=M1) or white hat (= !M1).
   A2 may wear red hat (=M2) or white hat (= !M2). *) 
Parameter A1 A2: agent.
Parameter M1 M2: prop.
(* S1 = A1 that said "I do not know whether I wears a red hat".
        Therefore, prop "A1 does not know M1", 
        is commom knowledge. *)
Definition S1 := C (!(K A1 M1)).
(* S2 = Because the king said "At least one of A1 and A2
        wears the red hat". Therefore "M1 or M2" is
        common knowledge. *)
Definition S2 := C(M2 || M1).
(* S3 = Because A1 can see the A2's hat, A1 would know
        !M2 if !M2 stood, and this is common knowledge. *)
Definition S3 := C(!M2 --> K A1 (!M2)). 
(* After A1 said "I do not know whether I wears a red hat",
   using the common knowledge {S1, S2, S3}, it becomes the
   common knowledge that A2 wears the red hat. *) 
Theorem two_wise_men : S1::S2::S3::O |-- C M2.
を証明する、ということになります。
証明に際しては、この証明の導出に関する幾つかの tactic を定義するなどを多少工夫してみました。

残念ながら勉強会当日には間に合わなかったけど、ようやく証明出来ました。


25 March, 2012

[Coq][Alloy] Proof of Alloy Example

本日の Formal Methods Forum で扱った Alloy の問題で、
assert union {
  all s:set univ, p,q : univ -> univ |
    s.(p + q) = s.p + s.q
}
check union for 4
で Counterexample が見つからない、従ってこの関係式は正しい、というのを確認する問題があった。
しかし、正しさを確認するには証明が必要であろう。

Coq で集合を扱うライブラリSets.Ensemblesというのもあるがここでは自前で集合演算などを定義して証明してみた。集合 S とは univ -> Prop というmembershipを表す述語であり、二項関係 xRy というのも univ -> univ -> Prop という述語であると言う点に注意すれば、あとは単に定義を述語論理で記述するだけである。

Section Alloy_Ex.

(* univ *)
Variable univ : Set.
(* relation *)
Definition Rel1 := univ -> Prop. (* arity=1 *)
Definition Rel2 := univ -> univ -> Prop. (* arity=2 *)

(* set = Rel1 *)
(* x is an element of s *)
Definition In1 (s:Rel1)(x:univ):Prop := s x.
(* A is a subset of B *)
Definition subset1 (A B:Rel1):Prop :=
 forall x:univ, In1 A x -> In1 B x.
(* A = B iff A includes B and B includes A *)
Definition eq1 (A B:Rel1):Prop :=
 (subset1 A B) /\ (subset1 B A).

(* join operation *)
Definition join12 (s:Rel1)(p:Rel2):Rel1 :=
 fun y:univ => (exists x:univ, In1 s x /\ p x y).

(* union *)
Definition union1 (p q:Rel1):Rel1 :=
 fun x:univ => (p x \/ q x).
Definition union2 (p q:Rel2):Rel2 :=
 fun x:univ => fun y:univ => (p x y \/ q x y).

Theorem alloy_ex_union : forall (s:Rel1)(p q:Rel2),
 eq1 (join12 s (union2 p q)) (union1 (join12 s p) (join12 s q)).
Proof.
intros s p q. unfold eq1. split.
 unfold subset1. intros x H.
 unfold In1 in *. unfold join12 in *.
 destruct H as [x0 [H1 H2]]. unfold union2 in H2.
 unfold union1.
 destruct H2; [left|right]; exists x0; split; auto.
unfold subset1. intros x H.
unfold In1 in *. unfold union1 in H.
unfold join12. unfold union2.
destruct H; unfold join12 in H; destruct H as [x0 [H1 H2]];
exists x0; split; auto.
Qed.