天泣記

#5 CPS な no confusion

noconf_nat_inv {m n} : m = n -> Noconf_nat m n は m と n の要素ごとの等式をまとめたものを返す。 nat の場合はすべてのコンストラクタで要素はたかだかひとつ (S の場合に要素がひとつ) なのだが、一般には複数の等式をまとめなければならない。

Equations では sigma 型を使って要素をすべてまとめてからひとつの等式にしているようだ。

Print NoConfusion_prod.
(*
NoConfusion_prod =
fun (A B : Type) (x : A * B) =>
let (H, H0) := x in fun y : A * B => let (H1, H2) := y in {| pr1 := H; pr2 := H0 |} = {| pr1 := H1; pr2 := H2 |}
     : forall A B : Type, A * B -> A * B -> Prop

Arguments NoConfusion_prod (A B)%type_scope x y
*)

prod というのはペアの型である。 let (H, H0) := x in で x をばらして {| pr1 := H; pr2 := H0 |} という等式の左辺を作っている。同様に let (H1, H2) := y in で y をばらして {| pr1 := H1; pr2 := H2 |} という等式の右辺を作っている。

ただ、これをやると、かならず最初の要素から等式を片付けていかないといけないと思うのだよな。ちゃんと解けるならいいんだけど、コンストラクタと変数以外が入っていて解けないこともあるわけで、そうすると解ける部分が残っているのに処理を進められないことになる。

ということでひとつの値にまとめるのがよろしくないのではないか、と思う。複数の値は複数の値のままで渡していくほうがよい、ということである。

といってもひとつの式の値はひとつなので、ちょっと細工が必要である。返値が複数必要ならば、CPS でやればいいのではないか。

これが可能かどうか確かめるために、ちょっと挑戦してみた。

From mathcomp Require Import all_ssreflect.
Require Vector.

まず、Noconf_nat は以下のように定義して、 nat のコンストラクタそれぞれについて、要素の等式を受け取って P の値を返す関数型、とする。 P は継続の answer type と理解してよい。

Definition Noconf_nat (m n : nat) (P : Type) : Type :=
  match m, n with
  | 0, 0 => P
  | m'.+1, n'.+1 => m' = n' -> P
  | _, _ => False -> P
  end.

これを使って、要素の等式の証明を受け取って m = n の証明を返す Noconf_nat m n (m = n) を定義する。

Definition noconf_nat {m n : nat} : Noconf_nat m n (m = n).
  case: m => [|m]; case: n => [|n]; rewrite /Noconf_nat //.
  by move=> <-.
Defined.

また、m = n の証明を受け取って、継続に要素の等式の証明を渡して呼び出す以下を定義する。ここでは要素の等式の証明を f_equal predn H として明示的に書いてみた。明示的に書かずに SSReflect の case で H を分解して得ても同じだが、後でこの項を書くことになるので、人間が簡単に書ける形にしてみた。

Definition noconf_nat_inv {m n : nat} (H : m = n) {P : Type} : (Noconf_nat m n P) -> P.
  move: H.
  case: m => [|m]; case: n => [|n] //.
  move=> /= H X.
  apply/X.
  by apply (f_equal predn H).
Defined.

これらが逆関数になっていることを以下で証明する。 CPS なので、noconf_nat_inv H noconf_nat は H を noconf_nat_inv で変換した結果を noconf_nat に渡すという意味で、それが H に戻るという補題である。

Lemma noconf_natK {m n : nat} (H : m = n) : noconf_nat_inv H noconf_nat = H.
Proof.
  case: m H => [|m] H.
    by subst n.
  by subst n.
Defined.

Compute fun (n : nat) => @noconf_nat_inv n.+1 n.+1 erefl _ (fun e => e).

Import EqNotations.

で、Vector.t の場合分けを証明する。

