天泣記

SSReflect には choice というライブラリがある:

ここには choiceType というものが定義されているのだが、これはなんなのだろうか。すこしドキュメントやソースを読んで、以下のような疑問が浮かぶ。

choice という単語からは選択公理 (axiom of choice) が連想されるが、どんな関係があるか
ユーザ向けのインターフェース (xchoose と choose) と、choiceType を実装するときのインターフェース (find_subdef) が異なるが、なぜなのか
find_subdef の型には nat (自然数) が出てくるが、これは実数など不可算な対象を choiceType にするのに困らないか

最初に自分なりの結論を書いておく。

choice がなにをするものなのかというのは、マニュアルの冒頭に書いてあるタイトル "Types with a choice operator" のとおりである。 choice operator が使える型、である。

choice operator というのは、述語 (なんらかの型 T の値を受け取って bool を返す関数) を満たす値を示す式を作り出すものである。 (具体的な値がわかるわけでなない)

choice operator は、Coq の帰納型に対するものであれば Coq の中で (公理を追加せずに) 実装できる。 (ここでいう帰納型の中には、関数や型など不可算なものは入っていないものとする。) このときに述語を満たす値を探索する関数を書くことになる。この関数は実際に動かすわけではないが、そのような関数を記述することにより (Coq では関数は必ず停止して値を返すので) 述語を満たす値が存在することが保証される。

そして、型 A, B から直積 A * B を作るなど、複数の型を合成することがあるが、それぞれの型の choice operator から合成した型の choice operator を生成したい。これはユーザ向けのインターフェース (xchoose と choose) では無理なので、内部的なインターフェース (find_subdef) は異なるものになっている。 find_subdef の型に nat が出てくるのは、この合成のためである。 (ユーザ向けのインターフェースでやろうとすると深さ優先探索になってしまって解があっても発見できないことがあり、確実に解を発見できる探索順序にするため、と思う。)

そして、実数などの不可算な対象については Coq 内で実装することはできないが、公理を追加すれば choice operator を作れる。 Coq で不可算な対象を扱うときは公理を追加するので、これはしかたないし、それを許容すれば mathcomp のライブラリをそういう対象に対しても利用できる。 (なお、追加する複数の公理が矛盾しないことはだれかがちゃんと考察してくれているものとする) また、find_subdef の nat は探索順序を制御するが、探索順序に関係なく探索できる公理によって choice operator を作れば問題にならない。

あと選択公理については、Coq にも選択公理と呼ばれるものはあるのだが、普通の (集合論の) 選択公理とは意味合いが異なるようで、choiceType との関係が大きな意味を持つかどうかはわからない。

というように、なんとなくわかったうえでドキュメントを読み直すとたしかにそんなことが書いてあるのだが、わからない段階で読んでもよくわからなかった。 <URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.3.0/mathcomp/ssreflect/choice.v#L222-L259>

#3 choice の使い方

まず choice の使い方であるが、何らかの条件を満たした値が存在するという証明から、その条件を満たした値を示す式を得る、というのが xchoose である。

xchoose は、ある (choiceType な) 型 T と、その型の述語 P および、その述語を満たす値が存在するという証明 (exists x : T, P x) を受け取ると、T 型の値を返す。なお、pred T は T -> bool である。

From mathcomp Require Import all_ssreflect.

About xchoose.
(* xchoose : forall {T : choiceType} {P : pred T}, (exists x : T, P x) -> T *)

xchoose を使うと、例えば exists n, 2 < n の証明 H から、xchoose H として 2 よりも大きいなんらかの値という式を得ることができる。具体的な値はわからないが、xchooseP という定理により xchoose H が 2 よりも大きいという証明を得られるので、以下のような証明ができる。

Section S.
Variable H : exists n, 2 < n.

Goal 2 < xchoose H.
Proof.
  exact (xchooseP H).
Qed.
End S.

最初に「choice operator というのは、述語を満たす値を示す式を作り出す」と書いたが、ここでの述語は 2 < n であり、述語を満たす値を示す式は xchoose H である。

なお、Coq は直観主義なので、なにかが存在するという証明は、具体的にその何かを構成することである。つまり、H の中には 2 < n が成り立つ n が含まれている。

ということは、xchoose はそれを取り出しているだけではないのか、という疑問が浮かぶが、そうではない。証明に入っている値が異なっても xchoose の結果は同じになるという eq_xchoose という定理がある。

たとえば、以下のように、2 < n となる n が存在するという証明として、具体的に 8 と 42 という異なる値を使ったものに xchoose を適用した結果は等しいことが証明できる。

Definition ex1 : exists n, 2 < n := ex_intro (fun n => 2 < n) 8 erefl.
Definition ex2 : exists n, 2 < n := ex_intro (fun n => 2 < n) 42 erefl.

Goal xchoose ex1 = xchoose ex2.
Proof.
  by apply: eq_xchoose.
Qed.

#4 choiceType の作り方

ある型 T を choiceType とするためには、以下のレコード hasChoice を用いて、hasChoice T 型の値を構成しなければならない。 hasChoice T 型には、find_subdef : pred T -> nat -> option T という、述語からその述語を満たす値を探し出す関数がはいっており、 find_subdef がたしかにそういう性質を持っている証明を含めなければならない。

