演算子の優先順位というものは小学校で習うわけである。足し算よりも掛け算を優先するとかそういう感じで。
しかし、厳密な定義は、といわれると習った覚えがない。
yacc とかのパーサージェネレータには優先順位を指定する機能があるが、 これは LR構文解析の shift/reduce 競合の解決法を指定するもので、 結局のところどんな状況を目指しているのかというのはわかっていなかった。 優先順位というものは左右対称だと思うのだが、パーサの動作は左右対称じゃないからこれが本質という気もしない。
ところが、最近、演算子の優先順位をちゃんと定義する論文を見つけた。
Precedences in specifications and implementations of programming languages
二項演算子だけなら小学校で習う知識をすこし一般化すればなんとかなるが、単項演算子（前置演算子と後置演算子）を扱うとなるとあまり自明ではない。 とくに、優先順位の低い単項演算子は難しい。 それがちゃんと定義されていてすばらしい。 左右対称だし。
なかなかよいと思うのだが、これは yacc の優先順位と同じものなのだろうか。 それが疑問である。
しばらく自分で考えて、（二項演算子については）ちょっとわかった。 項が作られるのは reduce のときで、shift/reduce conflict が reduce に解決されるのは LR スタックに積まれている規則 (演算子) と lookahead symbol の優先順位を比較して前者の優先順位が高いときなので、 reduce が何回か行われて作られた項 (木構造) の右端に並んでいる演算子はすべて lookahead の演算子よりも優先順位が高いのだ。 (ここで優先順位が同じ場合、左結合と右結合でそれぞれ左右どちらかが高いとみなす)
しかし、これと左右対称な性質 (木構造の左側に並んでいる演算子はその項の左側にある演算子よりも優先順位が高い) は頭の中で考えていても納得できない。 しかたないので AI に相談すると、なぜそうなるかを説明してくれて、（しばらく考えて）納得できた。 shift/reduce conflict で shift が選ばれるのは lookahead のほうが優先順位が高い場合で、そうやって shift したものが後から reduce されることで左にある演算子の下位に入っていくのだな。 上の reduce が連続して起こるのと違って、もうちょっと大きな単位で動作を理解しないと納得できない話であった。
あと、ここまでは二項演算子だけの話だが、単項演算子は前置と後置それぞれでまた考える必要がある。 でも LR 構文解析の動作を頭のなかでイメージできればなんとかわかる。
前置演算子が出現するのは項の先頭で、ここでは shift/reduce conflict がないので、即座に shift される。 その後で、前置演算子の優先順位よりも高い演算子で構成された塊がひとつの項としてまとまり、その後で前置演算子とその項が reduce される。 この塊の中の演算子は、前置演算子と優先順位が比較されることはあるが、前置演算子よりも前に出現した演算子との比較は起きない。 だから、高い優先順位の二項演算子の右引数に低い優先順位の前置単項演算子があると、その内部にはかっこなしで二項演算子よりも低い優先順位の演算子が出現することがある。 たとえば、OCaml の if 式が（単項演算子じゃなくて 3項演算子だけど）そういう性質を持っている。 2 * if b then 3 else 4 + 5 という式は 2 * (if b then 3 else (4 + 5)) と解釈される。 OCaml では、乗算、加算、if 式、という順番の優先順位になっている。 乗算の優先順位よりも if 式の優先順位が低いため、if 式の (else 節) 内部の加算は if 式と優先順位が比べられ、加算の優先順位が高いので、 if 式の内部の式と解釈される。 乗算と加算の優先順位の比較は行われない。
後置演算子も、LR構文解析の動作は違うのだが、結局は似たような結果になる。 後置演算子が lookahead になったときに、それよりも優先順位の高い塊はその後置演算子の引数として reduce され、後置演算子よりも後で出現する演算子の優先順位は関知されない。
さて、こうやって納得したのはいいのだが、ふと思いついて、 Claude Code に Rocq (と mathcomp) でこのことを証明するように指示してみた。 そうすると、たいしてかからずに（測らなかったけど10分くらい?）で証明を作ってきた。
出来上がったものは以下にある。
<URL:https://gist.github.com/akr/50d9c2ac265b0ec9b1dac6e84dda7381>
出来上がったはいいが、これが本当に期待した性質を証明しているかどうかは自分で確認する必要がある。 証明の本体は読まなくても、命題の部分は読まないといけない。
ということで、命題の部分（およびその内部で参照している部分）だけを取り出してきた。 証明ぜんぶだと 450行くらいあるが、命題だけだと160行くらいなので、ずいぶんと短くなっている。
(** * Aasa (1995) の precedence correct と yacc 流 shift/reduce 競合解決の一致
A. Aasa, "Precedences in specifications and implementations of
programming languages", TCS 142 (1995) 3-26.
曖昧な文法
<<
E ::= E inl E | E inr E | pre E | E post | atom
>>
に対し、
- 論文 Definition 3/4 の Lw, Rw, Pc (ここでは [pc]) を定義し、
- yacc/bison が生成する LR 構文解析器 (shift/reduce 競合を
%left/%right と優先順位で解決したもの) をスタック機械 [parse] として
モデル化し、
- [parse ts = Some t <-> pc t /\ flatten t = ts] を証明する。
副産物として論文の Theorem 12 (各文にちょうど一つの precedence correct
な木が存在する) も得られる。
優先順位の向きは論文に従い「数が大きいほど結合が弱い」。
yacc では後に宣言した行ほど結合が強いので、数は宣言順の逆になる。 *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(** 演算子の種類 (論文の Left, Right, Pre, Post) *)
Inductive kind := InL | InR | Pre | Post.
Section Prec.
Variables atom op : Type.
Variable P : op -> nat. (* 優先順位 *)
Variable kind_of : op -> kind.
(** 論文の仮定: 種類の異なる演算子は同じ優先順位を持たない。
(yacc でも一つの %left/%right 行は一つの結合性しか持たない。)
原子式の重み 0 と区別するため優先順位は正とする。 *)
Hypothesis P_pos : forall o, 0 < P o.
Hypothesis P_kind : forall a b, P a = P b -> kind_of a = kind_of b.
Definition is_infix o := if kind_of o is (InL | InR) then true else false.
Definition is_prefix o := if kind_of o is Pre then true else false.
Definition is_postfix o := if kind_of o is Post then true else false.
Definition is_left o := if kind_of o is InL then true else false.
(** ** 構文木と字句列 *)
Inductive tree :=
| Leaf of atom
| Inf of tree & op & tree
| Pref of op & tree
| Postf of tree & op.
Inductive token := Atom of atom | Op of op.
Fixpoint flatten t :=
match t with
| Leaf a => [:: Atom a]
| Inf l o r => flatten l ++ Op o :: flatten r
| Pref o t => Op o :: flatten t
| Postf t o => flatten t ++ [:: Op o]
end.
(** ** 論文の定義 (Definition 3, 4) *)
Fixpoint Lw t :=
match t with
| Leaf _ => 0
| Inf l o _ => maxn (P o) (Lw l)
| Pref _ _ => 0
| Postf t o => maxn (P o) (Lw t)
end.
(** 論文では Rw(lt op rt) = max(P(op), Lw(rt)) と印刷されているが、
本文の説明どおり Rw(rt) とする。 *)
Fixpoint Rw t :=
match t with
| Leaf _ => 0
| Inf _ o r => maxn (P o) (Rw r)
| Pref o t => maxn (P o) (Rw t)
| Postf _ _ => 0
end.
(** [lbound o w]: 右重み w の木が o の左オペランドになれる。
[rbound o w]: 左重み w の木が o の右オペランドになれる。 *)
Definition lbound o w :=
match kind_of o with InL => w <= P o | InR | Post => w < P o | Pre => false end.
Definition rbound o w :=
match kind_of o with InR => w <= P o | InL | Pre => w < P o | Post => false end.
Fixpoint pc t :=
match t with
| Leaf _ => true
| Inf l o r => [&& is_infix o, pc l, pc r, lbound o (Rw l) & rbound o (Lw r)]
| Pref o t => [&& is_prefix o, pc t & rbound o (Lw t)]
| Postf t o => [&& is_postfix o, pc t & lbound o (Rw t)]
end.
(** ** yacc の LR 構文解析器のモデル
この文法の LR オートマトンの状態はスタックの形で決まる:
- [SA fs] : オペランドを待っている (直前が演算子か先頭)
- [SB fs t] : オペランド [t] を還元し終えた
[fs] は未完了の規則 [E inl . E] / [pre . E] の列 (先頭がスタック最上部)。
競合が起こるのは [SB] で、スタック最上部が [E o E .] または [o E .]、
先読みが中置/後置演算子 [l] の場合だけである。yacc の規則
(規則の優先順位 = 規則中の演算子 [o] の優先順位) により:
- [o] が [l] より強ければ reduce、弱ければ shift
- 同じ優先順位なら %left は reduce、%right は shift
入力終端では常に reduce。原子式 [atom] と後置規則 [E post] は
shift 直後に競合なしで reduce される。 *)
Inductive frame := FInf of tree & op | FPre of op.
Definition fop f := match f with FInf _ o => o | FPre o => o end.
Definition combine f t :=
match f with FInf l o => Inf l o t | FPre o => Pref o t end.
Definition should_reduce o (la : option op) :=
match la with
| None => true
| Some l => (P o < P l) || ((P o == P l) && is_left l)
end.
Arguments should_reduce : simpl never.
Fixpoint reduce fs t la :=
match fs with
| [::] => ([::], t)
| f :: fs' =>
if should_reduce (fop f) la then reduce fs' (combine f t) la else (fs, t)
end.
Inductive state := SA of seq frame | SB of seq frame & tree.
Fixpoint run st ts :=
match ts with
| [::] => if st is SB fs t then Some (reduce fs t None).2 else None
| tk :: ts' =>
match st, tk with
| SA fs, Atom a => run (SB fs (Leaf a)) ts'
| SA fs, Op o => if is_prefix o then run (SA (FPre o :: fs)) ts' else None
| SB _ _, Atom _ => None
| SB fs t, Op o =>
match kind_of o with
| Pre => None
| Post => let: (fs', t') := reduce fs t (Some o) in
run (SB fs' (Postf t' o)) ts'
| _ => let: (fs', t') := reduce fs t (Some o) in
run (SA (FInf t' o :: fs')) ts'
end
end
end.
Definition parse ts := run (SA [::]) ts.
(** ** 主定理: yacc 流の競合解決で得られる木 = 論文の precedence correct な木 *)
Theorem yacc_iff_pc ts t : parse ts = Some t <-> pc t /\ flatten t = ts.
Admitted.
End Prec.
読んでみると、だいたいは論文の定義のままで（論文の間違いの修正はされている）、読むのが面倒なのは LR parser の実行の run 関数あたりくらいだな。 この形式化だと、二項演算子と単項演算子専用になっているので、一般的な LR parser ではない。 でも、run を読んで、頭の中にある LR parser の動作と整合していることを確認すれば、最終的な定理 yacc_iff_pc ts t : parse ts = Some t <-> pc t /\ flatten t = ts を信じることができる。 トークン列 ts を yacc 流に parse した結果、(syntax error がなく) 成功して木構造 t が得られるのと、 論文の pc (precedence correct) という性質が成り立つ木 t の葉を並べたトークン列が ts であることは等価である、という。
というわけで、演算子の優先順位についての長年の疑問が解決してちょっとすっきりした。 もちろんこれはひとつの定義であって、異なる定義がまちがっているというわけではないが、すくなくともひとつ納得できる定義があるということはわかった。
Lean の if 式は if c then t else e という普通の形なのだが、 条件節 c には命題を書くというのが面白い。
if c then t else e という式は ite という関数を用いて ite c t e と実装される。 ただし、ここには Decidable c 型の暗黙の引数が隠れていて、場合分けはこの Decidable c 型の引数に対して行われる。
<URL:https://github.com/leanprover/lean4/blob/v4.32.1/src/Init/Prelude.lean#L1100-L1121>
/--
`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
-/
/-
Because Lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
-/
@[macro_inline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
h.casesOn (fun _ => e) (fun _ => t)
まぁ、bool の式を書きたければ if term = true then t else e と書けばいいので、上位互換であると言えるかも知れない。
でも、こんなところに依存型を使うと、厄介なことが起きるのではないかと思って考えてみて、以下の例を思いついた。
theorem foo (a b : Nat) : (if a < b then 1 else 2) = (if (1+a) < (1+b) then 1 else 2) := by
rw [Nat.add_lt_add_iff_left] -- この rw が失敗する
#check Nat.add_lt_add_iff_left
-- Nat.add_lt_add_iff_left {k n m : Nat} : k + n < k + m ↔ n < m
ここでは条件節が a < b と (1+a) < (1+b) と違いだけの項が等しい、ということを証明しようとしている。 そのために Nat.add_lt_add_iff_left を使って (1+a) < (1+b) を a < b に書き換えようとしている。 しかし、その書き換えが失敗する。 これは、ite 関数の条件節 (命題な引数) を書き換えても、Decidable な引数がそのままで、 それらが整合しなくなってしまうからである。
まぁ、simp [Nat.add_lt_add_iff_left] とすると動くので、rw でうまくいかなかったら simp を使えば良い、と対応されている話ではあるのかも。
命題は証明可能と反証可能以外に、証明も反証もできないということがあり得るので、 true と false の 2種類に場合分けできるとは限らない。
しかし、2種類に場合分けできることも多々ある。
そのようなことを示すのに、SSReflect では、reflect という型で命題と bool が対応していることを表現する。
<URL:https://github.com/rocq-prover/rocq/blob/v9.3/theories/Corelib/Init/Datatypes.v#L51-L59>
(************************************************)
(** * Reflect: a specialized inductive type for
relating propositions and booleans,
as popularized by the Ssreflect library. *)
(************************************************)
Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
Lean には Decidable という型があって、ある命題が判定可能であることを表現する。
<URL:https://github.com/leanprover/lean4/blob/v4.32.1/src/Init/Prelude.lean#L962-L976>
`Decidable` instances are primarily used via `if`-expressions and the tactic `decide`. In
conditional expressions, the `Decidable` instance for the proposition is used to select a branch. At
run time, this case distinction code is identical to that which would be generated for a
`Bool`-based conditional. In proofs, the tactic `decide` synthesizes an instance of `Decidable p`,
attempts to reduce it to `isTrue h`, and then succeeds with the proof `h` if it can.
Because `Decidable` carries data, when writing `@[simp]` lemmas which include a `Decidable` instance
on the LHS, it is best to use `{_ : Decidable p}` rather than `[Decidable p]` so that non-canonical
instances can be found via unification rather than instance synthesis.
-/
class inductive Decidable (p : Prop) where
/-- Proves that `p` is decidable by supplying a proof of `¬p` -/
| isFalse (h : Not p) : Decidable p
/-- Proves that `p` is decidable by supplying a proof of `p` -/
| isTrue (h : p) : Decidable p
reflect も Decidable も、場合分けすると真の場合と偽の場合に分かれるので、 真でも偽でもない (その命題を証明も反証もできない) ということはありえないことを示している。
reflect と Decidable の違いは、bool の index である。 reflect と Decidalbe は引数の数が異なり、前者は 2引数で、後者は 1引数である。 最初の引数は命題でどちらも同じだが、reflect は reflect P b と bool な第2引数がある。
reflet は、命題と bool の関係を示しているので、命題と bool を変換することに利用できる。 これに対して、Lean の Decidable は、単に命題が判定可能という性質を示すだけなので、bool との変換は想定されていないのだと思う。 これは、Lean が bool よりは命題を好むことと関係しているのかも。
あと、reflect の index は、場合分けをしたときに同時に書き換えを行うのに利用される。 これにより、いちいち書き換えをするように指定しなくてよいので便利である。
まず、命題は計算できない。True と True /\ True は異なる項であり、型検査でも区別される。
それに対して bool の式は計算できる。 そして、CIC の型検査はそういった計算による変形をしても同じ項とみなす。
そのため、term = true という命題で term を計算して true になるなら、 reflexivity (rfl) でそのまま証明できる。
ただ、term に変数が入っていると計算が進まない。 たとえば、x || ~~ x = true は x の具体的な値が不明なので、 orb (||) や negb (~~) の内部での場合分けが簡約できない。 そこで変数 x を場合分けすると、x が true に置換された場合と false に置換された場合の変数が消えたふたつの goal ができて、 あとは計算で証明を終わらせられる。
ということを SSReflect では by case: x. などと書くわけである。 変数が複数あっても by case: x; case: y. などと証明できるので簡単である。 (ただ、変数が多くなってくるとサブゴールが多くなりすぎて証明に時間がかかってしまうが、そんなにたくさんの変数が出てくることは稀である。)
なお、この計算というのは、true || x は計算が進んで x になるが、x || true は計算を進められないなど、 関数 (この場合 orb) の中身に依存した挙動がある。 仕組みを理解していればわかるのだが、わかりやすいとはいえないかもしれない。
上にも書いたが、この計算というのは bool だからできるのであって、命題ではできない。
しかし、Lean の simp は上述の、命題の部分項を rewrite できるという機能を利用し、命題の単純化も行う。 simp はデフォルトでいろいろな定理を利用するが、その中には or_true と true_or も含まれており、 命題の単純化もしてしまう。
or_true (p : Prop) : (p ∨ True) = True true_or (p : Prop) : (True ∨ p) = True
これは命題で計算しているようなものかも知れない。
まず、bool の便利なところとして、部分項を rewrite できるという点がある。 これは rewrite というのは内部的には eq_ind_r : forall [A : Type] [x : A] (P : A -> Prop), P x -> forall [y : A], y = x -> P y の適用であり、 goal をまず P y という関数適用の形に変形し、y を置き換えて x にする、というものだからで、 P y という形で括り出せるかぎりはどの部分項でも置換できるからである。
それに対して、A <-> B という前提があっても、 素朴にはゴール全体を A から B に変える、あるはその逆にしか使えない。 これは、A <-> B の証明は、A -> B の証明と B -> A の証明のペアだからである。 A -> B の証明があれば、apply により goal を B から A に変えられる。 しかし apply というのは goal 全体に適用するものであり、 goal の部分項に apply するということはできない。 したがって、部分項を書き換えることは (素朴には) できないのである。
ところが、Lean では命題でも部分項を rewrite できる。
theorem foo (A B C : Prop) (h : A <-> B) : (A /\ C) <-> (B /\ C) := by rw [h] #print foo /- theorem foo : ∀ (A B C : Prop), (A ↔ B) → (A ∧ C ↔ B ∧ C) := fun A B C h => Eq.mpr (id (congrArg (fun _a => _a ∧ C ↔ B ∧ C) (propext h))) Iff.rfl -/
証明項をみると、propext というのが使われている。 propext というのは、公理 propositional extensionality のようだ。 公理を使って、命題の等価性 (<->) を等値性 (=) に変換して、部分項を書き換えているようだ。
ちなみに、最近は Rocq でも setoid rewrite により似たことが可能になった。
Require Setoid.
Theorem foo (A B C : Prop) (h : A <-> B) : (A /\ C) <-> (B /\ C).
Proof.
rewrite h.
reflexivity.
Qed.
Print foo.
(*
foo =
fun (A B C : Prop) (h : A <-> B) =>
(fun lemma : A <-> B =>
Morphisms.trans_co_eq_inv_impl_morphism RelationClasses.iff_Transitive
(A /\ C) (B /\ C)
(Morphisms_Prop.and_iff_morphism A B lemma C C
(Morphisms.reflexive_proper_proxy
(Morphisms.reflexive_reflexive_proxy RelationClasses.iff_Reflexive) C))
(B /\ C) (B /\ C) (Morphisms.eq_proper_proxy (B /\ C)))
h (RelationClasses.reflexivity (B /\ C))
: forall A B C : Prop, A <-> B -> A /\ C <-> B /\ C
*)
証明項をみると、Lean よりも Rocq のほうがずいぶんと長い。 これは公理を使わずにがんばって実現しているためだろう。
形式証明において、本質的ではない面倒くささの一端は、 似ているけれど違うので直接は使えない、という状況に真面目に対応する必要があることである。
CIC (Rocq とか Lean の基礎) において、命題と bool はまさにこの典型例である。 命題と bool はどちらも成り立ったり成り立たなかったりするし、 and や or といった論理演算はどちらにも存在して、対応がある。
ここで、Rocq/SSReflect でも Lean でも、命題の and は /\ 演算子で表現し、bool の and は && 演算子で表現する。
そして、一方 (例えば bool 式) が真であることがわかっている場合に、 対応するもう一方 (命題) が真であることを証明しようとするのは、 素朴な CIC では手間がかかる。 人間の感覚としては自明なのに手間が必要というのは、そこには改善の余地があるということだ。
また、bool と命題では証明を行うときの便利さが異なる。
bool が便利なところ:
命題が便利なところ:
証明においてはこれら両方の便利さを利用したいわけで、 SSReflect や Lean ではそれなりに系統的な対策が行われている。
どういう対策かというと、SSReflect では、bool で表現できるものはなるべく bool で表現し、必要になった場合には bool と命題を簡単に変換できる、というようになっている。 (このへんは mathcomp book に詳しい。)
Lean では (少し観察した限りでは) なるべく命題で扱うようになっていると思う。 たとえば、if 式では条件節に bool ではなく命題を書く。 しかし、bool には bool の便利さがあるので、その便利さもなるべく得られるような仕掛けがある。
Lean 4 では証明の中で現在証明している定理を利用できる。
つまり再帰できるわけだが、Lean は一般の再帰はできない (recursor しか使えない) はずなので、 equation compiler がどうやってコンパイルしているのか気になる。
これはどうやっているか調べると、 構造再帰で済む場合には帰納型の recursor を使い、 それでは済まない場合は整礎帰納法になるようだ。 整礎帰納法の場合、引数が小さくなることの証明が必要だが、簡単な場合は自動証明で済み、そうでなければ人間が与える、ということらしい。
プリミティブはなるべく一般的にしたほうがいい。 前回は idkeys, ctkeys, values, idin, ctin, idfind, ctfind, idlookup, ctlookup と個々に関数を定義していたのを、 今回は lookup だけで済ましている。 これにより個々の関数について用意していた補題が、lookup についての補題だけを用意するだけ済む。 また、補題を使うときも選択肢が減って考えることが少なくなる。 再帰関数として lookup を定義したことにより、(引数にコンストラクタが渡された場合に) 期待した形に計算を進めるのを simpl で可能になった。 これにより計算を進める補題が減った。 lookup ... = None でなく ~~ lookup ... という形で扱うことにした利点を確認したところ、明確に利点があったのが一ヶ所あった。 lookupP で ~~ lookup ... を生成した結果を対偶 (contraNN) の前提として使っていて、これは lookup ... = None という形だと扱いにくい。 他は None の形でもあまり困らなかった気がする。 LLM にファイル全体をつっこんで証明の改善を提案させると、いろいろ提案してくる。 プリミティブをまとめたほうがいいというのは、自分でもはじめから思っていて、LLM も必ず指摘するのでやったのだが、 in_lookupv と in_lookupb の両方が必要とか、微妙なところはやってみないとわからなくて、LLM はそのへんでうまくいかないことを伝えるとうまい解決法を提示できず、 ぜんぜん違う方法 (関数を使わない形) でやりなおすといいとか言ってくるので提案を取り入れるかどうかは人間の判断力が必要になる。 あと、具体的な証明を提示してくることもあるけれど、基本的に間違っていて Rocq を通る証明が出てくることはまずない。 ただ、一回だけ、自分では wfassoc_singlevalue を帰納法で証明していたのを in_lookupv で簡単に証明できるとしてきたのはそのまま通って素晴らしかった。 (in_lookupv は (k, v) \in assoc ならば lookup k assoc = Some v というもので、in が関数のように振る舞うという意味とみなせて、wfassoc_singlevalue はまさにそうやって証明できる。 ) まぁ、結局 wfassoc_singlevalue は使わなくなってしまったのだが。
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)
*)