天泣記

#1 Coq の eq

Coq はカリーハワード対応を利用して、命題を型、その命題の証明をその型のプログラムとして表現する。たしかに、証明を受け取って証明を返す関数が含意の証明であるとか、and や or を帰納的データ型 (いくつかのコンストラクタで型を定義するやつ) で表現できるというのは納得できる。

しかし、値の等しさはどうだろうか。x = y というようなやつである。そのへんはよく分かっていないので少し調べてみた。

Coq における x = y は eq という帰納的データ型であり以下のように定義される。

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.

Notation "x = y" := (x = y :>_) : type_scope.

Arguments eq {A} x _.

見かけをいじるために Notation や Arguments による細工が行われているが、それらをばっさり無視すると、以下の定義になる。

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : eq A x x.

つまり、eq という型は eq_refl というコンストラクタをひとつ持つ型である。

Notation により、x = y :> A と書くと eq A x y と解釈されるとか、x = y とだけ書くと eq _ x y となって _ の部分は推論にまかせるという指定がされている。また、Arguments により、eq 自身も A は省略するように指定されている。(@eq の @ は引数を省略しないという指示である)

ここで x の型は A であり、A の型は Type である。A が Type ということは、A が nat など普通の値の型の可能性があり、つまり x は値かもしれない。つまり eq は値を引数にとる (値に依存する) ので依存型である。

たとえば、eq_refl 5 という式の型推論結果を表示させると、以下のように、5 = 5 という型になることがわかる。つまり、eq_refl 5 というプログラムは 5 = 5 という命題の証明である。5 という値が型の中に現れるのが依存型っぽい。まぁ、証明を書くと命題を教えてくれるというのはあまり役に立つ感じではないが。

Coq < Set Printing Implicit.

Coq < Check eq_refl 5.
@eq_refl nat 5
     : 5 = 5

プログラムの中に明示的に型を書いて、その型が正しいかどうか Coq に検査させることもできる。以下では、eq_refl 5 に 5 = 5 という型を書いて、それが Coq に受け入れられるので、eq_refl 5 は 5 = 5 の証明として正しいということが確認できている。これは、証明の正しさを機械が確認してくれるということで、複雑な証明については役に立ちそうである。

Coq < Check eq_refl 5 : 5 = 5.
@eq_refl nat 5 : 5 = 5
     : 5 = 5

さらに、5 のかわりに 7-2、3+2、2+3 と書いてもうまくいく。これは、eq_refl (7-2) は 3+2 = 2+3 という命題の証明として正しいと Coq が認めたことになる。

Coq < Check eq_refl (7-2) : 3+2 = 2+3.
@eq_refl nat (7 - 2) : 3 + 2 = 2 + 3
     : 3 + 2 = 2 + 3

eqの説明によれば、eq は Leibniz equality だそうである。Leibniz equality は x and y are equal iff every property on A which is true of x is also true of y ということで、Coq 的には、forall (A : Type) (x y : A), x = y <-> (forall (P : A -> Prop), P x -> P y) と表現できるだろう。

Wikipedia の Equality (mathematics) によれば、Leibniz equality はもともと Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y). というもので、P x -> P y ではなく、P x <-> P y というものだったようだ。こちらのほうが x と y が対称で、どんな述語によっても x と y を区別できない、という気分がよく表されているように思える。ただ、P x -> P y でも等価らしい。たしかに、P が「どんな述語」でもよいので、P = ~Q として ~Q(x) -> ~Q(y) を考えれば、対偶が Q(y) -> Q(x) になり、逆は導けるということでそれはそうだろう。(でも、Coq だと (直観主義だと) 対偶が等価であるとは証明できないので、違う説明が必要な気はする)

なお、「どんな述語」といっても、できることは制限されているように思える。もし、x と y の定義をデータとして取り出すようなことが可能なら、内部で使われている変数名の違いなど、明らかに外に影響を与えない違いを検出することができてしまう。たぶん、関数なら適切な型の引数に適用すること、帰納的データ型の値ならどのコンストラクタで作られているか調べることといった、まともなことしかできないのは前提なのだろう。

さて、個人的な印象としては、Leibniz equality は任意の述語について成り立つ性質で、なんとなく、Coq の eq より強力に感じられる。eq は本当に Leibniz equality なのだろうか。

確認してみよう。

