[Coq] Group on Setoid

@cocoatomo さんの blog に Python で群論をという記事があったので、同じことを Coq でやってみました。

証明を含む実際のコードは https://github.com/tmiya/coq/blob/master/group/setoid_group.v にあります。以下は解説です。
将来的に剰余群みたいなものを定義することを考え、集合の上の等号を自分で定義出来る様にします。つまり同値関係を定義し、setoid の上に群を定義することになります。

まず setoid の定義に必要なライブラリと、サンプルを証明するのに必要なライブラリを Import します。

Require Import Relation_Definitions Setoid Morphisms.
Require Import Arith Omega.

次いでサンプルとして、$\mathbb{Z}' := \{(a,b)\; | \; a,b \in \mathbb{N}\}$ として自然数の組を使って整数を表す例を考えます。同値関係は $(a,b) \sim (a',b') \Leftrightarrow a+b' = a'+b$ と定義し、$z=(a,b)$ に対して $z^{-1}= (b,a)$, $(a,b) \ast (a',b') = (a+a',b+b')$ と定義すると、整数 $\mathbb{Z}'$ 上の加法に関する群を構成出来ます --- ということを後から示します。まずは $\mathbb{Z}'$ とその上の演算を定義します。

Inductive Z' : Set :=
| mkZ' : nat -> nat -> Z'.

Definition eq'(z1 z2:Z') : Prop :=
  match z1,z2 with
  | (mkZ' p1 n1),(mkZ' p2 n2) => (p1+n2 = p2+n1)
  end.

Definition minus'(z:Z') :=
  match z with
  | mkZ' a b => mkZ' b a
  end.

Definition plus'(z1 z2:Z') :=
  match z1,z2 with
  | (mkZ' a1 b1),(mkZ' a2 b2) => (mkZ' (a1+a2) (b1+b2))
  end.

さて eq' が Z' の同値関係になっていることを示す必要があります。 以下の様に示します。Add Paramereic Relation 云々は setoid であることを Coq に登録する手続きです。

Lemma refl_eq' : reflexive _ eq'.
Lemma sym_eq' : symmetric _ eq'.
Lemma trans_eq' : transitive _ eq'.

Add Parametric Relation : Z' eq'
  reflexivity proved by refl_eq'
  symmetry proved by sym_eq'
  transitivity proved by trans_eq' as Z'_setoid.

次いで、minus', plus' が well-defined であることを示す必要があります。どういうことかというと、$z, z' \in \mathbb{Z}'$ について、$z \sim z'$ ならば $z^{-1} \sim z'^{-1}$ などを示す必要があるということです。これも以下の様に示します。

Add Parametric Morphism : 
  minus' with signature (eq' ==> eq') as minus'_mor.

Add Parametric Morphism :
  plus' with signature (eq' ==> eq' ==> eq') as plus'_mor.

ここまできたら、群の定義をします。同値関係の話は通常の数学では自明として述べないと思いますが、後々の証明で使いたい公理なので群の定義の他に含めて書くことにします。

Class Group {S:Set}(eq:S->S->Prop)
  (e:S)(inv:S->S)(op:S->S->S) := {
  equiv : Equivalence eq ;
  equiv_dec : 
    forall x y:S, {eq x y} + {~(eq x y)} ;
  inv_mor : 
    forall x y:S, eq x y -> eq (inv x) (inv y) ;
  op_mor :
    forall x1 y1 x2 y2:S, eq x1 y1 -> eq x2 y2 ->
    eq (op x1 x2) (op y1 y2) ;
  op_assoc :
    forall x y z:S, eq (op (op x y) z) (op x (op y z)) ;
  left_unit :
    forall x:S, eq (op e x) x ;
  right_unit :
    forall x:S, eq (op x e) x ;
  left_inv :
    forall x:S, eq (op (inv x) x) e ;
  right_inv :
    forall x:S, eq (op x (inv x)) e
}.

最後に先ほど作った $\mathbb{Z}'$ が群であることを示します。

