天泣記

帰納型の場合分け tactic の違いをまとめると以下のようになる。

case は conclusion 内の対象を置換する。context 内の対象、および context/conclusion 内のインデックスについて置換するかどうかは、at の有無、eqn: の有無、インデックス付きかどうかに依存して変化する。
case_eq は、対象とコンストラクタの等式を生成する。インデックスがある場合はコンストラクタ同士の意味のない等式が生成される。
destruct (at なし) は context と conclusion 内の対象をコンストラクタに置換する。context と conclusion 内のインデックスも置換する。
destruct (at あり) は conclusion 内の対象をコンストラクタに置換する。context と conclusion 内のインデックスも置換する。
simple inversion は各インデックスについて等式を生成する。
dependent simple inversion は各インデックスについて等式を生成する。conclusion 内の対象をコンストラクタに置換する。conclusion 内のインデックスも置換する。
case (SSReflect) は conclusion 内の対象をコンストラクタに置換する。conclusion 内のインデックスも置換する。対象もインデックスも、どこを置換するか指定できる。

SSReflect でも、inversion に相当する match 式を生成することは可能である。インデックス毎に等式を生成してから場合分けして左辺だけを置換すればいい。この方法を拡張して、場合分けの対象の等式も生成することができ、場合分けで判明するすべての情報を得ることができる。 (これを自動的にやってくれる tactic があるといいんだけど。)

SSReflect に inversion 相当の tactic がない理由を説明しているメールを紹介した。そこで述べられている方法も、inversion のかわりに使える。

case (SSReflect) と case (vanilla Coq) では、任意の match 式を構築できる。 (ただし case (vanilla Coq) で置換対象を制御するのはかなり面倒くさい) なので上記の、場合分けの対象の等式を生成するのは、vanilla Coq の case でも可能なはずである。

vanilla Coq では (場合分けの tactic で) どんな match 式でも生成できるだろうか。どの場合分け tactic もインデックスの置換の場所を指定することはできないので、簡単ではなさそうである。

SSReflect では可能だった TestNat01 について試してみよう。

Inductive TestNat01 : nat -> nat -> Type := C : TestNat01 0 1.

Lemma L a (H : TestNat01 a a) : False.
Proof.

SSReflect では move: (erefl a) (erefl a) として a = a という等式をふたつ作ったが、vanilla Coq ではこれを generalize で行える。

generalize (eq_refl a), (eq_refl a).
(*
1 goal
a : nat
H : TestNat01 a a
______________________________________(1/1)
a = a -> a = a -> False
*)

問題はここからである。 vanilla Coq の場合分け tactic はインデックスの置換を無差別に行うので、これをどうにかして制御する必要がある。ひとつの方法は、case は conclusion しか置換しないので、置換したくないものは set tactic で context に移してしまうという方法が考えられる。ただ、ふたつのインデックスが同じく a なので、これらを区別できるようにしなければならない。ということで、各インデックスを別の変数に置き換える。また、インデックスといっしょに置き換えたいものもその変数に置き換えておくことにする。 (なお、destruct は context 内も置換するため、この方法に destruct は使えない。)

まず H を conclusion に動かす。

revert H.
(*
1 goal
a : nat
______________________________________(1/1)
TestNat01 a a -> a = a -> a = a -> False
*)

そして、1,3番目の a を a1 という新しい変数に置換し、 2,5番目の a を a2 という新しい変数に置換する。

TestNat01 a a -> a = a -> a = a -> False
          1 2    3   4    5   6

set (a1 := a) at 1 3.
set (a2 := a) at 1 3.
(*
1 goal
a : nat
a1, a2 := a : nat
______________________________________(1/1)
TestNat01 a1 a2 -> a1 = a -> a2 = a -> False
*)

なお、a2 で at 2 5 ではなく at 1 3 になっているのは、a1 の置換により、以下のように番号がずれるためである。

TestNat01 a1 a -> a1 = a -> a = a -> False
             1         2    3   4

ということで、set (a1 := a) at 1 3 と set (a2 := a) at 1 3 としている

ここでの新しい変数の導入には set tactic を使っている。 set は証明項として let-in を構築する。 let-in で束縛された変数は context においては a1, a2 := a : nat の ":= a" のように定義の形になり、型検査において定義を展開できるため、変数の導入前と同じく型検査できる。つまり、型は壊れない。

case で場合分けをするには対象が context になければならないので H を context に動かす。

intros H.
(*
1 goal
a : nat
a1, a2 := a : nat
H : TestNat01 a1 a2
______________________________________(1/1)
a1 = a -> a2 = a -> False
*)

で、case H すると、期待通りに 0 = a, 1 = a になっている。

case H.
(*
1 goal
a : nat
a1, a2 := a : nat
H : TestNat01 a1 a2
______________________________________(1/1)
0 = a -> 1 = a -> False
*)

証明項は以下のようになっていて、期待通りに match H0 in (TestNat01 n n0) return (n = a -> n0 = a -> False) with となっている。また、a1, a2 が let-in で束縛されていることもわかる。

Show Proof.
(*
(fun (a : nat) (H : TestNat01 a a) =>
 (let a1 := a in
  let a2 := a in
  fun H0 : TestNat01 a1 a2 =>
  match H0 in (TestNat01 n n0) return (n = a -> n0 = a -> False) with
  | C => ?Goal@{H:=H0}
  end) H eq_refl eq_refl)
*)

あとは、0 = a, 1 = a を context に動かして、a を subst で除去すると 1 = 0 が残るので discriminate で証明が完了する。

intros H1 H2.
subst a.
discriminate.
Qed.

というわけで、set tactic で各インデックスに別の変数をわりあてれば、 vanilla Coq の case でも所望の match 式を生成できた。

この置換したいところだけ別の変数に変えておくというやりかたを使えば、インデックスの置換を完全に制御できて、任意の match 式を生成できると思う。 (必要ならインデックスだけでなく、場合分けの対象の置換も同様に制御できると思う)

もちろん、この場合には inversion や refine をつかえばもっと簡単に所望の match 式を生成できる。

simple inversion を使えば以下の等式を生成できるし、inversion ならいきなり証明が終わる。

H0 : 0 = a
H1 : 1 = a

refine なら、以下のように直接 match 式を記述することもできる。

refine (match H in TestNat01 x y return x = a -> y = a -> False with C => _ end).
(*
1 goal
a : nat
H : TestNat01 a a
______________________________________(1/1)
0 = a -> 1 = a -> False
*)

なのでわざわざ case でやる必要はないのだが、case でも可能である、ということがわかった。 inversion では作ってくれない等式を生成するときなどには使えるかもしれない。まぁ、refine で match 式を直接書いた方が簡単な気はするけれど。

SSReflect の case では、インデックスについてもどの出現を置換するかを指定できるので、任意の match 式を生成できそうである。

ただ、ひとつ気になるところとして、場合分け対象のインデックスが複数あり、それらが同じ項だった場合にちゃんと制御できるのか、という点がある。結論からいうと、これは可能である。

From mathcomp Require Import all_ssreflect.

以下の帰納型 TestNat01 を考える。これにはインデックスがふたつあり、コンストラクタ C でのみ値が生成され、そのときのインデックスは 0 と 1 である。

Inductive TestNat01 : nat -> nat -> Type := C : TestNat01 0 1.

そして、(H : TestNat01 a a) を前提とした証明を考えよう。ふたつのインデックスはどちらも a となっているが、1番目のインデックスは 0 でなければならず、2番目のインデックスは 1 でなければならないので、TestNat01 a a には要素はなく、ありえない前提が与えられていることになる。この矛盾を (inversion を使わずに) 取り出してみよう。

Lemma L a (H : TestNat01 a a) : False.
Proof.

ふたつのインデックスそれぞれに等式が欲しいので、a = a という等式をふたつ作る。

move: (erefl a) (erefl a).
(*
1 goal
a : nat
H : TestNat01 a a
______________________________________(1/1)
a = a -> a = a -> False
*)

そして、H で場合分けするのだが、その際に a = a -> a = a -> の中の、1番目の a を 1番目のインデックスで置換し、3番目の a を 2番目のインデックスで置換する。そうすると、0 = a と 1 = a という等式が得られる。

case: {1}_ {3}_ / H.
(*
1 goal
a : nat
______________________________________(1/1)
0 = a -> 1 = a -> False
*)

以下のように、証明項では return 節に (beta reduction すると) n = a -> n0 = a -> False という項が与えられていて、期待通りに置換する指定にできている。

Show Proof.
(*
(fun (a : nat) (H : TestNat01 a a) =>
 (fun _evar_0_ : (fun n n0 : nat => fun=> n = a -> n0 = a -> False) 0 1 C =>
  match H as t in (TestNat01 n n0) return ((fun n1 n2 : nat => fun=> n1 = a -> n2 = a -> False) n n0 t) with
  | C => _evar_0_
  end) ?Goal (erefl a) (erefl a))
*)

top assumption の 0 = a を使って 1 = a の a を 0 に書き換えれば 1 = 0 となって矛盾となるので証明は成功する。

by move=> <-.
Qed.

というわけで、たぶん、SSReflect の case はどんな match 式でも生成できると思う。

項 t の型がインデックス付き帰納型だったとしよう。

inversion t ではインデックスの等式が得られるが、t がどんなコンストラクタで作られたかの情報はわからない。

dependent inversion t では、インデックスの等式が得られ、さらに t がコンストラクタで作られる項に置換される。

なので、dependent inversion は場合分けによって得られるすべての情報が得られて素晴らしい、と言いたいところだが、残念ながら t の置換はうまくいかないことが多い。というのは、インデックス付き帰納型の場合、t とコンストラクタで作られる項は型が違う (convertible でない) ため、置換でしばしば型が壊れるからである。

そこで、場合分けの対象も等式で表現することを考える。対象がインデックス付き帰納型の場合、この等式は型を合わせるために existT の等式としなければならない。

たとえば、le の定義は次であった。

Print le.
(*
Inductive le (n : nat) : nat -> Prop :=
  le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m.
*)

ここで、H : le a b を inversion したとき、 H が le_n で作られた場合は a = b という等式が得られ、 le_S で作られた場合は S m = b という等式が得られる。

さらに、 H が le_n で作られた場合は le_n a = H という等式、 le_S で作られた場合は le_S a m = H という等式が欲しい。

しかしこれは型があわないので、 existT (le a) a (le_n a) = existT (le a) b H と existT (le a) (S m) (le_S a m H') = existT (le a) b H という等式とする。

そして、conclusion に含まれる H は置換したくない。どうせそのまま置換すると型が壊れるので、上の等式で後から書き換えればいい。

これを行うには、以下のようにすればよい。

From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (H : le a b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H
*)
move: (erefl (existT (le a) b H)).
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
existT (le a) b H = existT (le a) b H -> H = H
*)
case: {1}_ / {1}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
existT (le a) a (le_n a) = existT (le a) b H -> H = H
______________________________________(2/2)
forall (m : nat) (l : (a <= m)%coq_nat), existT (le a) m.+1 (le_S a m l) = existT (le a) b H -> H = H
*)
Abort.

