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