天泣記

#2 Eqdep_dec.K_dec を使った eq_irrelevance の証明

検索していると、また別の eq_irrelevance の証明を見つけた:

<URL:https://people.mpi-sws.org/~viktor/arefs/Veq.html>

eq_irrelevance のところだけ取り出すと、以下のようになる。

From mathcomp Require Import all_ssreflect.

Theorem eq_irrelevance : forall (T : eqType) (x y : T) (e1 e2 : x = y), e1 = e2.
Proof.
  intros; revert e2; subst y.
  apply Eqdep_dec.K_dec; try done.
  clear; intros; case (@eqP T x y).
  move=> Heq; by left.
  move=> Hne; by right.
Qed.

ここでは、Eqdep_dec.K_dec を使っている。これは以下の型の定理である。(公理は使っていない)

Eqdep_dec.K_dec :
forall [A : Type],
(forall x y : A, x = y \/ x <> y) ->
forall (x : A) (P : x = x -> Prop), P (erefl x) -> forall p : x = x, P p

Eqdep_dec の定理であることから、eq_rect_eq_dec と同じような立ち位置なのだろうな、と思う。

証明の中身を追っているときに気がついたのだが、subst tactic が e1 という変数を erefl x に置換することに気がついた。

Theorem eq_irrelevance : forall (T : eqType) (x y : T) (e1 e2 : x = y), e1 = e2.
Proof.
  intros; revert e2.
  (* forall e2 : x = y, e1 = e2 *)
  subst y.
  (* forall e2 : x = x, erefl x = e2 *)
  apply Eqdep_dec.K_dec; try done.
  clear; intros; case (@eqP T x y).
  move=> Heq; by left.
  move=> Hne; by right.
Qed.

マニュアルを確認すると、 <URL:https://coq.inria.fr/doc/V8.19.0/refman/proofs/writing-proofs/equality.html#coq:tacn.subst> に Note として "If the hypothesis is itself dependent in the goal, it is replaced by the proof of reflexivity of equality." という記載があって、この挙動のことを示しているのだろうな、と思った。

#1 SSReflect の eq_irrelevance の証明を読む

自前で eq_irrelevance を証明できたが、SSReflect はどうやって証明しているのだろうか。 eq_rect を使っているのだろうか。

SSReflect では、 <URL:https://github.com/math-comp/math-comp/blob/mathcomp-2.2.0/mathcomp/ssreflect/eqtype.v#L290-L297> にあるように、以下の証明となっている。

Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
Proof.
pose proj z e := if x =P z is ReflectT e0 then e0 else e.
suff: injective (proj y) by rewrite /proj => injp e e'; apply: injp; case: eqP.
pose join (e : x = _) := etrans (esym e).
apply: can_inj (join x y (proj x (erefl x))) _.
by case: y /; case: _ / (proj x _).
Qed.

ふむ、表面的には、eq_rect は使っていないようだ。

しかし、なにをやっているのかわからないので、なんとか読んでみよう...

かなり時間がかかったが、なんとか読めたので、どうやっているか説明してみる。

まず、省略されているところを書き足して、ちょっと冗長にしたバージョンが以下である。

Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
Proof.
pose proj (z : T) (e : x = z) : x = z := if @eqP T x z is ReflectT e0 then e0 else e.
suff: injective (proj y).
  by rewrite /proj => injp e e'; apply: injp; case: eqP.
pose join (s1 s2 : T) (e3 : x = s1) (e4 : x = s2) : s1 = s2 := etrans (esym e3) e4.
apply: (@can_inj (x = y) (x = y) (proj y) (join x y (proj x (erefl x)))).
by case: y /; case: {1 2 3 4 5}x / (proj x (erefl x)).
Qed.

この証明の中には、pose で始まる行がふたつあって、これらは関数 (proj と join) を定義している。残りが証明である。

suff: injective (proj y). という行の直前ではゴールは forall e1 e2 : x = y, e1 = e2 である。 suff tactic は「それを証明するにはこれを証明すれば十分である」という意味（を実現する tactic）で結局、injective (proj y) の証明と、injective (proj y) -> forall e1 e2 : x = y, e1 = e2 の証明にゴールを分けている。