HB.mixin Record hasChoice T := Mixin {
  find_subdef : pred T -> nat -> option T;
  choice_correct_subdef {P n x} : find_subdef P n = Some x -> P x;
  choice_complete_subdef {P : pred T} : (exists x, P x) -> exists n, find_subdef P n;
  choice_extensional_subdef {P Q : pred T} : P =1 Q -> find_subdef P =1 find_subdef Q
}.

<URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.3.0/mathcomp/ssreflect/choice.v#L261-L268>

まず、hasChoice bool を構成してみよう。 (なんか、hasChoice の値を構成するにはコンストラクタを使うが、参照するには hasChoice.Axioms_ としなければいけない模様)

Lemma my_bool_hasChoice : hasChoice bool.
Proof.
  apply: (hasChoice.Axioms_ (fun P n => if P true then Some true else if P false then Some false else None)).
      move=> P _ x.
      case Ht: (P true).
        by case => <-.
      case Hf: (P false).
        by case => <-.
      by [].
    move=> P [x px].
    exists 0.
    case: x px => ->.
      by [].
    by case: (P true).
  move=> P Q pq x.
  by rewrite !pq.
Qed.

コンストラクタ hasChoice.Axioms_ はレコードのフィールドの数だけ引数をもつので 4引数だが、ここでは最初の引数 find_subdef だけ指定して、ほかのフィールドは後から証明している。

find_subdef は以下の関数を指定した。

fun P n =>
  if P true then Some true
  else if P false then Some false
  else None

つまり、述語 P と自然数 n を受け取り、n は無視して、 P true が成り立つなら Some true を返し、 P false が成り立つなら Some false を返し、どちらでもないなら None を返す。

bool には true と false しか値がないので、この関数はたしかに bool 全体を探索しており、 P x が成り立つような x に対して Some x を返す。 (ちなみに P true と P false の両方が成り立ったら、Some true を返すが、これはどちらでもいい)

この find_subdef に対して、3つの性質が成り立つことを示さなければならない。

choice_correct_subdef {P n x} : find_subdef P n = Some x -> P x;
choice_complete_subdef {P : pred T} : (exists x, P x) -> exists n, find_subdef P n;
choice_extensional_subdef {P Q : pred T} : P =1 Q -> find_subdef P =1 find_subdef Q

choice_correct_subdef は find_subdef P n が Some x を返したら、必ず P x が成り立っている、という find_subdef の結果の正しさである。

choice_complete_subdef は、P x が成り立つ x が存在するなら、なんらかの n を指定すれば find_subdef P n は Some y を返す、という完全性である。ここで、前提の x と、find_subdef が返す Some y の y は同じ値とは限らない。

choice_extensional_subdef は、ふたつの述語 P, Q があったとき、それらを呼び出した結果が一致するならば、 find_subdef はそれらに対して同じ結果を返す、という外延性である。なお、f =1 g は forall x, f x = g x である。

上で証明に成功しているように、上の find_subdef はこれらの性質を満たす。

さて、上の find_subdef では引数に与えられた自然数 n を利用しなかったが、この n を利用すると、bool 全体をいっきに探索しなくてもよい。 bool では値がふたつしかないのですべての値を探索するのは簡単だが、無限に要素を持つ型については探索を実装できない。 (Coq では停止性が保証できない関数は許されない。) 呼出側が繰り返し異なる n を与えて呼び出してくれるので、その n によって探索範囲を分割して、部分的に (停止性を保証できる範囲で) 探索する。要素数が可算 (自然数と1対1対応が存在する) であれば、停止性が保証される find_subdef で対象全体 (無限要素) を探索できる。

bool は有限要素なので、n を使う利点はとくにないのだが、単なる例として、bool に対して n を利用した探索を実装してみよう。以下では、n が 0 のときには false だけを探索し、1 のときには true だけを探索する。こうやっても、hasChoice bool を構成できる。

Lemma my_bool_hasChoice': hasChoice bool.
  apply: (hasChoice.Axioms_ (fun P n => match n with
                                        | 0 => if P false then Some false else None
                                        | 1 => if P true then Some true else None
                                        | _ => None
                                        end)).
      move=> P n x.
        case: n => [|[|]]; last by [].
        case H: (P false); last by [].
        by case=> <-.
      case H: (P true); last by [].
      by case=> <-.
    move=> P [[|] px].
      exists 1.
      by rewrite px.
    exists 0.
    by rewrite px.
  move=> P Q pq n.
  by case: n => [|[|]]; rewrite ?pq.
Qed.

可算無限要素の nat について hasChoice nat を構成してみよう。以下では n が与えられたとき、P n だけを探索する。これでも hasChoice nat を構成できる。

Lemma my_nat_hasChoice : hasChoice nat.
Proof.
  apply: (hasChoice.Axioms_ (fun P n => if P n then Some n else None)).
      move=> P n x.
      case: ifPn.
        by move=> pn [] <-.
      by [].
    move=> P [x px].
    exists x.
    by rewrite px.
  move=> P Q pq n.
  rewrite pq.
  by case: (Q n).