ここでは、move: (erefl (existT (le a) b H)) として existT (le a) b H = existT (le a) b H という等式を生成し、その左辺の b, H を case: {1}_ / {1}H で置換している。

その結果、ふたつのサブゴール (le_n の場合と le_S の場合) ができていて、それぞれで existT (le a) a (le_n a) = existT (le a) b H と existT (le a) m.+1 (le_S a m l) = existT (le a) b H という等式が得られている。

ここではインデックスについての等式 a = b と S m = b は生成していない。これは existT の等式から EqdepFacts.eq_sig_fst で得られるからである。

生成したければ以下のようにすればよい。ただし、出現の番号については conclusion を (notation を抑制し、implicit arguments を表示し) 確認して調べる必要がある。

move: (erefl b) (erefl (existT (le a) b H)).
case: {1 3}_ / {1}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
a = b -> existT (le a) a (le_n a) = existT (le a) b H -> H = H
______________________________________(2/2)
forall (m : nat) (l : (a <= m)%coq_nat), m.+1 = b -> existT (le a) m.+1 (le_S a m l) = existT (le a) b H -> H = H
*)

これを自動的にやってくれる tactic があればいいんだけど、どうかなぁ。 simple inversion の拡張とかどうかな。

case (SSReflect) は (次に述べるようにどんな match 式でも生成できるので) プリミティブとしてはよいのだが、インデックス付き帰納型の場合分けを常に失敗せずに進められる tactic があればそれはそれでよいことだと思う。 (既存の tactic は失敗したり、必要な情報を得られないこともあるので、常に成功する、場合分けで得られる情報がすべて入手できる tactic があってもいいではないか。)

SSReflect では、「move: (erefl b) で b = b という等式を生成し、case: {1}b / {-}H でその等式の左辺の b だけを置換する」ということで inversion と同じ等式を生成できたが、上のメールをみると、違う機能が示されているので、もしかしたら、そっちを使った方が簡単かもしれない。というわけで試してみた。

試してみると、対象が H : le a b の場合、simple inversion H に相当する動作は case E: {-}_ / {-}H => [|m H'] で可能なようだ。

From mathcomp Require Import all_ssreflect.

Lemma L (a b : nat) (H : le a b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) => ?Goal)
*)
case E: {-}_ / {-}H => [|m H'].
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
E : b = a
______________________________________(1/2)
H = H
______________________________________(2/2)
H = H
*)
Show 2.
(*
goal 2 is:

  a, b : nat
  H : (a <= b)%coq_nat
  m : nat
  H' : (a <= m)%coq_nat
  E : b = m.+1
  ============================
  H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) =>
 (fun (_evar_0_ : (fun n : nat => fun=> protect_term (b = n) -> H = H) a (le_n a))
    (_evar_0_0 : forall (m : nat) (l : (a <= m)%coq_nat),
                 (fun n : nat => fun=> protect_term (b = n) -> H = H) m.+1 (le_S a m l)) =>
  match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> protect_term (b = n) -> H = H) n0 l) with
  | @le_n _ => _evar_0_
  | @le_S _ m l => _evar_0_0 m l
  end) ((fun E : b = a => ?Goal) : protect_term (b = a) -> H = H)
   (fun (m : nat) (H' : (a <= m)%coq_nat) => (fun E : b = m.+1 => ?Goal0) : protect_term (b = m.+1) -> H = H)
   (erefl b))
*)
Abort.

ふたつのサブゴールにそれぞれ E : b = a と E : b = m.+1 が得られているので、simple inversion と同じ等式が前提として得られている。(左右は逆だけど)

証明項の match 式は match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> protect_term (b = n) -> H = H) n0 l) with となっている。 protect_term というのが入っているが、これは id と同じようなので、期待した match 式が生成されている。

ただ、等式を複数作る場合については、うまくいかなかった。以下のように試したのだが、move Eb: b => ib として等式を作ると conclusion 内の b が ib に変わる。そして H : TestNat2 a ib について場合分けを行うと、ib が置換されて b = 2 が得られるのだが、 H の型は TestNat2 a ib なので、b = 2 が得られても、H との関係が消えている。

From mathcomp Require Import all_ssreflect.

Inductive TestNat2 : nat -> nat -> Type := C2 : TestNat2 1 2.

Lemma L (a b : nat) (H : TestNat2 a b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : TestNat2 a b
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : TestNat2 a b) => ?Goal)
*)
move: H.
move Eb: b => ib.
move=> H.
case Ea: {-}_ {1}_ / {-}H Eb => Eb.
(*
1 goal
a, b, ib : nat
H : TestNat2 a ib
Ea : a = 1
Eb : b = 2
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun a b : nat =>
 [eta (fun (ib : nat) (Eb : b = ib) (H0 : TestNat2 a ib) =>
       (fun _evar_0_ : (fun n n0 : nat => fun=> protect_term (a = n) -> b = n0 -> H0 = H0) 1 2 C2 =>
        match
          H0 as t in (TestNat2 n n0)
          return ((fun n1 n2 : nat => fun=> protect_term (a = n1) -> b = n2 -> H0 = H0) n n0 t)
        with
        | C2 => _evar_0_
        end) ((fun (Ea : a = 1) (Eb0 : b = 2) => ?Goal@{H:=H0; Eb:=Eb0}) : protect_term (a = 1) -> b = 2 -> H0 = H0)
         (erefl a) Eb) b (erefl b)])
*)
Abort.

H と b の関係に興味が無いのであれば、これでいいのかもしれない。

H と b の関係が必要ならば b = ib という等式をコピーして残しておけば可能である。これは以下のように move: (Eb) => Eb' とすればできる。

move: H.
move Eb: b => ib.
move: (Eb) => Eb'.
move=> H.
case Ea: {-}_ {1}_ / {-}H Eb => Eb.
(*
1 goal
a, b, ib : nat
Eb' : b = ib
H : TestNat2 a ib
Ea : a = 1
Eb : b = 2
______________________________________(1/1)
H = H
*)
subst ib.
(*
1 goal
a, b : nat
H : TestNat2 a b
Ea : a = 1
Eb : b = 2
______________________________________(1/1)
H = H
*)

しかし、こんな迂遠なことをするくらいなら、move: (erefl ...) で等式を作って場合分けしたほうが簡単だと思う。そうすれば 2行で済む。

あと、結局 case Ea: {-}_ {1}_ / {-}H Eb => Eb のところでは出現の番号をひとつ書く必要があって、出現番号が不要になってないし。

でも考えてみると、{1}_ と書かないといけないのは、H = H が @eq (TestNat2 a ib) H H であるために ib が conclusion に出現しているからで、場合分けの対象が conclusion に含まれていなければ、出現の番号を書かなくてもいい気はする。

件のメールは inversion 相当のことをする方法という話だったら、インデックスについての等式さえ得られればいい、という想定だったのかもしれない。

上記のように、inversion 相当の動作を SSReflect で行うことは可能である。また、SSReflect を使っていても、vanilla Coq の tactic が技術的に禁止されているわけではないので inversion 自体を使うことはできる。

しかし、SSReflect の流儀 (自動的に変数名をつけないとか) にしたがった動作をする tactic がない、という点について戸惑うユーザは少なくないと思う。この理由について、以下のメールで説明がされている。

2014-10-16 Georges Gonthier

inversion と同等の機能実現する部品を用意している、という主張のようだ。

ではどうするか、というと、以下のように可能、と書いてある

インデックスのための新しい変数と等式の導入: ":" tactical に等式を導入する機能があって、それを利用可能。 case と同時にできるので、場合分けといっしょにできるし、等式がもっと必要なら move で導入できる。
対象の場合分け (コンストラクタに引数があれば変数として導入される): case もしくは elim で行う。(elim を使うのは帰納法を使う場合だろう)
等式の両辺が異なるコンストラクタになっているゴールの解決 (discriminate): intro pattern の // を利用可能。
等式の両辺が同じコンストラクタになっている等式の分解 (injection): intro pattern の [eqs] で分解できる。
等式を使ってコンストラクタの引数を可能な範囲で置換して場合分けで導入された変数を消す: intro pattern の ->/_/{x} が使える。(と書いてあるが、ここはよくわからない)

このようにすることで手間は増えるけれど、変数の名前や、どんな等式を作るか、また不要な等式を作らない、などといった細い制御が可能になる、というのが利点。

そして帰納型の定義のところで、そもそもインデックス付き帰納型でなく、各コンストラクタに等式の証明をつけるのを容易にする記法 (of/&) も提供している。 (この部分は、そもそもインデックス付き帰納型を使わないほうがいい、という話だろう)

というように書いてある。

SSReflect には inversion 相当の tactic がないのだが、要するにインデックスに対応する等式を作って、場合分けで等式の左辺だけ置換すればいい、と理解してしまえば、以下のようにすればよいことがわかる

From mathcomp Require Import all_ssreflect.

Lemma L (a b : nat) (H : le a b) : H = H /\ b = b.
Proof.
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) => ?Goal)
*)

まず、simple inversion でどういうサブゴールが生成されるかを確認する。もともとの conclusion の H = H /\ b = b はそのままなので、simple inversion は等式を加えるだけで、もともとの conclusion 内の置換は行わないことがわかる。

simple inversion H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
H0 : a = b
______________________________________(1/2)
H = H /\ b = b
______________________________________(2/2)
(a <= m)%coq_nat -> H = H /\ b = b
*)
Show 2.
(*
goal 2 is:

  a, b : nat
  H : (a <= b)%coq_nat
  m : nat
  H1 : m.+1 = b
  ============================
  (a <= m)%coq_nat -> H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) =>
 let H0 : (fun n : nat => n = b -> H = H /\ b = b) b :=
   match H as _ in (_ <= n)%coq_nat return (n = b -> H = H /\ b = b) with
   | @le_n _ => fun H0 : a = b => ?Goal
   | @le_S _ m x => (fun (m0 : nat) (H0 : (a <= m0)%coq_nat) (H1 : m0.+1 = b) => ?Goal0@{m:=m0} H0) m x
   end in
 H0 (erefl b))
*)
Undo.

最初のサブゴール (le_n の場合) では H0 : a = b、後のサブゴール (le_S の場合) では H1 : m.+1 = b という前提が得られている。

Undo で simple inversion の前に戻ってから、 move: (erefl b) で b = b という等式を生成し、 case: {1}b / {-}H でその等式の左辺の b だけを置換する。

move: (erefl b).
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
b = b -> H = H /\ b = b
*)
case: {1}b / {-}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
a = b -> H = H /\ b = b
______________________________________(2/2)
forall m : nat, (a <= m)%coq_nat -> m.+1 = b -> H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (H : (a <= b)%coq_nat) =>
 (fun (_evar_0_ : (fun n : nat => fun=> n = b -> H = H /\ b = b) a (le_n a))
    (_evar_0_0 : forall (m : nat) (l : (a <= m)%coq_nat),
                 (fun n : nat => fun=> n = b -> H = H /\ b = b) m.+1 (le_S a m l)) =>
  match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> n = b -> H = H /\ b = b) n0 l) with
  | @le_n _ => _evar_0_
  | @le_S _ m l => _evar_0_0 m l
  end) ?a ?a0 (erefl b))