by rewrite /proj => injp e e'; apply: injp; case: eqP. の行が injective (proj y) -> forall e1 e2 : x = y, e1 = e2 をを証明している。

apply: (@can_inj (x = y) (x = y) (proj y) (join x y (proj x (erefl x)))). の行は can_inj という補題の名前からも想像されるように、 injective を cancel に変えている。具体的には injective (proj y) を cancel (proj y) (join x y (proj x (erefl x))) に変えている。

そして、最後の by case: y /; case: {1 2 3 4 5}x / (proj x (erefl x)). が cancel (proj y) (join x y (proj x (erefl x))) を証明している。

というのが証明の構造である。

たぶん、injective を cancel に変えることで、場合分けの対象を 2つから 1つに変えているのだと思う。 (場合分けの対象が 2つあると、片方を場合分けしたことで型が壊れるから)

個々の部分の証明を説明する。

by rewrite /proj => injp e e'; apply: injp; case: eqP. は injective (proj y) -> forall e1 e2 : x = y, e1 = e2 の証明である。 proj というのは

pose proj (z : T) (e : x = z) : x = z := if @eqP T x z is ReflectT e0 then e0 else e.

と導入された 2引数関数である。 injective (proj y) というのは proj y : (x = y) -> (x = y) という関数が injective (単射) である、という命題である。

単射というのは、関数の返値が同じなら引数も同じということである。以下のように定義されている。まぁ、最後の f x1 = f x2 -> x1 = x2 というところが肝心で、f の返値が同じなら引数も同じ、という命題である。

injective =
fun (rT aT : Type) (f : aT -> rT) => forall x1 x2 : aT, f x1 = f x2 -> x1 = x2
   : forall rT aT : Type, (aT -> rT) -> Prop

証明の by rewrite /proj => injp e e'; apply: injp; case: eqP. を分解してみよう。

まず、rewrite /proj => injp e e'. で、proj 関数を展開し、injective (proj y), e1, e2 をコンテキストに動かして injp, e, e' という名前をつける。これでゴールは e = e' となる。 (コンテキストの injp, e, e' も示してある)

