天泣記

2025-01-13 (Mon)

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

#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 がなくてもどうにかする、また、どこまでできるか、という話なのだと思う。

#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 を使って書き換えているだけだと思う。

#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 というのはすべての帰納型でうまく作れるのか、というのが問題かな。

#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 でシンプルに記述できたが、いつもそうとはかぎらない。

2025-01-14 (Tue)

#1 forall {m n : nat} (H : m.+1 = n.+1), f_equal succn (f_equal predn H) = H を証明する

昨日の my_vector_caseS で Hn を noconf_nat_inv Hn noconf_nat に置き換えるのに noconf_natK という補題を使った。 そのために no confusion という準備が必要だった。

さらに置き換えた後に noconf_nat_inv Hn noconf_nat を展開して noconf_nat (f_equal predn Hn) にした。

でも、ここで Hn は n.+1 = n'.+1 という型なので、 両辺の先頭が S なのはすでに判明している。 なので、もっと直接的に noconf_nat (f_equal predn Hn) = Hn という補題を作れないだろうか。

もちろんこれは noconf_natK を等式の両辺が S のときの場合に限った命題なので、noconf_natK を使って簡単に証明できる。

Lemma eqprK_nat_S {m n : nat} (Hn : m.+1 = n.+1) : @noconf_nat m.+1 n.+1 (f_equal predn Hn) = Hn.
Proof.
  change (noconf_nat_inv Hn noconf_nat = Hn).
  by apply noconf_natK.
Defined.

ただ、noconf_natK を使わないで、直接的に証明できないだろうか。

ここで、この場合 (両辺が S の場合) noconf_nat は等式の両辺に S を適用するので、 結局 f_equal succn (f_equal predn H) = H となる。 これを証明できないか考えよう。

これが証明できれば、証明のときに Hn を noconf_nat_inv Hn noconf_nat にしてから展開するとか no confusion とか CPS を持ち出す必要もなくなる。

というわけで挑戦してみよう。

From mathcomp Require Import all_ssreflect.

Lemma eqprK_nat_S {m n : nat} (H : m.+1 = n.+1) :
  @f_equal nat nat succn m.+1.-1 n.+1.-1 (@f_equal nat nat predn m.+1 n.+1 H) = H.
Proof.

ここで、H を場合分けして erefl に具体化できれば、証明は完了するはずであるが、以下のように destruct H は失敗する。

Fail destruct H.
(*
Abstracting over the terms "n0" and "H" leads to a term
fun (n1 : nat) (H0 : m.+1 = n1) => @f_equal nat nat succn m.+1.-1 n1.-1 (@f_equal nat nat predn m.+1 n1 H0) = H0
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "m.+1.-1.+1 = n1.-1.+1" : "Prop"
 "@f_equal nat nat succn m.+1.-1 n1.-1 (@f_equal nat nat predn m.+1 n1 H0)" : "m.+1.-1.+1 = n1.-1.+1"
 "H0" : "m.+1 = n1"
The 3rd term has type "m.+1 = n1" which should be a subtype of "m.+1.-1.+1 = n1.-1.+1".
*)

依存型エラーのときはだいたいそうだが、どういう項が作られてなぜエラーになっているのかわからない。 なので、自分で match を書いてやってみよう。

Fail refine
  (match H as H' in _ = x return
    @f_equal nat nat succn m.+1.-1 x.-1 (@f_equal nat nat predn m.+1 x H') = H'
  with
  | erefl => _
  end).
(*
The command has indeed failed with message:
In environment
m, n : nat
H : m.+1 = n.+1
x : nat
H' : m.+1 = x
The term "H'" has type "m.+1 = x" while it is expected to have type "m.+1.-1.+1 = x.-1.+1".
*)

上のエラーでは "m.+1 = n1" と "m.+1.-1.+1 = n1.-1.+1" が異なる、というものだったが、 今回は "m.+1 = x" と "m.+1.-1.+1 = x.-1.+1" が異なる、となっていて、変数の名前は違うだけなので、たぶん destruct はこういう項を作っているのだろう。

これをみて考えると、return 節では n.+1 を x に置き換えているので、もともとは S n という形 (つまり 1 以上の自然数) の場合だけに限定されていた命題が 任意の自然数についての命題に変わっていて、0 の場合に型が壊れているのが問題と理解できる。

とすると、0 の場合も含めて型がつく命題である必要があるのではないか。 そして、no confusion はまさに 0 の場合も扱っているので、それで証明できるのだということがわかる。

しかしここでは no confusion を導入せずに証明したい。

ここでアイデアが思い浮かんだ。 0 の場合は扱っていないので、0 の場合は自明な命題になるようにしてしまえばいいのではないか。 ということで、以下のように変形する。 0 の場合は True にしてしまうのである。(ちなみに型がつけばなんでもよく、False でもよい)

refine
  (match H as H' in _ = x return
    match x with
    | 0 => fun=> True
    | n'.+1 => fun H' => @f_equal nat nat succn m.+1.-1 n'.+1.-1 (@f_equal nat nat predn m.+1 n'.+1 H') = H'
    end H'
  with
  | erefl => _
  end).

こうすると、ゴールは @f_equal nat nat succn m.+1.-1 m.+1.-1 (@f_equal nat nat predn m.+1 m.+1 erefl) = erefl になった。 H が erefl になったのでこれは計算を進められるようになり、reflexivity で証明できる。

ただ、refine を使う必要は無くて、ゴールをその形にしておけばよい。 (destruct はそのときのゴールを return 節にするため。)

change
  (match n.+1 with
  | 0 => fun=> True
  | n'.+1 => fun H => @f_equal nat nat succn m n' (@f_equal nat nat predn m.+1 n'.+1 H) = H
  end H).

これで destruct H が通って証明できた。

by destruct H.

試行錯誤を除いた最終的な証明を示しておく。 (あと、命題のところで .+1.-1 が出てくるのは無駄なので消しておいた。)

Lemma eqprK_nat_S {m n : nat} (H : m.+1 = n.+1) :
  @f_equal nat nat succn m n (@f_equal nat nat predn m.+1 n.+1 H) = H.
Proof.
  change
    (match n.+1 with
    | 0 => fun=> True
    | n'.+1 => fun H => @f_equal nat nat succn m n' (@f_equal nat nat predn m.+1 n'.+1 H) = H
    end H).
  by destruct H.
Defined.

[latest]