*)
Abort.

simple inversion とこちらを比較すると、生成された等式が context に出てくるか、conclusion の assumption に出てくるか、という違いはあるが、同じ前提が得られている。

また、証明項の match 式をみると、以下のように始まっている。

match H as _ in (_ <= n)%coq_nat return (n = b -> H = H /\ b = b) with
match H as l in (_ <= n0)%coq_nat return ((fun n : nat => fun=> n = b -> H = H /\ b = b) n0 l) with

SSReflect のほうはちょっと複雑だが、beta reduction すると return n0 = b -> H = H /\ b = b となり、 (束縛変数の名前が n と n0 と違うのを無視すれば) どちらも同じ形となっている。つまり、同じ場合分けをしているのである。

インデックスが複数あればその数だけ等式をつくり、インデックスの中に依存があれば existT の等式にする必要があるが、 SSReflect で inversion と同様の場合分けを行うのはこうやって可能である。

ただ、出現の番号を記述する必要があるのは面倒くさいし、いくらか間違いやすいとは思う。

あと、inversion は等式を生成した後に等式を整理し、矛盾したサブゴールを解決してくれるが、上記の方法は等式を生成するだけの simple inversion 相当の動作なので、そのへんは手動で行う必要がある。

インデックス付き帰納型を case (SSReflect) で場合分けしてみよう。インデックス付き帰納型として、ここでは vanilla Coq の le (less than or equal) を使う。

From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (E : b = b) (H : le a b) : H = H /\ a = b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H /\ a = b
*)
Show Proof.
(* (fun (a b : nat) (E : b = b) (H : (a <= b)%coq_nat) => ?Goal) *)
case: H.
(*
2 goals
a, b : nat
E : b = b
______________________________________(1/2)
le_n a = le_n a /\ a = a
______________________________________(2/2)
forall (m : nat) (l : (a <= m)%coq_nat), le_S a m l = le_S a m l /\ a = m.+1
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : (a <= b)%coq_nat) =>
 (fun (_evar_0_ : (fun (n : nat) (l : (a <= n)%coq_nat) => l = l /\ a = n) a (le_n a))
    (_evar_0_0 : forall (m : nat) (l : (a <= m)%coq_nat),
                 (fun (n : nat) (l0 : (a <= n)%coq_nat) => l0 = l0 /\ a = n) m.+1 (le_S a m l)) =>
  match H as l in (_ <= n0)%coq_nat return ((fun (n : nat) (l0 : (a <= n)%coq_nat) => l0 = l0 /\ a = n) n0 l) with
  | @le_n _ => _evar_0_
  | @le_S _ m l => _evar_0_0 m l
  end) ?Goal ?Goal0)
*)
Abort.

場合分けの結果、conclusion にあった H はコンストラクタの形 (le_n と le_S) に置換され、インデックス b は a と m.+1 に置換されている。

context の E : b = b の b は変わっておらず、context 内のインデックスは置換されないことがわかる。

証明項の match 式には (簡約すると) match H as l in (_ <= n0)%coq_nat return l = l /\ a = n0 with と記述されている。つまり H で場合分けを行い、H = H /\ a = b の H と b が置換される。

なお、notation を外すと、もとの conclusion は and (@eq (le a b) H H) (@eq nat a b) であり、 match には as l in (le _ n0) return and (@eq (le a n0) l l) (@eq nat a n0) と記述されている。

conclusion に、b と H の出現の番号を付記すると以下のようになる。 (eq の implicit argument の中に b が出現しているので、この番号を調べるには、notation を抑制し、implicit argument を表示する必要がある。)

and (@eq (le a b) H H) (@eq nat a b)
               1  1 2             2

eq では第1引数が第2,3引数の型でなければならないので、 1番目の b と、1,2番目の H は、同時に置換しないと型があわなくなる。しかし、2番目の b は、置換してもしなくても (型は nat のままなので) 型は壊れない。

1番目の b と 1,2番目の H だけを置換するには case: {1}b / {1 2}H とすればよい。そうすると、構築される match 式は as l in (le _ n0) return and (@eq (le a n0) l l) (@eq nat a b) となって、最後の b は置換されなくなる。

逆に、2番目の b だけを置換するには case: {2}b / {-}H とすればよい。そうすると、構築される match 式は as l in (le _ n0) return and (@eq (le a b) H H) (@eq nat a n0)) n0 l となって、最後の b だけが置換される。

どの出現も置換しないという occ_switch は {-} で指定可能なようだ。{} だと、(たぶん) clear_switch に解釈されて、ここでは受け付けられない。

あと、場合分けの対象の項がわかれば、その型からインデックスはわかるので、 case: {occurs_1}i1 ... {occurs_n}in / {occurs_t}term というのは case: {occurs_1}_ ... {occurs_n}_ / {occurs_t}term と書いても良い。

では、インデックスの項を明示的に記述できることに意味はないかというと、そうでもない。この項は置換するところを探すというところで使われるが、型からわかるインデックスと convertible であるが、項としては異なる、というものを置換するときに利用できる。以下の場合の b と 0 + b は convertible ではあるが、同じ項ではない。 H の型からインデックスは b とわかるが、あえて 0 + b を探させている。そのため、H = H つまり @eq (le a b) H H の中に出現している b は置換されていない。 (implicit argument の中にあるので見えていないが、もし置換されていたら、型があわなくてエラーになっているはずである)

From mathcomp Require Import all_ssreflect.
Lemma L (a b : nat) (H : le a b) : H = H /\ a = (0 + b).
Proof.
Show Proof.
(* (fun (a b : nat) (H : (a <= b)%coq_nat) => ?Goal) *)
(*
1 goal
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/1)
H = H /\ a = 0 + b
*)
case: (0 + b) / {-}H.
(*
2 goals
a, b : nat
H : (a <= b)%coq_nat
______________________________________(1/2)
H = H /\ a = a
______________________________________(2/2)
forall m : nat, (a <= m)%coq_nat -> H = H /\ a = m.+1
*)
Abort.

まず、以下の状況で case (SSReflect) により case: n とした場合、n is used in hypothesis H. というエラーになる。 case (vanilla Coq) では、エラーにならずに場合分けしていたので、それとは挙動が異なる。

From mathcomp Require Import all_ssreflect.

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
case: n.
(* n is used in hypothesis H. *)

これは case: n の ": n" の部分は discharge つまり case の前に context から conclusion に動かすという意味の指定であるが、 n を conclusion に単純に動かすと H : n = n の中で参照している n が使えなくなってしまうので、エラーになる。

ここで、ふたつの選択肢がある。

n に加えて H も discharge してから場合分けする (destruct のような動作)
n を discharge せずにそのまま場合分けする (case (vanilla Coq) のような動作)

最初の「n に加えて H も discharge してから場合分けする」とするには case: n H とすればよい。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
Show Proof.
(* (fun (n : nat) (H : n = n) => ?Goal) *)
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
case: n H.
(*
2 goals
______________________________________(1/2)
0 = 0 -> 0 = 0
______________________________________(2/2)
forall n : nat, n.+1 = n.+1 -> n.+1 = n.+1
*)
Show Proof.
(*
(fun n : nat =>
 [eta (fun (_evar_0_ : (fun n0 : nat => n0 = n0 -> n0 = n0) 0)
         (_evar_0_0 : forall n0 : nat, (fun n1 : nat => n1 = n1 -> n1 = n1) n0.+1) =>
       match n as n0 return ((fun n1 : nat => n1 = n1 -> n1 = n1) n0) with
       | 0 => _evar_0_
       | n0.+1 => _evar_0_0 n0
       end) ?Goal ?Goal0])
*)
(*
(fun (n : nat) (H : eq n n) =>
 (fun (_evar_0_ : (fun n0 : nat => forall _ : eq n0 n0, eq n0 n0) 0)
    (_evar_0_0 : forall n0 : nat, (fun n1 : nat => forall _ : eq n1 n1, eq n1 n1) (S n0)) =>
  match n as n0 return ((fun n1 : nat => forall _ : eq n1 n1, eq n1 n1) n0) with
  | 0 => _evar_0_
  | S n0 => _evar_0_0 n0
  end) ?Goal ?Goal0 H)
*)
Abort.

case: n H とした後のゴールをみると、 0 = 0 -> 0 = 0 と forall n : nat, n.+1 = n.+1 -> n.+1 = n.+1 になっており、 H が conclusion に移動してから、H の中の n も含めて場合分けされていることがわかる。

証明項には、[eta ...] というのがあって項がどうなっているのかわかりにくいので notation を抑制して表示し直した結果もつけてある。これを少し簡約して単純化すると、以下のようになっている。

(fun (n : nat) (H : eq n n) =>
  match n as n0 return n0 = n0 -> n0 = n0 with
  | 0 => ?Goal
  | S n0 => ?Goal0 n0
  end H)

これをみると、match ... end H というように関数適用の引数として H が出てきていて、discharge が行われているのがわかる。これは destruct が context も含めて場合分けするのと同じである。

なお、destruct は場合分けした後で context に戻すが、case (SSReflect) ではそれは行わない。それは、introduction tactical でユーザが記述できる。

また「n を discharge せずにそのまま場合分けする (case (vanilla Coq) のような動作)」を行うには、case に与える項を変数名でない項とすればよい。具体的にはかっこでくって case: (n) とすればよい。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
Show Proof.
(* (fun (n : nat) (H : n = n) => ?Goal) *)
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
case: (n).
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = 0
______________________________________(2/2)
forall n0 : nat, n0.+1 = n0.+1
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
 (fun (_evar_0_ : (fun n0 : nat => n0 = n0) 0) (_evar_0_0 : forall n0 : nat, (fun n1 : nat => n1 = n1) n0.+1) =>
  match n as n0 return ((fun n1 : nat => n1 = n1) n0) with
  | 0 => _evar_0_
  | n0.+1 => _evar_0_0 n0
  end) ?e ?e0)
*)
Abort.

discharge tactical を使った tactic: term というのは証明項として (_ term) を作るものである。 case: n と case: (n) はどちらも (_ n) という証明項をつくる。ただ、discarge のときに context の変数名を記述した場合は context からその変数を取り除く、という動作が追加して発生する。そのため、変数名を指定した場合は context から conclusion に移動したように見える。また、context 内にその変数が使われていると、エラーにならざるを得ない。

というわけで、case: (n) とすれば、context から n を消さずに場合分けだけを行える。これは、case (vanilla Coq) の動作に相当する。

SSReflect を使っていても vanilla Coq の case は利用可能である。

どう区別できるかというと、コロンがなく項がカンマ区切りでひとつ以上指定されているものが vanilla Coq で、項がなにも指定されていないかコロンの後に指定されているものが SSReflect である。

(* vanilla Coq *)
case term, ...

(* SSReflect *)
case
case: term...
case: term... / term...
case E: term... => [...]

