Ruby の identity base の Hash とそうでない Hash の包含判定についての証明をいろいろいじって短くしてみた。 1289行から736行に減った。
ファイル全体は <URL:https://gist.github.com/akr/3f0fcdaa0abc0f7cb7096470aa5d2d94/d4808f4297b9a0bcc93e63115428f1994ad29b36> にある。
まず、なにを意図しているファイルかをコメントで書く。
(* Ruby has Hash class for hash table. By default, it compares keys using eql? method. However compare_by_identity method changes it to equal? method, that tests identity equality. Hash also has <=, ==, >= methods for Hash inclusion. This Rocq file examines impossibility of proper implementation of Hash#== and Hash#>= for identity-based hash and non-identity-based hash. *)
option 型の項 t を場合分けするときに、t = Some x と ~~ t (notation を使わず coercion を明示的に書くと negb (isSome t)) が出てくるものが欲しくなったので、そのための帰納型と補題を定義する。
Variant optneg_spec [T : Type] (t : option T) : option T -> Prop := | optnegSome : forall (x : T), t = Some x -> optneg_spec t (Some x) | optnegNone : ~~ t -> optneg_spec t None. Lemma optnegP [T : Type] (t : option T) : optneg_spec t t. Proof. (* 1 lines *) Qed.
ここからハッシュの包含についての話。 (optnegP は純粋に option の話で包含の話には依存していない。)
Section SubHash.
型の定義や等価性の notation は変わらない。
Variable idType : eqType. (* object id as dictionary key *) Variable ctType : eqType. (* object content as dictionary key *) Variable ct_of_id : idType -> ctType. Variable valType : eqType. (* dictionary values *) Notation "x \ct= y" := (ct_of_id x = ct_of_id y) (at level 70, no associativity). Notation "x \ct== y" := (ct_of_id x == ct_of_id y) (at level 70, no associativity). Notation "x !\ct= y" := (ct_of_id x <> ct_of_id y) (at level 70, no associativity). Notation "x !\ct== y" := (ct_of_id x != ct_of_id y) (at level 70, no associativity). Definition assocType := seq (idType * valType).
今回は、lookup を identity base の連想配列とそうでない連想配列の両方に使える一般化した関数として定義し、それをもとに証明を行う。 obs_of_id がキーを比較を行う型に変換する関数で、 identity base なら恒等関数 id であり、内容で比較するなら ct_of_id にするわけである。 また、普通の再帰関数として定義したため、assoc がコンストラクタの形で適用されている項は simpl で (期待する形に) 計算を進めた形に展開される。 これにより計算を進める補題が不要になっている。
Section Lookup.
Variable obsType : eqType.
Variable obs_of_id : idType -> obsType.
Section LookupK.
Variable k : idType.
Fixpoint lookup (assoc : assocType) : option valType :=
if assoc is (k1, v1) :: assoc' then
if obs_of_id k == obs_of_id k1 then
Some v1
else
lookup assoc'
else
None.
End LookupK.
lookup は option 型を返すので結果は Some x か None のどちらかになるのだが、 これを場合分けして lookup k assoc = Some x と ~~ lookup k assoc を得たいことが多々ある。 というか、今回はキーが存在しないことを ~~ lookup k assoc と表現することにするので、lookup k assoc = None という形が出てくるといちいち変換しなければならない。 ということで optnegP を lookup に特殊化した補題を用意する。 これにより、case: lookupP で (1) ゴールの中から lookup を探し、(2) 場合分けを行って、(3) lookup 呼び出しを Some x か None に置換し、(4) それぞれの場合に lookup k assoc = Some x と ~~ lookup k assoc の前提を付け加える、というのをいっきに行える。 この4つをいっきに行えるのが inductive spec のパワフルなところだよな。 なお、optnegP をそのまま使うと最初の「ゴールの中から lookup を探し」という部分をやってくれないので、lookupP を改めて証明しているのはその部分のためである。
Lemma lookupP (k : idType) (assoc : assocType) : optneg_spec (lookup k assoc) (lookup k assoc). Proof. (* 1 lines *) Qed.
lookup と in の関係についていくつか補題を証明する。 lookup は連想リストから値を取り出すが、一般に連想リストには同じキーが複数存在することがある。 そのため、lookup k assoc = Some v ならば (k, v) \in assoc は無条件に成り立つが、 逆は assoc が重複キーを持たない前提が必要になる。 しかし、値を気にしない isSome (lookup k assoc) と exists v, (k, v) \in assoc はキーの重複があってもなくても等価である。 そのため、in から lookup に変換する補題は、重複なしの前提をもち値を考慮する in_lookupv と、 重複なしの前提不要で値を考慮しない in_lookupb の二種類を用意している。 これらはどちらかからもう一方を導出することはできなくて、両方とも induction で証明している。
Lemma lookup_in k v assoc : lookup k assoc = Some v -> exists k', obs_of_id k = obs_of_id k' /\ (k', v) \in assoc. Proof. (* 12 lines *) Qed. Definition wfassoc (assoc : assocType) : bool := uniq (map (obs_of_id \o fst) assoc). Lemma in_lookupv k v (assoc : assocType) : wfassoc assoc -> (k, v) \in assoc -> lookup k assoc = Some v. Proof. (* 20 lines *) Qed. Lemma in_lookupb k v (assoc : assocType) : (k, v) \in assoc -> lookup k assoc. Proof. (* 8 lines *) Qed.
obs_of_id で観測した結果が等しければキーを変えても結果が変わらないという補題。
Lemma obseq_lookup k' k [assoc : assocType] : obs_of_id k' = obs_of_id k -> lookup k' assoc = lookup k assoc. Proof. (* 5 lines *) Qed.
重複が存在しないことを示す wfassoc についての補題。 assoc が cons のときに展開するものと、wfassoc が成り立っていれば in が関数のような挙動になるというものを用意する。
Lemma wfassoc_cons k v assoc : wfassoc ((k, v) :: assoc) = ~~ lookup k assoc && wfassoc assoc. Proof. (* 15 lines *) Qed. Lemma wfassoc_singlevalue k1 k2 v1 v2 assoc : obs_of_id k1 = obs_of_id k2 -> wfassoc assoc -> (k1, v1) \in assoc -> (k2, v2) \in assoc -> v1 = v2. Proof. (* 4 lines *) Qed. End Lookup.
notation で idlookup, ctlookup, \idin, \ctin 等を用意する。 これらは lookup を使っている。 定義でなく notation を使うことにより、lookup に関する補題を直接利用できるようにする。 (定義としてしまうと、展開しないと lookup に関する補題を利用できない。)
Notation idlookup := (@lookup idType id). Notation ctlookup := (@lookup ctType ct_of_id). Notation "k \idin assoc" := (isSome (@lookup idType id k assoc)) (at level 70, no associativity, format "'[hv' k '/ ' \idin assoc ']'"). Notation "k \ctin assoc" := (isSome (@lookup ctType ct_of_id k assoc)) (at level 70, no associativity, format "'[hv' k '/ ' \ctin assoc ']'"). Notation "k !\idin assoc" := (~~ (isSome (@lookup idType id k assoc))) (at level 70, no associativity, format "'[hv' k '/ ' !\idin assoc ']'"). Notation "k !\ctin assoc" := (~~ (isSome (@lookup ctType ct_of_id k assoc))) (at level 70, no associativity, format "'[hv' k '/ ' !\ctin assoc ']'").
idwf, ctwf は wfassoc を使った定義として用意する。 (できあがった証明をみるとこれらを明示的に展開しているのは idwf_cons だけなので、notation にしてもあまり変わらないと思う。 もともと wfassoc が uniq と map を使った定義で simpl による展開は期待した簡単な形にはならないし。)
Definition idwf (assoc : assocType) : bool := wfassoc id assoc. Definition ctwf (assoc : assocType) : bool := wfassoc ct_of_id assoc.
assoc_EQ などを定義する。 以前とほぼ同じだが、idlookup k idassoc = None となっていたのは None と書くのを避けて k !\idin idassoc と書くようにした。 なるべくこっちの形で統一して、補題もこの形で用意しているため。
(* equal *)
Definition assoc_EQ (idassoc ctassoc : assocType) : Prop :=
forall k, idlookup k idassoc = ctlookup k ctassoc.
(* less than or equal *)
Definition assoc_LE (idassoc ctassoc : assocType) : Prop :=
forall k, k !\idin idassoc
\/ idlookup k idassoc = ctlookup k ctassoc.
(* greater than or equal *)
Definition assoc_GE (idassoc ctassoc : assocType) : Prop :=
forall k, k !\ctin ctassoc
\/ idlookup k idassoc = ctlookup k ctassoc.
(* less than *)
Definition assoc_LT (idassoc ctassoc : assocType) : Prop :=
assoc_LE idassoc ctassoc /\ ~ assoc_EQ idassoc ctassoc.
(* greater than *)
Definition assoc_GT (idassoc ctassoc : assocType) : Prop :=
assoc_GE idassoc ctassoc /\ ~ assoc_EQ idassoc ctassoc.
(* incomparable *)
Definition assoc_IC (idassoc ctassoc : assocType) : Prop :=
~ assoc_LE idassoc ctassoc /\ ~ assoc_GE idassoc ctassoc.
antisym は同じ。
Lemma antisym (idassoc ctassoc : assocType) : assoc_LE idassoc ctassoc -> assoc_GE idassoc ctassoc -> assoc_EQ idassoc ctassoc. Proof. (* 8 lines *) Qed.
補題をいろいろ定義する。 だいたいは lookup に関する補題を特殊化しているだけ。
(* idwf *) Lemma idwf_nil : idwf [::]. Proof. (* 1 lines *) Qed. Lemma idwf_cons k v assoc : idwf ((k, v) :: assoc) = (k !\idin assoc) && idwf assoc. Proof. (* 1 lines *) Qed. (* idlookup *) Lemma idlookup_nil k : idlookup k [::] = None. Proof. (* 1 lines *) Qed. Lemma idlookup_head k v assoc : idlookup k ((k, v) :: assoc) = Some v. Proof. (* 1 lines *) Qed. Lemma idlookup_tail k k' v assoc : k != k' -> idlookup k' ((k, v) :: assoc) = idlookup k' assoc. Proof. (* 2 lines *) Qed. Lemma idlookup_cons k k' v assoc : idlookup k' ((k, v) :: assoc) = if k == k' then Some v else idlookup k' assoc. Proof. (* 1 lines *) Qed. Lemma idlookup1 k k' v : idlookup k' [:: (k, v)] = if k == k' then Some v else None. Proof. (* 1 lines *) Qed. Lemma idlookup_in k v assoc : idwf assoc -> (idlookup k assoc == Some v) = ((k, v) \in assoc). Proof. (* 5 lines *) Qed. (* ctlookup *) Lemma ctlookup_nil k : ctlookup k [::] = None. Proof. (* 1 lines *) Qed. Lemma ctlookup_head k k' v assoc : k \ct= k' -> ctlookup k' ((k, v) :: assoc) = Some v. Proof. (* 2 lines *) Qed. Lemma ctlookup_tail k k' v assoc : k !\ct== k' -> ctlookup k' ((k, v) :: assoc) = ctlookup k' assoc. Proof. (* 2 lines *) Qed. Lemma ctlookup_cons k k' v assoc : ctlookup k' ((k, v) :: assoc) = if k \ct== k' then Some v else ctlookup k' assoc. Proof. (* 1 lines *) Qed. Lemma ctlookup1 k k' v : ctlookup k' [:: (k, v)] = if k \ct== k' then Some v else None. Proof. (* 1 lines *) Qed. Lemma ctlookup_in k v assoc : ctlookup k assoc = Some v -> exists k', k \ct= k' /\ (k', v) \in assoc. Proof. (* 1 lines *) Qed. Lemma in_ctlookup k v assoc : ctwf assoc -> (k, v) \in assoc -> ctlookup k assoc = Some v. Proof. (* 2 lines *) Qed.
assoc_LE に関する補題。
(* assoc comparisons *) Lemma assoc_LE_nilL ctassoc : assoc_LE [::] ctassoc. Proof. (* 2 lines *) Qed. Lemma assoc_LE_consL k v (idassoc ctassoc : assocType) : idwf ((k, v) :: idassoc) -> assoc_LE ((k, v) :: idassoc) ctassoc <-> (ctlookup k ctassoc = Some v) /\ assoc_LE idassoc ctassoc. Proof. (* 28 lines *) Qed.
assoc_LE の実装 assoc_le と補題を用意し、assoc_le が assoc_LE と等価であることを証明する。
(* assoc_LE implementation *)
Fixpoint assoc_le (idassoc ctassoc : assocType) : bool :=
if idassoc is (k1, v1) :: idassoc' then
if ctlookup k1 ctassoc is Some v2 then
(v1 == v2) && assoc_le idassoc' ctassoc
else
false
else
true.
Lemma assoc_le_nilL ctassoc : assoc_le [::] ctassoc.
Proof. (* 1 lines *) Qed.
Lemma assoc_le_consL k v idassoc ctassoc :
idwf ((k, v) :: idassoc) ->
assoc_le ((k, v) :: idassoc) ctassoc <->
(ctlookup k ctassoc = Some v) /\ assoc_le idassoc ctassoc.
Proof. (* 14 lines *) Qed.
Lemma assoc_le_ok idassoc ctassoc :
idwf idassoc -> ctwf ctassoc ->
(assoc_le idassoc ctassoc <-> assoc_LE idassoc ctassoc).
Proof. (* 21 lines *) Qed.
assoc_EQ と assoc_GE が実装不能であることを証明するために、 eq/le/ge を一般化した関数を定義する。 generic_assoc_cmp は与えられた idassoc, ctassoc を連結して、そこにあるすべてのキーバリューペアについてある条件が成り立つという形にして、以前よりも短くなっている。 (以前は idassoc と ctassoc を別々に処理していた。)
(* generic eq/le/ge *)
Definition pairs_for_ct (assoc : assocType) (ct : ctType) : seq (idType * valType) :=
filter (pred1 ct \o ct_of_id \o fst) assoc.
Definition values_for_ct (idassoc : assocType) (ct : ctType) : seq valType :=
map snd (pairs_for_ct idassoc ct).
Definition generic_assoc_cmp (f : nat -> bool -> bool) (idassoc ctassoc : assocType) : bool :=
all (fun (kv : idType * valType) =>
let (k, v) := kv in
let ct_v_opt := ctlookup k ctassoc in
let vals := values_for_ct idassoc (ct_of_id k) in
let vals' := (if ct_v_opt is Some v' then [:: v'] else [::]) ++ vals in
all (pred1 v) vals' && f (size vals) ct_v_opt)
(idassoc ++ ctassoc).
(assoc_EQ と assoc_GE が実装不能であることを証明する前に) この generic_assoc_cmp でも assoc_LE が実装可能であることを示す。
(* assoc_LE implementation based on generic_assoc_cmp *)
Definition assoc_le' (idassoc ctassoc : assocType) : bool :=
generic_assoc_cmp (fun n b => (n == 0) || b) idassoc ctassoc.
Lemma values_for_ct_P v ct (assoc : assocType) :
reflect
(exists k, ct_of_id k = ct /\ (k, v) \in assoc)
(v \in values_for_ct assoc ct).
Proof. (* 13 lines *) Qed.
Lemma values_for_ct_empty ct assoc :
(size (values_for_ct assoc ct) == 0)
= ~~ has ((pred1 ct \o ct_of_id) \o fst) assoc.
Proof. (* 1 lines *) Qed.
Lemma LE_in_lookup k v idassoc ctassoc :
idwf idassoc ->
assoc_LE idassoc ctassoc ->
(k, v) \in idassoc ->
idlookup k idassoc = Some v /\ ctlookup k ctassoc = Some v.
Proof. (* 10 lines *) Qed.
Lemma assoc_le'_ok idassoc ctassoc :
idwf idassoc -> ctwf ctassoc ->
(assoc_le' idassoc ctassoc <-> assoc_LE idassoc ctassoc).
Proof. (* 54 lines *) Qed.
assoc_EQ と assoc_GE が実装不能であることを証明する。 証明の流れは以前と同じだが、共通部分をくくりだして短くしている。
Section EQ_GE_Impossible.
Lemma generic_assoc_cmp_single f k v :
generic_assoc_cmp f [:: (k, v)] [:: (k, v)] = f 1 true.
Proof. (* 3 lines *) Qed.
Variable v : valType.
Variable a1 a2 : idType.
Hypothesis Ha_id12 : a1 != a2.
Hypothesis Ha_ct12 : a1 \ct= a2.
Variable b : idType.
Hypothesis Hb_unique : forall k, k \ct= b -> k = b.
Let assoc_a := [:: (a1, v)].
Let assoc_b := [:: (b, v)].
Let idwf_a : idwf assoc_a. Proof. (* 1 lines *) Qed.
Let idwf_b : idwf assoc_b. Proof. (* 1 lines *) Qed.
Let ctwf_a : ctwf assoc_a. Proof. (* 1 lines *) Qed.
Let ctwf_b : ctwf assoc_b. Proof. (* 1 lines *) Qed.
Lemma not_assoc_EQ_a : ~ (assoc_EQ assoc_a assoc_a).
Proof. (* 6 lines *) Qed.
Lemma assoc_EQ_b : assoc_EQ assoc_b assoc_b.
Proof. (* 11 lines *) Qed.
Lemma not_assoc_GE_a : ~ (assoc_GE assoc_a assoc_a).
Proof. (* 7 lines *) Qed.
Lemma assoc_GE_b : assoc_GE assoc_b assoc_b.
Proof. (* 11 lines *) Qed.
Section GenericImpossible.
Variable R : assocType -> assocType -> Prop.
Hypothesis R_bad :
~ R assoc_a assoc_a.
Hypothesis R_good :
R assoc_b assoc_b.
Lemma generic_impossible :
~ exists (f : nat -> bool -> bool),
(forall (idassoc ctassoc : assocType),
idwf idassoc -> ctwf ctassoc ->
generic_assoc_cmp f idassoc ctassoc <-> R idassoc ctassoc).
Proof. (* 17 lines *) Qed.
End GenericImpossible.
Lemma eq_impossible :
~ exists (f : nat -> bool -> bool),
(forall (idassoc ctassoc : assocType),
idwf idassoc -> ctwf ctassoc ->
generic_assoc_cmp f idassoc ctassoc <-> assoc_EQ idassoc ctassoc).
Proof. (* 3 lines *) Qed.
Lemma ge_impossible :
~ exists (f : nat -> bool -> bool),
(forall (idassoc ctassoc : assocType),
idwf idassoc -> ctwf ctassoc ->
generic_assoc_cmp f idassoc ctassoc <-> assoc_GE idassoc ctassoc).
Proof. (* 3 lines *) Qed.
End EQ_GE_Impossible.
End SubHash.
About eq_impossible.
(*
eq_impossible :
forall [idType ctType : eqType] [ct_of_id : idType -> ctType]
[valType : eqType],
valType ->
forall [a1 a2 : idType],
a1 != a2 ->
ct_of_id a1 = ct_of_id a2 ->
forall [b : idType],
(forall k : idType, ct_of_id k = ct_of_id b -> k = b) ->
~
(exists f : nat -> bool -> bool,
forall idassoc ctassoc : assocType idType valType,
idwf idassoc ->
ctwf ct_of_id ctassoc ->
generic_assoc_cmp ct_of_id f idassoc ctassoc <->
assoc_EQ ct_of_id idassoc ctassoc)
*)
About ge_impossible.
(*
ge_impossible :
forall [idType ctType : eqType] [ct_of_id : idType -> ctType]
[valType : eqType],
valType ->
forall [a1 a2 : idType],
a1 != a2 ->
ct_of_id a1 = ct_of_id a2 ->
forall [b : idType],
(forall k : idType, ct_of_id k = ct_of_id b -> k = b) ->
~
(exists f : nat -> bool -> bool,
forall idassoc ctassoc : assocType idType valType,
idwf idassoc ->
ctwf ct_of_id ctassoc ->
generic_assoc_cmp ct_of_id f idassoc ctassoc <->
assoc_GE ct_of_id idassoc ctassoc)
*)こういう補題のデザインについて書いてある文献として MathComp book が思い浮かぶので、見直してみる。
MathComp book, 4.3.5 On the usability of lemmas
あと MathComp book には reflect の説明もがっつりあったし、indexed inductive type family を使って、場合分けと置換をいっきに行う話も書いてあったと思う。
でも、ハブをつくる話は見当たらない気がする (見逃しているだけかもしれない)
そういえば SSReflect でも、似たような関数で補題が多いものと少ないものがある。 たとえば、今回 idlookup と ctlookup に onth を使った。 onth と nth は両方ともリストの i 番目の要素を取り出すものである。 onth は option 型を返すもので、i が範囲外ならば None を返す。 nth は範囲外の場合に返す値を引数で指定する。 どちらも似たような関数だが、関連する補題は nth のほうがずっと多いと思う。
これは nth がハブになっているということなのかもしれない。
(ただ onth を簡単確実に nth に変換する補題は見当たらないが...)
あと、\in も関連する補題が多くて、ハブになっている気がする。
Rocq などの証明支援系では、普通の数学の証明では省略されることも明示的に記述する必要がある。 つまり、命題の自明な変形や導出を行う必要がある。
たとえば今回は 連想リストに対して、(identity による比較を行う) idin, idfind, idlookup という関数を定義した。
Definition idin (id : idType) (assoc : assocType) : bool. Definition idfind (assoc : assocType) (id : idType) : nat. Definition idlookup (assoc : assocType) (id : idType) : option valType.
id \idin assoc は assoc の中に id というキーがあるかどうかを判定する。 idfind assoc id は assoc の中に id というキーがあるインデックスを返し、なければ size assoc を返す。 idlookup assoc id は assoc の中に (id, v) というペアがあれば Some v を返し、なければ None を返す。
また、SSReflect には x \in s という記法があって、リストに特定の要素があるかどうかを判定できる。
ということで、証明の中ではこれらのあいだの変換が必要になる。 たとえば、(重複がないという前提で) (id, v) \in assoc と idlookup assoc id = Some v は等価である。 前提にどちらかがあって、証明にはもう一方が必要な場合、変換しなければならない。 (重複がないことは前提としてこれ以降は触れないことにする。)
必要になった補題を場当たり的につくっていくというのもひとつの手ではあるが、 今回は idin, idfind, idlookup, \in という 4つもあって、場当たり的にそれらの関係を証明していくと似た証明を複数回やることになりそうだし、 content による比較を行う ctin, ctfind, ctlookup についても一貫した同様な補題を用意したいと思ったので、ちょっと計画的に補題をデザインしようと考えた。
まず、命題の中に値が出現しないものとして、id \idin assoc, idfind assoc id < size assoc, isSome (idlookup assoc id) は等価である (isSome は Some なら true, None なら false を返す関数で、coercion なので通常は表示されない。)
値が出現する命題としては idlookup assoc id = Some v と (id, v) \in assoc が等価である。
値が出現する命題と出現しない命題の関係としては、(id, v) \in assoc -> id \idin assoc を考えられる。 これの逆方向については exists を使って、(exists v, (id, v) \in assoc) -> id \idin assoc を考えられる。
こういう、等価な命題 A1, A2, ..., An があり、また (Ai とは異なる) 等価な命題 B1, B2, ..., Bn があるという状況で、 どのような補題を用意するのがいいか考える。
なんでもかんでも変換を用意していくと最終的には O(n^2) の補題が必要になるが、これはよろしくない。
まぁ、誰でも考えつくとは思うのだが、こういうときはハブアンドスポーク戦略だよな。
A1, A2, ..., An の中でハブとなるものをひとつ決めて A とおき、A <-> A1, A <-> A2, ... という補題を作る。 これにより、Ai から Aj に変換するには Ai -> A -> Aj と変換できるようになる。 これで補題の数は n-1 個、最大2回で目的の形に変形できる。 (実際には、A <-> Ai をひとつの補題とするか、方向ごとに別にするかで数は変わるけど O(n) で済むのは変わらない)
B1, B2, ..., Bn も同様にハブになるのを B とする。
で、A <-> B という補題を作る。 A と B は等価ではないので <-> という書き方は変だが、上の exists みたいなのをつくって対応させる。
というわけで値が出現しない命題としては id \idin assoc をハブとして idfind と idlookup と相互に変換する補題を作った。 自然に (普通に rewrite して左から右に変形したときに) ハブになるよう、右側に id \idin assoc を配置してある。
Lemma idfind_idin (assoc : assocType) (id : idType) : (idfind assoc id < size assoc) = (id \idin assoc). Lemma idlookup_idin id assoc : isSome (idlookup assoc id) = (id \idin assoc).
値が出現する命題については、(id, v) \in assoc をハブとして idlookup と変換する補題をつくった。
Lemma idlookup_in id v assoc : idwf assoc -> (idlookup assoc id == Some v) = ((id, v) \in assoc).
で、値が出現しない命題と値が出現する命題のあいだの関係として、それぞれのハブの間で変換する補題を作った。
Lemma idinP (id : idType) (assoc : assocType) : reflect (exists v, (id, v) \in assoc) (id \idin assoc). Lemma in_idin id v assoc : (id, v) \in assoc -> id \idin assoc.
exists を使うと bool じゃなくて Prop になるので、= で接続することはできない。-> でやってもいいのだが、せっかくなので reflect を使ってみた。 また、原理的には前者の idinP だけでも済むはずだが、(id, v) \in assoc が前提にある時にこれを使うのは面倒くさいので、in_idin も作った。
さて、identity 比較のほうはこれで済むが、content 比較のほうはもっと複雑になる。 ctlookup assoc id などとして検索したときに見つかる assoc 内のペアのキーは id そのものでなく、id と content 比較で等価な別のものかもしない。 そのため、変換が必要になる命題はもっと増える。
ということで、content比較で同じキーの場合に結果が同じという補題を作った。
Lemma cteq_ctin id1 id2 assoc : id1 \ct= id2 -> (id1 \ctin assoc) = (id2 \ctin assoc). Lemma cteq_ctfind id1 id2 assoc : id1 \ct= id2 -> ctfind assoc id1 = ctfind assoc id2. Lemma cteq_ctlookup id1 id2 assoc : id1 \ct= id2 -> ctlookup assoc id1 = ctlookup assoc id2.
値が出現しない命題については id \ctin assoc をハブとして idfind と idlookup と相互に変換する補題を作った。
Lemma ctfind_ctin (assoc : assocType) (id : idType) : (ctfind assoc id < size assoc) = (id \ctin assoc). Lemma ctlookup_ctin id assoc : isSome (ctlookup assoc id) = (id \ctin assoc).
値が出現する命題については、ctlookup と \in があるが、これは identity 比較とは異なり、 単純に対応するものではない。 ctlookup assoc id = Some v と (id, v) \in assoc を考えると、後者が成り立てば前者がなりたつが、逆はそうでない。 ctlookup assoc id = Some v が成り立っていても、assoc の中に入っているのは id とは異なる (でも content としては等しい) id' かもしれないからである。
ということで、これらは異なる命題と考えられる。 といっても変換が必要になることはあるので、以下の補題を用意した。 (in_ctlookup のほうは、content比較で等しい別の identity にするところまでやるかとも考えたのだが、それは cteq_ctlookup にまかせることにして、そこまではせずに補題を単純な形で済ますことにした。)
Lemma ctlookup_in id v assoc : ctlookup assoc id = Some v -> exists id', id \ct= id' /\ (id', v) \in assoc. Lemma in_ctlookup id v assoc : ctwf assoc -> (id, v) \in assoc -> ctlookup assoc id = Some v.
あと、値が出現しない命題と値が出現する命題のあいだの関係としては、それぞれのハブの間で変換する補題を作った。
Lemma ctinP (id : idType) (assoc : assocType) : reflect (exists id' v, id \ct= id' /\ (id', v) \in assoc) (id \ctin assoc). Lemma in_ctin id v assoc : (id, v) \in assoc -> id \ctin assoc.
たとえば values_cons id v assoc : values ((id, v) :: assoc) = v :: values assoc は values を展開すると map が出てきて、引数が cons なので計算を進められて右辺と一致する、というだけの証明で 1行で済むものである。 でも、証明をする側からすると、展開して証明するのは下位レイヤに意識を向けなければならない。 そこで values を展開せずに (下位レイヤに意識を向けずに) 計算を進められる補題を用意している。
なお、計算を進めるというのがよく必要になるのは、場合分けや induction で指定した対象は (普通は) コンストラクタ (と 0個以上の新しい変数) に変わるので、 そのコンストラクタを処理して話を進める必要があるというのが理由である。 上記の values_cons なら、ゴールに values x があったときに、x を場合分けすると nil と cons に場合分けされるので、cons の場合に使えるというわけである。
あと、values_cons は values の引数に cons があったときに、cons が外側に出てくるように変形するが、 変形後がどういう形になるかは処理に依存する。(消えてしまうこともある。) たとえば idin_cons は id' \idin ((id, v) :: assoc) = (id' == id) || (id' \idin assoc) というもので、内側にあった cons が外側の orb (|| 演算子) に変わる。
また、値を作る方法はコンストラクタが基本であるが、それ以外にもよく使う方法があることもある。 たとえばリストなら、1要素のリストを直接つくるのと、リストの連結をすることはよくある。 そういうデータを作るよく使う方法に対しても補題があると便利だろう。
idin1 は id' \idin [:: (id, v)] = (id' == id) という感じで、1要素のリストに対して idin が結局どんな結果になるのかを直接示している。
idin_cat は id \idin (assoc1 ++ assoc2) = ((id \idin assoc1) || (id \idin assoc2)) であり、 リストの連結に対して idin するのは、それぞれのリストに対する idin の結果を orb でまとめるのと等しいという補題である。 これも大きなリストに対する処理を小さなリストに対する処理に分解している
この話を証明するのに、補題をいろいろ作った。
(* values *)
Lemma size_values (assoc : assocType) : size (values assoc) = size assoc.
Proof. (* 1 lines *) Qed.
Lemma values_cons id v assoc : values ((id, v) :: assoc) = v :: values assoc.
Proof. (* 1 lines *) Qed.
Lemma nth_values did dv assoc i :
(nth (did, dv) assoc i).2 = nth dv (values assoc) i.
Proof. (* 5 lines *) Qed.
(* idkeys *)
Lemma size_idkeys (assoc : assocType) : size (idkeys assoc) = size assoc.
Proof. (* 1 lines *) Qed.
Lemma idkeys_cons id v assoc : idkeys ((id, v) :: assoc) = id :: idkeys assoc.
Proof. (* 1 lines *) Qed.
Lemma nth_idkeys did dv assoc i :
(nth (did, dv) assoc i).1 = nth did (idkeys assoc) i.
Proof. (* 5 lines *) Qed.
Lemma nth_idkeys_values did dv i assoc :
(nth did (idkeys assoc) i, nth dv (values assoc) i) = nth (did, dv) assoc i.
Proof. (* 2 lines *) Qed.
(* idin *)
Lemma idin_nil id : id \idin [::] = false.
Proof. (* 1 lines *) Qed.
Lemma idin_cons id' id v assoc :
id' \idin ((id, v) :: assoc) = (id' == id) || (id' \idin assoc).
Proof. (* 1 lines *) Qed.
Lemma idin1 id' id v : id' \idin [:: (id, v)] = (id' == id).
Proof. (* 2 lines *) Qed.
Lemma idin_cat id assoc1 assoc2 :
id \idin (assoc1 ++ assoc2) = ((id \idin assoc1) || (id \idin assoc2)).
Proof. (* 8 lines *) Qed.
Lemma in_idin id v assoc :
(id, v) \in assoc -> id \idin assoc.
Proof. (* 5 lines *) Qed.
Lemma idinP (id : idType) (assoc : assocType) :
reflect (exists v, (id, v) \in assoc) (id \idin assoc).
Proof. (* 6 lines *) Qed.
(* idwf *)
Lemma idwf_nil : idwf [::].
Proof. (* 1 lines *) Qed.
Lemma idwf_cons id v assoc :
idwf ((id, v) :: assoc) = (id !\idin assoc) && idwf assoc.
Proof. (* 2 lines *) Qed.
Lemma idwf_head id v assoc :
idwf ((id, v) :: assoc) -> id !\idin assoc.
Proof. (* 1 lines *) Qed.
Lemma idwf_tail id v assoc :
idwf ((id, v) :: assoc) -> idwf assoc.
Proof. (* 1 lines *) Qed.
Lemma idwf1 id v : idwf [:: (id, v)].
Proof. (* 1 lines *) Qed.
Lemma idwf_singlevalue id v1 v2 idassoc :
idwf idassoc ->
(id, v1) \in idassoc ->
(id, v2) \in idassoc ->
v1 = v2.
Proof. (* 30 lines *) Qed.
(* idfind *)
Lemma idfind_nil id : idfind [::] id = 0.
Proof. (* 1 lines *) Qed.
Lemma idfind_cons id id' v assoc :
idfind ((id, v) :: assoc) id'
= if id == id' then 0 else (idfind assoc id').+1.
Proof. (* 1 lines *) Qed.
Lemma idfind_head id v assoc : idfind ((id, v) :: assoc) id = 0.
Proof. (* 1 lines *) Qed.
Lemma idfind_tail id id' v assoc :
id != id' -> idfind ((id, v) :: assoc) id' = (idfind assoc id').+1.
Proof. (* 2 lines *) Qed.
Lemma idfind1 id id' v :
idfind [:: (id, v)] id' = if id == id' then 0 else 1.
Proof. (* 1 lines *) Qed.
Lemma idfind_idin (assoc : assocType) (id : idType) :
(idfind assoc id < size assoc) = (id \idin assoc).
Proof. (* 3 lines *) Qed.
Lemma in_idfind d id v assoc :
idwf assoc ->
(id, v) \in assoc ->
idfind assoc id < size assoc /\ nth d assoc (idfind assoc id) = (id, v).
Proof. (* 24 lines *) Qed.
(* idlookup *)
Lemma idlookup_nth (x : valType) (id : idType) (assoc : assocType) :
idlookup assoc id
= if idfind assoc id < size assoc then
Some (nth x (values assoc) (idfind assoc id))
else
None.
Proof. (* 5 lines *) Qed.
Lemma idlookup_nil id : idlookup [::] id = None.
Proof. (* 1 lines *) Qed.
Lemma idlookup_head id v assoc : idlookup ((id, v) :: assoc) id = Some v.
Proof. (* 2 lines *) Qed.
Lemma idlookup_tail id id' v assoc :
id != id' -> idlookup ((id, v) :: assoc) id' = idlookup assoc id'.
Proof. (* 2 lines *) Qed.
Lemma idlookup_cons id id' v assoc :
idlookup ((id, v) :: assoc) id'
= if id == id' then Some v else idlookup assoc id'.
Proof. (* 3 lines *) Qed.
Lemma idlookup1 id id' v :
idlookup [:: (id, v)] id' = if id == id' then Some v else None.
Proof. (* 1 lines *) Qed.
Lemma idlookup_idin id assoc : isSome (idlookup assoc id) = (id \idin assoc).
Proof. (* 4 lines *) Qed.
Lemma idlookup_in id v assoc :
idwf assoc ->
(idlookup assoc id == Some v) = ((id, v) \in assoc).
Proof. (* 41 lines *) Qed.
(* ctkeys *)
Lemma size_ctkeys (assoc : assocType) : size (ctkeys assoc) = size assoc.
Proof. (* 1 lines *) Qed.
Lemma ctkeys_cons id v assoc : ctkeys ((id, v) :: assoc) = ct_of_id id :: ctkeys assoc.
Proof. (* 1 lines *) Qed.
(* ctin *)
Lemma ctin_nil id : id \ctin [::] = false.
Proof. (* 1 lines *) Qed.
Lemma ctin_cons id' id v assoc :
id' \ctin ((id, v) :: assoc) = (id' \ct== id) || (id' \ctin assoc).
Proof. (* 1 lines *) Qed.
Lemma ctin1 id' id v : id' \ctin [:: (id, v)] = (id' \ct== id).
Proof. (* 2 lines *) Qed.
Lemma ctin_cat id assoc1 assoc2 :
id \ctin (assoc1 ++ assoc2) = (id \ctin assoc1) || (id \ctin assoc2).
Proof. (* 8 lines *) Qed.
Lemma cteq_ctin id id' assoc : id \ct= id' -> (id \ctin assoc) = (id' \ctin assoc).
Proof. (* 6 lines *) Qed.
Lemma ctinP (id : idType) (assoc : assocType) :
reflect (exists id' v, id \ct= id' /\ (id', v) \in assoc)
(id \ctin assoc).
Proof. (* 9 lines *) Qed.
Lemma in_ctin id v assoc :
(id, v) \in assoc -> id \ctin assoc.
Proof. (* 7 lines *) Qed.
(* ctwf *)
Lemma ctwf_nil : ctwf [::].
Proof. (* 1 lines *) Qed.
Lemma ctwf_cons id v assoc :
ctwf ((id, v) :: assoc) = (id !\ctin assoc) && ctwf assoc.
Proof. (* 2 lines *) Qed.
Lemma ctwf_head id v assoc :
ctwf ((id, v) :: assoc) -> id !\ctin assoc.
Proof. (* 1 lines *) Qed.
Lemma ctwf_tail id v assoc :
ctwf ((id, v) :: assoc) -> ctwf assoc.
Proof. (* 1 lines *) Qed.
Lemma ctwf1 id v : ctwf [:: (id, v)].
Proof. (* 1 lines *) Qed.
Lemma ctwf_in_cons id' v' id v assoc :
ctwf ((id, v) :: assoc) ->
(id', v') \in (id, v) :: assoc ->
(((id' \ct== id) && (v' == v)) ||
((id' !\ct== id) && ((id', v') \in assoc))).
Proof. (* 25 lines *) Qed.
Lemma ctwf_singlevalue id1 id2 v1 v2 ctassoc :
id1 \ct= id2 -> ctwf ctassoc ->
(id1, v1) \in ctassoc ->
(id2, v2) \in ctassoc ->
v1 = v2.
Proof. (* 28 lines *) Qed.
(* ctfind *)
Lemma ctfind_nil id : ctfind [::] id = 0.
Proof. (* 1 lines *) Qed.
Lemma ctfind_head id id' v assoc :
id \ct= id' -> ctfind ((id, v) :: assoc) id' = 0.
Proof. (* 2 lines *) Qed.
Lemma ctfind_tail id id' v assoc :
id !\ct== id' -> ctfind ((id, v) :: assoc) id' = (ctfind assoc id').+1.
Proof. (* 3 lines *) Qed.
Lemma ctfind_cons id id' v assoc :
ctfind ((id, v) :: assoc) id'
= if id \ct== id' then 0 else (ctfind assoc id').+1.
Proof. (* 2 lines *) Qed.
Lemma ctfind1 id id' v :
ctfind [:: (id, v)] id' = if id \ct== id' then 0 else 1.
Proof. (* 1 lines *) Qed.
Lemma ctfind_ctin (assoc : assocType) (id : idType) :
(ctfind assoc id < size assoc) = (id \ctin assoc).
Proof. (* 3 lines *) Qed.
Lemma in_ctfind d id v assoc :
ctwf assoc ->
(id, v) \in assoc ->
ctfind assoc id < size assoc /\ nth d assoc (ctfind assoc id) = (id, v).
Proof. (* 34 lines *) Qed.
Lemma cteq_ctfind id1 id2 assoc :
id1 \ct= id2 ->
ctfind assoc id1 = ctfind assoc id2.
Proof. (* 2 lines *) Qed.
Lemma nth_ctfind d id assoc :
ctfind assoc id < size assoc ->
id \ct= nth d (idkeys assoc) (ctfind assoc id).
Proof. (* 9 lines *) Qed.
(* ctlookup *)
Lemma ctlookup_nth (x : valType) (id : idType) (assoc : assocType) :
ctlookup assoc id
= if ctfind assoc id < size assoc then
Some (nth x (values assoc) (ctfind assoc id))
else
None.
Proof. (* 5 lines *) Qed.
Lemma ctlookup_nil id : ctlookup [::] id = None.
Proof. (* 1 lines *) Qed.
Lemma ctlookup_head id id' v assoc :
id \ct= id' ->
ctlookup ((id, v) :: assoc) id' = Some v.
Proof. (* 3 lines *) Qed.
Lemma ctlookup_tail id id' v assoc :
id !\ct== id' -> ctlookup ((id, v) :: assoc) id' = ctlookup assoc id'.
Proof. (* 2 lines *) Qed.
Lemma ctlookup_cons id id' v assoc :
ctlookup ((id, v) :: assoc) id'
= if id \ct== id' then Some v else ctlookup assoc id'.
Proof. (* 3 lines *) Qed.
Lemma ctlookup1 id id' v :
ctlookup [:: (id, v)] id' = if id \ct== id' then Some v else None.
Proof. (* 1 lines *) Qed.
Lemma cteq_ctlookup id1 id2 assoc :
id1 \ct= id2 ->
ctlookup assoc id1 = ctlookup assoc id2.
Proof. (* 3 lines *) Qed.
Lemma ctlookup_ctin id assoc : isSome (ctlookup assoc id) = (id \ctin assoc).
Proof. (* 4 lines *) Qed.
Lemma ctlookup_in id v assoc :
ctlookup assoc id = Some v ->
exists id', id \ct= id' /\ (id', v) \in assoc.
Proof. (* 8 lines *) Qed.
Lemma in_ctlookup id v assoc :
ctwf assoc ->
(id, v) \in assoc ->
ctlookup assoc id = Some v.
Proof. (* 8 lines *) Qed.
(* assoc comparisons *)
Lemma assoc_LE_nilL ctassoc : assoc_LE [::] ctassoc.
Proof. (* 2 lines *) Qed.
Lemma assoc_LE_consL id v (idassoc ctassoc : assocType) :
idwf ((id, v) :: idassoc) ->
assoc_LE ((id, v) :: idassoc) ctassoc <->
(ctlookup ctassoc id = Some v) /\ assoc_LE idassoc ctassoc.
Proof. (* 29 lines *) Qed.
これらの補題は多くが、展開せずに計算を進めるものと、等価な命題の変換をするものである。
だいたいわかったところで、確信を得るために Rocq で形式化してみよう。
Rocq で形式化したファイル全体は <URL:https://gist.github.com/akr/3f0fcdaa0abc0f7cb7096470aa5d2d94/403384d856844e23fe7f197a14ea4e75174a0cfe> に置いてある。
例によって mathcomp を使う
From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section SubHash.
Ruby では identity というものが言語自体に存在するが、Rocq では (数学と同様に) そんなものは存在しないので、ここで identity の型 idType と中身の型 ctType が存在すると仮定し、 idType から ctType への関数が存在するとして表現する。
Variable idType : eqType. (* object id as dictionary key *) Variable ctType : eqType. (* object content as dictionary key *) Variable ct_of_id : idType -> ctType.
(hash の) 値の型も用意する。
Variable valType : eqType. (* dictionary values *)
これら idType, ctType, valType はすべて eqType なので、比較が可能である。
そして、キーの content (内容) で比較する二項演算子 x \ct= y と x \ct== y を用意する。 前者が Prop で後者が bool である。 (否定の x !\ct= y と x !\ct== y も用意する)
Notation "x \ct= y" := (ct_of_id x = ct_of_id y) (at level 70, no associativity). Notation "x \ct== y" := (ct_of_id x == ct_of_id y) (at level 70, no associativity). Notation "x !\ct= y" := (ct_of_id x <> ct_of_id y) (at level 70, no associativity). Notation "x !\ct== y" := (ct_of_id x != ct_of_id y) (at level 70, no associativity).
ハッシュテーブルを Rocq で用意するのは面倒くさすぎるので、連想リストを使うことにする。 連想リストの型を assocType と定義する。 ここで assocType は idType のキーと valType の値のペアのリストである。 Ruby で hash が identity base かどうかは hash 内部に記録されていたが、 ここでは利用する側で検索関数を選ぶことにして、内部には記録しない。
Definition assocType := seq (idType * valType).
idkeys, ctkeys はキーのリストを取り出す。 idkeys は連想リストから単に取り出すだけだが、ctkeys は ct_of_id でキーを identity から content に変換する。 values は値のリストを取り出す。
Definition idkeys (assoc : assocType) := map fst assoc. Definition ctkeys (assoc : assocType) := map (ct_of_id \o fst) assoc. Definition values (assoc : assocType) := map snd assoc.
連想リストがあるキーをもつということを示す、id \idin assoc と id \ctin assoc を用意する。 後者はキーを content として比較する。
Definition idin (id : idType) (assoc : assocType) : bool := id \in idkeys assoc. Definition ctin (id : idType) (assoc : assocType) : bool := ct_of_id id \in ctkeys assoc. Notation "id \idin assoc" := (idin id assoc) (at level 70, no associativity, format "'[hv' id '/ ' \idin assoc ']'"). Notation "id \ctin assoc" := (ctin id assoc) (at level 70, no associativity, format "'[hv' id '/ ' \ctin assoc ']'"). Notation "id !\idin assoc" := (~~ (idin id assoc)) (at level 70, no associativity, format "'[hv' id '/ ' !\idin assoc ']'"). Notation "id !\ctin assoc" := (~~ (ctin id assoc)) (at level 70, no associativity, format "'[hv' id '/ ' !\ctin assoc ']'").
連想リストは、データ構造としては同じキーが複数存在していることを許すが、今回はそういう状況には興味が無い。 Ruby の Hash だとそういうものは存在できないし。 そこで、そういうキーがないことを idwf, ctwf という述語で表現する。
Definition idwf (assoc : assocType) : bool := uniq (idkeys assoc). Definition ctwf (assoc : assocType) : bool := uniq (ctkeys assoc).
連想リストの中からキーを探してそのインデックスを返す関数 idfind, ctfind を定義する。 mathcomp の find を使っているので、キーが存在しない時にはリストのサイズを返す。
Definition idfind (assoc : assocType) (id : idType) : nat := find (pred1 id) (idkeys assoc). Definition ctfind (assoc : assocType) (id : idType) : nat := find (pred1 (ct_of_id id)) (ctkeys assoc).
連想リストの中からキーを探してその値を返す関数 idlookup, ctlookup を定義する。 キーがないときには None を返す。キーがあったときには (対応する値が x の場合) Some x を返す。 onth はそういう option 型を返すものである。
Definition idlookup (assoc : assocType) (id : idType) : option valType := onth (values assoc) (idfind assoc id). Definition ctlookup (assoc : assocType) (id : idType) : option valType := onth (values assoc) (ctfind assoc id).
idlookup, ctlookup を使って、連想リストの包含関係を定義する。 半順序なので、比較不能 (incomparable) という場合もある。 とはいえ、idlookup, ctlookup を直接使って定義されるのは assoc_EQ, assoc_LE, assoc_GE で、 残りの assoc_LT, assoc_GT, assoc_IC は前者 3つから定義される。
そしてこれらの関係は、forall id, ... という全称命題を使っているため、そのまま実行できるものではない。
(* equal *)
Definition assoc_EQ (idassoc ctassoc : assocType) : Prop :=
forall id, idlookup idassoc id = ctlookup ctassoc id.
(* less than or equal *)
Definition assoc_LE (idassoc ctassoc : assocType) : Prop :=
forall id, idlookup idassoc id = None
\/ idlookup idassoc id = ctlookup ctassoc id.
(* greater than or equal *)
Definition assoc_GE (idassoc ctassoc : assocType) : Prop :=
forall id, ctlookup ctassoc id = None
\/ idlookup idassoc id = ctlookup ctassoc id.
(* less than *)
Definition assoc_LT (idassoc ctassoc : assocType) : Prop :=
assoc_LE idassoc ctassoc /\ ~ assoc_EQ idassoc ctassoc.
(* greater than *)
Definition assoc_GT (idassoc ctassoc : assocType) : Prop :=
assoc_GE idassoc ctassoc /\ ~ assoc_EQ idassoc ctassoc.
(* incomparable *)
Definition assoc_IC (idassoc ctassoc : assocType) : Prop :=
~ assoc_LE idassoc ctassoc /\ ~ assoc_GE idassoc ctassoc.
この時点でなんか証明できないかな、と思って、とりあえず反対称律を証明してみた。 (後で使うわけではない)
Lemma antisym (idassoc ctassoc : assocType) : assoc_LE idassoc ctassoc -> assoc_GE idassoc ctassoc -> assoc_EQ idassoc ctassoc. Proof. (* 6 lines *) Qed.
補題をいろいろ定義する。(これについては後で述べる)
さて、idh <= cth は実装可能というのを証明してみよう。 まず実装してみる。 idh のそれぞれの key-value pair (id1, v1) について cth で lookup して、値があったら等しい、というのをぜんぶ試すという実装である。 これは (全称命題だった assoc_LE とは異なり) 現実的に実行できる。
(* assoc_LE implementation *)
Fixpoint assoc_le (idassoc ctassoc : assocType) : bool :=
if idassoc is (id1, v1) :: idassoc' then
if ctlookup ctassoc id1 is Some v2 then
(v1 == v2) && assoc_le idassoc' ctassoc
else
false
else
true.
この実装が、assoc_LE と等価であるということを証明する。
Lemma assoc_le_nilL ctassoc : assoc_le [::] ctassoc. Proof. (* 1 lines *) Qed. Lemma assoc_le_consL id v idassoc ctassoc : idwf ((id, v) :: idassoc) -> assoc_le ((id, v) :: idassoc) ctassoc <-> (ctlookup ctassoc id = Some v) /\ assoc_le idassoc ctassoc. Proof. (* 14 lines *) Qed. Lemma assoc_le_ok idassoc ctassoc : idwf idassoc -> ctwf ctassoc -> (assoc_le idassoc ctassoc <-> assoc_LE idassoc ctassoc). Proof. (* 25 lines *) Qed.
証明できたので、assoc_le という実装は assoc_LE という仕様と等価で、正しく実装できていることがわかった。
さて、次に assoc_EQ と assoc_GE が実装できないことを証明したい。
実装可能であることを検証するには、(上記の assoc_le のように) 実装して仕様と合致していることを証明すればいいのだが、 実装不能であることはどう証明すればいいだろうか。
そういう関数が存在したら矛盾することを示せばいいのだろうか。
たとえば、assoc_EQ という仕様に対して、それと対応する assocType -> assocType -> bool 型の関数 assoc_eq が存在しないことは次の命題で表現できる。
~ exists (assoc_eq : assocType -> assocType -> bool),
(forall (idassoc ctassoc : assocType),
idwf idassoc -> ctwf ctassoc ->
assoc_eq idassoc ctassoc <-> assoc_EQ idassoc ctassoc).
しかし、考えてみると、これは証明できそうにない。
最初に書いた文字列キーとシンボルキーの例では、 「idh の key で cth を検索して結果を調べる、また、cth の key で idh を検索して結果を調べる、という結果だけ」から判断する限りは実装不能と 書いたが、この assoc_eq は idassoc と ctassoc を受けとるため、それらの中身のキーを調べて文字列とシンボルを区別して結果を変えることができる。 なので、そこで生じる矛盾を再現できない。
また idType と ctType の具体的な型を指定していないので、極端な例として、idType と ctType が unit であれば、 キーは常に等しいので、assoc_eq は容易に実装可能だろう。
さらにとても極端な例として idType と ctType が空集合なら、assoc_eq はどう実装しても上記の命題を満たす。
こういう極端な例であっても実装可能であれば、実装不能であることは証明できない。
というわけで、実装不能であることを証明するには、どういう条件下での話なのかを明確化する必要がある。 (また、Ruby のオブジェクトを、矛盾を導ける程度に再現する必要がある。)
で、assoc_eq が idassoc と ctassoc を直接引数に受け取るから (文字列とシンボルを) 区別できてしまうのがいかんので、 idassoc と ctassoc からキーや値そのものは削り、比較に必要最小限な情報を取り出して、それを比較することにする。
具体的には、generic_assoc_cmp という関数を考える。 これは eq, le, ge を一般化した関数である。
generic_assoc_cmp f idassoc ctassoc と呼び出すのだが、 これは idassoc と ctassoc の中から content の意味で同じキーそれぞれについて、idassoc の中にいくつあるか、ctassoc の中にそのキーが入っているかどうかを調べる。 (idassoc の中には複数入っている可能性があるが、ctwf ctassoc により重複は禁止なので、ctassoc の中にはたかだかひとつしか入っていない。) そして、対応する値に異なるものがあれば、idassoc と ctassoc は incomparable なので、false を返す。 対応する値がすべて等しければ f を呼び出す。 そうやって呼び出した f の結果をぜんぶ論理積でまとめたものを最終的な結果とする。 (eq, le, ge はどれも各要素についての条件をすべて論理積にするのでこれで eq, le, ge を表現できる)
Definition pairs_for_ct (assoc : assocType) (ct : ctType) : seq (idType * valType) :=
filter (pred1 ct \o ct_of_id \o fst) assoc.
Definition values_for_ct (idassoc : assocType) (ct : ctType) : seq valType :=
map snd (pairs_for_ct idassoc ct).
Definition generic_assoc_cmp (f : nat -> bool -> bool) (idassoc ctassoc : assocType) : bool :=
all (fun (id_v : idType * valType) =>
let (id, v) := id_v in
let vals := values_for_ct idassoc (ct_of_id id) in
if all (pred1 v) vals then
f (size vals) true
else
false)
ctassoc
&&
all (fun (id_v : idType * valType) =>
let (id, v) := id_v in
if ctlookup ctassoc id then
true
else
let vals := values_for_ct idassoc (ct_of_id id) in
if all (pred1 v) vals then
f (size vals) false
else
false)
idassoc.
長ったらしいが、idassoc と ctassoc の両方で繰り返さないと与えられた全てのキーを試せないので仕方ない。
これで assoc_eq, assoc_ge が実装不能であることを証明する前に、まず assoc_LE を generic_assoc_cmp で実装可能であることを証明してみる。 これは generic_assoc_cmp が意図どおりの定義になっているかどうかの確認である。
generic_assoc_cmp に渡す f として (fun n b => (n == 0) || b) を指定している。 これは、あるキーに対する (content 比較で等しい) キーが idassoc の中に n 個、ctassoc の中に入っているかどうかを b として与えられて、 idassoc が小さいか等しいというのは、n が 0 であるか、b が真 (ctassoc の中にそのキーが入っている) であれば、真ということである。 それをすべてのキーについて判定して論理積をとれば less than or equal になるはずである。
Definition assoc_le' (idassoc ctassoc : assocType) : bool :=
generic_assoc_cmp (fun n b => (n == 0) || b) idassoc ctassoc.
Lemma values_for_ct_P v ct (assoc : assocType) :
reflect
(exists id, ct_of_id id = ct /\ (id, v) \in assoc)
(v \in values_for_ct assoc ct).
Proof. (* 13 lines *) Qed.
Lemma values_for_ct_empty ct assoc :
(size (values_for_ct assoc ct) == 0)
= ~~ has ((pred1 ct \o ct_of_id) \o fst) assoc.
Proof. (* 1 lines *) Qed.
Lemma assoc_le'_ok idassoc ctassoc :
idwf idassoc -> ctwf ctassoc ->
(assoc_le' idassoc ctassoc <-> assoc_LE idassoc ctassoc).
Proof. (* 107 lines *) Qed.
これで assoc_le' は generic_assoc_cmp を使って定義され、assoc_LE を正しく実装していることを確認できた。
で、次は assoc_EQ と assoc_GE が実装不能であることの証明である。
Section EQ_GE_Impossible.
ここで、最初に述べた文字列キーとシンボルキーの話を再現する。
まず、なにか valType の値の存在を仮定する。 (valType が空集合だと、連想リストは空リストしか作れないので、常に真を返す関数が assoc_EQ と assoc_GE の実装として正しくなってしまう)
Variable v : valType.
ふたつの文字列キーに対応する、idType の a1, a2 という値を仮定する。 これらは identity としては異なるが、content にすると同じになる。
Variable a1 a2 : idType. Hypothesis Haid12 : a1 != a2. Hypothesis Hact12 : a1 \ct= a2.
シンボルキーに対応する、idType の b という値を仮定する。 これが content として等しいのは、b だけである。
Variable b : idType. Hypothesis Hb_unique : forall id, id \ct= b -> id = b.
文字列キーの連想リスト assoc_a とシンボルキーの連想リスト assoc_b を用意する。 これらは自明に well formed (キーに重複がない) である。
Let assoc_a := [:: (a1, v)]. Let assoc_b := [:: (b, v)]. Let idwf_a : idwf assoc_a. Proof. (* 1 lines *) Qed. Let idwf_b : idwf assoc_b. Proof. (* 1 lines *) Qed. Let ctwf_a : ctwf assoc_a. Proof. (* 1 lines *) Qed. Let ctwf_b : ctwf assoc_b. Proof. (* 1 lines *) Qed.
assoc_EQ assoc_a assoc_a は否定される。 これは左側が identity での比較で、右側が content での比較なので、 a2 で lookup すると、左側は値がなく、右側は v と異なるからである。
Lemma not_assoc_EQ_a : ~ (assoc_EQ assoc_a assoc_a). Proof. (* 5 lines *) Qed.
assoc_EQ assoc_b assoc_b は成り立つ。 上の assoc_a とは異なり、a2 のような、内容は同じだが identity が異なるというものが存在しないためである。
Lemma assoc_EQ_b : assoc_EQ assoc_b assoc_b. Proof. (* 14 lines *) Qed.
assoc_GE assoc_a assoc_a と assoc_GE assoc_b assoc_b も同様に、前者は否定され、後者は成り立つ。
Lemma not_assoc_GE_a : ~ (assoc_GE assoc_a assoc_a). Proof. (* 6 lines *) Qed. Lemma assoc_GE_b : assoc_GE assoc_b assoc_b. Proof. (* 11 lines *) Qed.
これらを使うと、assoc_EQ や assoc_GE を実装する (generic_assoc_cmp に渡す) f が存在しないことを証明できる。
Lemma eq_impossible :
~ exists (f : nat -> bool -> bool),
(forall (idassoc ctassoc : assocType),
idwf idassoc -> ctwf ctassoc ->
generic_assoc_cmp f idassoc ctassoc <-> assoc_EQ idassoc ctassoc).
Proof. (* 26 lines *) Qed.
Lemma ge_impossible :
~ exists (f : nat -> bool -> bool),
(forall (idassoc ctassoc : assocType),
idwf idassoc -> ctwf ctassoc ->
generic_assoc_cmp f idassoc ctassoc <-> assoc_GE idassoc ctassoc).
Proof. (* 26 lines *) Qed.
End EQ_GE_Impossible.
End SubHash.
SubHash セクションを終了してから eq_impossible と ge_impossible の型を表示させてみる。 そうすると、valType の値がひとつあるとか、a1, a2 があるとかいった仮定がすべてそれらの引数に付け加えられていることがわかる。
About eq_impossible. (* eq_impossible : forall [idType ctType : eqType] [ct_of_id : idType -> ctType] [valType : eqType], valType -> forall [a1 a2 : idType], a1 != a2 -> ct_of_id a1 = ct_of_id a2 -> forall [b : idType], (forall id : idType, ct_of_id id = ct_of_id b -> id = b) -> ~ (exists f : nat -> bool -> bool, forall idassoc ctassoc : assocType idType valType, idwf idassoc -> ctwf ct_of_id ctassoc -> generic_assoc_cmp ct_of_id f idassoc ctassoc <-> assoc_EQ ct_of_id idassoc ctassoc) *) About ge_impossible. (* ge_impossible : forall [idType ctType : eqType] [ct_of_id : idType -> ctType] [valType : eqType], valType -> forall [a1 a2 : idType], a1 != a2 -> ct_of_id a1 = ct_of_id a2 -> forall [b : idType], (forall id : idType, ct_of_id id = ct_of_id b -> id = b) -> ~ (exists f : nat -> bool -> bool, forall idassoc ctassoc : assocType idType valType, idwf idassoc -> ctwf ct_of_id ctassoc -> generic_assoc_cmp ct_of_id f idassoc ctassoc <-> assoc_GE ct_of_id idassoc ctassoc) *)
外から与えたキーで検索する挙動だけで等価性や包含関係の判定を実装できるか考えてみると、これは難しい。
しばらく考えると、idh <= cth は実装可能だが、idh == cth と idh >= cth は実装できない感じがする。
(ここからは idh を左引数、cth を右引数に固定する。そう固定しても左右対称なので一般性は失わない。)
「実装できない」というのはちょっと強い表現で、これには前提がある。 ここで意図しているのは、 idh の key で cth を検索して結果を調べる、また、cth の key で idh を検索して結果を調べる、 という結果だけから idh == cth と idh >= cth を求めることはできない、という意味である。
これは上記の例で、idh.has_key?(k) と cth.has_key?(k) が 文字列キーでもシンボルキーでも以下の結果となっていて区別がつかないことからわかる。
p idh.has_key?(k) #=> true p cth.has_key?(k) #=> true
k2 という、k と等しいが identity が異なるオブジェクトが文字列では存在し、シンボルでは存在しない。 このことがわかると、文字列キーでは idh と cth は異なることがわかる。 しかしこれは「idh の key で cth を検索して結果を調べる、また、cth の key で idh を検索して結果を調べる、という結果だけ」からはわからない。 そのため区別が付かず、idh == cth が true と false のどちらを返しても、文字列キーとシンボルキーのどちらかでは間違ってしまう。 (idh >= cth も同様)
それに対して、idh <= cth は問題なく実装できそうである。 k2 のような、k と等しいが identity が異なるオブジェクトがあって、idh では存在せず cth だけで存在するキーがあっても、idh <= cth を否定することにはならない。 そのため、「idh の key で cth を検索して結果を調べる、また、cth の key で idh を検索して結果を調べる、という結果だけ」で idh <= cth を判定できる。
すこし前に、Hash の包含関係の判定がおかしいという話があった。 (なお Ruby では Hash クラスはハッシュテーブルの実装である)
Bug #21921: Hash inconsistent ==, >=, <= behavior
Hash の包含関係を ==, >=, <= で検査できるというのはあまり使っている人はいないのではないかと思うが、 この話はさらに Hash#compare_by_identity で比較を identity で行うようにした Hash とそうでない Hash の判定で、 まぁ使っているひとはいそうにない話である。
さて、Ruby では、Hash のキーの等価性は通常 eql? メソッドで検査される。 が、Hash#compare_by_identity により identity で比較するように設定すると、 (identity の比較である) equal? で比較するようになる。
Hash の等価性判定 (== メソッド) はマニュアルに以下のように記載されている。
(hash == object という == メソッドの呼び出しは) Returns true if all of the following are true: * object is a Hash object. * hash and object have the same keys (regardless of order). * For each key key, hash[key] == object[key]. Otherwise, returns false.
Hash のマニュアルには <= が subset, >= が superset と書いてあるが、 それ以上の説明はない。
compare_by_identity との関係についてはどちらも触れられていない。
なお、順序にはいろいろあるのだが、 包含関係は半順序だろう。(明らかに順序関係にないものがあるわけだし。) そして、半順序は反射律・推移律・反対称律を満たす関係である。
上記の == メソッドのマニュアルで、hash == object はちょっと混同しやすいので X == Y とすると (あと key key はわかりにくいので key k とすると)、 重要な性質は X and Y have the same keys と For each key k, X[k] == Y[k] となる。
でも、前者の same keys は、compare_by_identity が混じったときにどういう意味かはっきりしない。
ちょっと試してみよう。ここでは ruby-4.0.3 を使っている。 (idh というのは identity-based hash のつもりで、cth は content-based hash のつもりである)
なお、hash の値はあまり問題にはならないので、ここでは常に true としている。 (キーが存在するならば値は常に true なので、キーの存在だけで包含関係を検討できる)
idh = {}.compare_by_identity
k = "a".freeze # freeze されていない文字列 key は内部的に複製されるため、freeze でそれを避けている
k2 = k.dup.freeze
idh[k] = true
p idh.has_key?(k) #=> true
p idh.has_key?(k2) #=> false
cth = {}
cth[k] = true
p cth.has_key?(k) #=> true
p cth.has_key?(k2) #=> true
p [idh <= cth, cth >= idh] #=> [true, true]
p idh == cth #=> false
p [idh >= cth, cth <= idh] #=> [true, true]
idh = {}.compare_by_identity
k = :a
idh[k] = true
p idh.has_key?(k) #=> true
cth = {}
cth[k] = true
p cth.has_key?(k) #=> true
p [idh <= cth, cth >= idh] #=> [true, true]
p idh == cth #=> false
p [idh >= cth, cth <= idh] #=> [true, true]
とりあえず、idh <= cth と idh >= cth が true なのに idh == cth が false になっているので反対称律が成り立っていない。 つまり半順序になっていない。
ここで compare_by_identity かどうかという内部の話を無視して、外から与えたキーで検索する挙動だけで等価性や包含関係を考えてみる。
上記の例をみて考えると、前半の文字列キーの場合は idh.has_key?(k2) と cth.has_key?(k2) が異なる (それぞれ false, true) ので、idh と cth は異なる。 なので、idh == cth が false になっているのは正しい。
しかし、後半のシンボルキーの場合は、そのように異なる結果になるものは考えられない。 (等しいシンボルはそれ自身しかないので、普通の Hash でも、identity の比較をしているのと挙動を区別できない。) とすると、idh == cth が false になっているのは変である。
後半のシンボルキーでは、idh と cth は (外から観測する限りは) 等しいので、idh <= cth や idh >= cth が true なのは問題ない。
前半の文字列キーでは、idh <= cth なのは問題ない。 たくさんある "a" という文字列オブジェクトのうち、k (という変数に束縛されているオブジェクト) だけは idh と cth の両方で有効なキーであり、 それ以外の "a" は cth だけで有効なキーである。 両方で有効なキーでは同じ値 (true) をもち、片方で有効なキーは cth だけで有効ということで、idh は cth に包含されている。 なので、idh <= cth は正しい。
しかし、文字列キーで idh >= cth が true になっているのはおかしい。 k 以外の "a" オブジェクトは cth だけで有効なキーなので、 idh で無効で cth で有効なキーが存在し、idh は cth を包含していない。 なので、idh >= cth が false なのは変である。
カンマ区切りの構文は BNF では書きにくいよなぁ、と思う