Qed.

とくに意味はないが、与えられた n に対して、P (n*2) と P (n*2+1) を探索するようにしても、以下のように hasChoice nat を構成できる。

Lemma my_nat_hasChoice' : hasChoice nat.
Proof.
  apply: (hasChoice.Axioms_ (fun P n => if P n.*2 then Some n.*2 else if P n.*2.+1 then Some n.*2.+1 else None)).
      move=> P n x.
      case: ifPn => [pn [] <-|nP] //.
      by case: ifPn => [pn [] <-|].
    move=> P [n px].
    exists n./2.
    case: ifPn => //.
    case: ifPn => //.
    case H: (odd n).
      rewrite odd_halfK // prednK; last by apply odd_gt0.
      by rewrite px.
    rewrite even_halfK; last by rewrite H.
    by rewrite px.
  move=> P Q pq n.
  by rewrite 2!pq.
Qed.

というわけで、型の要素が可算個であれば、hasChoice は構成できる。公理は必要ない。

しかし型の要素数が不可算だと、find_subdef を実装できない。探索範囲を可算個に分割しても要素を有限個には抑えられず、停止する関数として find_subdef を記述できない。そのため、構成するには公理が必要になる。

ここで使える公理として、標準ライブラリの Epsilon に epsilon_statement というものがある。 (あと、関数の外延性の公理 functional_extensionality_dep も使う)

Require Import Epsilon.
Require Import FunctionalExtensionality.

About epsilon_statement.
(* epsilon_statement : forall [A : Type] (P : A -> Prop), inhabited A -> {x : A | (exists x0 : A, P x0) -> P x} *)
(*
epsilon_statement :
forall [A : Type] (P : forall _ : A, Prop) (_ : inhabited A),
sig (fun x : A => forall _ : ex (fun x0 : A => P x0), P x)
*)

ここで、{x : A | (exists x0 : A, P x0) -> P x} というのは sig 型で、A 型の値 x と、(exists x0 : A, P x0) -> P x の証明のペアである。 (後で詳しく述べる)

epsilon_statement を使うと、空でない任意の型 T に対して、hasChoice T を構成できる。

Section choiceT.

Variable T : Type. (* 任意の型 *)
Variable inhabited_T : inhabited T. (* T が空でない *)

Definition find_subdef_T (P : pred T) : option T :=
  let s := epsilon inhabited_T P in
  if P s then Some s else None.

Print Assumptions find_subdef_T. (* find_subdef_T が利用している公理を表示 *)
(* epsilon_statement : forall (A : Type) (P : A -> Prop), inhabited A -> {x : A | (exists x0 : A, P x0) -> P x} *)

Lemma hasChoice_T : hasChoice T.
Proof.
  apply: (hasChoice.Axioms_ (fun P n => find_subdef_T P)).
      move=> P _ x /=.
      rewrite /find_subdef_T.
      case: ifPn.
        by move=> H [] <-.
      by [].
    move=> P E /=.
    exists 0.
    rewrite /find_subdef_T /epsilon.
    case: (epsilon_statement (fun x : T => P x) inhabited_T) => x H /=.
    by rewrite H.
  move=> P Q pq _ /=.
  by rewrite (functional_extensionality _ _ pq).
Qed.
Print Assumptions hasChoice_T.
(*
functional_extensionality_dep :
  forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g
epsilon_statement : forall (A : Type) (P : A -> Prop), inhabited A -> {x : A | (exists x0 : A, P x0) -> P x}
*)

End choiceT.

About hasChoice_T.
(* hasChoice_T : forall T : Type, inhabited T -> hasChoice.phant_axioms T *)

この hasChoice_T を使えば、型が空でないかぎり、どんな型でも choiceType にできるので、実数などにも対応できる。 Coq の標準ライブラリにある公理しか使っていないので、(たぶん誰かがそれらは CIC と矛盾しないと証明していると思うので) 問題は少ないはずである。

#5 hasChoice で xchoose を実現

choiceType の内部実装の hasChoice は、find_subdef という関数を提供するが、ユーザは xchoose (あるいは choose) を使う。

xchoose は find_subdef で出てきた自然数 n をいろいろと変えて、find_subdef を呼び出して探索する。容易に想像できると思うが、いちばん小さい n を探索するようになっている。

これを実現するのに、choice では ex_minn を利用している。 (find は find_subdef である)

Fact xchoose_subproof P exP :
  {x | find P (ex_minn (@choice_complete_subdef _ P exP)) = Some x}.
Proof.  ...  Qed.

<URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.3.0/mathcomp/ssreflect/choice.v#L295>

ex_minn は ssrnat で定義されている

ex_minn : forall P : pred nat, (exists n, P n) -> nat
This returns the smallest n such that P n holds.

<URL:https://math-comp.github.io/htmldoc_2_3_0/mathcomp.ssreflect.ssrnat.html>