最後の case E: term... => [...] は、等式を生成する指定である。
context に E という名前で、(場合分け前の項) = (場合分け後の項) という等式の証明が追加される。
場合分け後の項はコンストラクタの形となるが、コンストラクタに引数があるなら、その名前を => [...] の部分で指定する。

たとえば、n の型が nat であれば、
case E: n => [|m].
は nat の場合分けを行ってふたつのゴールを生成するが、それぞれのゴールの context には E: n = 0 と E: n = m.+1 という等式が追加される。
(=> [...] の部分を省略すると、代わりにユーザが使えない変数が導入される)

なお、conclusion の先頭の assumption を場合分けする場合は、等式を生成することはできないようだ。
まぁ、: term... の部分を消すと、case E => [...] になってしまうので、vanilla Coq の case に => をつけたものと区別できなくなるか。

SSReflect の case tactic は、以下の形式で利用できる。

case: {occurs_1}i1 ... {occurs_n}in / {occurs_t}term

この tactic は、帰納型の項 term を場合分けするが、その帰納型のインデックス i1, ..., in については、 occurs_1, ..., occurs_n で指定される箇所を置換し、 term については occurs_t で指定される箇所を置換する。

また、場合分けで置換の対象になるのは conclusion のみである。

なお、SSReflect の : は discharge のための tactical (tactic を修飾するもの) であり、 tactic: term は tactic が動作する前に (_ term) という形の証明項を作る (term : T とすると、conclusion は T -> old_conclusion になる) という動作である、という説明がされることがある。しかし、上記の {occurs_1}i1 ... {occurs_n}in / の部分を考えると、: と / のあいだの指示は、case が match 式を生成するのに必要な情報を提供していて、単純に case が動く前に discharge するというだけの tactical とはいえないと思う。まぁ、/ 以降についてはそうなのだが。

dependent inversion という tactic がある。 inversion の同じく、これの match 式をつくる部分だけ動かす dependent simple inversion という tactic がある。

inversion はインデックスの等式を context に追加するが、場合分けの対象がどのコンストラクタで生成されたのかという情報は残してくれない。

case は、場合分けの対象をコンストラクタの形に置換してくれるが、インデックスの等式は作ってくれない。

dependent inversion はこの両方をしてくれる tactic である。

Lemma L (a b : nat) (H : a <= b) : H = H.
Proof.
(*
1 goal
a, b : nat
H : a <= b
______________________________________(1/1)
H = H
*)
Show Proof.
(*
(fun (a b : nat) (H : a <= b) => ?Goal)
*)
dependent simple inversion H.
(*
2 goals
a, b : nat
H : a <= b
H0 : a = b
______________________________________(1/2)
le_n a = le_n a
______________________________________(2/2)
le_S a m l = le_S a m l
*)
Show 2.
(*
goal 2 is:

  a, b : nat
  H : a <= b
  m : nat
  l : a <= m
  H0 : S m = b
  ============================
  le_S a m l = le_S a m l
*)
Show Proof.
(*
(fun (a b : nat) (H : a <= b) =>
 let H0 : (fun (b0 : nat) (H0 : a <= b0) => b0 = b -> H0 = H0) b H :=
   match H as l in (_ <= n) return (n = b -> l = l) with
   | le_n _ => fun H0 : a = b => ?Goal
   | le_S _ m l => (fun (m0 : nat) (l0 : a <= m0) (H0 : S m0 = b) => ?Goal0@{m:=m0; l:=l0}) m l
   end in
 H0 eq_refl)
*)
Abort.

inversion と異なり、conclusion 内の H が le_n a や le_S a m l に置換されている。

また、H = H は @eq (le a b) H H であり、 le_n a = le_n a は @eq (le a a) (le_n a) (le_n a) である。 implicit argument で隠れているが、第1引数の le a b が le a a に変化している。つまり、conclusion 内の b が a に置換されている。まぁ、置換しないと le_n a = le_n a という等式の型があわないので、置換しているのだろう。

生成された match 式をみると、as l in (_ <= n) return (n = b -> l = l) となっていて、as 節と in 節が両方指定されている。 in (_ <= n) で束縛された n を使って、n = b という等式が記述されているのは inversion と同じである。そして、as l で束縛された l が、conclusion 内の H の代わりに記述されており、これは case と同じである。

というしかけで、インデックスの等式と、場合分け対象の置換が両方行われる。

マニュアルに inversion は Prop なインデックスの等式はデフォルトでは生成しないが、 Set Keep Proof Equalities と設定すると生成する、と書いてある。

これを確認してみよう。

まず、Prop な依存型 DP を定義する。 (上記の D と同じだが、sort が Prop になっている)

Inductive DP {T : Type} : T -> Prop := DPC : forall (x : T), DP x.

この DP をインデックスに使った帰納型を定義して simple inversion すると、おや、existT の等式が生成されている。生成しないんじゃなかったのか?

Inductive Test7 : forall (a : nat) (b : DP a), Type := C7 : Test7 0 (DPC 0).
Lemma L a b (t : Test7 a b) : False.
Proof.
simple inversion t.
(*
1 goal
a : nat
b : DP a
t : Test7 a b
H : 0 = a
H0 : existT (fun a : nat => DP a) 0 (DPC 0) = existT (fun a : nat => DP a) a b
______________________________________(1/1)
False
*)
Abort.

simple inversion じゃなくて inversion ならどうか、ということで試すと、こっちは生成されない。なるほど。証明項をみると、生成しないのではなく、内部的には生成しているようだ。それを表示しないようにしているのだろう。

Lemma L a b (t : Test7 a b) : False.
Proof.
inversion t.
(*
1 goal
a : nat
b : DP a
t : Test7 a b
H, H1 : 0 = a
______________________________________(1/1)
False
*)
Show Proof.
(*
(fun (a : nat) (b : DP a) (t : Test7 a b) =>
 let H :
   (fun (a0 : nat) (b0 : DP a0) =>
    a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False) a b :=
   match
     t in (Test7 a0 b0)
     return (a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False)
   with
   | C7 =>
       fun (H : 0 = a) (H0 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
       (fun (H1 : 0 = a) (H2 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
        let H3 : 0 = a := f_equal (fun e : {a0 : nat & DP a0} => let (x, _) := e in x) H2 in
        (fun H4 : 0 = a => let H5 : 0 = a := H4 in eq_ind 0 (fun _ : nat => False) ?Goal@{H:=H1; H1:=H4} a H5) H3) H
         H0
   end in
 H eq_refl eq_refl)
*)
Abort.

なんか、f_equal を使っているが、これはなにかというと、existT (fun a : nat => DP a) 0 (DPC 0) = existT (fun a : nat => DP a) a b の証明から 0 = a の証明を取り出しているようだな。その取り出した結果が H1 になっているのか。そして、eq_ind で a を 0 に書き換えているが、もともとの conclusion の False に a は含まれないので、そこで変化は起きない。

それはそれとして、Keep Proof Equalities してから inversion してみよう。こちらでは existT の等式が残っている。

Set Keep Proof Equalities.

Lemma L a b (t : Test7 a b) : False.
Proof.
inversion t.
(*
1 goal
a : nat
b : DP a
t : Test7 a b
H, H1 : 0 = a
H2 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b
______________________________________(1/1)
False
*)
Show Proof.
(*
(fun (a : nat) (b : DP a) (t : Test7 a b) =>
 let H :
   (fun (a0 : nat) (b0 : DP a0) =>
    a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False) a b :=
   match
     t in (Test7 a0 b0)
     return (a0 = a -> existT (fun a1 : nat => DP a1) a0 b0 = existT (fun a1 : nat => DP a1) a b -> False)
   with
   | C7 =>
       fun (H : 0 = a) (H0 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
       (fun (H1 : 0 = a) (H2 : existT (fun a0 : nat => DP a0) 0 (DPC 0) = existT (fun a0 : nat => DP a0) a b) =>
        let H3 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b :=
          f_equal
            (fun e : {a0 : nat & DP a0} => let (x, d) := e in existT (fun x0 : nat => (fun a0 : nat => DP a0) x0) x d)
            H2 in
        (let H4 : 0 = a := f_equal (fun e : {a0 : nat & DP a0} => let (x, _) := e in x) H2 in
         (fun (H5 : 0 = a) (H6 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b) =>
          let H7 : existT (fun x : nat => DP x) 0 (DPC 0) = existT (fun x : nat => DP x) a b := H6 in
          eq_ind (existT (fun x : nat => DP x) 0 (DPC 0)) (fun _ : {x : nat & DP x} => False)
            ?Goal@{H:=H1; H1:=H5; H2:=H6} (existT (fun x : nat => DP x) a b) H7) H4) H3) H H0
   end in
 H eq_refl eq_refl)
*)
Abort.

なんかさらに証明項が大きくなっている。あまり読む気がしないが、f_equal が 2回、eq_ind が 1回使われている。最初の f_equal は H2 から H3 を作っているが、型は同じでなんか意味が無さそう。後の f_equal は Set Keep Proof Equalities しなかったときと同じく 0 = a の証明を取り出していている。 eq_ind は existT (fun x : nat => DP x) a b を existT (fun x : nat => DP x) 0 (DPC 0) に置き換えていると思うのだが、そんな項は conclusion に含まれていないので意味は無い。

inversion はインデックスについて等式を作るが、インデックスの中に依存型があったらどうなるか。インデックスが match の外側と内側で違う (convertible でない) ので、そういうインデックスに依存した型は、外側と内側で型が異なることになり、ふつうに等式をつくると、型があわなくなるはずである。

以下のようにいろいろ試したところ、inversion はそういう場合に existT の等式を作るようだ。

まず、とりあえずどんな型の値でも型の中に取り込める帰納型 D を定義する。 D 1 とか D true とか、どんな値でもインデックスとして指定できる。

Inductive D {T : Type} : T -> Type := DC : forall (x : T), D x.

この D を使って、インデックスのところに (a : nat) (b : D a) と記述した帰納型をつくる。インデックスがふたつあって、最初のインデックスが 2番目のインデックスの型に現れている。これを simple inversion すると、等式が 2個生成される。追加された等式だけをコメントで示しているが、 H : 0 = a が最初のインデックスの等式であり、 H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b が 2番目のインデックスの等式である。

Inductive Test1 : forall (a : nat) (b : D a), Type := C1 : Test1 0 (DC 0).
Lemma L a b (t : Test1 a b) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b
*)
Abort.

2番目のインデックスは、match の外側では b, 内側では DC 0 なので、素朴には DC 0 = b という等式を期待してしまうが、DC 0 : D 0 と b : D a では型が D 0 と D a と異なる (convertible でない) ので等式 DC 0 = b は型がつかない。そこで、その D 0 と D a の異なる部分 (0 と a) を existT で隠蔽して等式を作っている。なお、existT (fun a : nat => D a) 0 (DC 0) と existT (fun a : nat => D a) a b は両方とも {x : nat & D x} という型である。 (notation を抑制すると、sigT (fun x : nat => D x) という型であることがわかる。) この型には 0 や a は出てこない。

次に、インデックスを (a : nat) (b : nat) (c : D (a, b)) としてみる。 1番目と2番目のインデックス (a, b) に 3番目のインデックス (c) の型が依存している。そうすると、3個の等式のうち、3番目のインデックスだけが existT の等式になっている。また、その等式では、existT がネストしており、依存しているインデックス a, b をそれぞれで隠蔽しているようだ。

Inductive Test2 : forall (a : nat) (b : nat) (c : D (a, b)), Type := C2 : Test2 0 0 (DC (0, 0)).
Lemma L a b c (t : Test2 a b c) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : 0 = b
H1 : existT (fun a : nat => {b : nat & D (a, b)}) 0 (existT (fun b : nat => D (0, b)) 0 (DC (0, 0))) =
     existT (fun a : nat => {b : nat & D (a, b)}) a (existT (fun b : nat => D (a, b)) b c)
*)
Abort.

インデックスを (a : nat) (b : D a) (c : nat) (d : D c) としてみると、依存型のインデクスの b, d に対応する等式が existT の形になっている。

Inductive Test3 : forall (a : nat) (b : D a) (c : nat) (d : D c), Type := C3 : Test3 0 (DC 0) 1 (DC 1).
Lemma L a b c d (t : Test3 a b c d) : False.
Proof.
  simple inversion t.
(*
H : 0 = a
H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b
H1 : 1 = c
H2 : existT (fun c : nat => D c) 1 (DC 1) = existT (fun c : nat => D c) c d
*)
Abort.

インデックスを (a : nat) (b : nat) (c : D a) (d : D b) と順番を変えても、依存型のインデクスの c, d に対応する等式が existT の形になっている。

Inductive Test4 : forall (a : nat) (b : nat) (c : D a) (d : D b), Type := C4 : Test4 0 1 (DC 0) (DC 1).
Lemma L a b c d (t : Test4 a b c d) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : 1 = b
H1 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a c
H2 : existT (fun b : nat => D b) 1 (DC 1) = existT (fun b : nat => D b) b d
*)
Abort.