(* injective (proj y) -> forall e1 e2 : x = y, e1 = e2 *)
rewrite /proj => injp e e'.
(*
injp : @injective (x = y) (x = y)
         (fun e : x = y =>
          match @eqP T x y with
          | ReflectT _ e0 => e0
          | ReflectF _ _ => e
          end)
e, e' : x = y
*)
(* e = e' *)

次に、injp を apply する。 injp は injective (proj y) で、proj y は x = y の証明を受け取って x = y の証明を返す関数である。なので、返値の x = y の証明が同じなら、引数の x = y の証明も同じ、ということで、ちょうど eq_irrelevance と同じ結論なので、ゴールに適用できる。適用すると、以下のようになる。

apply: injp.
(*
match @eqP T x y with
| ReflectT _ e0 => e0
| ReflectF _ _ => e
end =
match @eqP T x y with
| ReflectT _ e0 => e0
| ReflectF _ _ => e'
end
*)

等式の左辺と右辺に match 式がある。左辺と右辺はだいたい同じだが、ReflectF の分岐は、左辺が e で右辺が e' になっているところだけが違う。

match の条件式は左辺と右辺で同じなので、そこで場合分けする。そうすると、ReflectT の場合の等式と ReflectF の場合の等式に分かれる。

ReflectT の場合は forall p : x = y, p = p というゴールになって、p = p は自明に証明できる。

ReflectF の場合は x <> y -> e = e' というゴールになって、x <> y というのはコンテキストにある e, e' : x = y と矛盾するのでこれも自明に証明される。

case: (@eqP T x y).
  (* ReflectTの場合: forall p : x = y, p = p *)
  by [].
(* ReflectFの場合: x <> y -> e = e' *)
by [].

proj の定義は以下であった。

pose proj (z : T) (e : x = z) : x = z := if @eqP T x z is ReflectT e0 then e0 else e.

proj が何をやっているかというと、 @eqP T x z によって x と z が等しい (ReflectT) か、等しくない (ReflectF) のどちらかという場合分けを行い、等しい場合は ReflectT コンストラクタから取り出した x = z の証明を返し、等しくない場合は引数に渡された e を返している。

injp を apply した後の場合分けで、 ReflectT の場合はコンストラクタから取り出した証明が左辺右辺で等しいとしているが、この場合分けでは @eqP T x y を、ReflectT をなにか謎の引数に適用して作られた値に置き替えるが、謎ではあるが左辺と右辺にある @eqP T x y を同じく置き替えるので、結局左辺と右辺が等しいということはわかるので証明できる。

ReflectF の場合つまり x と y が異なる場合というのは、もともと proj が e : x = z を受け取っているので、ありえない場合なので、そこから矛盾がでてきて証明できている。

というわけで、injective (proj y) -> forall e1 e2 : x = y, e1 = e2 の証明はできた。

次は injective (proj y) である。

この証明のために、join という関数を定義している。

pose join (s1 s2 : T) (e3 : x = s1) (e4 : x = s2) : s1 = s2 := etrans (esym e3) e4.

型をみるとわかるが、x = s1 の証明と x = s2 の証明を受け取って s1 = s2 の証明を返す関数である。等式の交換律と推移律を使っていて、esym が交換律で、etrans が推移律である。

証明の apply: (@can_inj (x = y) (x = y) (proj y) (join x y (proj x (erefl x)))). の行は、 join を使って、injective (proj y) をまず cancel (proj y) (join x y (proj x (erefl x))) に変形する。 (Coq は逆方向に証明を進めるので「cancel (proj y) (join x y (proj x (erefl x))) ならば injective (proj y)」を証明している)

cancel というのは、以下のように定義されていて、cancel f g というのが g が f の逆関数であるという命題となる。

cancel =
fun (rT aT : Type) (f : aT -> rT) (g : rT -> aT) => forall x : aT, g (f x) = x
     : forall rT aT : Type, (aT -> rT) -> (rT -> aT) -> Prop

逆関数があるなら単射である、というのはそれはそうだろう。単射でなかったら結果が混ざってしまうから元に戻せない。

なので、cancel ならば injective という補題 can_inj が用意されている。

can_inj :
forall [rT aT : Type] [f : aT -> rT] [g : rT -> aT],
@cancel rT aT f g -> forall x1 x2 : aT, f x1 = f x2 -> x1 = x2

明示的に inejective とは書いていないが、f x1 = f x2 -> x1 = x2 というところが injective だろう。

証明は apply: (@can_inj (x = y) (x = y) (proj y) (join x y (proj x (erefl x)))). である。 apply: に渡している項の型は以下である。

@can_inj (x = y) (x = y) (proj y) (join x y (proj x (erefl x)))
     : @cancel (x = y) (x = y) (proj y) (join x y (proj x (erefl x))) ->
       @injective (x = y) (x = y) (proj y)

cancel -> injective という型なので、これを apply すれば、cancel になる、というわけである。

なお、x = y には値がたかだかひとつしかないので、結局のところ逆関数は引数をそのまま返せば良い、と考えてしまうと、join じゃなくて id でもいいのではないか、と思ってしまうかもしれない。実際、ここで apply: (@can_inj (x = y) (x = y) (proj y) id). としてもエラーにはならない。ここで join というものを導入して使っているのは次のステップで行われる場合分けをするためである。

これでゴールが @cancel (x = y) (x = y) (proj y) (join x y (proj x (erefl x))) となった。 implicit argument を省略すれば cancel (proj y) (join x y (proj x (erefl x))) である。

これが by case: y /; case: {1 2 3 4 5}x / (proj x (erefl x)) で証明される。

分解してみよう。

(* @cancel (x = y) (x = y) (proj y) (join x y (proj x (erefl x))) *)
move=> w.
(* join x y (proj x (erefl x)) (proj y w) = w *)
case: y / w.
(* join x x (proj x (erefl x)) (proj x (erefl x)) = erefl x *)
case: {1 2 3 4 5}x / (proj x (erefl x)).
(* join x x (erefl x) (erefl x) = erefl x *)
by [].

最初の case: y / というのは、ゴール先頭の変数(forall) で場合分けしているので、そのまえに move=> w で明示的な変数として、どんなゴールを場合分けしているのか可視化する。すると、case: y / w 直前では、join x y (proj x (erefl x)) (proj y w) = w となっていることがわかった。

case: y / w により、w が場合分けされ、erefl x に変わっている。 w は x = y 型なので、コンストラクタは erefl x のひとつの場合しかない。

case: y / というように、case: には、変数... / という指定をつけられる。これは、インデックス付き帰納型の場合分けをしたときに、インデックスの置換をどこで行うかの指定である。 case: y / w は、w で場合分けして、w の型は x = y 型なので、y がインデックスであり、場合分けにより y は x に対応することが判明するので、すべての y を x に置換するというわけである。

ここで、等式の左右の型が x = y 型から、x = x 型に変わっているが、左右が同時に変わっているため、うまくいっている。

次に、case: {1 2 3 4 5}x / (proj x (erefl x)) とすると、(proj x (erefl x)) が場合分けされ、 (その型は x = x なので) それが erefl x に変わる。

そうすると、join x x (erefl x) (erefl x) = erefl x となるが、これは簡約を進めると erefl x = erefl x になるので、自明に証明される。

ここで、case: {1 2 3 4 5}x / (proj x (erefl x)) の {1 2 3 4 5}x は、 (proj x (erefl x)) (これの型は x = x である) を場合分けする際のインデックスの x の置換をどれで行うかという指定で、 1番めと 2番めと 3番めと 4番めと 5番めを置換せよ、という意味である。

このときのゴールは join x x (erefl x) (erefl x) = erefl x なので、1番めから5番めというのは全てじゃないのかと思えるのだが、 case: x / (proj x (erefl x)) とすると x is used in conclusion. というエラーになる。

このゴールは、ぜんぶ省略しないで書くと以下になる。

@eq (@eq (Equality.sort T) x x)
  (join x x (proj x (@Logic.eq_refl (Equality.sort T) x))
     (proj x (@Logic.eq_refl (Equality.sort T) x)))
  (@Logic.eq_refl (Equality.sort T) x)

こうすると x が 9回出てくることがわかるのだが、その最初の 5個を置換するのかというとそうとも思えない。

case: {1 2 3 4 5}x / (proj x (erefl x)) のかわりに refine で証明項を直接与えると、以下のようになる。

refine (match (proj x (erefl x)) as e in _ = a
        return @eq (a = a) (join a a e e) (erefl a)
        with
        | erefl => _
        end).

return 節に書いてある @eq (a = a) (join a a e e) (erefl a) の a の部分が (in _ = a と指定してあるので) 置換されるところである。結局、場合分けの対象の (proj x (erefl x)) の内部以外に現れる x はすべて置換している。

なんか、case: x / (proj x (erefl x)) とすると、(proj x (erefl x)) の内部の x を置換しようとしてしまうんじゃないかという気がしているが、確信はない。 (case: _ / (proj x (erefl x)) と書けばうまくやってくれるので、わざわざ x と指定した場合はそれとは違う動作をしてくれるのかもしれない。どのように役に立つのかは分からないが。)

この match がうまくいく (型がつく) のが join の意義である。 (proj x (erefl x)) の型は x = x であるが、 return 節の中で、(as e と書いてあるので) それが e として表現され、e の型は x = a となる。

現在のゴールは join x x (erefl x) (erefl x) = erefl x であって、左辺と右辺の型は x = x である。それが return 節では @eq (a = a) (join a a e e) (erefl a) と a = a 型になっている。

e は x = a 型なので、この等式に入れるのは難しいのだが、 join が交換律と推移律を使って e : x = a から a = a 型の式を作り出している。

上で書いた、join じゃなくて id でもいいのではないか、という考えで id を使うとここで破綻する。

ともかく、この場合分けによりゴールは join x x (erefl x) (erefl x) = erefl x と変形される。変形前は proj が入っていて、proj は (@eqP T x z というところに) T という実体が与えられていない変数を使っていたため、簡約を十分に進めることができなかった。しかし、変形後は proj が消えており、簡約を充分に進めることができる。簡約を進めると、このゴールは erefl x = erefl x となり、左辺と右辺が一致するので証明できるのである。

さて、証明は読めたのだが、eq_rect は出てこないことがわかった。なんと eq_irrelevance は eq_rect を使わずに証明可能なのだな。

もちろん、eq_rect を使わないからといっても、インデックスに decidable equality が必要なのはかわらない。 proj の中で eqP を使っているので、T はどうしても eqType でなければならない。 proj は証明を全体で (最後に除去するまで) 出てくるので、どこもかしこも decidable equality に依存しているともいえるが、とくに最初の injective (proj y) -> forall e1 e2 : x = y, e1 = e2 の証明で eqP を場合分けして ReflectT と ReflectF の場合に分割しているのは x = y であるか x <> y であるかのどちらかであるかが確認できるという decidable equality を直接使っているといえると思う。

不幸にしてインデックス付き帰納型を使わなければならず、ライブラリが適切な場合分けの補題を用意してくれていないという場合、自分で補題を用意する必要があるかもしれない。

Vector についてはライブラリが提供してくれているので問題ないのだが、自分でやるならどうするか、ということで、Vector.case0 と Vector.caseS' を例として、これらがなにをやっているのか説明してみよう。

これらの型は以下のとおりである。

Vector.case0 :
  forall {A : Type} (P : Vector.t A 0 -> Type),
  P (Vector.nil A) -> forall v : Vector.t A 0, P v

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

ここで重要なのは、結論 P v の v の型が、Vector.t A 0 と Vector.t A n.+1 になっている点である。

最初に書いた Vector.t の場合分けがうまくいかないのは、forall (v : Vector.t A n), P v を証明するのに P (Vector.nil A) と forall (n' : nat) (v' : Vector.t A n'), P (Vector.cons A n' v') のふたつの証明で済ましたいというのが P と引数の型があわないので無理だった、というのはここでは、P の型がそれぞれ Vector.t A 0 -> Type と Vector.t A n.+1 -> Type になっていることで解決されている。 Vector.case0 の場合だと P : Vector.t A 0 -> Type なので、P v を P (Vector.nil A) に置き換えても型は合う。

case0 を自分で定義してみよう。標準ライブラリの実装を見ずに書いたら以下のようになった。

From mathcomp Require Import all_ssreflect.
Require Vector.

Definition my_case0 :
    forall {A : Type} (P : Vector.t A 0 -> Type),
    P (Vector.nil A) -> forall v : Vector.t A 0, P v.
  move=> A P H v.
  move: H.
  (* P (Vector.nil A) -> P v *)
  refine (match v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end).
    (* P (Vector.nil A) -> P (Vector.nil A) *)
    by apply.
  (* IDProp *)
  by exact idProp.
Defined.

ゴールを P (Vector.nil A) -> P v という形にした後に、 refine で match v with ... end という証明項を作っている。 match の各分岐にはとくになにも書いていなくて、後で埋めることになる。

そうすると、nil と cons に対応したふたつのゴールができる。それぞれ P (Vector.nil A) -> P (Vector.nil A) と IDProp となる。

nil の場合の P (Vector.nil A) -> P (Vector.nil A) は、自明に証明できる。 P (Vector.nil A) の証明を受け取って P (Vector.nil A) の証明を返す関数を書けばいいので、単に引数を返す恒等関数が証明となる。

cons の場合には IDProp という謎の命題が出てくるが、検索すると idProp: IDProp というのがあるので、idProp で証明できる。 v : Vector.t A 0 であることから、v が cons で作られることはありえないので、簡単に証明できる命題として IDProp が出てくるのだろう。

ちなみに、IDProp の中身は forall A : Prop, A -> A というもので、 idProp は fun (A : Prop) (x : A) => x である。簡単に証明できるというなら True とかでもいいと思うのだが、たぶん、Coq の内部から、True みたいなライブラリの定義を参照するのを嫌ったのではないかという気がする。（とはいえ、IDProp と idProp も Coq.Init.Datatypes で定義される定数なので、結局ライブラリ定義を参照しているのだが。昔の Coq だと定数になっていなかったりしないだろうか? 調べてないけど）

さて、この定義は簡単に書けたが、じつは Coq がたくさん助けてくれているのである。定義を表示すると以下のようになる。

Print my_case0. (* my_case0 =
fun (A : Type) (P : Vector.t A 0 -> Type) (H : P (Vector.nil A))
  (v : Vector.t A 0) =>
match
  v as v0 in (Vector.t _ n)
  return
    (match n as x return (Vector.t A x -> Type) with
     | 0 => fun v1 : Vector.t A 0 => P (Vector.nil A) -> P v1
     | n0.+1 => fun=> IDProp
     end v0)
with
| @Vector.nil _ => id
| @Vector.cons _ _ _ _ => idProp
end H
     : forall (A : Type) (P : Vector.t A 0 -> Type),
       P (Vector.nil A) -> forall v : Vector.t A 0, P v
*)

自分では書かなかったが match に as-in-return 節が付加されていて、そのなかでさらに match しているという複雑なことになっている。

return節は、match 式自体の型を指定するもので、ここでは、n が 0 の場合とそうでない場合 (n0.+1 の場合) で場合分けしている。それぞれの場合は nil と cons の場合に対応しているのだが、 cons の場合は (今回は n が 0 なので) ありえなくて、その場合はすぐに証明できる IDProp という命題としている。 nil の場合は、P (Vector.nil A) -> P v1 という命題にしている。 v1 というのはさらに match が関数を返してそれを即座に呼び出しているといった複雑なことになっているが、最終的には、match の (nil の) 分岐の中では Vector.nil A になり、外では v になる、というように指示されている。

なお、match が関数を返して、その関数を即座に呼び出すのは convoy pattern と呼ばれているテクニックで、型を変えるためもものである。ここでは、v0 の型が Vector.t A n 型であって P には渡せないのを、Vector.t A 0 型の v1 で受け取って、P に渡せるようにしている。

では、caseS' も自前で証明してみよう。こっちは難航した。

From mathcomp Require Import all_ssreflect.

Definition my_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.
  move=> A n v P.
  refine (match v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end).
  (* IDProp と
     (forall (h : A) (t0 : Vector.t A n), P (Vector.cons A h n t0)) -> P v に
     なるが、話が進んでいない。どうやら、自分で as-in-return 節を書く必要があるようだ *)
  Undo.
  refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => True
      | n1.+1 =>
          ((forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end); [by constructor|].
  (* nil の場合は True ということにして、即座に by constructor で証明してしまう。
     残りのが (forall (h : A) (t0 : Vector.t A n), P (Vector.cons A h n t0)) -> P v
     のまま変わらないことを確認 *)
  Undo.
  (* P v の部分は、match の中と外で変えたいので、as 節に書いた v0 に置き換える。 *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => True
      | n1.+1 =>
          ((forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end); [by constructor|].
  (* The term "v0" has type "Vector.t A n0" while it is expected to have type
 "Vector.t A n.+1". というエラーになってしまう。*)
  (* P の型は Vector.t A n.+1 -> Type なので、n.+1 を n0 に置き換えないといけないのだろうな、ということで P を convoy pattern で変えてみよう *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => forall P, True
      | n1.+1 => forall (P : Vector.t A n0 -> Type),
          ((forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* 今度は The term "Vector.cons A h n t" has type "Vector.t A n.+1"
while it is expected to have type "Vector.t A n0". というエラーになった。*)
  (* あぁ、n1.+1 の分岐にも n がふたつ使われているので match の内外で変わるやつにしないといけないか。
    n.+1 が n0 に対応していて、n0 が n1.+1 に対応しているので、n を n1 にすればいいだろう。
 *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => forall P, True
      | n1.+1 => forall (P : Vector.t A n0 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* The term "Vector.cons A h n1 t" has type "Vector.t A n1.+1"
while it is expected to have type "Vector.t A n0". になった *)
  (* P が Vector.t A n0 を受けとるのではダメで、n1.+1 にしないといけなさそう *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => forall P, True
      | n1.+1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v0)
      end
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* The term "v0" has type "Vector.t A n0" while it is expected to have type
 "Vector.t A n1.+1". というエラーになった *)
  (* v0 の型を Vector.t A n0 から Vector.t A n1.+1 に変えるために convoy pattern を使う *)
  Fail refine (
    match v as v0 in Vector.t _ n0 return
      match n0 with
      | 0 => fun v1 => forall P, True
      | n1.+1 => fun v1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1)
      end v0
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* The term
       "forall P : Vector.t A n1.+1 -> Type,
        (forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1"
     has type "Type" while it is expected to have type "Prop"
     (universe inconsistency: Cannot enforce max(Set, Top.25711, Top.25872+1) <=
     Prop). というエラーになった *)
  (* えーと、なんだろ？　match n0 の return 節が変に補完されてるのか?
     自分で書いてみよう *)
  refine (
    match v as v0 in Vector.t _ n0 return
      match n0 as x return Vector.t A x -> Type with
      | 0 => fun v1 => forall P, True
      | n1.+1 => fun v1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1)
      end v0
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* やった。成功した。でも、nil の場合が
     ?Goal@{n0:=0; v0:=Vector.nil A; v1:=Vector.nil A} -> True
     という謎の前提がくっついてるな。P の型を書かなかったからか? *)
  Undo.
  refine (
    match v as v0 in Vector.t _ n0 return
      match n0 as x return Vector.t A x -> Type with
      | 0 => fun v1 => forall (P : Vector.t A 0 -> Type), True
      | n1.+1 => fun v1 => forall (P : Vector.t A n1.+1 -> Type),
          ((forall (h : A) (t : Vector.t A n1), P (Vector.cons A h n1 t)) -> P v1)
      end v0
    with
    | Vector.nil => _
    | Vector.cons _ _ _ => _
    end P).
  (* 謎の ?Goal は消えたのでこれでよし *)
    (* (Vector.t A 0 -> Type) -> True *)
    by [].
  (* forall P0 : Vector.t A n0.+1 -> Type,
     (forall (h : A) (t0 : Vector.t A n0), P0 (Vector.cons A h n0 t0)) ->
     P0 (Vector.cons A a n0 t) *)
  (* 結局、P0 (Vector.cons A h n0 t0)) -> P0 (Vector.cons A a n0 t) なので自明に証明できる *)
  by [].
Qed.

Print my_caseS'. (* my_caseS' =
fun (A : Type) (n : nat) (v : Vector.t A n.+1) =>
[eta match
       v as v0 in (Vector.t _ n0)
       return
         (match n0 as x return (Vector.t A x -> Type) with
          | 0 => fun=> (Vector.t A 0 -> Type) -> True
          | n1.+1 =>
              fun v1 : Vector.t A n1.+1 =>
              forall P0 : Vector.t A n1.+1 -> Type,
              (forall (h : A) (t : Vector.t A n1), P0 (Vector.cons A h n1 t)) ->
              P0 v1
          end v0)
     with
     | @Vector.nil _ => fun=> I
     | @Vector.cons _ h n0 t =>
         fun (P0 : Vector.t A n0.+1 -> Type)
           (X : forall (h0 : A) (t0 : Vector.t A n0),
                P0 (Vector.cons A h0 n0 t0)) => X h t
     end]
     : 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
*)

難航したが、証明できた。基本的には (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v の v を Vector.cons A h n t に置き換えるという方針のもとに、型エラーにひとつずつ対処していくという話である。

なお、IDProp でなくても簡単に証明できるものであればいいはず、ということで True を使ってみた。

しかし、見直してみると、P の型を convoy pattern で変えているが、最初に Coq に補助させようとしたときには P がゴールに入っていなかったのがうまくいかなかった理由かもしれない。ゴールに P を残したまま refine するとどうだろうか。

Definition my_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.
  move=> A n v.
  (* forall P : Vector.t A n.+1 -> Type,
     (forall (h : A) (t : Vector.t A n), P (Vector.cons A h n t)) -> P v *)
  refine (match v with
          | Vector.nil => _
          | Vector.cons _ _ _ => _
          end).
    by exact idProp.
  (* forall P : Vector.t A n0.+1 -> Type,
      (forall (h : A) (t0 : Vector.t A n0), P (Vector.cons A h n0 t0)) ->
      P (Vector.cons A a n0 t) *)
  move=> P.
  by apply.
Qed.

おぉ、うまくいった。

天泣記

2024-07-23 (Tue)

2024-06-08 (Sat)

2024-05-07 (Tue)

2024-04-09 (Tue)

2024-03-22 (Fri)