Rel: 関係の性質
この短い（オプションの）章では、Coqでいくつかの基本的な定義と二項関係の定理の証明を行います。
重要な定義は実際に使う際（「プログラミング言語の基礎」のSmallstep章）に再度定義されます。
もしこれらに慣れているならばこの章を流し読みするか飛ばしても問題ありません。
しかし、Coqの基本的推論機構を使う良い練習問題ともなるので、IndProp章の直後に見ておくとよいかもしれません。
まぎらわしいことに、Coqの標準ライブラリでは、一般的な用語「関係(relation)」を、この特定の場合を指すためだけに使っています。
ライブラリとの整合性を保つために、ここでもそれに従います。
したがって、Coq の識別子relationは常に、集合上の二項関係を指すために使います。
一方、日本語の「関係」は、Coq の relation を指す場合もあれば、
より一般の任意の数の（それぞれ別のものかもしれない）集合の間の関係を指す場合もあります。
どちらを指しているかは常に議論の文脈から明らかになるようにします。
====> Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m
(Why did we write it this way instead of starting with Inductive
le : relation nat...? Because we wanted to put the first nat
to the left of the :, which makes Coq generate a somewhat nicer
induction principle for reasoning about <=.)
大学の離散数学の講義で習っているように、関係を「一般的に」議論し記述する方法がいくつもあります。
関係を分類する方法（反射的か、推移的か、など）、関係のクラスについて一般的に証明できる定理、
関係からの別の関係の構成、などです。例えば...
集合X上の関係Rは、すべてのxに対して、R x yとなるyは高々1つであるとき、言い換えると、R x y1かつR x y2ならば y1 = y2 となるとき、「部分関数(partial function)」です。
Definition partial_function {X: Type} (R: relation X) :=
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
例えば、前に定義したnext_nat関係は部分関数です。
Print next_nat.
Check next_nat : relation nat.
Theorem next_nat_partial_function :
partial_function next_nat.
Proof.
unfold partial_function.
intros x y1 y2 H1 H2.
inversion H1. inversion H2.
reflexivity. Qed.
しかし、数値上の<=関係は部分関数ではありません。
（ <=が部分関数であると仮定すると、0<=0かつ0<=1から、0=1となります。
これはおかしなことです。
したがって、<=が部分関数だという仮定は矛盾するということになります。）
Theorem le_not_a_partial_function :
~ (partial_function le).
Proof.
unfold not. unfold partial_function. intros Hc.
assert (0 = 1) as Nonsense. {
apply Hc with (x := 0).
- apply le_n.
- apply le_S. apply le_n. }
discriminate Nonsense. Qed.
Definition reflexive {X: Type} (R: relation X) :=
forall a : X, R a a.
Theorem le_reflexive :
reflexive le.
Proof.
unfold reflexive. intros n. apply le_n. Qed.
Definition transitive {X: Type} (R: relation X) :=
forall a b c : X, (R a b) -> (R b c) -> (R a c).
Theorem le_trans :
transitive le.
Proof.
intros n m o Hnm Hmo.
induction Hmo.
- apply Hnm.
- apply le_S. apply IHHmo. Qed.
Theorem lt_trans:
transitive lt.
Proof.
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
apply le_S in Hnm.
apply le_trans with (a := (S n)) (b := (S m)) (c := o).
apply Hnm.
apply Hmo. Qed.
練習問題:★★, standard, optional (le_trans_hard_way)
Theorem lt_trans' :
transitive lt.
Proof.
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
induction Hmo as [| m' Hm'o].
Admitted.
☐
Theorem lt_trans'' :
transitive lt.
Proof.
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
induction o as [| o'].
Admitted.
☐
leの推移性は、同様に、後に(つまり以下の反対称性の証明において)
有用な事実を証明するのに使うことができます...
Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
Proof.
intros n m H. apply le_trans with (S n).
- apply le_S. apply le_n.
- apply H.
Qed.
☐
練習問題:★★, optional (le_Sn_n_inf)
☐
反射性と推移性は後の章で必要となる主要概念ですが、Coq で関係を扱う練習をもう少ししましょう。
次のいくつかの概念もよく知られたものです。
☐
関係Rが「反対称的(antisymmetric)」であるとは、R a bかつR b aならば a = b となることです。
つまり、Rにおける「閉路(cycle)」は自明なものしかないということです。
☐
☐
関係が「同値(equivalence)」であるとは、その関係が、反射的、対称的、かつ推移的であることです。
Definition equivalence {X:Type} (R: relation X) :=
(reflexive R) /\ (symmetric R) /\ (transitive R).
関係が「半順序(partial order)」であるとは、その関係が、反射的、「反」対称的、かつ推移的であることです。
Coq 標準ライブラリでは、半順序のことを単に「順序(order)」と呼びます。
前順序(preorder、または擬順序)とは、半順序の条件から反対称性を除いたものです。
Definition preorder {X:Type} (R: relation X) :=
(reflexive R) /\ (transitive R).
Theorem le_order :
order le.
Proof.
unfold order. split.
- apply le_reflexive.
- split.
+ apply le_antisymmetric.
+ apply le_trans. Qed.
Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
| rt_step x y (H : R x y) : clos_refl_trans R x y
| rt_refl x : clos_refl_trans R x x
| rt_trans x y z
(Hxy : clos_refl_trans R x y)
(Hyz : clos_refl_trans R y z) :
clos_refl_trans R x z.
Theorem next_nat_closure_is_le : forall n m,
(n <= m) <-> ((clos_refl_trans next_nat) n m).
Proof.
intros n m. split.
-
intro H. induction H.
+ apply rt_refl.
+
apply rt_trans with m. apply IHle. apply rt_step.
apply nn.
-
intro H. induction H.
+ inversion H. apply le_S. apply le_n.
+ apply le_n.
+
apply le_trans with y.
apply IHclos_refl_trans1.
apply IHclos_refl_trans2. Qed.
上の反射推移閉包の定義は自然です。
定義はRの反射推移閉包がRを含み反射律と推移律について閉じている最小の関係であることを明示的に述べています。
しかし、この定義は、証明をする際にはあまり便利ではありません。
rt_trans 規則の「非決定性(nondeterminism)」によって、しばしばわかりにくい帰納法になってしまいます。
以下は、より使いやすい定義です。
Inductive clos_refl_trans_1n {A : Type}
(R : relation A) (x : A)
: A -> Prop :=
| rt1n_refl : clos_refl_trans_1n R x x
| rt1n_trans (y z : A)
(Hxy : R x y) (Hrest : clos_refl_trans_1n R y z) :
clos_refl_trans_1n R x z.
新しい反射推移閉包の定義は、rt_step規則とrt_trans規則を「まとめ」て、
1ステップの規則にします。
このステップの左側はRを1回だけ使います。このことが帰納法をはるかに簡単なものにします。
次に進む前に、二つの定義が同じものを定義していることを確認しなければなりません。
最初に、clos_refl_trans_1nが、「失われた」2つのclos_refl_transコンストラクタの働きを代替することを示す二つの補題を証明します。
Lemma rsc_R : forall (X:Type) (R:relation X) (x y : X),
R x y -> clos_refl_trans_1n R x y.
Proof.
intros X R x y H.
apply rt1n_trans with y. apply H. apply rt1n_refl. Qed.
Lemma rsc_trans :
forall (X:Type) (R: relation X) (x y z : X),
clos_refl_trans_1n R x y ->
clos_refl_trans_1n R y z ->
clos_refl_trans_1n R x z.
Proof.
Admitted.
forall (X:Type) (R: relation X) (x y z : X),
clos_refl_trans_1n R x y ->
clos_refl_trans_1n R y z ->
clos_refl_trans_1n R x z.
Proof.
Admitted.
☐
そして、反射推移閉包の2つの定義が同じ関係を定義していることを証明するために、
上記の事実を使います。
Theorem rtc_rsc_coincide :
forall (X:Type) (R: relation X) (x y : X),
clos_refl_trans R x y <-> clos_refl_trans_1n R x y.
Proof.
Admitted.
forall (X:Type) (R: relation X) (x y : X),
clos_refl_trans R x y <-> clos_refl_trans_1n R x y.
Proof.
Admitted.
☐