合流するとどうだろうか、ということでインデックスを (a : nat) (b : D a) (c : nat) (d : D c) (e : D (b, d)) としてみると最後のインデックス e : D (b, d) に対応する等式は existT が 4重にネストして、a, b, c, d を隠蔽していることがわかる。

Inductive Test5 : forall (a : nat) (b : D a) (c : nat) (d : D c) (e : D (b, d)), Type :=
  C5 : Test5 0 (DC 0) 1 (DC 1) (DC ((DC 0), (DC 1))).
Lemma L a b c d e (t : Test5 a b c d e) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b
H1 : 1 = c
H2 : existT (fun c : nat => D c) 1 (DC 1) = existT (fun c : nat => D c) c d
H3 : existT (fun a : nat => {b : D a & {c : nat & {d : D c & D (b, d)}}}) 0
       (existT (fun b : D 0 => {c : nat & {d : D c & D (b, d)}}) (DC 0)
          (existT (fun c : nat => {d : D c & D (DC 0, d)}) 1
             (existT (fun d : D 1 => D (DC 0, d)) (DC 1) (DC (DC 0, DC 1))))) =
     existT (fun a : nat => {b : D a & {c : nat & {d : D c & D (b, d)}}}) a
       (existT (fun b : D a => {c : nat & {d : D c & D (b, d)}}) b
          (existT (fun c : nat => {d : D c & D (b, d)}) c
             (existT (fun d : D c => D (b, d)) d e)))
*)
Abort.

分岐、合流する場合は、ということで (a : nat) (b : D a) (c : D a) (d : D (b, c)) とすると、最後のインデックス d : D (b, c) に対応する等式は existT が 3重にネストして、a, b, c を隠蔽していることがわかる。

Inductive Test6 : forall (a : nat) (b : D a) (c : D a) (d : D (b, c)), Type :=
  C6 : Test6 0 (DC 0) (DC 0) (DC ((DC 0), (DC 0))).
Lemma L a b c d (t : Test6 a b c d) : False.
Proof.
simple inversion t.
(*
H : 0 = a
H0 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a b
H1 : existT (fun a : nat => D a) 0 (DC 0) = existT (fun a : nat => D a) a c
H2 : existT (fun a : nat => {b : D a & {c : D a & D (b, c)}}) 0
       (existT (fun b : D 0 => {c : D 0 & D (b, c)}) (DC 0)
          (existT (fun c : D 0 => D (DC 0, c)) (DC 0) (DC (DC 0, DC 0)))) =
     existT (fun a : nat => {b : D a & {c : D a & D (b, c)}}) a
       (existT (fun b : D a => {c : D a & D (b, c)}) b
          (existT (fun c : D a => D (b, c)) c d))
*)
Abort.

inversion がどういう等式を作るかということを上記から推測すると、各インデックスについて依存しているインデックスを調べて、それを順に existT で隠蔽する、という仕掛けで作られているのではないかと思う。

なお existT を使えば、inversion の場合分け対象そのものの等式を生成することもできるはずだが、そういう機能はなさそうである。

あと、simple inversion の後に証明を続けるときにどうするかであるが、existT の等式 E : existT D a x = existT D a' x' からは、まず EqdepFacts.eq_sig_fst により a = a' を取り出せる。これにより書き換えを行い、E : existT D a x = existT D a x' という形にできたら、 Eqdep_dec.inj_pair2_eq_dec により x = x' を取り出せる。このとき公理は不要であるが、a の型に decidable equality が必要である。

まぁ、inversion はすべてのインデックスに等式を生成するので、EqdepFacts.eq_sig_fst で取り出さなくてもその等式は別に生成されるため、EqdepFacts.eq_sig_fst は使わなくて済む気がする。

inversion は等式を生成する、というが、どんな等式を生成するかはマニュアルを読んでもはっきりしない。

Each such goal includes the hypotheses needed to deduce the proposition. と書いてあるが、 proposition を deduce するのに必要な hypotheses といわれても、具体性に欠ける。

まぁ、実際のところ、帰納型のインデックスについての等式を生成するのである。

たとえば、vanilla Coq で、自然数の less than or equal (<=) というのは le という帰納型で定義される。

Print le.
(*
Inductive le (n : nat) : nat -> Prop :=
  le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m.
*)

ここでは、a <= b は le a b の記法で、le の第1引数はパラメータで、第2引数がインデックスである。

p : le a b をコンストラクタ毎に場合分けすると、le_n a : le a a と le_S a m (_ : le a m) : le a (S m) になるので、インデックスは le_n の場合 a, le_S の場合 S m になる。なので、inversion はそれぞれの場合に a = b と S m = b という等式を生成する。

Lemma L (a b : nat) (E : b = b) (H : a <= b) : H = H /\ b = b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
______________________________________(1/1)
H = H /\ b = b
*)
simple inversion H.
(*
2 goals
a, b : nat
E : b = b
H : a <= b
H0 : a = b
______________________________________(1/2)
H = H /\ b = b
______________________________________(2/2)
a <= m -> H = H /\ b = b
*)
Show 2.
(*
goal 2 is:

  a, b : nat
  E : b = b
  H : a <= b
  m : nat
  H1 : S m = b
  ============================
  a <= m -> H = H /\ b = b
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) =>
 let H0 : (fun n : nat => n = b -> H = H /\ b = b) b :=
   match H as _ in (_ <= n) return (n = b -> H = H /\ b = b) with
   | le_n _ => fun H0 : a = b => ?Goal
   | le_S _ m x => (fun (m0 : nat) (H0 : a <= m0) (H1 : S m0 = b) => ?Goal0@{m:=m0} H0) m x
   end in
 H0 eq_refl)
*)
Abort.

証明項の match 式をみると、in (_ <= n) return (n = b -> H = H /\ b = b) という形で型が指定されている。 in 節の in (_ <= n) によって、インデックスが n に束縛され、 return 節の型 n = b -> H = H /\ b = b の中で使われている。 n は match 式全体、各分岐それぞれで置換される。 match 式全体では match で場合分けの対象とした H : a <= b のインデックス b に n が置換されるので b = b -> H = H /\ b = b 型となる。 le_n の分岐では le_n a : a <= a のインデックス a に置換されるので、a = b -> H = H /\ b = b になる。 le_S の分岐では le_S a m _ : a <= (S m) のインデックス S m に置換されるので、S m = b -> H = H /\ b = b になる。

convoy pattern により、match 式の外側で生成した eq_refl : b = b という項が、各分岐では、それぞれの等式の型となり、それを関数の引数として受けとっているので、context に等式が現れる。

また、context の E : b = b や、conclusion の H = H /\ b = b に含まれる b は置換されていない。

inversion は、各コンストラクタに場合分けして等式を追加し、等式を整理し、矛盾するゴールを除去する、という tactic である。 match 式が生成されるのは最初の部分で、その部分だけ行うのが simple inversion である。

destruct の対象がインデックス付き帰納型の項であった場合、 context と conclusion のインデックスをすべて置換するが、そんな大雑把な方法では失敗することもあるだろうと思う。

というわけでしばらく考えた結果、以下のように destruct が失敗する例を作れた。

Definition f (m n : nat) := le m (S n).

Lemma L a b (E : b = b) (H : le a (S b)) (H2 : f a b) : H = H2.
Proof.
destruct H.
(*
Abstracting over the terms "n" and "H" leads to a term fun (n0 : nat) (H0 : a <= n0) => H0 = H2
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
 "a <= n0" : "Prop"
 "H0" : "a <= n0"
 "H2" : "f a b"
The 3rd term has type "f a b" which should be a subtype of "a <= n0".
*)

ここでは、f という関数を用意して、それを使って型を記述することにより、 S を表面上隠している。

destruct H はインデックスの S b を置換するが、f によって隠れた S により、H2 の型を変えることができず、 H = H2 という等式の型が壊れ、エラーになっている。

もっと単純にすると以下のようにもできる。 S の別名として S' をつくってS を隠し、インデックスの置換を防げば、失敗させることができる。 (S の別名を作るというのはあまり現実味がないかもしれないが)

Definition S' := S.

Lemma L a b (E : b = b) (H : le a (S b)) (H2 : le a (S' b)) : H = H2.
Proof.
destruct H.
(*
Abstracting over the terms "n" and "H" leads to a term fun (n0 : nat) (H0 : a <= n0) => H0 = H2
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
 "a <= n0" : "Prop"
 "H0" : "a <= n0"
 "H2" : "a <= S' b"
The 3rd term has type "a <= S' b" which should be a subtype of "a <= n0".
*)

インデックスをぜんぶ置換するというのは、インデックスが単純な変数ならうまくいくのだろうが、それより複雑な項になると、うまくいかないことが出てくるのだと思う。

インデックス付き帰納型の場合分けを destruct でやってみよう。 destruct は context の中も置換するので、context 内の b は convoy pattern で置換されると予想できる。

Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)
destruct H.
(*
2 goals
a : nat
E : a = a
H2 : le_n a = le_n a
______________________________________(1/2)
le_n a = le_n a /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m H = le_S a m H /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:

  a, m : nat
  E : S m = S m
  H : a <= m
  H2 : le_S a m H = le_S a m H
  ============================
  le_S a m H = le_S a m H /\ S m = S m /\ a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
 match H as l in (_ <= n) return (n = n -> l = l -> l = l /\ n = n /\ a <= n) with
 | le_n _ => fun (E0 : a = a) (H3 : le_n a = le_n a) => ?Goal@{E:=E0; H2:=H3}
 | le_S _ m l =>
     (fun (m0 : nat) (H0 : a <= m0) (E0 : S m0 = S m0) (H3 : le_S a m0 H0 = le_S a m0 H0) =>
      ?Goal0@{m:=m0; E:=E0; H:=H0; H2:=H3}) m l
 end E H2)
*)
Abort.

