https://github.com/akr/all-ruby は https://github.com/ruby/all-ruby へ移行した
なんか、自動化の都合でそうしたかったらしい
要約: 以前、インデックス付き帰納型の場合分けについて書いたが、 もっと一般化して、インデックスが複数の場合、さらには、その複数のなかに依存型が現れる場合を 検討した結果、existT の等式を使えばそういうのも場合分け可能であることがわかった
あと、こんなものは使わないで済むほうがよくて、SSReflect の tuple や fintype を使うほうがよい
以前、インデックス付き帰納型の場合分けについて書いたが、 そのとき扱ったのは Vector.t, eq, le で、どれもインデックスがひとつのものだった。
インデックスが複数あっても対応できるだろうか、と思ったのでやってみた
インデックスが複数ある帰納型として、SSReflect に ltn_xor_geq があるので、それを使ってみる。 まぁ、ltn_xor_geq は、証明を対話的に行う中で使うツールなので、 証明を値としてデータの中に埋め込むことは考えにくく、 証明を場合分けしたり一意性の証明が必要になったりすることは考えにくいのだが、 ただ、インデックスが 6個もあるというただそれだけの理由で対象に選んだ。
ltn_xor_geq は以下のように定義されている。 nat -> nat -> nat -> nat -> bool -> bool -> という部分がインデックスで、nat が 4個、bool が 2個ある。
Variant ltn_xor_geq m n : nat -> nat -> nat -> nat -> bool -> bool -> Set := | LtnNotGeq of m < n : ltn_xor_geq m n m m n n false true | GeqNotLtn of n <= m : ltn_xor_geq m n n n m m true false.
やってみたところ、以下のように場合分けの補題 ltn_xor_geq_case を証明できた。 それほど苦労したわけではないが、長い。 あと、書いている最中はともかく、後から読んで何をやっているのかはわかりにくそうである。
From mathcomp Require Import all_ssreflect.
Lemma ltn_xor_geq_case :
forall m n a1 a2 a3 a4 a5 a6 (P : ltn_xor_geq m n a1 a2 a3 a4 a5 a6 -> Prop),
(forall (ltn_mn : m < n) (p1 : m = a1) (p2 : m = a2) (p3 : n = a3) (p4 : n = a4) (p5 : false = a5) (p6 : true = a6),
P (eq_rect m (fun c1 : nat => ltn_xor_geq m n c1 a2 a3 a4 a5 a6)
(eq_rect m (fun c2 : nat => ltn_xor_geq m n m c2 a3 a4 a5 a6)
(eq_rect n (fun c3 : nat => ltn_xor_geq m n m m c3 a4 a5 a6)
(eq_rect n (fun c4 : nat => ltn_xor_geq m n m m n c4 a5 a6)
(eq_rect false ((ltn_xor_geq m n m m n n)^~ a6)
(eq_rect true (ltn_xor_geq m n m m n n false)
(LtnNotGeq (m:=m) (n:=n) ltn_mn) a6 p6) a5 p5) a4 p4) a3 p3) a2 p2) a1 p1)) ->
(forall (leq_nm : n <= m) (p1 : n = a1) (p2 : n = a2) (p3 : m = a3) (p4 : m = a4) (p5 : true = a5) (p6 : false = a6),
P (eq_rect n (fun c1 : nat => ltn_xor_geq m n c1 a2 a3 a4 a5 a6)
(eq_rect n (fun c2 : nat => ltn_xor_geq m n n c2 a3 a4 a5 a6)
(eq_rect m (fun c3 : nat => ltn_xor_geq m n n n c3 a4 a5 a6)
(eq_rect m (fun c4 : nat => ltn_xor_geq m n n n m c4 a5 a6)
(eq_rect true ((ltn_xor_geq m n n n m m)^~ a6)
(eq_rect false (ltn_xor_geq m n n n m m true)
(GeqNotLtn (m:=m) (n:=n) leq_nm) a6 p6) a5 p5) a4 p4) a3 p3) a2 p2) a1 p1)) ->
(forall x, P x).
Proof.
move=> m n a1 a2 a3 a4 a5 a6 P H1 H2 x.
refine (match x as x' in ltn_xor_geq _ _ b1 b2 b3 b4 b5 b6
return forall (p1 : b1 = a1) (p2 : b2 = a2) (p3 : b3 = a3)
(p4 : b4 = a4) (p5 : b5 = a5) (p6 : b6 = a6),
(eq_rect b1 (fun c1 => ltn_xor_geq m n c1 a2 a3 a4 a5 a6)
(eq_rect b2 (fun c2 => ltn_xor_geq m n b1 c2 a3 a4 a5 a6)
(eq_rect b3 (fun c3 => ltn_xor_geq m n b1 b2 c3 a4 a5 a6)
(eq_rect b4 (fun c4 => ltn_xor_geq m n b1 b2 b3 c4 a5 a6)
(eq_rect b5 (fun c5 => ltn_xor_geq m n b1 b2 b3 b4 c5 a6)
(eq_rect b6 (ltn_xor_geq m n b1 b2 b3 b4 b5)
x' a6 p6) a5 p5) a4 p4) a3 p3) a2 p2) a1 p1) = x ->
P x with
| LtnNotGeq ltn_mn => _
| GeqNotLtn leq_nm => _
end erefl erefl erefl erefl erefl erefl erefl).
move=> p1 p2 p3 p4 p5 p6 <-.
by exact (H1 ltn_mn p1 p2 p3 p4 p5 p6).
move=> p1 p2 p3 p4 p5 p6 <-.
by exact (H2 leq_nm p1 p2 p3 p4 p5 p6).
Defined.
場合分けの補題を証明できたので、証明の一意性も証明してみた。
Lemma ltn_xor_geq_irrelevance m n x1 x2 x3 x4 y1 y2 (p1 p2 : ltn_xor_geq m n x1 x2 x3 x4 y1 y2) : p1 = p2.
Proof.
apply ltn_xor_geq_case => {p2}.
move=> ltn_mn q1 q2 q3 q4 q5 q6.
pattern p1.
apply ltn_xor_geq_case => {p1}.
move=> ltn_mn' r1 r2 r3 r4 r5 r6.
move: (q1); rewrite -{}q1 in r1 * => q1.
move: (q2); rewrite -{}q2 in r2 * => q2.
move: (q3); rewrite -{}q3 in r3 * => q3.
move: (q4); rewrite -{}q4 in r4 * => q4.
move: (q5); rewrite -{}q5 in r5 * => q5.
move: (q6); rewrite -{}q6 in r6 * => q6.
do 8 rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
do 4 rewrite -(Eqdep_dec.eq_rect_eq_dec Bool.bool_dec).
congr (LtnNotGeq _).
by apply eq_irrelevance.
move=> leq_nm.
exfalso.
move: ltn_mn.
by rewrite ltnNge leq_nm.
move=> leq_nm q1 q2 q3 q4 q5 q6.
pattern p1.
apply ltn_xor_geq_case => {p1}.
move=> ltn_mn.
exfalso.
move: ltn_mn.
by rewrite ltnNge leq_nm.
move=> leq_nm' r1 r2 r3 r4 r5 r6.
move: (q1); rewrite -{}q1 in r1 * => q1.
move: (q2); rewrite -{}q2 in r2 * => q2.
move: (q3); rewrite -{}q3 in r3 * => q3.
move: (q4); rewrite -{}q4 in r4 * => q4.
move: (q5); rewrite -{}q5 in r5 * => q5.
move: (q6); rewrite -{}q6 in r6 * => q6.
do 8 rewrite -(Eqdep_dec.eq_rect_eq_dec PeanoNat.Nat.eq_dec).
do 4 rewrite -(Eqdep_dec.eq_rect_eq_dec Bool.bool_dec).
congr (GeqNotLtn _).
by apply eq_irrelevance.
Qed.ltn_xor_geq_case が分かりにくいのは、やはり eq_rect をたくさん使ってネストしているところだと思うのだが、 いろいろ調べたところ、Coq.Init.Logic に EqNotations というのが用意されていて、これを使うと、読みやすい記法を使えるようだ。
これにより、以下のように記述できた。
Import EqNotations.
Lemma ltn_xor_geq_case2 :
forall m n a1 a2 a3 a4 a5 a6 (P : ltn_xor_geq m n a1 a2 a3 a4 a5 a6 -> Prop),
(forall (ltn_mn : m < n) (p1 : m = a1) (p2 : m = a2) (p3 : n = a3) (p4 : n = a4) (p5 : false = a5) (p6 : true = a6),
P (rew [fun c1 => ltn_xor_geq m n c1 a2 a3 a4 a5 a6] p1 in
rew [fun c2 => ltn_xor_geq m n m c2 a3 a4 a5 a6] p2 in
rew [fun c3 => ltn_xor_geq m n m m c3 a4 a5 a6] p3 in
rew [fun c4 => ltn_xor_geq m n m m n c4 a5 a6] p4 in
rew [fun c5 => ltn_xor_geq m n m m n n c5 a6] p5 in
rew [fun c6 => ltn_xor_geq m n m m n n false c6] p6 in
(LtnNotGeq (m:=m) (n:=n) ltn_mn))) ->
(forall (leq_nm : n <= m) (p1 : n = a1) (p2 : n = a2) (p3 : m = a3) (p4 : m = a4) (p5 : true = a5) (p6 : false = a6),
P (rew [fun c1 => ltn_xor_geq m n c1 a2 a3 a4 a5 a6] p1 in
rew [fun c2 => ltn_xor_geq m n n c2 a3 a4 a5 a6] p2 in
rew [fun c3 => ltn_xor_geq m n n n c3 a4 a5 a6] p3 in
rew [fun c4 => ltn_xor_geq m n n n m c4 a5 a6] p4 in
rew [fun c5 => ltn_xor_geq m n n n m m c5 a6] p5 in
rew [fun c6 => ltn_xor_geq m n n n m m true c6] p6 in
(GeqNotLtn (m:=m) (n:=n) leq_nm))) ->
(forall x, P x).
Proof.
move=> m n a1 a2 a3 a4 a5 a6 P H1 H2 x.
refine (match x as x' in ltn_xor_geq _ _ b1 b2 b3 b4 b5 b6
return forall (p1 : b1 = a1) (p2 : b2 = a2) (p3 : b3 = a3)
(p4 : b4 = a4) (p5 : b5 = a5) (p6 : b6 = a6),
(rew [fun c1 => ltn_xor_geq m n c1 a2 a3 a4 a5 a6] p1 in
rew [fun c2 => ltn_xor_geq m n b1 c2 a3 a4 a5 a6] p2 in
rew [fun c3 => ltn_xor_geq m n b1 b2 c3 a4 a5 a6] p3 in
rew [fun c4 => ltn_xor_geq m n b1 b2 b3 c4 a5 a6] p4 in
rew [fun c5 => ltn_xor_geq m n b1 b2 b3 b4 c5 a6] p5 in
rew [fun c6 => ltn_xor_geq m n b1 b2 b3 b4 b5 c6] p6 in x') = x ->
P x with
| LtnNotGeq ltn_mn => _
| GeqNotLtn leq_nm => _
end erefl erefl erefl erefl erefl erefl erefl).
move=> p1 p2 p3 p4 p5 p6 <-.
by exact (H1 ltn_mn p1 p2 p3 p4 p5 p6).
move=> p1 p2 p3 p4 p5 p6 <-.
by exact (H2 leq_nm p1 p2 p3 p4 p5 p6).
Defined.
a = b 型の項 H があるときに、rew H in term で、term と同じだがその型の中の a を b に変えたものとなるのだと思うが、 意図したところを書き換えてくれない場合は rew [f] H in term として、f でどこを書き換えるか指定する。
上のコードを見ればなんとなくわかるかと思うが、refine の中では、ltn_xor_geq m n b1 b2 b3 b4 b5 b6 型の x' を 6回書き換えて、ltn_xor_geq m n a1 a2 a3 a4 a5 a6 型に変えている。
なお、記法を使って書いただけで、中身の項は同じ (eq_rect を使っている) なので、以下のように ltn_xor_geq_case = ltn_xor_geq_case2 を証明できる。
Goal ltn_xor_geq_case = ltn_xor_geq_case2. Proof. reflexivity. Qed.
rew を使うことでマシにはなったが、やはり長いので、インデックスをまとめることはできないか考えて、以下のようにしてみた。
6個のインデックスを 6個の引数で受けとるのでなく、6要素のタプルで受け取る ltn_xor_geq' という定義を行って、 これを使って場合分けの補題を証明したところ以下のようになった。
Definition ltn_xor_geq' m n args :=
let: (a1, a2, a3, a4, a5, a6) := args in
ltn_xor_geq m n a1 a2 a3 a4 a5 a6.
Lemma ltn_xor_geq_case3 :
forall m n a1 a2 a3 a4 a5 a6 (P : ltn_xor_geq m n a1 a2 a3 a4 a5 a6 -> Prop),
(forall (ltn_mn : m < n) (pf : (m, m, n, n, false, true) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (LtnNotGeq (m:=m) (n:=n) ltn_mn : ltn_xor_geq' m n (m, m, n, n, false, true)))) ->
(forall (leq_nm : n <= m) (pf : (n, n, m, m, true, false) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (GeqNotLtn (m:=m) (n:=n) leq_nm : ltn_xor_geq' m n (n, n, m, m, true, false)))) ->
(forall x, P x).
Proof.
move=> m n a1 a2 a3 a4 a5 a6 P H1 H2 x.
refine (match x as x' in ltn_xor_geq _ _ b1 b2 b3 b4 b5 b6
return forall (pf : (b1, b2, b3, b4, b5, b6) = (a1, a2, a3, a4, a5, a6)),
(rew pf in (x' : ltn_xor_geq' m n (b1, b2, b3, b4, b5, b6))) = x -> P x with
| LtnNotGeq ltn_mn => _
| GeqNotLtn leq_nm => _
end erefl erefl).
clear H2.
move=> pf; move: (pf).
case: pf => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H1 x *.
move=> pf <-.
by exact (H1 ltn_mn pf).
clear H1.
move=> pf; move: (pf).
case: pf => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H2 x *.
move=> pf <-.
by exact (H2 leq_nm pf).
Qed.
rew がたくさん (6*3=18回) あったのが、3回で済んでいる。
そのぶん、証明の中でタプルの分解などが必要になるのですこし長くなっているが、問題ないレベルだと思う。
ちょっと素直でなかったのは、前提の (LtnNotGeq (m:=m) (n:=n) ltn_mn : ltn_xor_geq' m n (m, m, n, n, false, true)) の部分で、明示的に cast を書いて ltn_xor_geq m n m m n n false true 型から ltn_xor_geq' m n (m, m, n, n, false, true) 型に変えないと 型検査を通らなかった。
タプルにしたことで match の return 節は等式ふたつにできたが、 rew を使っているので、ふたつめの等式が非対称になっている。
これをどうにかできないか考えて、sigT 型を使って、existT の等式にすればよいと気がついた。
sigT は依存ペアというやつで、以下の帰納型と定義されている。
Inductive sigT [A : Type] (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}.
右端の {x : A & P x} は sigT P の記法である。
ここで興味深いのは、sigT P 型の値 existT P x p には、(x : A) と (p : P x) が含まれているが、 existT P x p の型は sigT P であり、x は含まれていないことである。
そのため、p1 と p2 の型が P x1 と P x2 というように違っても、existT P x1 p1 と existT P x2 p2 はどちらも sigT P 型であり、 existT P x1 p1 = existT P x2 p2 という等式は型エラーにならない。
そのため、refine のところで rew (eq_rect) を使わないで済む。
また、ペアの等式は、第1要素同士の等式と第2要素同士の等式のふたつと等価なので、等式をひとつにまとめられる。
というわけで refine で追加する等式にこれを使い、以下のように証明できる。
Require Import EqdepFacts.
Lemma ltn_xor_geq_case4 :
forall m n a1 a2 a3 a4 a5 a6 (P : ltn_xor_geq m n a1 a2 a3 a4 a5 a6 -> Prop),
(forall (ltn_mn : m < n) (pf : (m, m, n, n, false, true) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (LtnNotGeq (m:=m) (n:=n) ltn_mn : ltn_xor_geq' m n (m, m, n, n, false, true)))) ->
(forall (leq_nm : n <= m) (pf : (n, n, m, m, true, false) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (GeqNotLtn (m:=m) (n:=n) leq_nm : ltn_xor_geq' m n (n, n, m, m, true, false)))) ->
(forall x, P x).
Proof.
move=> m n a1 a2 a3 a4 a5 a6 P H1 H2 x.
refine (match x as x' in ltn_xor_geq _ _ b1 b2 b3 b4 b5 b6
return
existT (ltn_xor_geq' m n) (b1, b2, b3, b4, b5, b6) x' =
existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x ->
P x with
| LtnNotGeq ltn_mn => _
| GeqNotLtn leq_nm => _
end erefl).
clear H2.
move=> pf.
case: (eq_sigT_fst pf) => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H1 x pf *.
rewrite -(eq_sigT_snd pf).
by exact (H1 ltn_mn (eq_sigT_fst pf)).
clear H1.
move=> pf.
case: (eq_sigT_fst pf) => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H2 x pf *.
rewrite -(eq_sigT_snd pf).
by exact (H2 leq_nm (eq_sigT_fst pf)).
Defined.
existT (ltn_xor_geq' m n) (b1, b2, b3, b4, b5, b6) x' = existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x という等式ひとつで、 インデックス 6個 (a1, a2, a3, a4, a5, a6) と場合分け対象の x の等値性を示している。
ここで existT P x1 p1 = existT P x2 p2 の証明 pf から、x1 = x1 と p2 = p2 を取り出す必要がある。 このために、EqdepFacts.eq_sigT_fst と EqdepFacts.eq_sigT_snd を使っている。
eq_sigT_fst : forall [X : Type] [P : X -> Type] [x1 x2 : X] [H1 : P x1] [H2 : P x2], existT P x1 H1 = existT P x2 H2 -> x1 = x2 eq_sigT_snd : forall [X : Type] [P : X -> Type] [x1 x2 : X] [H1 : P x1] [H2 : P x2] (H : existT P x1 H1 = existT P x2 H2), rew [P] eq_sigT_fst H in H1 = H2
x1 と x2 は両方 X 型なので、x1 = x2 はそのまま取り出せる。 p1 と p2 は P x1 型と P x2 型と異なるので、取り出せるのは rew を使って型を合わせた等式 rew [P] eq_sigT_fst pf in p1 = p2 となる。
(Coq.Init.Specif で定義されている projT1_eq と projT2_eq も使えることがあるが、結果がシンプルでないため rewrite に使おうとするとうまくマッチしてくれないので、eq_sigT_fst と eq_sigT_sndeq_sigT_snd を使う)
ltn_xor_geq_case4 の場合、そうやって rew を使った等式がそのまま使える形の前提が与えられるようにしてあるので、 その前提を使えば証明が終わる。
(eq_sigT_snd で取り出される等式は左辺だけに rew が使われていて非対称だが、型が同じになることがわかっている状況では、Eqdep_dec.inj_pair2_eq_dec を使うと rew がない対称的な等式をすぐに得られる。後述する)
なお、当然、ltn_xor_geq_case4 を利用する側では rew を消したくなるが、 公理を使わずに rew を消すには、Eqdep_dec.eq_rect_eq_dec を使う。 ここで、x1 と x2 が同じであり、さらに X 型に decidable equality が必要となる。 x1 と x2 が同じというのは eq_sigT_fst で得た等式が与えられるので、それで x2 を x1 に変えてから Eqdep_dec.eq_rect_eq_dec を使えばよい。 また、ltn_xor_geq_case4 の場合、decidable equality が必要になるのは nat * nat * nat * nat * bool * bool であり、 nat と bool の prod による組み合わせである。 SSReflect によって、この型は eqType とみなされるので decidable equality は簡単に得られる。
上記のコードでは refine で match 式を直接与えているが、refine を使わずに同じことをやることも不可能ではない
Lemma ltn_xor_geq_case5 :
forall m n a1 a2 a3 a4 a5 a6 (P : ltn_xor_geq m n a1 a2 a3 a4 a5 a6 -> Prop),
(forall (ltn_mn : m < n) (pf : (m, m, n, n, false, true) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (LtnNotGeq (m:=m) (n:=n) ltn_mn : ltn_xor_geq' m n (m, m, n, n, false, true)))) ->
(forall (leq_nm : n <= m) (pf : (n, n, m, m, true, false) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (GeqNotLtn (m:=m) (n:=n) leq_nm : ltn_xor_geq' m n (n, n, m, m, true, false)))) ->
(forall x, P x).
Proof.
move=> m n a1 a2 a3 a4 a5 a6 P H1 H2 x.
move: (erefl (existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x)).
set a1' := {2}a1.
set a2' := {2}a2.
set a3' := {2}a3.
set a4' := {2}a4.
set a5' := {2}a5.
set a6' := {2}a6.
move: {2 3}x => x'.
case: x => [ltn_mn|leq_nm].
rewrite {}/a1' {}/a2' {}/a3' {}/a4' {}/a5' {}/a6'.
rename x' into x.
clear H2.
move=> pf.
case: (eq_sigT_fst pf) => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H1 x pf *.
rewrite -(eq_sigT_snd pf).
by exact (H1 ltn_mn (eq_sigT_fst pf)).
rewrite {}/a1' {}/a2' {}/a3' {}/a4' {}/a5' {}/a6'.
rename x' into x.
clear H1.
move=> pf.
case: (eq_sigT_fst pf) => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H2 x pf *.
rewrite -(eq_sigT_snd pf).
by exact (H2 leq_nm (eq_sigT_fst pf)).
Defined.
Goal ltn_xor_geq_case4 = ltn_xor_geq_case5.
Proof. reflexivity. Qed.
ここでは、move: (erefl (existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x)) で goal に existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x = existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x という等式を加え、 set a1' := {2}a1 から move: {2 3}x => x' で case に書き換えられたくない変数を細工している。 (set ではあとで戻す必要があるので set tactic で let-in を導入し、x は戻さなくてよいので move で discharge/introduction している。あと、x を let-in の導入でやろうとしたら場合分けでエラーになったのでそうした)
その後で case: x で場合分けすると、ltn_xor_geq_case4 で refine で導入した match 式と同じものを生成できる。
これは本当に同じ (convertible な) 式になるので、ltn_xor_geq_case4 = ltn_xor_geq_case5 という命題を reflexivity で証明できる。
ただ正直なところ、これは match 式を直接書いた方がわかりやすいと思う。
場合分けしないものをガードする、 case のところでなにか指定できたような、と思って試すと、以下のようにできるようだ
Lemma ltn_xor_geq_case6 :
forall m n a1 a2 a3 a4 a5 a6 (P : ltn_xor_geq m n a1 a2 a3 a4 a5 a6 -> Prop),
(forall (ltn_mn : m < n) (pf : (m, m, n, n, false, true) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (LtnNotGeq (m:=m) (n:=n) ltn_mn : ltn_xor_geq' m n (m, m, n, n, false, true)))) ->
(forall (leq_nm : n <= m) (pf : (n, n, m, m, true, false) = (a1, a2, a3, a4, a5, a6)),
P (rew pf in (GeqNotLtn (m:=m) (n:=n) leq_nm : ltn_xor_geq' m n (n, n, m, m, true, false)))) ->
(forall x, P x).
Proof.
move=> m n a1 a2 a3 a4 a5 a6 P H1 H2 x.
move: (erefl (existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x)).
case: {1}a1 {1}a2 {1}a3 {1}a4 {1}a5 {1}a6 / {1}x => [ltn_mn|leq_nm].
clear H2.
move=> pf.
case: (eq_sigT_fst pf) => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H1 x pf *.
rewrite -(eq_sigT_snd pf).
by exact (H1 ltn_mn (eq_sigT_fst pf)).
clear H1.
move=> pf.
case: (eq_sigT_fst pf) => e1 e2 e3 e4 e5 e6.
rewrite -{}e1 -{}e2 -{}e3 -{}e4 -{}e5 -{}e6 in P H2 x pf *.
rewrite -(eq_sigT_snd pf).
by exact (H2 leq_nm (eq_sigT_fst pf)).
Defined.
これならかなりマシかも
ここで case: {1}a1 {1}a2 {1}a3 {1}a4 {1}a5 {1}a6 / {1}x の直前でゴールは以下のようになっている
existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x = existT (ltn_xor_geq' m n) (a1, a2, a3, a4, a5, a6) x -> P x
1 1 1 1 1 1 1 2 2 2 2 2 2 2 3
a1, a2, a3, a4, a5, a6, x の出現の番号を下に付記してあるが、 場合分けで変えたいのは 1番目の a1, a2, a3, a4, a5, a6, x であり、 それ以降のは変えたくない。 なので、case: {1}a1 {1}a2 {1}a3 {1}a4 {1}a5 {1}a6 / {1}x とぜんぶに 1 とつけてある。
自前で変えたくないのをガードするのは以下のようになっていて、変えたくないものを指定していた
set a1' := {2}a1.
set a2' := {2}a2.
set a3' := {2}a3.
set a4' := {2}a4.
set a5' := {2}a5.
set a6' := {2}a6.
move: {2 3}x => x'.
まぁ、変えたいものを指定するほうが直感的だよな
せっかく existT の等式を使う方法を思いついたので、Vector.case0, Vector.caseS', eq_case, le_case の証明をやりなおしてみる。
From mathcomp Require Import all_ssreflect.
Require Import EqdepFacts.
Require Import Eqdep_dec.
Require Vector.
Definition vector_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.
refine (match v as v' in Vector.t _ n'
return existT (Vector.t A) n' v' = existT (Vector.t A) 0 v -> P v with
| Vector.nil => _
| Vector.cons h n t => _
end erefl).
(* existT (Vector.t A) 0 (Vector.nil A) = existT (Vector.t A) 0 v -> P v *)
move=> pf.
by rewrite -(inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ pf).
(* existT (Vector.t A) n.+1 (Vector.cons A a n t) = existT (Vector.t A) 0 v -> P v *)
move=> pf.
by move: (eq_sigT_fst pf).
Defined.
Definition 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.
move=> A n v P H.
refine (match v as v' in Vector.t _ n'
return existT (Vector.t A) n' v' = existT (Vector.t A) n.+1 v -> P v with
| Vector.nil => _
| Vector.cons h n' t => _
end erefl).
(* existT (Vector.t A) 0 (Vector.nil A) = existT (Vector.t A) n.+1 v -> P v *)
move=> pf.
by move: (eq_sigT_fst pf).
(* existT (Vector.t A) n0.+1 (Vector.cons A a n0 t) = existT (Vector.t A) n.+1 v -> P v *)
move=> pf.
move: (eq_sigT_fst pf) => [] eq_nn.
rewrite {n'}eq_nn in t pf.
by rewrite -(inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ pf).
Defined.
Lemma eq_case :
forall (T : Type) (x y : T) (P : x = y -> Prop),
(forall (pf : x = y), P (eq_rect x (eq x) erefl y pf)) ->
(forall e, P e).
Proof.
move=> T x y P H e.
refine (match e as e' in _ = y'
return existT (eq x) y' e' = existT (eq x) y e -> P e with
| erefl => _
end erefl).
move=> pf.
move: (e) pf => e'.
rewrite -{y}e in P H e' * => pf.
rewrite -(eq_sigT_snd pf).
by apply H.
Defined.
Lemma le_case :
forall a b (P : le a b -> Prop),
(forall (pf : a = b), P (eq_rect a (le a) (le_n a) b pf)) ->
(forall b' (pf : b'.+1 = b) (x : le a b'), P (eq_rect b'.+1 (le a) (le_S a b' x) b pf)) ->
(forall x, P x).
Proof.
move=> a b P H1 H2 x.
refine (match x as x' in le _ b'
return existT (le a) b' x' = existT (le a) b x -> P x with
| le_n => _
| le_S b' le_ab' => _
end erefl).
move=> pf.
by move: (eq_sigT_snd pf) => <-.
move=> pf.
by move: (eq_sigT_snd pf) => <-.
Defined.
どれもとくに問題なく証明できる。
また、EqdepFacts.eq_sigT_snd を使うと rew が出てきてしまうが、 Eqdep_dec.inj_pair2_eq_dec を使うと (decidable equality を与えることで) rew なしの等式を直接得られる。 左辺右辺の対称性をたもちながら変形をすすめられてよいので、使える場合にはこれをつかっている。
EqdepFacts と Eqdep_dec を調べると、 EqdepFacts.eq_dep というのがあることに気がつく。
これは JMeq みたいに両辺の型が一致していない等式の帰納型で、 さらに JMeq と異なり（インデックスに decidable equality がある場合は）公理を使わずに eq に変換できるようだ。
これは existT の等式と等価で、その等価性は EqdepFacts に以下の定理として証明されている
Lemma eq_sigT_iff_eq_dep :
forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
existT P p x = existT P q y <-> eq_dep p x q y.
existT の等式のかわりに eq_dep を使って vector_case0, vector_caseS', eq_case, le_case を証明してみたが、 だいたい同じで、利点は感じられなかった。 （implicit argument になっていなくて引数に _ を書く必要があったところがけっこうあったのとか、eq_sigT_fst に相当する定理がみあたらなくて eq_dep_eq_sigT で existT の等式に変換してから eq_sigT_fst を使う必要があったとか、むしろ少し不便）
あと下で述べるが、Vector.Forall などでは existT をネストさせる必要があり、 その内側の existT の部分に eq_dep を使うことはできず、結局 existT は必要になる
ltn_xor_geq で、複数のインデックスがある帰納型の場合分け補題を証明したが、 インデックスはどれも単純な型 (nat と bool) で、依存型ではなかった。
インデックスに依存型がある帰納型はあまりないのだが、禁止されているわけではなく、使われることはある。
たとえば VectorDef には、 Forall や Exists といった帰納型があって、インデックスの部分に依存型が使われている。 これらは Vector.t という依存型に対する述語なので、インデックスに依存型が出てくるのである。
Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
|Forall_nil: Forall P []
|Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v).
Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop :=
|Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v)
|Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v).
"Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop" の forall {n} (v: t A n) という部分がインデックスの指定なので、n と v がインデックスだが、v の型は Vector.t A n であり、n というインデックスが v の型の中で参照されている。
Vector.Forall は、Forall_nil と Forall_cons があって、リストみたいな構造である。 Forall_nil が空リストで、 Forall_cons でリストを伸ばす毎に要素 (x : A) とその x に関する P の証明 (pf : P x) が追加されていく。 その結果、各要素 x についての P の証明 (pf : P x) がリストのように並ぶことになる。 そういうリストが、ちょうどそれぞれの要素のリスト (Vector.t) をインデックスとする型 (Vector.Forall) に値として割り当てられる。
結局、インデックスに Vector.t の値があって、Vector.t の値それぞれについて型があり、 その型に入れられる証明は対象の Vector.t の値と同じ形で選択肢がないため、 (P x の証明に一意性があれば) Vector.Forall の証明にも一意性が成り立ちそうである。
Vector.Exists は、Vector.t の先頭要素が述語 P を満たす (Exists_cons_hd)、もしくは 後続のいずれかの要素が述語 P を満たす (Exists_cons_tl) という構造になっている。 こちらは、先頭要素と後続の要素のどちらにも P を満たす要素がある場合、どちらを選んでも証明できるので、 証明の一意性はなさそうである。
とりあえず、Vector.Forall を場合分けできるだろうか。
まぁ、Vector.Forall とかの証明をデータの中に埋め込むことは考えていないので、 純粋に、インデックスつき帰納型の場合分けがどこまで可能なのかということに興味があるだけである。
ということで挑戦してみたところ、Vector.Forall の場合分け補題を証明できた。 また、証明の一意性も証明できた。 公理は使っていない。 (A が eqType であることと P a の証明の一意性が前提として必要になった。)
(Vector.Exists については試していないが、場合分け補題はたぶん証明可能だと思う。証明の一意性はそもそも一意でないので証明できないはず)
どうやったか以下に示す。
From mathcomp Require Import all_ssreflect.
Require Import EqdepFacts.
Require Import Eqdep_dec.
Require Vector.
Import EqNotations.
Print Vector.Forall.
(*
Inductive Forall (A : Type) (P : A -> Prop) : forall n : nat, Vector.t A n -> Prop :=
Forall_nil : Vector.Forall P (Vector.nil A)
| Forall_cons : forall (n : nat) (x : A) (v : Vector.t A n),
P x -> Vector.Forall P v -> Vector.Forall P (Vector.cons A x n v).
*)
About Vector.Forall.
(*
Vector.Forall : forall {A : Type}, (A -> Prop) -> forall n : nat, Vector.t A n -> Prop
Vector.Forall is not universe polymorphic
Arguments Vector.Forall {A}%type_scope P%function_scope {n}%nat_scope v
Expands to: Inductive Coq.Vectors.Vector.Forall (syntactically equal to Coq.Vectors.VectorDef.Forall)
*)
まず、インデックスがふたつあると、existT P p x という形で書けないので、インデックスがひとつの形の型が必要である。 (p がインデックスだが、ここに n と v を入れたい) ltn_xor_geq_case4 ではタプルとしたが、今回は依存型なので依存ペアを使う。 n と v を依存ペア sigT (Vector.t A) 型の値としてまとめたものをインデックスとして受け取り、もともとの Vector.Forall 型を返す関数を作る。
Definition vector_forall {A : Type} (P : A -> Prop) (dv : sigT (Vector.t A)) :=
match dv with
| existT n v => @Vector.Forall A P n v
end.
あと、decidable equality が必要なので、先に証明しておく。
eqType ならなんでも decidable equality があるというのは以下のように証明できる。
Lemma eqtype_dec {T : eqType} (x y : T) : {x = y} + {x <> y}.
Proof.
by case: (boolP (x == y)) => /eqP H; [left|right].
Qed.
sigT (Vector.t A) 型の値は、A が eqType なら decidable equality がある。 これを以下のように証明する。
sigT (Vector.t A) 型は、Vector.t 型が中に入っているが、 インデックスの n は中に隠れていて型に含まれないので、 等式 x = y と書いたときに x と y の (中に入っている Vector.t の) 長さが同じである保証はない。 そこで、まず長さを比べて違っていたら違う項であると証明する。 長さが同じなら、長さについての帰納法を使う。
Lemma eqtype_sigvec_dec {A : eqType} (x y : sigT (Vector.t A)) : {x = y} + {x <> y}.
Proof.
case: x => nx vx.
case: y => ny vy.
(* まず長さを比べて、違っていたらそこから x <> y の証明をする *)
case: (PeanoNat.Nat.eq_dec nx ny); last first.
(* 長さが違っていた場合 *)
move=> Hn; right; move: Hn.
apply: contra_not => He.
by exact (eq_sigT_fst He).
(* 長さが同じ場合 *)
move=> Hn.
rewrite -{ny}Hn in vy *.
rename nx into n.
(* {existT (Vector.t A) n vx = existT (Vector.t A) n vy} + {existT (Vector.t A) n vx <> existT (Vector.t A) n vy} *)
(* 長さが同じと分かったからには existT は不要なので、外した形に変換する *)
suff: ({vx = vy} + {vx <> vy}).
case.
by move=> Hv; left; rewrite -Hv.
move=> Hv; right; move: Hv.
apply: contra_not => He.
by exact (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ He).
(* n についての帰納法で証明する *)
elim: n vx vy.
(* 長さ 0 の場合はどちらも Vector.nil なので vx = vy が証明できる *)
move=> vx vy.
left.
pattern vx; apply Vector.case0.
pattern vy; apply Vector.case0.
by [].
(* 長さ 1以上の場合 *)
move=> n IH vx vy.
pattern vx; apply Vector.caseS' => hx tx.
pattern vy; apply Vector.caseS' => hy ty.
(* 先頭要素を比較する *)
case: (eqtype_dec hx hy); last first.
(* 要素が異なるなら、vx <> vy が証明できる *)
move=> Hh; right; move: Hh.
apply: contra_not.
by case/Vector.cons_inj.
move=> <- {hy}; rename hx into h.
(* 帰納法の仮定により先頭要素を除いた残り比較する *)
case: (IH tx ty).
(* 一致する場合は全体が一致して、vx = vy が証明できる *)
move=> <- {ty}.
by left.
(* 一致しない場合は vx <> vy が証明できる *)
move=> Ht; right; move: Ht.
apply: contra_not.
by case/Vector.cons_inj.
Qed.
Vector.Forall の場合分け補題を証明する。 match の中で導入する等式は existT (vector_forall P) (existT (Vector.t A) n' v') q' = existT (vector_forall P) (existT (Vector.t A) n v) q であり、 existT がネストしている。 sigT 型にはインデックスの値が含まれないため、等式 (eq) を使うことができる。
Lemma vector_forall_case :
forall (A : eqType) (P : A -> Prop) (n : nat) (v : Vector.t A n)
(Q : Vector.Forall P v -> Prop),
(forall (e : existT (Vector.t A) 0 (Vector.nil A) = existT (Vector.t A) n v),
Q (rew e in (Vector.Forall_nil P : vector_forall P (existT (Vector.t A) 0 (Vector.nil A))))) ->
(forall n1 x1 v1 px1 vp1 (e : existT (Vector.t A) n1.+1 (Vector.cons A x1 n1 v1) = existT (Vector.t A) n v),
Q (rew e in (Vector.Forall_cons P x1 v1 px1 vp1 : vector_forall P (existT (Vector.t A) n1.+1 (Vector.cons A x1 n1 v1))))) ->
(forall q, Q q).
Proof.
move=> A P n v Q H1 H2 q.
refine (match q as q' in @Vector.Forall _ _ n' v'
return existT (vector_forall P) (existT (Vector.t A) n' v') q' =
existT (vector_forall P) (existT (Vector.t A) n v ) q ->
Q q with
| Vector.Forall_nil => _
| Vector.Forall_cons n1 x1 v1 px1 vp1 => _
end erefl).
clear H2.
move=> pf.
case: (eq_sigT_fst pf) => eq_n eq_v.
rewrite -{}eq_n in v Q H1 q pf eq_v *.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_v) => {}eq_v.
rewrite -{}eq_v in Q H1 q pf *.
move: (inj_pair2_eq_dec _ eqtype_sigvec_dec _ _ _ _ pf) => <-.
move: (H1 (eq_sigT_fst pf)).
by rewrite -(eq_rect_eq_dec eqtype_sigvec_dec).
clear H1.
move=> pf.
case: (eq_sigT_fst pf) => eq_n eq_v.
rewrite -{n}eq_n in v Q H2 q pf eq_v *.
rewrite -(inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_v) in Q H2 q pf * => {v eq_v}.
rewrite -(inj_pair2_eq_dec _ eqtype_sigvec_dec _ _ _ _ pf).
move: (H2 n1 x1 v1 px1 vp1 (eq_sigT_fst pf)).
by rewrite -(eq_rect_eq_dec eqtype_sigvec_dec).
Defined.
Print Assumptions vector_forall_case. (* closed *)
Vector.Forall の証明の一意性を証明する。 n による帰納法を使って、vector_forall_case による場合分けを行う。
Lemma vector_forall_irrelevance :
forall (A : eqType) (P : A -> Prop)
(P_irrelevance : forall (a : A) (p1 p2 : P a), p1 = p2)
(n : nat) (v : Vector.t A n)
(q1 q2 : Vector.Forall P v), q1 = q2.
Proof.
move=> A P P_irrelevance.
elim.
move=> v q1 q2.
pattern q1; apply vector_forall_case.
move=> e1.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ e1) => e.
rewrite -{}e in q1 q2 e1 *.
rewrite -(eq_rect_eq_dec eqtype_sigvec_dec) => {e1}.
pattern q2; apply vector_forall_case.
move=> e2.
by rewrite -(eq_rect_eq_dec eqtype_sigvec_dec) => {e2}.
move=> n1 x1 v1 px1 vp1 e2; exfalso.
by move: (eq_sigT_fst e2).
move=> n1 x1 v1 px1 vp1 e1; exfalso.
by move: (eq_sigT_fst e1).
move=> n IH v q1 q2.
pattern q1; apply vector_forall_case.
move=> e1; exfalso.
by move: (eq_sigT_fst e1).
move=> n1 x1 v1 px1 vp1 e1.
case: (eq_sigT_fst e1) => eq_n.
rewrite {n1}eq_n in v1 px1 vp1 e1 *.
move: (inj_pair2_eq_dec nat PeanoNat.Nat.eq_dec (Vector.t A) n.+1 _ _ e1) => eq_v.
rewrite -{v}eq_v in q1 q2 px1 vp1 e1 *.
rewrite -(eq_rect_eq_dec eqtype_sigvec_dec) => {e1}.
pattern q2; apply vector_forall_case.
move=> e2; exfalso.
by move: (eq_sigT_fst e2).
move=> n2 x2 v2 px2 vp2 e2.
case: (eq_sigT_fst e2) => eq_n.
rewrite {n2}eq_n in v2 px2 vp2 e2 *.
move: (inj_pair2_eq_dec nat PeanoNat.Nat.eq_dec (Vector.t A) n.+1 _ _ e2) => /Vector.cons_inj [] eq_x eq_v.
rewrite {x2}eq_x in px2 vp2 e2 *.
rewrite {v2}eq_v in vp2 e2 *.
rewrite -(eq_rect_eq_dec eqtype_sigvec_dec) => {e2}.
rewrite -(P_irrelevance x1 px1 px2).
rewrite -(IH v1 vp1 vp2).
by [].
Qed.
Print Assumptions vector_forall_irrelevance. (* closed *)Vector.Forall は、インデックスがふたつあって、右の値が左の型の中に入っている、 というインデックスに依存型があるもののなかで最小限のものだった
もうちょっと複雑なものとして、Vector.Forall2 の場合分けと証明の一意性を考えよう
Print Vector.Forall2.
(*
Inductive Forall2 (A B : Type) (P : A -> B -> Prop) : forall n : nat, Vector.t A n -> Vector.t B n -> Prop :=
Forall2_nil : Vector.Forall2 P (Vector.nil A) (Vector.nil B)
| Forall2_cons : forall (m : nat) (x1 : A) (x2 : B) (v1 : Vector.t A m) (v2 : Vector.t B m),
P x1 x2 ->
Vector.Forall2 P v1 v2 -> Vector.Forall2 P (Vector.cons A x1 m v1) (Vector.cons B x2 m v2).
Arguments Vector.Forall2 {A B}%type_scope P%function_scope {n}%nat_scope _ _
Arguments Vector.Forall2_nil {A B}%type_scope P%function_scope
Arguments Vector.Forall2_cons {A B}%type_scope P%function_scope {m}%nat_scope x1 x2 v1 v2 _ _
*)
Vector.Forall2 はインデックスが 3個あって、forall n : nat, Vector.t A n -> Vector.t B n -> となっている。 まぁ、名前のとおりひとつじゃなくて 2個の vector に対する述語である
これを場合分けするには、この 3個の値を含む sigT 型を作らなければならない。 そして、そのインデックスは 2個の vector を含む sigT 型となる。
そのために、vector_pair と vector_forall2 を以下のように定義する。
Definition vector_pair (A B : Type) (n : nat) : Type := Vector.t A n * Vector.t B n.
Definition vector_forall2 {A B : Type} (P : A -> B -> Prop) (dvv : sigT (vector_pair A B)) : Type :=
let: existT n (va, vb) := dvv in
Vector.Forall2 P va vb.
これにより、ある Vector.Forall2 P 型の値 pf を existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf という形に existT でくるむことができる。 この項の型は sigT (vector_forall2 P) という、値 (n, va, vb) に依存しない型となるので、 この項を左右に持つ等式を用意すれば、左辺の中身の (内部的な型を変えてしまうような) 書き換えが可能となる。
まず、sigT (vector_pair A B) の decidable equality を証明する。 これは、eqtype_sigvec_dec と同様である。
Lemma eqtype_sigvec2_dec {A B : eqType} (x : sigT (vector_pair A B)) (y : sigT (vector_pair A B)) : {x = y} + {x <> y}.
Proof.
case: x => nx vvx.
case: y => ny vvy.
case: (PeanoNat.Nat.eq_dec nx ny); last first.
move=> H; right; move: H.
apply: contra_not.
move=> eq_nv.
by move: (eq_sigT_fst eq_nv).
move=> eq_n.
subst ny; rename nx into n.
suff: {vvx = vvy} + {vvx <> vvy}.
case => H.
left.
by subst vvy.
right.
move: H.
apply: contra_not => eq_vv.
by exact (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_vv).
elim: n vvx vvy.
move=> vvx vvy.
left.
case: vvx => vxa vxb.
case: vvy => vya vyb.
pattern vxa; apply Vector.case0.
pattern vxb; apply Vector.case0.
pattern vya; apply Vector.case0.
pattern vyb; apply Vector.case0.
by[].
move=> n IH vvx vvy.
case: vvx => vxa vxb.
case: vvy => vya vyb.
pattern vxa; apply Vector.caseS' => hxa txa.
pattern vxb; apply Vector.caseS' => hxb txb.
pattern vya; apply Vector.caseS' => hya tya.
pattern vyb; apply Vector.caseS' => hyb tyb.
case: (eqtype_dec hxa hya) => eq_ha; last first.
right.
by move: eq_ha; apply: contra_not => - [].
subst hya; rename hxa into ha.
case: (eqtype_dec hxb hyb) => eq_hb; last first.
right.
by move: eq_hb; apply: contra_not => - [].
subst hyb; rename hxb into hb.
case: (IH (txa,txb) (tya,tyb)) => eq_t; last first.
right.
move: eq_t; apply: contra_not => - [] => eq_ta eq_tb.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_ta) => <-.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_tb) => <-.
by [].
case: eq_t => eq_ta eq_tb.
subst tya tyb; rename txa into ta; rename txb into tb.
by left.
Qed.
場合分けの補題を証明する。 今回は、existT の等式を追加するだけの定理としてみた。 どうせゴール自体は変えないので、ゴールが Q q という形になっている必要はないだろう。 また、そうすることにより、eq_rect を使わなくて済む。
Lemma vector_forall2_case
{A B : Type} {P : A -> B -> Prop} {n : nat} {va : Vector.t A n} {vb : Vector.t B n}
(pf : Vector.Forall2 P va vb)
{Q : Prop}
{H1 : existT (vector_forall2 P) (existT (vector_pair A B) 0 (Vector.nil A, Vector.nil B)) (Vector.Forall2_nil P) =
existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf -> Q}
{H2 : forall ha hb m ta tb ph pt,
existT (vector_forall2 P) (existT (vector_pair A B)
m.+1 (Vector.cons A ha m ta, Vector.cons B hb m tb)) (Vector.Forall2_cons P ha hb ta tb ph pt) =
existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf -> Q} :
Q.
Proof.
refine (match pf as pf' in @Vector.Forall2 _ _ _ n' va' vb'
return existT (vector_forall2 P) (existT (vector_pair A B) n' (va',vb')) pf' =
existT (vector_forall2 P) (existT (vector_pair A B) n (va ,vb )) pf ->
Q with
| Vector.Forall2_nil => _
| Vector.Forall2_cons m ha hb ta tb ph pt => _
end erefl).
by exact H1.
by apply: H2.
Defined.
なお、refine を使わないでも、以下のように証明できる。ただし、置き換える出現を指定するときに {1 2 3}n と指定しなければならないのはちょっと難しい。
Lemma vector_forall2_case'
{A B : Type} {P : A -> B -> Prop} {n : nat} {va : Vector.t A n} {vb : Vector.t B n}
(pf : Vector.Forall2 P va vb)
{Q : Prop}
{H1 : existT (vector_forall2 P) (existT (vector_pair A B) 0 (Vector.nil A, Vector.nil B)) (Vector.Forall2_nil P) =
existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf -> Q}
{H2 : forall ha hb m ta tb ph pt,
existT (vector_forall2 P) (existT (vector_pair A B)
m.+1 (Vector.cons A ha m ta, Vector.cons B hb m tb)) (Vector.Forall2_cons P ha hb ta tb ph pt) =
existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf -> Q} :
Q.
Proof.
move: (erefl (existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf)).
case: {1 2 3}n {1}va {1}vb / {1}pf.
by exact H1.
move=> m ha hb ta tb ph pt.
by apply: H2.
Defined.
これは、existT (vector_forall2 P) (existT (vector_pair A B) n (va, vb)) pf に n は一見 1回しか現れていないように見えるが、じつは
@existT (@sigT nat (vector_pair A B)) (@vector_forall2 A B P) (@existT nat (vector_pair A B) n (@pair (Vector.t A n) (Vector.t B n) va vb)) pf
1 2 3 1 1 1
という項なので、3回出現しており、そのために {1 2 3}n と指定しなければならない。 ({in LHS} と書ければいいのだが、書けないようだ。) この形で書けば、場合分けは 2行 (move: と case:) で済むので、補題を作らなくてもいいかもしれないが、補題を作れば、出現の情報 {1 2 3} を毎回書かなくても済むのは利点だな
長いけどいちおうゴール全体も書いておく (出現の番号も)
forall _ : @eq (@sigT (@sigT nat (vector_pair A B)) (@vector_forall2 A B P)) (@existT (@sigT nat (vector_pair A B)) (@vector_forall2 A B P) (@existT nat (vector_pair A B) n (@pair (Vector.t A n) (Vector.t B n) va vb)) pf) (@existT (@sigT nat (vector_pair A B)) (@vector_forall2 A B P) (@existT nat (vector_pair A B) n (@pair (Vector.t A n) (Vector.t B n) va vb)) pf), Q
1 2 3 1 1 1 4 5 6 2 2 2
Vector.Forall2 の証明の一意性を証明する。
vector_forall2_case が existT の等式を追加するだけになったので、 こちらでは、vector_forall2_case で場合分けし、 eq_sigT_fst で取り出した等式でインデックスを同じ形にして、 inj_pair2_eq_dec で等式を取り出して書き換える、という感じで証明を進めている。 このやりかたをしている限りは、eq_rect は出てこない。
Lemma vector_forall2_irrelevance :
forall (A B : eqType) (P : A -> B -> Prop)
(P_irrelevance : forall (a : A) (b : B) (p1 p2 : P a b), p1 = p2)
(n : nat) (va : Vector.t A n) (vb : Vector.t B n)
(q1 q2 : Vector.Forall2 P va vb), q1 = q2.
Proof.
move=> A B P P_irrelevance.
elim.
move=> va vb q1 q2.
apply: (vector_forall2_case q1) => [eq_q1|ha hb m ta tb ph pt eq_q1].
move: (eq_sigT_fst eq_q1) => eq_vab.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_vab) => [] eq_va eq_vb.
subst va vb => {eq_vab}.
rewrite -(inj_pair2_eq_dec _ eqtype_sigvec2_dec _ _ _ _ eq_q1).
apply: (vector_forall2_case q2) => [eq_q2|ha hb m ta tb ph pt eq_q2].
by rewrite -(inj_pair2_eq_dec _ eqtype_sigvec2_dec _ _ _ _ eq_q2).
by move: (eq_sigT_fst (eq_sigT_fst eq_q2)).
by move: (eq_sigT_fst (eq_sigT_fst eq_q1)).
move=> n IH va vb q1 q2.
apply: (vector_forall2_case q1) => [eq_q1|ha1 hb1 m ta1 tb1 ph1 pt1 eq_q1].
by move: (eq_sigT_fst (eq_sigT_fst eq_q1)).
move: (eq_sigT_fst (eq_sigT_fst eq_q1)) => [] eq_mn; subst m.
move: (eq_sigT_fst eq_q1) => eq_vab.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_vab) => [] eq_va eq_vb.
subst va vb => {eq_vab}.
rewrite -(inj_pair2_eq_dec _ eqtype_sigvec2_dec _ _ _ _ eq_q1) => {q1 eq_q1}.
apply: (vector_forall2_case q2) => [eq_q2|ha2 hb2 m ta2 tb2 ph2 pt2 eq_q2].
by move: (eq_sigT_fst (eq_sigT_fst eq_q2)).
move: (eq_sigT_fst (eq_sigT_fst eq_q2)) => [] eq_mn; subst m.
move: (eq_sigT_fst eq_q2) => eq_vab.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_vab) => [] eq_ha eq_ta eq_hb eq_tb.
subst ha2 hb2; rename ha1 into ha; rename hb1 into hb.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_ta) => {}eq_ta.
subst ta2; rename ta1 into ta.
move: (inj_pair2_eq_dec _ PeanoNat.Nat.eq_dec _ _ _ _ eq_tb) => {}eq_tb.
subst tb2; rename tb1 into tb.
rewrite -(inj_pair2_eq_dec _ eqtype_sigvec2_dec _ _ _ _ eq_q2) => {q2 eq_q2}.
rewrite (P_irrelevance ha hb ph1 ph2).
rewrite (IH ta tb pt1 pt2).
by [].
Qed.
Print Assumptions vector_forall2_irrelevance. (* closed *)
あと、インデックスを rewrite で書き換えるのは面倒くさくなったので subst を使っている。 まぁ、変数を明示的に指定して消去するだけなら、意図以外の動作はしないだろう。 SSReflect 原理主義で subst 禁止なら、rewrite でやればよい。
インデックス付き帰納型の場合分けは、existT の等式を使うと少し簡単になり、 また、インデックスの中に依存型があるときにも対応できることがわかった
ただ、こんなものは使わないで済むほうがよくて、SSReflect の tuple や fintype で済むならそっちを使うほうがよい
インデックスがひとつの場合は、そのまま existT でも eq_rect でも扱える
インデックスが複数の場合で、依存型でない場合は、eq_rect ならたくさん並べて扱える。 (ltn_xor_geq' のように) インデックスをまとめた形で扱う型関数を用意すれば existT でも扱える
インデックスが複数の場合で、依存型の場合、 (vector_forall, vector_pair, vector_forall2 のような) インデックスをまとめた形で扱う型関数が用意して、 existT で扱える
あと繰り返すが、こんなものは使わないで済むほうがよくて、SSReflect の tuple や fintype で済むならそっちを使うほうがよい
[latest]