まず、Leibniz equality ならば eq である、ということを証明してみると、以下のように可能だった。Leibniz equality は任意の述語について成り立つ性質なので、うまく述語を選ぶと、x = y が出てくる。

Lemma L1 : forall (A : Type) (x y : A), (forall (P : A -> Prop), P x -> P y) -> x = y.
Proof.
  intros A x y H.
  apply (H (fun z => x = z)).
  reflexivity.
Qed.

生成された証明を表示させてみると以下のようになる。apply に書いたものがそのまま含まれていてそれっぽい。eq_refl は reflexivity という tactic から出てきたものだろう。 reflexivity のドキュメントによると、reflexivity は apply refl_equal に等しく、 refl_equal は eq_refl の Notation による別記法のようだ。

Print L1.
(*
L1 =
fun (A : Type) (x y : A) (H : forall P : A -> Prop, P x -> P y) => H (fun z : A => x = z) eq_refl
     : forall (A : Type) (x y : A), (forall P : A -> Prop, P x -> P y) -> x = y
*)

逆の、eq ならば Leibniz equality である、というのも証明してみると、これも可能だった。証明の途中のゴールの変化を観察すると、case H で P y が P x に変化する。H : x = y なので、(H は x = y という型の値なので) H という値は eq 型のいずれかのコンストラクタで生成されたはずである。case はコンストラクタの種類で場合分けを行うが、eq のコンストラクタは eq_refl のひとつしかないので、H が eq_refl で生成されたことが判明するだけである。eq_refl で生成されたということは、その値は x = x という型であるはずで、つまり y は x と同じものであることが判明し、Coq はゴールの P y を P x に変えてくれる。その結果、前提にある P x を適用できて、証明を終えられる。こういうふうに Coq が P y を P x に変えてくれるから、任意の述語について成り立つという強力な性質を証明できるということなのだろう。

Lemma L2 : forall (A : Type) (x y : A), x = y -> (forall (P : A -> Prop), P x -> P y).
Proof.
  intros A x y H P Px.
  case H. (* translates the goal P y to P x *)
  apply Px.
Qed.

生成された証明を表示させてみると以下のようになる。case で場合分けしたので、match が生成されている。match で H の場合分けを行うときに、in (_ = y0) で H の型の右辺を y0 で参照できるようにして、return (P y0) で、match 全体の型を P y0 としている。

match の外側の制約としては、P y 型の値を返さなければならない。H の型は x = y なので、y0 で参照できるようにした右辺は y であり、P y0 は P y となるのでこの制約を満たす。

match の内側では、唯一のコンストラクタの eq_refl の場合、H は x = x 型なので、x と y は同じもので、P x を返せば P y を返したのと同じことになる、のだと思う。ここで、「同じもの」というのはどのくらい同じなのかというのが気になる。eq_refl (7-2) という値が 3+2 = 2+3 という型の値であることを上で述べたように、完全に同じ形でなければならないというわけではないらしい。完全に同じ形でない場合も同じと考えるということは、許される違いを検出することは P の中では禁止されているということになるのだろうな。

Print L2.
(*
L2 =
fun (A : Type) (x y : A) (H : x = y) (P : A -> Prop) (Px : P x) =>
match H in (_ = y0) return (P y0) with
| eq_refl => Px
end
     : forall (A : Type) (x y : A), x = y -> forall P : A -> Prop, P x -> P y
*)

いちおう、eq と Leibniz equality が等価であることを証明しておくと、以下のようになる。両方向の証明がすでにあるので、等価 (iff, <->) を split で分解してそれぞれを使うだけである。

Lemma L : forall (A : Type) (x y : A), x = y <-> (forall (P : A -> Prop), P x -> P y).
Proof.
  constructor. (* conj *)
    apply L2.
  apply L1.
Qed.

証明を表示してみると以下のようになる。iff は両方向の証明を and でつなぐだけなので、and のコンストラクタの conj で、上記のふたつの証明を受け取ってひとつの証明にしているだけである。

Print L.
(*
L =
fun (A : Type) (x y : A) => conj (L2 A x y) (L1 A x y)
     : forall (A : Type) (x y : A), x = y <-> (forall P : A -> Prop, P x -> P y)
*)

ところで、reflexivity は apply eq_refl と同じだが、 reflexivity のドキュメントには、t = u で、t と u が convertible であることを検査して、そうであるならばゴールを解決する、と書いてある。