予想通り、context 内の H と b が置換されている。そのために convoy pattern で E と H2 の型を変えている。

destruct に at をつけるとどうなるだろうか。

Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)
destruct H at 1.
(*
2 goals
a : nat
E : a = a
H : a <= a
H2 : H = H
______________________________________(1/2)
le_n a = H /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m l = H /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:

  a, m : nat
  E : S m = S m
  H : a <= S m
  H2 : H = H
  l : a <= m
  ============================
  le_S a m l = H /\ S m = S m /\ a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
 let l : a <= b := H in
 match l as l0 in (_ <= n) return (n = n -> forall H0 : a <= n, H0 = H0 -> l0 = H0 /\ n = n /\ a <= n) with
 | le_n _ => fun (E0 : a = a) (H0 : a <= a) (H3 : H0 = H0) => ?Goal@{E:=E0; H:=H0; H2:=H3}
 | le_S _ m l0 =>
     (fun (m0 : nat) (l1 : a <= m0) (E0 : S m0 = S m0) (H0 : a <= S m0) (H3 : H0 = H0) =>
      ?Goal0@{m:=m0; E:=E0; H:=H0; H2:=H3; l:=l1}) m l0
 end E H H2)
*)
Abort.

destruct H at 1 としたので、conclusion 内の H は、1番目の出現だけがコンストラクタの形に置換されている。インデックスは context, conclusion の両方ですべて置換されている。

まぁ、インデックスは context 内のも置換しておかないと、le_n a = H のような等式に型がつかないので、インデックスはもともと context 内も含めてぜんぶ置換するというのが destruct の方針で、 at があってもなくてもそれは一貫している、ということかなぁ。

case の場合は (インデックス付きの場合に) context 内の置換の有無がいろいろ変わるので、その一貫性のなさが美しくないとはいえるかもしれない。

あと、destruct では、eqn: 節により、(case_eq のような) 等式の生成が可能である。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
destruct n eqn:E.
(*
2 goals
n : nat
E : n = 0
H : 0 = 0
______________________________________(1/2)
0 = 0
______________________________________(2/2)
S n0 = S n0
*)
Show 2.
(*
goal 2 is:

  n, n0 : nat
  E : n = S n0
  H : S n0 = S n0
  ============================
  S n0 = S n0
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
 let n0 := n in
 let E : n = n0 := eq_refl in
 match n0 as n1 return (n = n1 -> n1 = n1 -> n1 = n1) with
 | 0 => fun (E0 : n = 0) (H0 : 0 = 0) => ?Goal@{E:=E0; H:=H0}
 | S n1 => (fun (n2 : nat) (E0 : n = S n2) (H0 : S n2 = S n2) => ?Goal0@{n0:=n2; E:=E0; H:=H0}) n1
 end E H)
*)
Abort.

証明項をみると、(まずなぜか let n0 := n in で n0 という変数を導入した後) let E : n = n0 := eq_refl in で、n = n という等式の証明を E に束縛し、 convoy pattern で n = 0 と n = S n2 に変えている。

なお、eqn: をつけても、context 内の置換は行われるようだ。 H : n = n が 0 = 0 と S n0 = S n0 に変わっている。

(ちなみに、destruct n eqn:E at 1 というように、eqn: と at の両方をつけると、context 内の置換は抑制されるようである。)

case 同様、destruct でも at 節を使える。しかし、意図したことかどうかはわからないが、at を使うと、context 内での置換はされなくなるようである。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
destruct n at 1.
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = n
______________________________________(2/2)
S n0 = n
*)
Show 2.
(*
goal 2 is:

  n : nat
  H : n = n
  n0 : nat
  ============================
  S n0 = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
 let n0 := n in match n0 as n1 return (n1 = n) with
                | 0 => ?Goal
                | S n1 => (fun n2 : nat => ?Goal0@{n0:=n2}) n1
                end)
*)
Abort.

destrct n at 1 の後では、0 と S の場合に分岐しているが、 context にある H : n = n はそのまま n = n として残っている。

まぁ、そもそも、at のところには conclusion の中での出現の番号を並べるというものなので、 context 内の各出現の置換を行うかどうかを指定できなさそうではある。

あと、証明項をみると、convoy pattern が使われていない。 context の H を変えないので、使う必要が無いのだろう。

destruct は、vanilla Coq の標準的な場合分け tactic である。

context 内の項を case は置換しなかったのに対し、destruct は置換するはずなので、それがわかるように試してみよう。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
destruct n.
(*
2 goals
H : 0 = 0
______________________________________(1/2)
0 = 0
______________________________________(2/2)
S n = S n
*)
Show 2.
(*
goal 2 is:

  n : nat
  H : S n = S n
  ============================
  S n = S n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
 match n as n0 return (n0 = n0 -> n0 = n0) with
 | 0 => fun H0 : 0 = 0 => ?Goal@{H:=H0}
 | S n0 => (fun (n1 : nat) (H0 : S n1 = S n1) => ?Goal0@{n:=n1; H:=H0}) n0
 end H)
*)
Abort.

context 内にあった H : n = n が、destruct n の後では、H : 0 = 0 と H : S n = S n になっていて、たしかに置換されている。

また、証明項をみると、これも convoy pattern を使っているようだ。

なお、context は goal の外側で束縛された変数であるが、証明項における束縛変数の名前と、context 内の変数の名前の対応は好き勝手に変えることができる。この証明項の ?Goal@{H:=H0} の H:=H0 はその対応を示している。また、証明項の束縛変数を context から消すこともできる。上の例では、外側の fun (n : nat) (H : n = n) => という部分で束縛された H は消えている。

(ちなみに、手動で変数の名前を変えるには rename tactic, 変数を消すには clear tactic を利用できる)

case_eq にインデックス付き帰納型の項を与えたらどうなるだろうか。

Lemma L a b (H : le a b) : le a b.
Proof.
(*
1 goal
a, b : nat
H : a <= b
______________________________________(1/1)
a <= b
*)
case_eq H.
(*
2 goals
a, b : nat
H : a <= b
______________________________________(1/2)
le_n a = le_n a -> a <= a
______________________________________(2/2)
forall (m : nat) (l : a <= m), le_S a m l = le_S a m l -> a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (H : a <= b) =>
 (match H as l in (_ <= n) return (l = l -> a <= n) with
  | le_n _ => ?Goal
  | le_S _ m l => ?Goal0 m l
  end
  :
  H = H -> a <= b) eq_refl)
*)
Abort.

えーと、le_n a = le_n a と le_S a m l = le_S a m l が追加されているんですが、なんですかねこれは。両辺が同じで役に立たないんですが。

まぁ、単純に H = le_n a とかにするのは型があわないので無理ということはわかるのだが。

case at のように context を巻き込んで置換することはしないようだ。でも役に立たない等式を加えるよりは (適切なエラーメッセージの) エラーにしてもらった方が嬉しいような気がする。

case_eq は、場合分けの際に、もともとの項と場合分け結果の等式を生成する機能を case tactic に加えた tactic である。

Lemma L (n : nat) (H : n < n) : n < n.
Proof.
(*
1 goal
n : nat
H : n < n
______________________________________(1/1)
n < n
*)
Show Proof.
(*
(fun (n : nat) (H : n < n) => ?Goal)
*)
case_eq n.
(*
2 goals
n : nat
H : n < n
______________________________________(1/2)
n = 0 -> 0 < 0
______________________________________(2/2)
forall n0 : nat, n = S n0 -> S n0 < S n0
*)
Show Proof.
(*
(fun (n : nat) (H : n < n) =>
 (match n as n0 return (n = n0 -> n0 < n0) with
  | 0 => ?Goal
  | S n0 => ?Goal0 n0
  end : n = n -> n < n) eq_refl)
*)
Abort.

conclusion が n < n のときに、case_eq n とすると、 n が 0 と S n0 の場合に場合分けされる。 0 の場合は n = 0 という assumption が追加され、 S n0 の場合は n = S n0 という assumption が追加される。

もともとの conclusion の n < n は 0 < 0 と S n0 < S n0 に置換される。

証明項をみると、どうやって等式を生成しているのかわかる。 match 式では as n0 return (n = n0 -> n0 < n0) となっているので、この match 式全体の型は n = n -> n < n である。それを、等式の左辺の n は置換せず、右辺の n は置換することにより、各分岐の中では、 n とコンストラクタの等式になるようにしている。

match 式全体の型は、(なぜか) 証明項で match 式にキャストで型が明示されていて、n = n -> n < n と書いてあることからも分かる。

この match式の型は case_eq n 直前の conclusion とは異なり、n = n という assumption が付け加えられている。これは、n = n 型の式 eq_refl を引数とする関数適用 (_ eq_refl) で match 式をくるむことで実現されている。

なお、case_eq は、case 同様、context 内の項は置換しない。つまり、H : n < n の n は 0 や S n0 にはならない。

あと、case_eq は case と異なり、at 節は指定できないようだ。

なお、マニュアルでは case_eq よりも destruct の eqn: 節を使うのが勧められている。

case に at と eqn: をつけるかどうか、また、場合分け対象がインデックス付き帰納型かどうかで、context/conclusion のなにを置換するかをまとめてみた。

インデックス無し:

case n は conclusion 内の n を置換する
case n at ... は conclusion 内の at で指定された n を置換する
case n eqn:E は context と conclusion 内の n を置換する
case n eqn:E at ... は conclusion 内の at で指定された n を置換する

インデックス付き:

case H は conclusion 内のインデックスと H を置換する
case H at ... は context と conclusion 内のインデックスを置換し、conclusion 内の at で指定された H を置換する
case H eqn:E は context と conclusion 内のインデックスと H を置換する
case H eqn:E at ... は context と conclusion 内のインデックスを置換し、conclusion 内の at で指定された H を置換する

推測というか妄想になるが、最初は単に match を作るだけの tactic だったのが、インデックス付き帰納型で at をサポートする都合により、型をあわせるために (大雑把にも) コンテキスト内に出現するインデックスをすべて置換するようになって、 eqn: はなぜか destruct を使って実装され、 conclusion だけを変えるという当初の想定が崩れてよくわからない仕様になっている、という印象をもった。

まぁ、case (SSReflect) のように、インデックスを置換する箇所を指定できるようにして、どんな match 式でも生成できるようなプリミティブとして進化すればよかったのに、とは思う。