Lemma my_vector_caseS : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
Proof.
  move=> A n v P H.
  refine (
    match v as v' in Vector.t _ m return
      match m with
      | 0 => True
      | _ => forall (Hn : n.+1 = m) (Hv : rew Hn in v = v'), P v
      end
    with
    | Vector.nil => I
    | Vector.cons x n' t => _
    end erefl erefl).
  move=> Hn.
  rewrite -(noconf_natK Hn).
  rewrite /noconf_nat_inv.
  move: (f_equal predn Hn) => /= {}Hn.
  destruct Hn.
  simpl.
  move=> ->.
  apply/H.
Defined.

ここで、rewrite -(noconf_natK Hn) で Hn を noconf_nat_inv Hn noconf_nat に置き換えている。その後で、要素の等式の証明を変数に置き換えるのだが、noconf_nat_inv Hn noconf_nat という項には変数に置き換えるべき部分項が出てきていないので、 rewrite /noconf_nat_inv で noconf_nat_inv を展開している。展開すると noconf_nat (f_equal predn Hn) という項になるので、 f_equal predn Hn の部分が要素の等式の証明である。 (noconf_nat_inv の定義で f_equal predn H と明示的に指定たものがここに出現している。) これを一般化して、後は以前の証明と同様になる。

証明項を表示してみる。

Eval cbv beta zeta delta [my_vector_caseS] in my_vector_caseS.
(*
     = fun (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type)
         (H : forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) =>
       match
         v as v' in (Vector.t _ m)
         return match m with
                | 0 => True
                | _.+1 => forall Hn : n.+1 = m, rew [Vector.t A] Hn in v = v' -> P v
                end
       with
       | @Vector.nil _ => I
       | @Vector.cons _ x n' t =>
           fun Hn : n.+1 = n'.+1 =>
           rew [fun _pattern_value_ : n.+1 = n'.+1 =>
                rew [Vector.t A] _pattern_value_ in v = Vector.cons A x n' t -> P v] noconf_natK Hn in
           (rew dependent [fun n0 e => forall t0 : Vector.t A n0,
                                       rew [Vector.t A]
                                           eq_ind n (fun _pattern_value_ : nat => n.+1 = _pattern_value_.+1) erefl n0
                                             e in v = Vector.cons A x n0 t0 -> P v] f_equal predn Hn in
            (fun t0 : Vector.t A n => [eta eq_rect_r [eta P] (H x t0) (y:=v)])) t
       end erefl erefl
     : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v
*)

rew dependent [...] f_equal predn Hn in ... となっているが、以前の証明でここは rew dependent [...] noconf_nat_inv Hn in ... となっていた。

まぁ、要素の等式を得る関数はちゃんと自前で用意した方がよさそうである。今回は f_equal predn でシンプルに記述できたが、いつもそうとはかぎらない。

#4 Equations の depelim 同様のことを、自分でやってみる

depelim 同様のことを自分で (Equations を使わずに) やってみよう。

From mathcomp Require Import all_ssreflect.
Require Vector.

まず、nat に対する no confusion が必要なので定義する。

Definition Noconf_nat (m n : nat) : Prop :=
  match m, n with
  | 0, 0 => True
  | m'.+1, n'.+1 => m' = n'
  | _, _ => False
  end.

O の場合はコンストラクタに引数がないので、すべての要素が等しいといっても要素がないので True とする。 S の場合はコンストラクタに引数がひとつあるので、それが等しいということにする。それ以外、つまりコンストラクタが異なる場合はそれらが等しいというのはありえないので False とする。

Noconf_nat m n と m = n の相互変換を定義する。

Definition noconf_nat {m n} : Noconf_nat m n -> m = n.
  case: m; case: n => //.
  by move=> m n <-.
Defined.

Definition noconf_nat_inv {m n} : m = n -> Noconf_nat m n.
  case: m; case: n => //.
  by move=> m n <-.
Defined.

そして、m = n の証明を Noconf_nat m n を経由して m = n にすると元に戻ることを証明する。まぁ、等式 (eq 型) は、証明となるコンストラクタがひとつしかないので、subst で具体化してしまえば同じ項になるのがこの証明の仕掛けである。

Definition noconf_natK {m n} (H : m = n) : noconf_nat (noconf_nat_inv H) = H.
  case: m H => [|m] H.
    by subst n.
  by subst n.
Defined.

で、Vector.t の場合分けを証明する。 Equations では match で sigma 型の等式を生成していたが、直接 (DepElim.eq_simplification_sigma1_dep で変換した後の) e : n.+1 = n0.+1 と rew [Vector.t A] e in v = Vector.cons h n0 t の形を生成してもいいだろう、ということで、そうしている。

Import EqNotations.

Lemma my_vector_caseS : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
Proof.
  move=> A n v P H.
  refine (
    match v as v' in Vector.t _ m return
      forall (Hn : n.+1 = m) (Hv : rew Hn in v = v'), P v
    with
    | Vector.nil => _
    | Vector.cons x n' t => _
    end erefl erefl).
    by [].
  move=> Hn.
  rewrite -(noconf_natK Hn).
  move: (noconf_nat_inv Hn) => {}Hn.
  simpl in Hn; destruct Hn. (* subst n'. *)
  simpl.
  move=> ->.
  by apply H.
Defined.

証明を表示すると以下となる。 SSReflect は余計な let-in などを作るので、簡約して単純にするために cbv beta zeta としている。

Eval cbv beta zeta delta [my_vector_caseS] in my_vector_caseS.
(*
     = fun (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type)
         (H : forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) =>
       match v as v' in (Vector.t _ m) return (forall Hn : n.+1 = m, rew [Vector.t A] Hn in v = v' -> P v) with
       | @Vector.nil _ =>
           fun Hn : n.+1 = 0 =>
           fun=> False_rect (P v) (eq_ind n.+1 (fun e : nat => match e with
                                                               | 0 => False
                                                               | _.+1 => True
                                                               end) I 0 Hn)
       | @Vector.cons _ x n' t =>
           fun Hn : n.+1 = n'.+1 =>
           rew [fun _pattern_value_ : n.+1 = n'.+1 =>
                rew [Vector.t A] _pattern_value_ in v = Vector.cons A x n' t -> P v] noconf_natK Hn in
           (rew dependent [fun n0 e => forall t0 : Vector.t A n0,
                                       rew [Vector.t A] noconf_nat e in v = Vector.cons A x n0 t0 -> P v]
                noconf_nat_inv Hn in (fun t0 : Vector.t A n => [eta eq_rect_r [eta P] (H x t0) (y:=v)])) t
       end erefl erefl
     : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v
*)

これをみると、cons の場合に rew が 4回出現している。最初と 2番目の rew が refine で指定した match (とその return 節で使った rew) であり、残りが destruct Hn で生成されたものである。

あと、この証明では Vector.nil の場合に False_rect を使っているが、 return 節をいじって簡単に証明できる命題にかえてしまってもよい。そうすると、以下のようになる。

Lemma my_vector_caseS2 : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
Proof.
  move=> A n v P H.
  refine (
    match v as v' in Vector.t _ m return
      match m with
      | 0 => True
      | _ => forall (Hn : n.+1 = m) (Hv : rew Hn in v = v'), P v
      end
    with
    | Vector.nil => I
    | Vector.cons x n' t => _
    end erefl erefl).
  move=> Hn.
  rewrite -(noconf_natK Hn).
  move: (noconf_nat_inv Hn) => {}Hn.
  simpl in Hn; destruct Hn. (* subst n'. *)
  simpl.
  move=> ->.
  by apply H.
Defined.

Eval cbv beta zeta delta [my_vector_caseS2] in my_vector_caseS2.
(*
     = fun (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type)
         (H : forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) =>
       match
         v as v' in (Vector.t _ m)
         return match m with
                | 0 => True
                | _.+1 => forall Hn : n.+1 = m, rew [Vector.t A] Hn in v = v' -> P v
                end
       with
       | @Vector.nil _ => I
       | @Vector.cons _ x n' t =>
           fun Hn : n.+1 = n'.+1 =>
           rew [fun _pattern_value_ : n.+1 = n'.+1 =>
                rew [Vector.t A] _pattern_value_ in v = Vector.cons A x n' t -> P v] noconf_natK Hn in
           (rew dependent [fun n0 e => forall t0 : Vector.t A n0,
                                       rew [Vector.t A] noconf_nat e in v = Vector.cons A x n0 t0 -> P v]
                noconf_nat_inv Hn in (fun t0 : Vector.t A n => [eta eq_rect_r [eta P] (H x t0) (y:=v)])) t
       end erefl erefl
     : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v
*)

return 節で m が 0 の場合 (Vector.nil の場合) はゴールを True にしているので、対応する証明は I で済んでいる。

こうやって自分で証明しなおしてもやはり Eqdep_dec は使っておらず、 decidable equality には依存していないことが確認できた。

そして、この方法でどういう場合が解けるかというと、規則J による変数への代入と、no confusion による等式の両辺先頭のコンストラクタの除去で済む限りは解ける、ということなのだと思う。

Pattern Matching Without K には linear constructor forms の場合には解ける、と書いてある。ここでいう linear というのは各変数が 1回しか出現しないことで、constructor form というのは変数とコンストラクタしか出てこない形式である。その場合には、等式の両辺の先頭をみて、両方コンストラクタの場合、異なるコンストラクタだったら単一化失敗、同じコンストラクタだったら両辺から削る、というのを繰り返し、どちらかの辺が変数だったらその等式をその変数の解とする、というので済みそうである。 (各変数は1回しか出現しないので、両辺に同じ変数が出現することはない)

等式の片側が変数になって x = ... となった場合、規則J で代入されるが、そのときに ... の部分はどんな項であってもいいので、そこに変数が複数あったり、変数でもコンストラクタでもない項が入っていたりしても問題は生じない気がする。そういう意味で、linear constructor forms というのは説明しやすい保守的な条件なのだろう。

あと、no confusion というのはすべての帰納型でうまく作れるのか、というのが問題かな。

#3 Equations の depelim が生成する証明項を読む

Equations が提供する depelim tactic を使って Vector.t の (cons の場合の) 場合分けを証明して、その証明項を読んでみよう。

Vector.t はインデックスが nat で、nat には decidable equality があるのでもともと場合分けに公理は必要ないのだが、depelim はどうやって場合分けしているのだろうか。

From mathcomp Require Import all_ssreflect.
Require Vector.
Import EqNotations.
From Equations Require Import Equations.

Derive Signature for Vector.t.

Lemma depelim_vector_caseS : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v.
Proof.
  move=> A n v P H.
  depelim v.
  by apply H.
Defined.

Print depelim_vector_caseS.
(*
depelim_vector_caseS =
fun (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type) =>
[eta (let v0 := {| pr1 := n.+1; pr2 := v |} in
      (fun v' : nat =>
       [eta fun v2 : Vector.t A v' =>
            match
              v2 as t in (Vector.t _ n0)
              return
                ({| pr1 := n.+1; pr2 := v |} = {| pr1 := n0; pr2 := t |} ->
                 let H0 := CoreTactics.block in
                 forall P0 : Vector.t A n.+1 -> Type,
                 (forall (h : A) (t0 : Vector.t A n), P0 (Vector.cons A h n t0)) ->
                 let H1 := CoreTactics.block in P0 v)
            with
            | @Vector.nil _ =>
                DepElim.eq_simplification_sigma1_dep n.+1 0 v (Vector.nil A)
                  (apply_noConfusion n.+1 0
                     (Logic.False_rect_dep
                        (fun H0 : False =>
                         rew [[eta Vector.t A]] noConfusion H0 in v = Vector.nil A ->
                         let H1 := CoreTactics.block in
                         forall P0 : Vector.t A n.+1 -> Type,
                         (forall (h : A) (t : Vector.t A n), P0 (Vector.cons A h n t)) ->
                         let H2 := CoreTactics.block in P0 v)))
            | @Vector.cons _ h n0 t =>
                (fun (h0 : A) (n1 : nat) (v3 : Vector.t A n1) =>
                 DepElim.eq_simplification_sigma1_dep n.+1 n1.+1 v (Vector.cons A h0 n1 v3)
                   (apply_noConfusion n.+1 n1.+1
                      ((DepElim.solution_right_dep n
                          (fun v4 : Vector.t A n =>
                           [eta DepElim.solution_left (Vector.cons A h0 n v4)
                                  ((fun (P0 : Vector.t A n.+1 -> Type)
                                      (H2 : forall (h1 : A) (t0 : Vector.t A n), P0 (Vector.cons A h1 n t0)) =>
                                    let _H := CoreTactics.block in
                                    (H2 h0 v4 : P0 (Vector.cons A h0 n v4)) : P0 (Vector.cons A h0 n v4))
                                   :
                                   let H2 := CoreTactics.block in
                                   forall P0 : Vector.t A n.+1 -> Type,
                                   (forall (h1 : A) (t0 : Vector.t A n), P0 (Vector.cons A h1 n t0)) ->
                                   let H3 := CoreTactics.block in P0 (Vector.cons A h0 n v4)) v]) n1)^~ v3))) h n0 t
            end]) (pr1 v0) (pr2 v0) (erefl : {| pr1 := n.+1; pr2 := v |} = v0)) P]
     : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v

Arguments depelim_vector_caseS A%type_scope n%nat_scope v (P _)%function_scope
*)

なんか余計なものが入っているようなので、簡約してみよう。

Eval cbv beta zeta iota delta [depelim_vector_caseS] in depelim_vector_caseS.
(*
     = fun (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type) =>
       [eta match
              v as t in (Vector.t _ n0)
              return
                ({| pr1 := n.+1; pr2 := v |} = {| pr1 := n0; pr2 := t |} ->
                 forall P0 : Vector.t A n.+1 -> Type,
                 (forall (h : A) (t0 : Vector.t A n), P0 (Vector.cons A h n t0)) -> P0 v)
            with
            | @Vector.nil _ =>
                DepElim.eq_simplification_sigma1_dep n.+1 0 v (Vector.nil A)
                  (apply_noConfusion n.+1 0
                     (Logic.False_rect_dep
                        (fun H0 : False =>
                         rew [[eta Vector.t A]] noConfusion H0 in v = Vector.nil A ->
                         forall P0 : Vector.t A n.+1 -> Type,
                         (forall (h : A) (t : Vector.t A n), P0 (Vector.cons A h n t)) -> P0 v)))
            | @Vector.cons _ h n0 t =>
                DepElim.eq_simplification_sigma1_dep n.+1 n0.+1 v (Vector.cons A h n0 t)
                  (apply_noConfusion n.+1 n0.+1
                     ((DepElim.solution_right_dep n
                         (fun v0 : Vector.t A n =>
                          [eta DepElim.solution_left (Vector.cons A h n v0)
                                 (fun (P0 : Vector.t A n.+1 -> Type)
                                    (H2 : forall (h0 : A) (t0 : Vector.t A n), P0 (Vector.cons A h0 n t0)) =>
                                  H2 h v0) v]) n0)^~ t))
            end erefl P]
     : forall (A : Type) (n : nat) (v : Vector.t A n.+1) (P : Vector.t A n.+1 -> Type),
       (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v
*)

match で Vector.nil と Vector.cons に場合分けしている。 return 節は以下になっている。

return
  ({| pr1 := n.+1; pr2 := v |} = {| pr1 := n0; pr2 := t |} ->
   forall P0 : Vector.t A n.+1 -> Type,
   (forall (h : A) (t0 : Vector.t A n), P0 (Vector.cons A h n t0)) -> P0 v)

match 式自体を関数として、3つの引数がわたされている。最初のふたつは erefl と P である。最後は eta で隠されていて分かりにくいが、最初の証明では H と名づけた forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t) 型の値である。最初の引数 erefl を {| pr1 := n.+1; pr2 := v |} = {| pr1 := n0; pr2 := t |} 型として受け取って、等式を生成しているようだ。 P と H は、型が変わっていないようで、なんで convoy pattern にしているかは分からない。

{| pr1 := ...; pr2 := ... |} がなにかというと、Equations では、独自に sigma 型を定義しているようだ。

<URL:https://github.com/mattam82/Coq-Equations/blob/v1.3.1-8.20/theories/Init.v#L69-L75>

Set Primitive Projections.
Global Unset Printing Primitive Projection Parameters.
Polymorphic Cumulative Record sigma@{i} {A : Type@{i}} {B : forall (_ : A), Type@{i}} : Type@{i} :=
  sigmaI { pr1 : A; pr2 : B pr1 }.
Unset Primitive Projections.
Arguments sigma {A} B.
Arguments sigmaI {A} B pr1 pr2.

なんで標準の sigT を使っていないのかは分からない。 Polymorphic, Cumulative, (Primitive Projections な) Record のいずれかが理由だと推測されるが、なんだろうな。

match に as t in (Vector.t _ n0) と書いてあるので {| pr1 := n.+1; pr2 := v |} = {| pr1 := n0; pr2 := t |} の等式の t, n0 の部分が各分岐ではそれぞれのコンストラクタで得られるものに置き換えられる。 nil の場合は {| pr1 := n.+1; pr2 := v |} = {| pr1 := 0; pr2 := Vector.nil |} で、 cons の場合は {| pr1 := n.+1; pr2 := v |} = {| pr1 := n0.+1; pr2 := Vector.cons h n0 t |} となるのだろう。

Vector.nil の場合は {| pr1 := n.+1; pr2 := v |} = {| pr1 := 0; pr2 := Vector.nil |} という等式が発生する。この pr1 同士が等しいという、n.+1 = 0 は矛盾するので、その矛盾から Logic.False_rect_dep を使って証明しているのだろう。

Vector.cons の場合は {| pr1 := n.+1; pr2 := v |} = {| pr1 := n0.+1; pr2 := Vector.cons h n0 t |} という等式が発生する。ここでは n.+1 = n0.+1 と v = Vector.cons h n0 t という等式からなる単一化問題を解かなければならない。そう考えると、n.+1 = n0.+1 から n = n0 を得て、n0 を代入して v = Vector.cons h n t を得て、もともとのゴールにある v を Vector.cons h n t に置換する、というのが期待される。 (n0 は match のときに発生した変数なので、もともとのゴールには存在しない)

これを DepElim.eq_simplification_sigma1_dep, apply_noConfusion, DepElim.solution_right_dep, DepElim.solution_left という補題を使ってやっているようだ。いろいろ調べると、以下のようなことをしているようだ。

DepElim.eq_simplification_sigma1_dep は、{| pr1 := p; pr2 := x |} = {| pr1 := q; pr2 := y |} という等式を、e : p = q と rew [P] e in x = y に分ける
apply_noConfusion は n.+1 = n0.+1 の証明を、n = n0 の証明から作り直す
DepElim.solution_right_dep は n = n0 の等式の証明として erefl を作り出す
DepElim.solution_left は v = Vector.cons h n0 t の等式を解く (v を右辺に置き換える)

それぞれの型を調べると以下だった。

About DepElim.eq_simplification_sigma1_dep.
(*
DepElim.eq_simplification_sigma1_dep@{i j} :
forall {A : Type} {P : A -> Type} {B : Type} (p q : A) (x : P p) (y : P q),
(forall e : p = q, rew [P] e in x = y -> B) -> {| pr1 := p; pr2 := x |} = {| pr1 := q; pr2 := y |} -> B

DepElim.eq_simplification_sigma1_dep is universe polymorphic
Arguments DepElim.eq_simplification_sigma1_dep {A}%type_scope {P}%function_scope {B}%type_scope
  p q x y _%function_scope _
DepElim.eq_simplification_sigma1_dep is transparent
Expands to: Constant Equations.Prop.DepElim.eq_simplification_sigma1_dep
*)

About apply_noConfusion.
(*
apply_noConfusion :
forall {A : Type} {noconf : NoConfusionPackage A} (p q : A) {B : p = q -> Type},
(forall H : NoConfusion p q, B (noConfusion H)) -> forall H : p = q, B H

apply_noConfusion is not universe polymorphic
Arguments apply_noConfusion {A}%type_scope {noconf} p q {B}%function_scope _%function_scope H
apply_noConfusion is transparent
Expands to: Constant Equations.Prop.Classes.apply_noConfusion
*)

About DepElim.solution_right_dep.
(*
DepElim.solution_right_dep :
forall {A : Type} (t : A) {B : forall x : A, t = x -> Type}, B t erefl -> forall (x : A) (Heq : t = x), B x Heq

DepElim.solution_right_dep is not universe polymorphic
Arguments DepElim.solution_right_dep {A}%type_scope t {B}%function_scope _ x Heq
DepElim.solution_right_dep is transparent
Expands to: Constant Equations.Prop.DepElim.solution_right_dep
*)

About DepElim.solution_left.
(*
DepElim.solution_left : forall {A : Type} {B : A -> Type} (t : A), B t -> forall x : A, x = t -> B x

DepElim.solution_left is not universe polymorphic
Arguments DepElim.solution_left {A}%type_scope {B}%function_scope t p x e
DepElim.solution_left is transparent
Expands to: Constant Equations.Prop.DepElim.solution_left
*)

DepElim.eq_simplification_sigma1_dep は、{| pr1 := p; pr2 := x |} = {| pr1 := q; pr2 := y |} 型から e : p = q と rew [P] e in x = y に変えている。これらは sigT でいえば等価で、そのことは eq_sigT_uncurried_iff で証明されているので、それと同じことなのだろう。 Coq.Init.Specif : eq_sigT_uncurried_iff

今回 (cons) の場合 {| pr1 := n.+1; pr2 := v |} = {| pr1 := n0.+1; pr2 := Vector.cons h n0 t |} なので、 e : n.+1 = n0.+1 と rew [Vector.t A] e in v = Vector.cons h n0 t となる。

apply_noConfusion はなにかというと、ここでは n.+1 = n1.+1 の証明 H を、n = n1 の証明をもとに作り直している。

単に n.+1 = n1.+1 から n = n1 を導出するだけなら、両辺から 1 を引けばいい (vanilla Coq の injection や SSReflect の case でできる) が、ここでは、n.+1 = n1.+1 の証明 e が後で使われているので、 n = n1 の証明からその e を求められるような形で n = n1 の証明を作らなければならない。これは単純ではない。

そのために、no confusion というのが使われる。 no confusion というのは、各帰納型ごとに定義され、値の等式と、要素毎の等式を変換するものである。 (要素というのはコンストラクタの引数である)

Check fun (n n1:nat) => @apply_noConfusion nat NoConfusionPackage_nat n.+1 n1.+1.
(*
fun n n1 : nat => @apply_noConfusion nat NoConfusionPackage_nat n.+1 n1.+1
     : forall (n n1 : nat) (B : n.+1 = n1.+1 -> Type),
       (forall H : @NoConfusion nat NoConfusionPackage_nat n.+1 n1.+1,
        B (@noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H)) -> forall H : n.+1 = n1.+1, B H
*)

Check (fun (n n1:nat) => @apply_noConfusion nat NoConfusionPackage_nat n.+1 n1.+1) :
  forall (n n1 : nat) (B : n.+1 = n1.+1 -> Type),
    (forall H : n = n1, B (@noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H)) ->
    forall H : n.+1 = n1.+1, B H.

というわけで @apply_noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 の型は、以下である。

forall (B : n.+1 = n1.+1 -> Type),
       (forall H : n = n1, B (@noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H)) ->
       forall H1 : n.+1 = n1.+1, B H1.

これを使うと、B H1 を証明するのに、H : n = n1 を前提として B (@noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H) を証明すればよい、ということがわかる。 @noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H が n = n1 の証明である H から n.+1 = n1.+1 の証明を作っている。

そして、noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H は、H として erefl を与えると (その場合 n.+1 と n1.+1 は同じでなければならない) 以下のように、erefl に簡約される。

Compute fun n => @noConfusion nat NoConfusionPackage_nat n.+1 n.+1 erefl.
(*
     = fun n : nat => erefl
     : forall n : nat, n.+1 = n.+1
*)

というわけで、もともと H1 : n.+1 = n1.+1 だったところを @noConfusion nat NoConfusionPackage_nat n.+1 n1.+1 H とすれば、H : n = n1 をもとにした形に変形できることになる。

これは、単一化問題で n.+1 = n1.+1 を n = n1 に変形するところを実現しているといえる。

DepElim.solution_right_dep は、n = n0 を erefl として解く。 Coq では dependent match により、等式の片方が変数の場合 (かつ、もう一方にその変数が出現しない場合)、その証明を erefl に具体化できる。 (もちろん、そのときに、その変数がもう一方に置換される。) vanilla Coq の destruct や subst でそういう項を生成できる。この変形は規則J とも呼ばれるようだ。そうやって erefl が生成されると、rew [Vector.t A] e in v = Vector.cons h n0 t の e が erefl となり、rew がとれて v = Vector.cons h n0 t となる。

なお、destruct は帰納型の場合分けなので、場合分けした結果としてコンストラクタが出てくるのは自然だが、 subst もそうなるというのは Coq マニュアルの subst の項に Note として If the hypothesis is itself dependent in the goal, it is replaced by the proof of reflexivity of equality. と説明がある。例はないが、この動作のことを指しているのだと思う。

さらになお、SSReflect の case は、対象が eq 型の場合には特別に injection 相当の動作が割り当てられているので、このためには使えない。

最後に DepElim.solution_left だが、これは単に v = Vector.cons h n0 t を使って書き換えているだけだと思う。

#2 参考文献

dependent match を単一化問題ととらえて解く方法は、 dependent pattern match の話で研究されているようだ。

Pattern Matching Without K <URL:https://jesper.sikanda.be/publications.html>
Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq <URL:https://github.com/mattam82/Coq-Equations>

dependent pattern match は、パターンマッチを行うときに、自動的に単一化が起こっていくようなものである。 Agda の関数定義で使われている。

ただ、これは型理論の立場からいうと、公理K というものを使ってしまう。公理K は、Coq の FAQ の Axioms にも載っているが、等式の証明はひとつしかない、というものである。等価な公理がいろいろあって、いろいろな呼び方がある。UIP とか Unicity of equality proofs とか。 Coq 本体 (kernel) には公理Kは入っておらず、利用するにはライブラリ Coq.Logic.Eqdep を使う。

ただ、公理K は HoTT (Homotopy type theory) と矛盾するので、使いたくないという立場もある。 HoTT と関係なくても、単に公理は避けたいという立場もある。そのため、これを使わない範囲で dependent pattern match をやろうという話が Pattern Matching Without K で、それを Coq でやるのが Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq のようだ。 (Coq でやるだけでなくちょっと拡張されているのかもしれない)

なお、インデックスに decidable equality があれば Eqdep のかわりに Eqdep_dec を使えるので、公理を使わずに場合分けできるが、 decidable equality がなくてもどうにかする、また、どこまでできるか、という話なのだと思う。

#1 Coq の dependent match は単一化問題を発生させる

突然だが、Coq の dependent match は単一化問題を発生させるという認識に到達した。

インデックス付き帰納型 D i の項 x を場合分けするとして、その帰納型のコンストラクタ C が forall ..., D i' という型であり、match で C の分岐が選ばれた場合、

i = i'
x = C args

というふたつの等式が成り立つことになる。これらの等式から必要な情報を取り出すのが、やりたいことである。

この単一化問題はコンストラクタごとに (match の分岐ごとに) 生成される。また、一般にインデックスは複数あるので、等式はインデックスの数+1個生成される。

このような認識により、単一化の話を dependent match へ類推して適用することができる。

単一化問題と考えると、その解は、変数への代入である。 (また、そのような代入が存在しないというのも解である)

ということは、dependent match も、その解は変数への代入なのだろう。

ということで、dependent match で変数以外の項を置換してしまうことがあるが、それは一般には危ういやりかたなのだろう。もちろん、危うくても結果として証明に成功するかぎりは問題ないのだが、証明に悩んでいるときは、そこを疑うのは悪くないだろう。

ある型 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 と矛盾しないと証明していると思うので) 問題は少ないはずである。

天泣記

2025-01-14 (Tue)

2025-01-13 (Mon)

2024-12-22 (Sun)

2024-12-03 (Tue)