convertible とはなにかというと、マニュアルの 4.3 Conversion rulesに書いてある。β-reduction, ι-reduction, δ-reduction, ζ-reduction, η-expansion で変形して同じ形にたどりつけるもの、のようだ。

たぶん、こういう具体的な手順で定義した関係は、Leibniz equality よりも弱い気がする。つまり、convertible ではないが、どんな述語でも区別できないもの、というものが存在するのではないか。もしそういうものが存在するとすると、それは eq の意味で等しいのだろうか。(なお、変数が入っているもの、例えば a + b = b + a などが convertible でないのはしょうがないので、ここで気になっているのは変数が入っていないものについてである。)

そういうのを具体的に試してみたいと思って考えたところ、Ssreflect の eq_irrelevance を使う例を思いついた。

証明が同じという命題も eq で書くことができる。同じ命題の証明であればどんな方法で証明してあっても気にしないのが普通だが、いろんな証明 (であるところのプログラム) が convertible であるとは限らない。しかし、Ssreflect は特定の形の命題の証明はどんな証明でも eq の意味で等しいという定理 eq_irrelevance を提供している。(これは、Coq 本体の Coq.Logic.ProofIrrelevance とは異なる。こちらは公理を追加する。Ssreflect の eq_irrelevance は公理を追加せず、ただし、特定の形の命題に限定される。)

以下では、1 = 1 という命題をふたつの方法で証明する。

まず、最初は by [] で証明する。これは、Ssreflect の書き方だが、生成される証明は eq_refl 1 であり、reflexivity で証明したのと同じである。

From mathcomp Require Import ssreflect eqtype ssrbool ssrnat.

Lemma L11a : 1 = 1.
Proof.
  by [].
Defined.
Print L11a.
(*
L11a = @Logic.eq_refl nat 1
     : 1 = 1
*)

もうひとつは Ssreflect っぽく、1 = 1 を 1 == 1 に変換してから証明している。まぁ、この場合には証明が複雑になるという以上の意味はない。

Lemma L11b : 1 = 1.
Proof.
  by apply/eqP.
Defined.
Print L11b.
(*
L11b =
(fun _evar_0_ : is_true (1 == 1) => @elimT (1 = 1) (1 == 1) (@eqP nat_eqType 1 1) _evar_0_)
  (eqxx (T:=nat_eqType) 1)
     : 1 = 1
*)

これらの証明が等しいことは、reflexivity では証明できないが、eq_irrelevance で証明できる。

Lemma L11 : L11a = L11b.
  Fail reflexivity.
  by apply eq_irrelevance.
Qed.
Print L11.
(*
L11 = @eq_irrelevance nat_eqType 1 1 L11a L11b
     : L11a = L11b
*)

というわけで、reflexivity では証明できないが、eq である、という例はある。

reflexivity (eq_refl) では証明できないが、eq_irrelevance では証明できるというのは、Check でも確認できる。

Fail Check @Logic.eq_refl (1 = 1) L11a : @eq (1 = 1) L11a L11b.
Check @eq_irrelevance nat_eqType 1 1 L11a L11b : @eq (1 = 1) L11a L11b.

なお、上記の L11a と L11b の証明が Qed でなく Defined で終わっているのは、reflexivity で L11a とL11b を unfold して中身を調べるようにするためである。そうやって調べられるようにしないと、中身が同じであっても reflexivity では証明できなかったからだが、そういう可視性の問題で証明できたりできなかったりするのが上の結論に影響を与えていないかはちょっと心配。

もしその心配が問題ないとすると、eq_refl で作れない値が eq 型の値として認められるということで、それはそれで変な気はする。もしかして、上の心配があたっているのだろうか。

reflexivity では証明できないが、eq であるような、もっと単純な例はないかな。

追記:

Ssreflect をいじって、eqP, eq_refl, introTF, elimTF, elimT, iffP, idP, eqnP を unfold 可能にしたら (Qed を Defined に変えたら)、L11a = L11b を reflexivity で証明できた。

したがって、L11a と L11b は (十分に unfold できれば) convertible ということがわかった。つまり、心配は当たっていた。

うぅむ、変数が入っていなくて eq なものはすべて (十分に unfold できれば) convertible なのではないかという気がしてきた。

天泣記

2017-01-06 (Fri)

2017-01-08 (Sun)