なお、後述する destruct では、context のインデックスはいつも置換するように一貫している。まぁ、それがいいかというとそれはそれで問題なのだが。

case では、等式を生成する eqn: という指定ができる。

case H eqn:E2 として、等式を生成してみよう。

Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)
case H eqn:E2.
(*
2 goals
a : nat
E : a = a
H : a <= a
E2 : H = le_n a
H2 : le_n a = le_n a
______________________________________(1/2)
le_n a = le_n a /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m l = le_S a m l /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:

  a, m : nat
  E : S m = S m
  H : a <= S m
  l : a <= m
  E2 : H = le_S a m l
  H2 : le_S a m l = le_S a m l
  ============================
  le_S a m l = le_S a m l /\ S m = S m /\ a <= S m
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
 let l : a <= b := H in
 let E2 : H = l := eq_refl in
 match l as l0 in (_ <= n) return (n = n -> forall H0 : a <= n, H0 = l0 -> l0 = l0 -> l0 = l0 /\ n = n /\ a <= n) with
 | le_n _ =>
     fun (E0 : a = a) (H0 : a <= a) (E3 : H0 = le_n a) (H3 : le_n a = le_n a) => ?Goal@{E:=E0; H:=H0; E2:=E3; H2:=H3}
 | le_S _ m l0 =>
     (fun (m0 : nat) (l1 : a <= m0) (E0 : S m0 = S m0) (H0 : a <= S m0) (E3 : H0 = le_S a m0 l1)
        (H3 : le_S a m0 l1 = le_S a m0 l1) => ?Goal0@{m:=m0; E:=E0; H:=H0; l:=l1; E2:=E3; H2:=H3}) m l0
 end E H E2 H2)
*)
Abort.

ここでは context の場合分け対象 (H) とインデックスがぜんぶ置換されている。たとえば、H2 : H = H が H2 : le_n a = le_n a に変わっている。

at をつけていないからといって、context 内の H までコンストラクタに置換するのはやりすぎな気がするが。 (気がついたのだが、GitHub coq/coq issue #19487: case with eqn: modifies hypotheses, destructing an expression that does not even appear in the goal という issue があって、なんか、case eqn: は destruct で実装されているという話があるようだ)

なお、case H eqn:E2 at 1 として、eqn: と at を両方つけると、インデックスは context と conclusion の両方、場合分け対象 (H) は conclusion 内の at で指定されたものだけが置換されるようだ。

case では、どこを置換するかを at で指定できる。

ここで case H at 1 として、H の 1番目の出現だけを場合分けするようにしてみよう。

Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)

以下を見ると、conclusion の H = H が le_n a = H になっているのは指定したとおりであるが、考えてみるとちょっと奇妙で、le_n a は le a a 型で、H は le a b 型なので、型があわないはずである。と思って context を確認すると、H の型が a <= a (つまり le a a) に変わっている。というか、b が消えていて、E も a = a になっている。あと、conclusion 内のすべての b が a に変わっている。 (2番目のゴールでは、すべての b が S m に変わっている)

case H at 1.
(*
2 goals
a : nat
E : a = a
H : a <= a
H2 : H = H
______________________________________(1/2)
le_n a = H /\ a = a /\ a <= a
______________________________________(2/2)
le_S a m l = H /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:

  a, m : nat
  E : S m = S m
  H : a <= S m
  H2 : H = H
  l : a <= m
  ============================
  le_S a m l = H /\ S m = S m /\ a <= S m
*)

case は context を変えないんじゃなかったのか、と思いつつ証明項をみると、以下のようになっている。

Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
 let l : a <= b := H in
 match l as l0 in (_ <= n) return (n = n -> forall H0 : a <= n, H0 = H0 -> l0 = H0 /\ n = n /\ a <= n) with
 | le_n _ => fun (E0 : a = a) (H0 : a <= a) (H3 : H0 = H0) => ?Goal@{E:=E0; H:=H0; H2:=H3}
 | le_S _ m l0 =>
     (fun (m0 : nat) (l1 : a <= m0) (E0 : S m0 = S m0) (H0 : a <= S m0) (H3 : H0 = H0) =>
      ?Goal0@{m:=m0; E:=E0; H:=H0; H2:=H3; l:=l1}) m l0
 end E H H2)
*)
Abort.

ここでは、match 式が関数を返し、その関数に即座に E, H, H2 が引数として与えられ、 match 式で型が変えられ、各分岐で変えられた型の引数を受け取る、という形になっている。 return 節でその関数の引数の型が記述されるのだが、そこで置換がおこるようになっているために、 E, H, H2 を異なる型として受け取ることができている。 (こういうのを、convoy pattern という。) return 節の中で E は n = n となっているので、(n は in (_ <= n) で束縛されている変数なので) 両辺が置換される。 H, H2 も同様に、b が分岐の中でのインデックス (le_n の場合は a, le_S の場合は S m) になるように置換される。

まぁ、こうやって置換しないと、le_n a = H などは型が壊れるので、context も含めてやってくれるということだろう。

そして、どうやら、インデックスの置換は可能なすべての部分について行うようで、どこを置換するかを指定する機能はなさそうである。 (まぁ、conclusion はともかく、context のどこを変えるかを指定するのは番号だけでは難しそうである)

上の例だと、H のインデックスは b という変数だったので、変数 b を置換すれば、b を跡形もなく消すことができたが、もっと複雑な項だとそれが可能とは限らない。。そういう例として (H : le a (S b)) を試してみた。インデックスが S b なので、S b を置換するはずだが、それだと S がついていない b は残るのではないかと思う。

Lemma L a b (E : b = b) (E2 : S b = S b) (H : le a (S b)) (H2 : H = H) : H = H /\ b = b /\ S b = S b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
E2 : S b = S b
H : a <= S b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ S b = S b /\ a <= b
*)

以下のように H の 1番目の出現だけを場合分けすると、やはり、context の E : b = b や、conclusion の b = b はそのまま残る。

case H at 1.
(*
2 goals
a, b : nat
E : b = b
E2 : a = a
H : a <= a
H2 : H = H
______________________________________(1/2)
le_n a = H /\ b = b /\ a = a /\ a <= b
______________________________________(2/2)
le_S a m l = H /\ b = b /\ S m = S m /\ a <= b
*)
Show 2.
(*
goal 2 is:

  a, b : nat
  E : b = b
  m : nat
  E2 : S m = S m
  H : a <= S m
  H2 : H = H
  l : a <= m
  ============================
  le_S a m l = H /\ b = b /\ S m = S m /\ a <= b
*)
Show Proof.
(*
(fun (a b : nat) (E : b = b) (E2 : S b = S b) (H : a <= S b) (H2 : H = H) =>
 let l : a <= S b := H in
 let n := S b in
 match
   l as l0 in (_ <= n0) return (n0 = n0 -> forall H0 : a <= n0, H0 = H0 -> l0 = H0 /\ b = b /\ n0 = n0 /\ a <= b)
 with
 | le_n _ => fun (E3 : a = a) (H0 : a <= a) (H3 : H0 = H0) => ?Goal@{E2:=E3; H:=H0; H2:=H3}
 | le_S _ m l0 =>
     (fun (m0 : nat) (l1 : a <= m0) (E3 : S m0 = S m0) (H0 : a <= S m0) (H3 : H0 = H0) =>
      ?Goal0@{m:=m0; E2:=E3; H:=H0; H2:=H3; l:=l1}) m l0
 end E2 H H2)
*)
Abort.

というわけで、case H at 1 は、H のインデックスである S b を可能な限り置換して a にするが、それだけでは b を消すことはできない。また、a と b の関係 (le_n の場合 S b = a) は得られていない。

nat にはインデックスがなかったが、インデックスがある帰納型として、le を例として case で場合分けを行ってみる。

le の定義は以下のとおりである。これは自然数の less than or equal を表現している。 vanilla Coq では le a b は a <= b という notation で表示される。 (SSReflect では (a <= b)%coq_nat と表示される。)

Print le.
(*
Inductive le (n : nat) : nat -> Prop :=
  le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m.
*)

ここでは、le の第1引数 n はパラメータで、第2引数 (名前はついていない) がインデックスである。

以下のように試す。場合分けで、H 自身や b が置換されるかどうかを確認するため、context や conclusion に b = b や H = H を入れてある。

Lemma L a b (E : b = b) (H : le a b) (H2 : H = H) : H = H /\ b = b /\ le a b.
Proof.
(*
1 goal
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/1)
H = H /\ b = b /\ a <= b
*)

case H で場合分けすると、以下のように conclusion 内の H と b が置換される。 H は le_n a と le_S a m l に置換され、b は a と S m に置換される。 context 内の H, b は置換されない。

case H.
(*
2 goals
a, b : nat
E : b = b
H : a <= b
H2 : H = H
______________________________________(1/2)
le_n a = le_n a /\ a = a /\ a <= a
______________________________________(2/2)
forall (m : nat) (l : a <= m), le_S a m l = le_S a m l /\ S m = S m /\ a <= S m
*)
Show 2.
(*
goal 2 is:

  a, b : nat
  E : b = b
  H : a <= b
  H2 : H = H
  ============================
  forall (m : nat) (l : a <= m), le_S a m l = le_S a m l /\ S m = S m /\ a <= S m
*)

証明項をみると、return 節が (l = l /\ n = n /\ a <= n) となっていて、l と n の部分が置換されることがわかる。 context の a, b, E, H, H2 は外側の束縛のままなので、なにも変わらないことも確認できる。

Show Proof.
(*
(fun (a b : nat) (E : b = b) (H : a <= b) (H2 : H = H) =>
 match H as l in (_ <= n) return (l = l /\ n = n /\ a <= n) with
 | le_n _ => ?Goal
 | le_S _ m l => ?Goal0 m l
 end)
*)
Abort.

case (vanilla Coq) は、マニュアルで An older, more basic tactic to perform case analysis without recursion. と説明されていて、いちばん基本的な場合分け tactic である。

(destruct と違って) conclusion だけを変更し、context は変更しない、という説明もあるので、それがわかるような例を作って証明項を調べてみよう。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) => ?Goal)
*)
case n.
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = 0
______________________________________(2/2)
forall n0 : nat, S n0 = S n0
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) => match n as n0 return (n0 = n0) with
                              | 0 => ?Goal
                              | S n0 => ?Goal0 n0
                              end)
*)
Abort.

ここでは、context に (n : nat) (H : n = n) がある状態で n = n という conclusion を証明するという状態で、 case n を行っている。

証明項をみると、case n の直前には (fun (n : nat) (H : n = n) => ?Goal) だったのが、 case n により、?Goal のところに以下の match 式が生成されている。

match n as n0 return (n0 = n0) with
| 0 => ?Goal
| S n0 => ?Goal0 n0
end

証明項というのは、型が conclusion な項なので、 match 式の return 節は conclusion の n = n となる、のだが、ここでは n が n0 に置き換わっている。 n0 は as n0 で束縛されている変数で、match 式全体の型としては n となり、各分岐の型としてはコンストラクタ適用の形となる。