ex_minn P exP は、述語 P と P が成り立つ n が存在する証明を渡すと、P が成り立つ最小の n を返す。 P がどこかで成り立つ証明があるので停止性は保証される。 (ただ、証明からどの n で成り立つかは調べられないので、ex_minn の実装にはトリックが必要になる。このテクニックについては標準ライブラリの ConstructiveEpsilon にちょっと説明がある。)

というわけで、xchoose_subproof は choice_complete_subdef で発見した find_subdef が Some を返す最小の自然数 n を使って、find_subdef が発見する x と、それが find_subdef が返したものだという証明をペアにして返す。

xchoose はそのペアの最初の要素 x を取り出して返す。

Definition xchoose P exP := sval (@xchoose_subproof T P exP).

<URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.3.0/mathcomp/ssreflect/choice.v#L317>

xchoose は exP (P が成り立つ要素が存在する証明) を停止性のためだけに使っている。そのため xchoose が返す値は exP という証明がどんな値で構成されたかには依存せず、eq_xchoose という性質が成り立つ。

#6 hasChoice の合成

A と B がそれぞれ choiceType であったとして、直積 A * B も choiceType になってほしい。そして、その合成を自動的に行いたい。

残念ながら、これは xchoose というインターフェースでは無理である。

xchoose : forall {T : choiceType} {P : pred T}, (exists x : T, P x) -> T

A * B に対する xchoose は以下のように呼び出される。

@xchoose (A * B) predAB exAB

A と B は choiceType なので、それらに対して xchoose を呼び出したいが、 @xchoose A predA exA の、predA と exA をどう用意したらいいだろうか。

xchoose pred ex は pred を繰り返し呼び出して真になるものを探す関数なので、 @xchoose A で A の値を生成し、@xchoose B で B の値を生成し、両方をあわせて predAB に渡して述語が満たされるかどうか確認するしかなさそうである。そうすると、predA の中で @xchoose B を呼び出すことになり、たとえば以下のようになるだろう。

@xchoose A (fun a => @xchoose B (fun b => predAB (a, b)) exB) exA

exA と exB はどうしたらいいだろうか。 exAB は predAB が真を返す (a, b) というペアなので、この a から exA を作れそうである。しかし、exB が問題である。 exAB から b をひとつ取り出せるが、これは @xchoose A が生成した a と組み合わせて predAB が成立するとは限らない。というか、@xchoose A はいろいろな a を生成し、a によっては predAB を真にする b がないことがある。そのため、一般には exB は作れない

というわけで xchoose というインターフェースだと、合成はできそうにない。

この問題を解決するインターフェースが find_subdef である。

find_subdef : pred T -> nat -> option T;

find_subdef は存在の証明は受け取らない。かわりに探索範囲を限定する自然数を受け取る。

A, B それぞれの find_subdef を find_subdef_A, find_subdef_B とすると、以下のようにすれば、部分的な探索を行えそうである。

find_subdef_A (fun a => find_subdef_B (fun b => predAB (a, b)) nB) nA

ただ、nA, nB を自然数の組み合わせの範囲で探索しなければならない。 ex_minn はひとつの自然数を探索するので、自然数ひとつと自然数ふたつを対応させる必要がある。自然数は可算なのでこれは可能である。具体的な方法はともかく、そうやって nA, nB を自然数ひとつに合成すれば、その合成した自然数が最小になる predAB が満たされる要素を ex_minn で見つけることができる。

そういう自然数の合成と分解が可能だったとして、hasChoice (A * B) が構成してみよう。

Section pair.

Variable split_nat : nat -> (nat * nat).
Variable combine_nat : nat -> nat -> nat.
Variable combine_natK : forall m n, split_nat (combine_nat m n) = (m, n).