Instance Z'_group : Group eq' (mkZ' O O) minus' plus'.

[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.

[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 を定義するなどを多少工夫してみました。

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

[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.

[Coq] Even + Odd = Odd

日本数学会の「大学生数学基本調査」に基づく数学教育への提言によると、『「偶数と奇数の和が奇数になる」証明を明快に記述できる学生は稀』という調査結果が得られたそうです。

さて Coq で実際証明してみると判りますが、ちょっとした工夫をしないと、

Theorem plus_even_odd_odd : forall n m,
 even n -> odd m -> odd (n+m).

これを証明するのは難しいです。

まず、述語 even, odd を定義します。
標準的には下記の様に相互帰納的に定義するのが良いでしょう。

Inductive even:nat->Prop :=
| even_0 : even 0
| even_S : forall n, odd n -> even (S n)
with odd:nat->Prop :=
| odd_S : forall n, even n -> odd (S n).

その上で、「あえて」余分な性質も含めた定理を証明します。

Theorem plus_odd : forall n m,
 (even n -> odd m -> odd (n+m)) /\
 (odd n -> odd m -> even (n+m)).
Proof.
induction n. 
 intros. split.
  intros. simpl. auto.
 intros. inversion H.
intros. split.
 intros. destruct (IHn m). simpl. apply odd_S.
 apply H2.
  inversion H. auto.
 auto.
intros. destruct (IHn m). simpl. apply even_S.
apply H1.
 inversion H. auto.
auto.
Qed.

こうすることで n に関する帰納法が使いやすくなって証明出来ます。
最後に先ほど証明した定理の半分だけ取り出せばOKです。

Theorem plus_even_odd_odd : forall n m,
 even n -> odd m -> odd (n+m).
Proof.
intros. destruct (plus_odd n m). apply H1; auto.
Qed. 

以上、ライブラリや omega などを使わずに証明出来ました。

[Coq][Alloy] Properties of Relation

先日のFormal Methods Forum勉強会にて、Alloy本の演習問題を皆で解いた。Alloyとしての課題は、関係 r について各種性質（推移律とか単射とか）を Alloy の関係演算記法で書かれたものについて検討した後に、述語論理っぽく同等の性質を書き下し、同等性を Alloy でチェックする、というものだった。
その課題については kencoba さんの日記に回答が示されている。

同じことを Coq を用いて行ってみた。
Coq では univ を U:Set として現し、その上の関係 univ -> univ は U -> U -> Prop として表現できる。後は、関係に対する join などの演算子を定義すれば、同等性の証明を Coq で確認することが出来る。

証明してみた結果、これらの等価性を示すには U_dec: forall u u':U, {u=u'}+{u<>u'} や、Uが有限集合であることなどの性質を使わなくても等価であることが判る。

Section Alloy1.

(* See "Software Abstraction" Alloy Tutorial *)
(* http://d.hatena.ne.jp/kencoba/20120212 *)

(* univ *)
Parameter U:Set.
(* relation *)
Definition relation := U -> U -> Prop.

Definition JOIN(R S:relation):relation :=
 fun x => (fun z => (exists y:U, R x y /\ S y z)).

Definition INV(R:relation):relation :=
 fun x => (fun y => (R y x)).

Definition IN(R S:relation):Prop :=
 forall x y:U, R x y -> S x y.

Definition IDEN:relation :=
 fun x => (fun y => (x=y)).

Definition AND(R S:relation):relation :=
 fun x => (fun y => R x y /\ S x y).

Definition NO(R:relation):Prop :=
 forall x y, ~(R x y).

Definition SOME(R:relation):Prop :=
 exists x, exists y, R x y.

Lemma NonEmpty : forall r:relation,
 (SOME r) <->
 (exists x, exists y, r x y).
Proof.
intros. split.
 unfold SOME. intro. assumption.
intros. unfold SOME. assumption.
Qed.

Lemma Transitive : forall r:relation,
 (IN (JOIN r r) r) <->
 (forall x y z, r x y -> r y z -> r x z).
Proof.
intros. split.
 intros. unfold IN in H. unfold JOIN in H.
 specialize (H x z). eapply H.
 exists y. split; assumption.
intros. unfold IN. unfold JOIN.
intros x z H0. destruct H0 as [y [H1 H2]].
eapply (H x y z).
exact H1. exact H2.
Qed.

Lemma Irreflexive : forall r:relation,
 (NO (AND IDEN r)) <->
 (forall x, ~r x x).
Proof.
intros. split.
 intros. unfold NO in H. unfold AND in H.
 unfold IDEN in H. specialize(H x x).
 intro. elim H. split.
  reflexivity.
 assumption.
intros. unfold NO. unfold AND.
unfold IDEN. intros. intro. destruct H0.
rewrite <- H0 in *. elim (H x). assumption.
Qed.

Lemma Symmetric : forall r:relation,
 (IN (INV r) r) <->
 (forall x y, r x y -> r y x).
Proof.
intros. split.
 intros. unfold IN in H. unfold INV in H.
 eapply H. assumption.
intros. unfold IN. unfold INV.
intros. eapply H. assumption.
Qed.

Lemma Functional : forall r:relation,
 (IN (JOIN (INV r) r) IDEN) <->
 (forall x y1 y2, r x y1 -> r x y2 -> y1 = y2).
Proof.
intros. split.
 intros. unfold IN in H. unfold JOIN in H.
 unfold INV in H. unfold IDEN in H.
 specialize (H y1 y2). eapply H.
 exists x. split; assumption.
intros. unfold IN. unfold JOIN.
unfold INV. unfold IDEN.
intros. destruct H0. destruct H0.
eapply (H x0 x y); assumption.
Qed.

Lemma Injective : forall r:relation,
 (IN (JOIN r (INV r)) IDEN) <->
 (forall x1 x2 y, r x1 y -> r x2 y -> x1=x2).
Proof.
intros. split.
 intros. unfold IN in H. unfold JOIN in H.
 unfold INV in H. unfold IDEN in H.
 specialize(H x1 x2). eapply H.
 exists y. split; assumption.
intros. unfold IN. unfold JOIN.
unfold INV. unfold IDEN. intros.
destruct H0. destruct H0. 
eapply (H x y x0); assumption.
Qed.

Definition set := U -> Prop.

Definition SIN(R S:set):Prop :=
 forall x:U, R x -> S x.

Definition UNIV:set :=
 fun x:U => True.

Definition JOIN_SR(S:set)(R:relation):set :=
 fun y => (exists x:U, S x /\ R x y).

Definition JOIN_RS(R:relation)(S:set):set :=
 fun x => (exists y:U, R x y /\ S y).

Lemma Total : forall r:relation,
 (SIN UNIV (JOIN_RS r UNIV)) <->
 (forall x, exists y, r x y).
Proof.
intros. split.
 intros. unfold SIN in H. unfold JOIN_RS in H.
 unfold UNIV in H. specialize (H x).
 specialize(H I). destruct H. destruct H.
 exists x0. assumption.
intros. unfold SIN. unfold JOIN_RS.
unfold UNIV. intros. specialize(H x).
destruct H. exists x0. split; auto.
Qed.

Lemma Surjective : forall r:relation,
 (SIN UNIV (JOIN_SR UNIV r)) <->
 (forall y, exists x, r x y).
Proof.
intros. split.
 intros. unfold SIN in H. unfold JOIN_SR in H.
 unfold UNIV in H. specialize(H y).
 specialize(H I). destruct H. destruct H.
 exists x. auto.
intros. unfold SIN. unfold JOIN_SR.
unfold UNIV. intros. specialize(H x).
destruct H. exists x0. split; auto.
Qed.

End Alloy1.

[Coq] Scala PartialFunction is Monoid

「Scala の PartialFunction が orElse の演算に関して monoid になっているのでは？」という stackoverflow の議論 Scala PartialFunction can be Monoid? について twitter 上で目にしたので証明してみた。
Scala の PartialFunction[A,B] は失敗する関数と考えれば A -> option B と考えて良い。
Coq は外延性の公理を入れないと、(fun x => f x) = f が言えないので、ライブラリ Logic.FunctionalExtensionality を Import してるとか extensionality というタクティックを使ってるとかが目新しいぐらいで、他は単に型クラス定義してインスタンスが公理を満たすのを証明するだけ。

Section PartialFunctionMonoid.
(* See http://stackoverflow.com/questions/9067904/scala-partialfunction-can-be-monoid *)
 
Require Import Logic.FunctionalExtensionality.
 
Class Monoid(T:Type) := {
  op : T -> T -> T;
  e : T;
  left_id : forall t, op e t = t;
  right_id : forall t, op t e = t;
  assoc : forall t u v, op (op t u) v = op t (op u v)
}.
 
Variable A B:Type.
Definition pf := A -> option B.
Definition orElse(f g:pf):pf :=
fun a => match (f a) with
  | None => g a
  | Some b => Some b
  end.       
 
Instance pf_monoid : Monoid pf := {
  op := orElse;
  e := (fun a => None)
}.
Proof.
  intros. unfold orElse. simpl.
  extensionality a. auto.
 intros. unfold orElse.
 extensionality a. destruct (t a); auto.
intros. unfold orElse. extensionality a.
destruct (t a); auto.
Defined.
 
End PartialFunctionMonoid.

[Coq] Coq Tutorial on 1/12, 2/2, 2/9, and 2/16

イベントレポート：「Coqチュートリアル#1」 @ InfoQ

今回、豆蔵様より会場を提供していただけることになって、前々から計画していた平日夜の複数回開催のCoqチュートリアルを 1/12, 2/2, 2/9, 2/16 という予定で開催します。
参加申し込みについては上記リンクから辿って頂ければと思います。

[Coq] itoa in Coq

https://github.com/tmiya/coq/blob/master/Radix/Radix.v

自然数$n$を$p \ge 2$で割って余りを求め、商をまた割って、と繰り返すことで$n$の$p$進表示を得られますが、そのencode/decodeをCoqで書きました。勿論、encodeとdecodeが逆関数になっていることも証明済みです。
encode関数を使って、C言語にあるitoa関数を書きました。これがあれば、数字を文字列に変換出来ますからFizzBuzzもCoqで書けます。
そのうちCoq user contributionに登録しよう。