そのため、0 の分岐では 0 = 0 となり、 S の分岐では (S の引数が n0 であるとして) S n0 = S n0 となる。 (ここの n0 は、match 式が "| S n0 =>" の部分で束縛した変数であり、return 節のために "as n0" で束縛した変数とは別の変数である)

S の分岐では ?Goal0 n0 という項になっているので、?Goal0 には、n0 を受け取って S n0 = S n0 という型の値を返す関数を埋めなければならない。なので、case n が生成した 2番めのゴールでは、conclusion が forall n0 : nat, S n0 = S n0 となっている。

ところで、case n は conclusion の n = n を n0 = n0 に変えたが、ここの変え方は at 節で制御できる。

Lemma L (n : nat) (H : n = n) : n = n.
Proof.
(*
1 goal
n : nat
H : n = n
______________________________________(1/1)
n = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) => ?Goal)
*)
case n at 1.
(*
2 goals
n : nat
H : n = n
______________________________________(1/2)
0 = n
______________________________________(2/2)
S n0 = n
*)
Show Proof.
(*
(fun (n : nat) (H : n = n) =>
 let n0 := n in match n0 as n1 return (n1 = n) with
                | 0 => ?Goal
                | S n1 => (fun n2 : nat => ?Goal0@{n0:=n2}) n1
                end)
*)
Abort.

今回は、case n at 1 として、場合分けの対象を n の 1番目の出現と指定した。その結果、生成される match 式の as-return 節は as n1 return (n1 = n) となっており、場合分けによってコンストラクタ適用に置換されるのは = の左辺だけとなっている。

なぜか match 式の外側に不要な let が入っているが... なんでかな? (想像としては、match 式の生成では conclusion に出現する n を無差別に置換するようになっていて、それを事前に let で別名に置き換えることで、置換するかどうかを制御しているとか?)

なお、case n at 2 とすると、as n1 return (n = n1) となる。

case n at 1 2 とすれば、at 1 2 を指定しない場合と同じに、= の両辺が置換される。(let は入る)

(fun (n : nat) (H : n = n) =>
 let n0 := n in match n0 as n1 return (n1 = n1) with
                | 0 => ?Goal
                | S n1 => (fun n2 : nat => ?Goal0@{n0:=n2}) n1
                end)

case n at と、番号を指定しない形は syntax error のようだ。動作をするとしたら、置換を行わないという動作になると思うが、そうすると conclusion が変化しないので、意味が無いということだろう。

ところで、case は (destruct と違って) conclusion だけを変更し、local context は変更しない、という話がどうだったかというと、 context に入っている H : n = n はまったく変わっていないので、これは説明どおりに動作している。また、conclusion を型とする match 式を生成するかぎりは、context (外側の変数束縛) が変わるはずもないので、これは match 式の生成というところからみると、基本的で、予想通りの動作といえるだろう。単に match 式を生成する tactic を作ったら case tactic になりました、という感じである。

マニュアルを読むと、それぞれの機能は、だいたい以下のように説明されている

destruct はそれぞれのコンストラクタについてゴールを生成して場合分けを行う。それぞれのサブゴールでは対象の式がコンストラクタを使った形に置き換えられる。
case は古いもの。destruct がお勧め。goal だけを変更し、local context は変更しない。
case_eq は、対象の式とコンストラクタ (の呼び出し) の等式を生成する。case_eq よりも destruct の eqn: 節を使うのがお勧め。
simple inversion は、等式を生成するが、inversion が行う単純化はしない。
dependent simple inversion は説明がない。 dependent inversion は inversion に加えて場合分け対象をコンストラクタ呼び出しの式に置き換えるというものなので、 dependent simple inversion はその最初の部分だけを行うものだろう。
case (SSReflect) は SSReflect の基本 tactic のひとつで場合分けを行うもの。

帰納型 D は以下のように定義される。

Inductive D params : forall targs, sort :=
| C1 fargs_1 : D params indexes_1
...
| Cn fargs_n : D params indexes_n

ここで、params と targs は 0 個以上の変数束縛であり、D の引数である。

D は引数として params と targs をとり、その結果は sort に属する型である。そのため、params と targs の両方が空の場合は、ひとつの型を定義する。そうでなく、params と targs のどちらかでも空でない場合は、0個以上の型からなる型族 (type family) を定義することになる。

コンストラクタ C1, ..., Cn は、この帰納型の値を定義する。 Ci は引数として params, fargs_i を受け取り、D params indexes_i 型の値となる。コンストラクタの返値の型 D params indexes_i では、params は帰納型の params をそのまま指定しなければならない。 indexes_i は式であり、その中では params と fargs_i を使える。

ここで、D params targs 型の式 d の値がコンストラクタ Ci で作られた値だったとしよう。 Ci は、Ci params aargs_i という形で呼ばれ、その結果は D params indexes_i という型の値である。つまり、d : D params targs と Ci params aargs_i : D params indexes_i が等しいはず、ということがわかる。そして、それらの各部分が等しいので、以下のふたつが等しいことになる。 (targs と index_i は同数の要素を持ち、0 個以上なので、それぞれの要素が等しいことになる。)

d と Ci params aargs_i
targs と indexes_i

この帰納型 d : D params targs を場合分けする match 式は以下のようになる。

match d as d' in D _ targs' return P targs' d' with
| C1 ... => ...
...
| Cn ... => ...
end

ふつうの (ML とかの) match 式と似ているが、as d' in D _ targs' return P targs' d' の部分は Coq 特有のものである。

ふつうの match 式では、場合分けすると、コンストラクタの種類、およびその種類に応じたコンストラクタの引数が得られ、それらを利用して分岐の中身を記述できる。分岐の部分に書いた式の値が match 式の値となる。 Coq でもそれは同じである。

そして、ふつうの ML の match 式の型は、各分岐の型と等しい。まぁ、各分岐の値が match 式の値になるので、値が等しいので型も等しい、ということである。

しかし Coq では、as d' in D _ targs' return P targs' d' の部分によって、 match 式全体の型、および各分岐の型を指定することができる。といっても、各分岐の値が match 式の値になるので、分岐の型と match の型が同じはず、というのは同じで、この指定は、型の一部分をそこと同じ値であるずの式に置き換える、という指定だけができるようになっている。そうやって指定することで、結局のところ同じ型になる範囲で、型を変えることができる。

as d' in D _ targs' の部分で、d' と targs' が束縛され、 P targs' d' の部分には、型を書く。この型の中では targs' や d' を使ってよい。(使わなくてもよい)

なお、in D _ targs' の targs' は targs と同数の束縛を書く。あと、その前の _ は params と同数の _ を書くことになっている。 (params は分岐の返値の型にはそのまま記述することになっている、つまり分岐において変わらないことが保証されているので、そこを変えるための変数を束縛することはできない。)

match 式全体の型は P targs' d' の targs' と d' が targs と d に置換された結果となる。コンストラクタ Ci に分岐した場合の型は、P targs' d' の targs' と d' が indexes_i と Ci params aargs_i に置換された結果となる。

Ci に分岐した場合は、(targs, d) は (indexes_i, Ci params aargs_i) に等しいので、結局は同じ型であり、うまく P を作ると、それぞれが等しいという情報を分岐の中で利用できる。

ちょっと用語について確認しておく。

Coq < Lemma L (H : 0 = 0) : 1 = 1 -> 2 = 2 -> 3 = 3.
1 goal

  H : 0 = 0
  ============================
  1 = 1 -> 2 = 2 -> 3 = 3

Coq では上のような表示を tactic でいじっていくのだが、横線の上を context、下を conclusion という。上の例では、context の中には H : 0 = 0 があり、 conclusion は 1 = 1 -> 2 = 2 -> 3 = 3 である。

context と conclusion をあわせて goal という。

また、conclusion の中の、-> の左の部分 (1 = 1 や 2 = 2) を assumption という。とくに、いちばん左の assumption (1 = 1) を top assumption という。 (これは SSReflect の流儀にしたがっているつもりである)

なお、conclusion の部分を指して goal ということがある。マニュアルにもそういう表現があるので、文脈に応じて察する必要がある。

なにが知りたいかというと、とくに、それぞれがどんな match 式を証明項として生成するのか理解したい。帰納型の場合分けは結局は match 式なので、そこが本質である。

マニュアルを読んでそれぞれの tactic の位置づけを調べてみる。

まず、edestruct と ecase は、apply に対する eapply みたいなやつで、 existential variables を生成してもよい tactic のようだ。たぶん、生成される match 式は destruct や case と変わらないと思う。

simple destruct ident はマニュアルに intros until ident; case ident と同じと書いてある。 match 式は case が生成するものと同じなのだろう。

dependent destruction は、JMeq を使うもので、公理が必要になるので、とりあえず興味が無い。

inversion_clear は inversion した後で inversion が使った仮定を消すというものなので、生成される match 式は inversion と同じだろう。 dependent inversion_clear も同様である。

inversion は、各コンストラクタに場合分けして等式を追加し、等式を整理し、矛盾するゴールを除去する、という tactic なのだが、 match 式は最初の部分で生成される。そして、simple inversion は inversion の最初の部分だけを行う tactic である。なので、match 式の生成については simple inversion だけ調べればよい。 dependent inversion も、match 式の生成を行うのは dependent simple inversion だけ調べればよい。

というわけで、調べる対象は以下となった。

これらのどれを選んで使うのか、というのは自分でもよくわかっていない。 (まぁ、SSReflect に移行してしまったので、vanilla Coq の tactic をまじめに調べるモチベーションがほとんどなくなってしまったというのもあるが)

とくに vanilla Coq だと、まず destruct を使って、それでうまく行かない (必要な情報が出てこない) なら、 destruct の eqn: オプション (あるいは case_eq) を使うとか、 inversion を試してみる、という感覚である。どれがどう違うのかは、完全に理解しているとは言い難い。

SSReflect 流なら case 一択であるが、 inversion が必要になったときにはけっこう困る。 SSReflect には inversion に相当する (SSReflect 流の) tactic はない。これは inversion がなにをするものなのかをちゃんと理解していないのが原因な気がする。

あと、refine で match 式を直接記述できるが、他の tactic で生成できず、refine が絶対に必要な場合が存在するのかどうかというのも気になる。

というわけで、一念発起してそれぞれがどう違うのか調べてみた。

Coq で帰納型の式を各コンストラクタ毎に場合分けする tactic には case, destcut, inversion などさまざまなものがある。

Coq マニュアルの Reasoning with inductive types で、場合分けを行う tactic は以下が載っている。 (用途が限定されすぎている tactic は除いてある)

また SSReflect には、(上記の vanilla Coq の case とは異なる) case tactic がある。 (vanilla Coq というのは、Coq/SSReflect と対比して、もともとの Coq を指す用語だと思う)

case (SSReflect)

あと、任意の証明項を作る refine tactic がある。これは場合分けをするためだけのものではないが、match 式を作れば場合分けを行える。

refine

天泣記

2024-11-10 (Sun)

2024-10-30 (Wed)

2024-09-17 (Tue)

2024-09-16 (Mon)