自前で 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 を直接使っているといえると思う。
検索していると、また別の 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." という記載があって、 この挙動のことを示しているのだろうな、と思った。
[latest]