Lemma hasChoice_pair (A B : Type) (hcA : hasChoice.axioms_ A) (hcB : hasChoice.axioms_ B) : hasChoice (A * B)%type.
Proof.
  apply: (hasChoice.Axioms_
    (fun P n =>
    let (nA, nB) := split_nat n in
    match hasChoice.find_subdef hcA (fun a => hasChoice.find_subdef hcB (fun b => P (a, b)) nB) nA with
    | None => None
    | Some a =>
        match hasChoice.find_subdef hcB (fun b => P (a, b)) nB with
        | None => None
        | Some b => Some (a, b)
        end
    end)).
      move=> P n [a b] /=.
      case Hs: (split_nat n) => [nA nB].
      case Hab: (hasChoice.find_subdef hcA (fun a => hasChoice.find_subdef hcB (fun b => P (a, b)) nB) nA) => [a'|] //.
      case Hb: (hasChoice.find_subdef hcB (fun b => P (a', b)) nB) => [b'|] //.
      move=> [] <- <-.
      by exact (hasChoice.choice_correct_subdef Hb).
    move=> P [] [a b] pab.
    case: (hasChoice.choice_complete_subdef hcB (ex_intro (fun b' => P (a, b')) b pab)) => nB Hb.
    case: (hasChoice.choice_complete_subdef hcA
            (ex_intro (fun a => hasChoice.find_subdef hcB (fun b => P (a, b)) nB) a Hb)) => nA Hab.
    exists (combine_nat nA nB).
    rewrite combine_natK.
    case Ha': (hasChoice.find_subdef hcA (fun a0 : A => hasChoice.find_subdef hcB (fun b0 : B => P (a0, b0)) nB) nA) Hab => [a'|] // _.
    move: (hasChoice.choice_correct_subdef Ha').
    by case: (hasChoice.find_subdef hcB (fun b0 : B => P (a', b0)) nB).
  move=> P Q pq n.
  case: (split_nat n) => nA nB.
  rewrite (_ :
      hasChoice.find_subdef hcA (fun a : A => hasChoice.find_subdef hcB (fun b : B => P (a, b)) nB) nA =
      hasChoice.find_subdef hcA (fun a : A => hasChoice.find_subdef hcB (fun b : B => Q (a, b)) nB) nA); last first.
    apply: hasChoice.choice_extensional_subdef => a.
    congr isSome.
    apply: hasChoice.choice_extensional_subdef => b.
    by apply: pq.
  case: (hasChoice.find_subdef hcA (fun a : A => hasChoice.find_subdef hcB (fun b : B => Q (a, b)) nB) nA) => [a|] //.
  rewrite (_ :
    hasChoice.find_subdef hcB (fun b : B => P (a, b)) nB =
    hasChoice.find_subdef hcB (fun b : B => Q (a, b)) nB); last first.
    apply: hasChoice.choice_extensional_subdef => b.
    by apply: pq.
  by case: (hasChoice.find_subdef hcB (fun b : B => Q (a, b)) nB).
Qed.

End pair.

About hasChoice_pair.
(*
hasChoice_pair :
forall (split_nat : nat -> nat * nat) (combine_nat : nat -> nat -> nat),
(forall m n : nat, split_nat (combine_nat m n) = (m, n)) ->
forall A B : choiceType, hasChoice.phant_axioms (Choice.sort A * Choice.sort B)
*)
Print Assumptions hasChoice_pair. (* closed *)

なんとかできた。

split_nat, combine_nat, combine_natK が存在することは示してないが、自然数と有理数の濃度が同じことを示すときの斜めにスキャンするやつとか、 2進数と考えて偶数番目のビットと奇数番目のビットを分けるとか、いろいろ考えられる。まぁ、ちょっとがんばれば証明は可能だろうということで省略する。

ただ、これってヒルベルトのホテルだよな。可算無限ふたつの組み合わせなので「それぞれ無限人の客を乗せた無限台のバス」の話に対応する。これは対関数というらしい: 「対関数とは、2つの自然数を一意に符号化して1つの自然数を返す関数である。」

なお、SSReflect ではもっと一般的に、自然数のリストをひとつの自然数に対応させる写像 (Goedel-style one-to-one encoding of seq nat into nat と書いてある) を用意し、それを使って自然数2個のリストをひとつの自然数にエンコードしているようだ。 <URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.3.0/mathcomp/ssreflect/choice.v#L438> の if dc n is [:: ni; nt] then ... というのが、 n をデコード (dc) して 2要素だったらという条件判定だろう。

ところで、xchoose は exB を作れなくて合成できないと書いたが、exA, exB は停止性のために存在するので、停止しなくてもよいと考えるなら以下の xchoose を使った探索はうまく動くだろうか。

@xchoose A (fun a => @xchoose B (fun b => predAB (a, b)) exB) exA

考えてみると、@xchoose A が A の値を生成しては (fun a => ...) を呼び出し、@xchoose B が B の値を生成しては (fun b => ...) を呼び出す。これは深さ優先探索をしているとみなせる。そして、深さ優先探索では解があってもみつけられない場合がある。たとえば、最初に生成される A の値に対しては predAB は常に偽となるが、 2番目に生成される A の値に対しては predAB が真になる B の値が存在するとしよう。そうすると、まず最初に生成された A の値に対して、@xchoose B が B の値を生成して predAB で試すが、B の要素が無限にあると、いつまでたってもおわらない。そのため、2番目に生成される A の値を試すところまでいきつかず、解を発見できない。

find_subdef だとこれが扱われるかというと、find_subdef_A が A の値 a を生成し、find_subdef_B は B の値を生成するが、find_subdef_B は nB に対応した有限個の値しか生成しないのでいずれ終了し、 find_subdef_A が次の値を生成する。あるいは、nA に対応した値を生成し尽したら find_subdef_A が終了し、ex_minn で生成される次の自然数に対して find_subdef_A を呼び出す。つまり、いずれ (解が発見できるまで) すべての nA, nB の組み合わせが試されるため、深さ優先探索のように解が存在するのに発見できない、ということは起きない。

find_subdef_A (fun a => find_subdef_B (fun b => predAB (a, b)) nB) nA

深さ優先探索じゃないなら幅優先探索かというと、探索順序は nA, nB をどう求めるかによるので完全に幅優先とは言い難いが、幅優先と同じく (存在するなら) 解を必ず発見できるという性質は得られる。

#7 hasChoice の合成と公理

find_subdef を使うと合成できることはわかった。ただこれは、公理を使って find_subdef を構成しても同じだろうか。

もちろん公理を使っているから動作しない (reduction は進まない) が、それ以外の問題はないだろうか

ドライには、hasChoice_T を使う側からすれば、中で公理 (epsilon_statement, functional_extensionality_dep) を使っていてもいなくても、型は変わらないので、同じように使える (型検査を通る項を作れる) から同じように証明できて問題ない、といえる。

もうちょっと中身をイメージした認識を述べる。もともとの疑問は、「find_subdef の型には nat (自然数) が出てくるが、これは実数など不可算な対象を choiceType にするのに困らないか」というものだった。しかし、この自然数は探索順序を制御して解を確実に発見できるようにするという目的のものだった。そのため、有限時間で全解探索できるなら、使わなくても問題ない。実際、my_bool_hasChoice で (与えられる自然数 n を無視する) 以下の find_subdef を使って choiceType を構成できた。

fun P n =>
  if P true then Some true
  else if P false then Some false
  else None

ということは、解を発見できたことにする、という公理 (epsilon_statement) を使うと、探索順序の制御は無視して解を発見できたことになる、というように理解すればいいのではないだろうか。

#8 Coq のソートと ex, sig, sigT, inhabited

選択公理の話の前に、Coq のソートについて述べておく。

Coq の型は、ソートというもので分類されている。ソートは型の型である。

Set, Type, Prop, SProp の 4種類ある。 Type は Type(1), Type(2), ... と無限の階層になっている。ただ、いまは Type と Prop だけ考える。 Set は Type のいちばん低いレベルの Type と考えられる。SProp は Prop と似ている。

Set に属する型は (ふつうのプログラミングでいう) 型であり、その型の値はふつうの値である。 (bool や nat は Set に属する。)

それに対して、Prop に属する型は命題であり、その型の値は証明である。 (A /\ B や ~ A とか、n = 3 などは Prop に属する。)

Set と Type は型階層をなすが、ここからそれらを区別せず、Type ということにする。

この区別の必要性はCoqマニュアルのInductive types and recursive functionsに以下のふたつがあげられている。

extraction でプログラムを生成するときに証明を除去するが、そのときに証明に依存して値が決まることがあると、証明を除去できなくなる (extraction という語は抽出という意味だが、これは証明を取り除いた残りを抽出するということである)
ひとつの命題の証明はどれも同じものとみなすという proof-irrelevance という公理を追加することがあるが、異なる証明を区別する方法があると、その公理と矛盾が生じてしまう

このため、Prop というソートで証明を区別している。

ところで、述語論理の存在 (∃) は Coq では帰納型 ex として実現される。以下に定義を示す。 notation が定義されているので exists y, P y というのが出てくるが、notation を抑制して表示した定義も示してある。

About ex.
(* ex : forall [A : Type], (A -> Prop) -> Prop *)
Print ex.
(* Inductive ex (A : Type) (P : A -> Prop) : Prop :=  ex_intro : forall x : A, P x -> exists y, P y. *)
(* Inductive ex (A : Type) (P : forall _ : A, Prop) : Prop :=  ex_intro : forall (x : A) (_ : P x), ex P. *)

ある述語を満たす値が存在するというのは、その値とその値がその述語を満たす証明のペアと定義される。 ex は Prop に属するので命題である。 A というのが値の型であり、これは Type に属する。述語 P は A -> Prop なので、A 型の値によって変化する命題であり、その命題は (その値により) 成り立ったり成り立たなかったりする。 ex_intro はコンストラクタで、forall x : A, P x -> exists y, P y という型なので、A 型の値 x と P x の証明から ex P の値を構築する。

ex と同じ構造の帰納型であるが、帰納型が Prop ではなく Type に属するもの、また、帰納型が Type に属し、さらに述語の部分の Prop も Type になっているもの、という帰納型が定義されている。これらはそれぞれ sig と sigT という名前である。

About sig.
(* sig : forall [A : Type], (A -> Prop) -> Type *)
Print sig.
(* Inductive sig (A : Type) (P : A -> Prop) : Type :=  exist : forall x : A, P x -> {x : A | P x}. *)
(* Inductive sig (A : Type) (P : forall _ : A, Prop) : Type :=  exist : forall (x : A) (_ : P x), sig P. *)

About sigT.
(* sigT : forall [A : Type], (A -> Type) -> Type *)
Print sigT.
(* Inductive sigT (A : Type) (P : A -> Type) : Type :=  existT : forall x : A, P x -> {x : A & P x}. *)
(* Inductive sigT (A : Type) (P : forall _ : A, Type) : Type :=  existT : forall (x : A) (_ : P x), sigT P. *)

notation が有効だと sig P は {x : A | P x}、sigT P は {x : A & P x} と表示されるので ex との対応がわかりにくい。 notation を抑制すると以下のようにコンストラクタが同じ構造になっているのが明瞭になる。

ex_intro : forall (x : A) (_ : P x), ex P
exist : forall (x : A) (_ : P x), sig P
existT : forall (x : A) (_ : P x), sigT P

これらの違いは、extraction に以下のように影響する

ex は Prop なので、extraction するとぜんぶ消える
sig は述語の部分が Prop なので、extraction すると述語と証明の部分が消える (そして、フィールドがひとつだけレコードはそのフィールドの値が直接扱われる最適化があるので、そのフィールドの値が直接扱われる)
sigT は sigT 型がそのまま残る

試してみると以下のようになる。

Require Import Extraction.

Definition f1 (n : nat) (p : exists m, m < n) : nat := n.
Extraction f1. (* let f1 n = n *)

Definition f2 (n : nat) (p : {m | m < n}) : nat := proj1_sig p + n.
Extraction f2. (* let f2 n p = add p n *)

Definition f3 (n : nat) (p : {m & m < n}) : nat := projT1 p + n.
Extraction f3. (* let f3 n p = add (projT1 p) n *)

OCaml に extraction すると、ex を使っている f1 はぜんぶ消えて 1引数の関数となっているが、f2, f3 は 2引数である。 f2 は p が nat 型となっている (n と p が add の引数になっている) が、 f3 では p が sigT 型となっているのが推測できる。

このように extraction の動作を変えるというのが Type と Prop が分かれている理由のひとつである。

なお、f1 は ex 型から nat の値を取り出すことはできないので、f2 や f3 のように p から nat を取り出すと Coq で定義しようとしたときにエラーとなる。

Fail Definition f1' (n : nat) (p : exists m, m < n) : nat := ex_proj1 p + n.
(*
In environment
n : nat
p : exists m : nat, m < n
The term "p" has type "exists m : nat, m < n" while it is expected to have type "exists y, ?P y"
(unable to find a well-typed instantiation for "?A": cannot ensure that "Set" is a subtype of
"Prop").
*)

このようにエラーになるようにしているので、extraction では安全に証明を除去できる、ともいえる。

あと、ex と似ているが、単に値が入っているだけで述語や証明がない inhabited という型が用意されている。これは epsilon_statement が型に値が存在することを示すために使っていた。

About inhabited.
(* inhabited : Type -> Prop *)
Print inhabited.
(* Inductive inhabited (A : Type) : Prop :=  inhabits : A -> inhabited A. *)
(* Inductive inhabited (A : Type) : Prop :=  inhabits : forall _ : A, inhabited A. *)

#9 選択公理と直観主義および Coq

wikipedia:選択公理によれば、選択公理は、空でない集合の空でない任意の族に対して選択関数が存在する、というもののようだ。

choiceType との関係でいえば、この選択関数が choice operator なのだと思う。

なので、不可算な対象を扱うときには選択公理を Coq に導入し、それを利用して choice operator を実装する、ということが考えられる。 choice のコメントの以下の部分はそういうことをいっているのだと思う。(guidance は探索を制御する自然数を指していると思う。)

In the case of an axiomatic theory, such as that of the Coq reals library, postulating a suitable axiom of choice suppresses the need for guidance.

<URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.3.0/mathcomp/ssreflect/choice.v#L242C48-L244C53>

ただ、そもそも直観主義だと「空でない集合の空でない任意の族」であることを示すには選択関数を構成しなければならないので、選択公理は、選択関数が存在するなら選択関数が存在するという自明なものととなる気がする。

Coq では選択公理についてのいろいろな話が ChoiceFactsというライブラリとして提供されている。これをみると、選択関数を relation (A -> B -> Prop) で表現するか、関数 (A -> B) で表現するか、関数の値域を依存型にするか (forall (x:A), B x) とか選択公理を表現するにもいろいろあるようである。ここではわかりやすく選択関数を関数としてあつかうものについて述べる。そういう選択公理は FunctionalChoice という名前で定義されている。 (なお、FunctionalChoice は選択公理の命題 (型) に名前がついているということで、その証明があるとか公理が導入されているという話ではない。)

Definition FunctionalChoice :=
  forall (A B : Type) (R : A -> B -> Prop),
   (forall x : A, exists y : B, R x y) -> exists f : A -> B, forall x : A, R x (f x).

この命題は Coq では証明できないのだが、ちょっといじって、B のソートを Type から Prop に変えると証明できる。

From mathcomp Require Import all_ssreflect.

Goal forall (A : Type) (B : Prop) (R : A -> B -> Prop),
   (forall x : A, exists y : B, R x y) -> exists f : A -> B, forall x : A, R x (f x).
Proof.
  move=> A B R f.
  exists (fun a => ex_proj1 (f a)).
  move=> a.
  by exact (ex_proj2 (f a)).
Qed.

この証明がなにをしているかというと、前提の forall x : A, exists y : B, R x y は A の値 x から R x y を満たす y を返す関数なので、その関数を結論の exists f : A -> B, forall x : A, R x (f x) に与えて証明している。

つまり、前提として選択関数が与えられるので、結論として選択関数が存在する、というそれだけの話である。 (正確には、前提の選択関数の返値は単なる B の値ではなく、それが関係 R を満たしているという証明が付加された依存ペアになっているので、それを除いて A -> B の関数を作っている)

FunctionalChoice のまま (B : Type) だとなぜ証明できないかというと、先に説明したように Prop の情報を Type には移せないからである。 Type から Prop に変えたことにより、その制約にひっかからなくなり、証明できるようになったのである。

また、B が Type のままでも、前提の ex を sig に変えれば証明できる。結論の ex はそのままだが、Type の情報を Prop に移すのは問題ないので証明の妨げにはならない。

Goal forall (A B : Type) (R : A -> B -> Prop),
   (forall x : A, { y : B | R x y }) -> exists f : A -> B, forall x : A, R x (f x).
Proof.
  move=> A B R f.
  exists (fun a => proj1_sig (f a)).
  move=> a.
  by exact (proj2_sig (f a)).
Qed.

というわけで、選択公理を公理として Coq に導入することは、Prop から Type への情報の移行を認める、という話になる。

これは集合論における選択公理の意味合いとはずいぶんと異なると思う。

このへんの話は CPDT の Axioms of Choice の項にも書いてある。

#10 Epsilon

任意の型を choiceType にする hasChoice_T を構成するときに、公理として Epsilon の epsilon_statement と FunctionalExtensionality の functional_extensionality_dep) を利用した。

マニュアルによれば、epsilon は Hilbert's epsilon operator というものらしい。 Epsilon calculus というものから来ているのかな。ぜんぜん知らないけど。

これと選択公理の関係については、どうも epsilon は選択公理よりも強いもののようだ。

というか、Coq FAQ の Axioms のところの図をみると、 operator epsilon と functional extensionality に加えて predicate extensionality か proposition extensionality があれば、選択公理も含め (そこに載っている) すべての公理を導けるようだ。

この導ける公理には排中律も含まれる。

図を眺めると、選択公理と predicate extensionality から Diaconescu というもので排中律が導かれるようだ。 Diaconescu というのは人名かな。 Coq のライブラリに Diaconescu というのがある。

つまり、このへんの公理を導入すると古典論理になってしまう、ということだろうか。 Coq の選択公理は Prop から Type へ情報を渡せるというだけの話だったのになんでそんな大層な話になってしまったのだろう?

Diaconescu の pred_ext_and_rel_choice_imp_EM は relational choice と predicate extensionality から排中律を導くのだが、選択公理が Prop から Type へ情報を渡せるというだけの話とすると、predicate extensionality が重要なのだろうか?

Require Import ChoiceFacts.
About pred_ext_and_rel_choice_imp_EM.
(* pred_ext_and_rel_choice_imp_EM : PredicateExtensionality -> RelationalChoice -> forall P : Prop, P \/ ~ P *)

relational choice は関数じゃなくて関係で表現した選択公理で、以下のように定義されている。 (なお、functional choice から導けるので、こちらのほうが弱い)

Print RelationalChoice.
(* Notation RelationalChoice := (forall A B : Type, RelationalChoice_on A B) *)
Print RelationalChoice_on.
(* RelationalChoice_on =
fun A B : Type =>
forall R : A -> B -> Prop,
(forall x : A, exists y : B, R x y) ->
exists R' : A -> B -> Prop, subrelation R' R /\ (forall x : A, exists ! y : B, R' x y)
     : Type -> Type -> Prop
*)

predicate extensionality は (Diaconescu ライブラリでは) 以下で定義される。 bool に対する述語で <-> の意味で等価なものは = の意味で等しいというものである。

Definition PredicateExtensionality :=
  forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.

predicate extensionality からは proposisional extensionality と proof irrelevance が導かれる。

About prop_ext.
(* prop_ext : PredicateExtensionality -> forall A B : Prop, A <-> B -> A = B *)

About proof_irrel.
(* proof_irrel : PredicateExtensionality -> forall (A : Prop) (a1 a2 : A), a1 = a2 *)

しばらく pred_ext_and_rel_choice_imp_EM の証明を眺めていたのだが、あまりはっきりとした確信は得られなかった。

ただ、predicate extensionality, proposisional extensionality, proof irrelevance は論理の中ではいいとしても、カリーハワード対応でプログラムと考えると、かなり剣呑なのではないかと思った。 proposisional extensionality は、命題 A, B で、A <-> B なら A = B というものである。 A <-> B というのは、A が証明できるなら B が証明でき、かつ、B が証明できるなら A が証明できる、という意味である。カリーハワード対応により、命題は型に対応し、証明はその型の値である。ということは、A <-> B は、A に値があるなら B に値があり、かつ、B に値があるなら A に値がある、という意味になる。プログラムで扱う型では値が存在するのが普通なので、ほぼすべての型 A, B は A <-> B となる。 (Coq では <-> は Prop にしか使えないので、実際には受け付けられないが。) たとえば、nat <-> bool は当然成り立つ。ということは proposisional extensionality により、nat = bool ということになる。

また、proof irrelevance は命題 A の証明はどれも = の意味で等しい、ということなので、これもカリーハワード対応で、プログラムで扱う型と考えると、型 A の値はどれも = の意味で等しい、となる。ということは、nat の値 0, 1 は 0 = 1 と等しくなる。

こういう危うい話は Prop の中だけでやっているなら問題ないのだろうが、(Coq の) 選択公理により、Prop から Type へ情報を渡せるようにすると、矛盾が生じるまでではないが、排中律が証明できちゃったりするのだろう、と感じた。あまり確信はないけれど。

天泣記

2024-12-03 (Tue)

2024-12-22 (Sun)