『なんとなく』が許せない人のための Lean 4： Std.DHashMap編

依存型と証明を学習するにあたり、simpなどの自動化を目指す前に、カリーハワード（いずれはランベックも）対応によるプログラミングとはいかなるものか体験してみようと思いたち、その学習過程の記録を残すことにした。

最終的には、HTTPヘッダやJSONの置き場所として依存ハッシュマップの実務的なBCPを目指したいが、まずは、証明そのもののやり方を学んでいこうと思う。

ケース１　依存しないパターン

最初に頭に浮かんだ依存ハッシュマップのナイーブな使い方。

ヘテロリストのマップ版を考えていたが、依存ハッシュマップに触りたてでリゾルバの使い方などが分からなかったので、直和型を返すことにした。キーに依存するのではなく動的型付け言語のようなハッシュマップ。ただし、許容する型に制約を設けてある。

レンズのようなアクセス用の関数を別途用意するのでなければ、使い勝手も保守性も悪いので実用性はないが、証明でリゾルバに入り込む必要がないので導入の事例としてみた。

なお、Sum型の中置演算子は右結合。

import Std.Data.DHashMap

namespace hashmap_naive

  inductive MyError where
    | error1
    | error2
    deriving Repr

  def s : Std.DHashMap String (λ _ ↦ (Nat ⊕ String ⊕ Bool ⊕ MyError)) :=
    Std.DHashMap.emptyWithCapacity
      |>.insert "foo" (Sum.inl 123)
      |>.insert "bar" ((Sum.inr ∘ Sum.inl) "blah")
      |>.insert "baz" ((Sum.inr ∘ Sum.inr ∘ Sum.inl) true)
      |>.insert "qux" ((Sum.inr ∘ Sum.inr ∘ Sum.inr) .error2)
      |>.insert "qux" ((Sum.inr ∘ Sum.inr ∘ Sum.inr) .error1) -- 上書き

  -- ### ランタイムでの動作確認
  -- simpでもnative_decideでも可能。
  -- ただし、native_decideは固有の制限がある模様。後の課題とする。
  -- パフォーマンスはnative_decideの方が早いのかもしれないが未検証。
  #eval s.get "foo" (by simp [s]) -- Sum.inl 123
  #eval s.get "qux" (by native_decide) -- Sum.inr (Sum.inr (Sum.inr (MyError.error1)))

  -- ### 型レベルでの存在の証明
  -- コンパイル時点で存在が確定できるものであれば、`s` にエントリー `foo` や `qux` が
  -- 存在していることを強制できるので、`Maybe` や `Option` 地獄から解放される。
  -- （だけならば嬉しいのだが、依存型と証明を使うことは深淵を覗くことであるのかもしれない）
  example : "foo" ∈ s := by simp [s, Std.DHashMap.mem_insert]
  example : "qux" ∈ s := by simp [s, Std.DHashMap.mem_insert]

  -- ### 値の確認
  -- "foo" ∈ s ∧ s["foo"] = n : Nat
  -- １つ１つ手動で証明をしてみる。ただし、このやり方だと`s`が変更されるたびに証明は壊れる。
  example : ∃ (n : Nat), s.get "foo" (by simp [s]) = Sum.inl n := by
    exists 123
    unfold s

    -- 1. "qux" (error1) vs "foo"
    rw [Std.DHashMap.get_insert]
    split -- if "qux" == "foo" ...
    · rename_i h; simp at h -- 一致したとする枝は矛盾 (qux != foo)
    -- 不一致だった(else)枝で、次の get が現れる

    -- 2. "qux" (error2) vs "foo"
    rw [Std.DHashMap.get_insert]
    split
    · rename_i h; simp at h

    -- 3. "baz" vs "foo"
    rw [Std.DHashMap.get_insert]
    split
    · rename_i h; simp at h

    -- 4. "bar" vs "foo"
    rw [Std.DHashMap.get_insert]
    split
    · rename_i h; simp at h

    -- 5. "foo" に到達
    rw [Std.DHashMap.get_insert_self]

  -- quxエントリーが存在していて、かつ、それがMyErrorである。
  example
    : ∃ (e : MyError)
    , s.get "qux" (by native_decide) = (Sum.inr ∘ Sum.inr ∘ Sum.inr) e
    := by
      exists MyError.error1
      unfold s
      conv =>
        lhs
        rw [Std.DHashMap.get_insert_self]

end hashmap_naive

ケース２　依存するパターン

依存ハッシュマップを使いつつ、ナイーブなアプローチより使い勝手を向上させたい。
そのために依存解決コールバック resolver を定義する。

namespace hashmap_refined

  inductive MyError where
    | error1
    | error2

  -- diteをiteと書き換えて試行錯誤していたときは、@[reducible]属性が必要だったが、間違
  -- いを修正したあとはこの属性がなくとも型チェックするようになった。
  -- `h :`という数文字の入力忘れで連鎖的にさまざまな場所で躓いた。
  -- どこが躓きの原因だったかは後述する。
  def resolver : String → Type
    | "natural" => Nat
    | "string" => String
    | "boolean" => Bool
    | "my_error" => MyError
    | _ => String -- その他のエントリーは文字列型として許容する。

  def s₁ : Std.DHashMap String resolver :=
    Std.DHashMap.emptyWithCapacity
      |>.insert "natural" (123 : Nat)
      |>.insert "string" "you are my sun shine"
      |>.insert "boolean" true
      |>.insert "my_error" .error2
      |>.insert "foo" "undefined"
      |>.insert "bar" "undefined neither"
      |>.insert "my_error" .error1 -- .error1に上書き

  #eval s₁.get "my_error" (by native_decide) -- MyError.error1

  -- ### 存在の証明
  -- パターン1: "natural" エントリーが存在することの証明は簡単。
  example : "natural" ∈ s₁ := by simp [s₁]

  -- パターン2:
  -- key ∈ s₁ は Decidable (判定可能) なので、native_decide が使える。
  example : "natural" ∈ s₁ := by native_decide

  -- さらに、再利用を鑑みて定理として定義しておく。
  theorem natural_exists : "natural" ∈ s₁ := by
    native_decide

  example : "natural" ∈ s₁ := natural_exists

  -- ### 値の確認
  -- しかし、"natural" エントリーの値を証明しようとすると大変。
  -- スマートなやり方がではなく壊れやすくもあり実用的ではないものの、まずはなるべく手動
  -- で証明してみる。
  example : s₁.get "natural" natural_exists = (123 : Nat) := by
    unfold s₁
    conv =>
      lhs
      rw [Std.DHashMap.get_insert]
      change if h : "my_error" == "natural" then _ else _ -- 一番最後のinsert
      -- ^ *重要* change直前のif-then-elseはditeであることを確認し忘れて、iteに書き換
      -- えると証明が壊れる。
      -- InfoViewでrw直後のフォーカスを見てみると、このif-then-else(ite)がdependent
      -- if-then-else(dite)であることが確認できる。
      -- たとえば、もしここで `"my_error" == "natural" then` としてしまうと、rw直後
      -- にはditeだったものが、change後にiteに書き変わってしまう。これは、iteとditeで
      -- 微妙にif肢の定義が違うから。また、elseの引数`h`も取得できなくなってしまう。
      -- 不注意でiteに書き換えてたことに気づかず、証明が進まなくなり、かなり時間を浪費
      -- してしまった。
      enter [3, h₁]
      -- ここでの3という数字はditeの明示的な引数の順番である。diteには(c : Prop)
      -- (t : c → α) (e : Not c → α) という3つの明示的な引数がある。3番目はelse肢を
      -- 指しているということになる。
      -- なお、依存if-then-elseは `dite c (fun h => t(h)) (fun h => e(h))` の構文糖。
      -- ただし、AIによれば状況によってはこの番号が異なることもあるらしいので、InfoView
      -- でコンテキストを確認したほうがよさそうだ。
      --
      -- diteのシグネチャは次の通り。
      -- `def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α`
      -- argやenterに渡す数値は、FFIでLeanオブジェクトを作成する際に
      -- lean_alloc_ctorに渡す数値とは異なりそうだ。

      rw [Std.DHashMap.get_insert] -- if "bar" == "natural"
      enter [3, h₂]
      -- ここでは変数名を衝突しないように命名しているが、仮に同じ変数名を使ってしまっても
      -- Leanが自動的に衝突しないよう調節してくれる。
      rw [Std.DHashMap.get_insert] -- if "foo" == "natural"
      enter [3, h₃]
      rw [Std.DHashMap.get_insert] -- if "my_error" == "natural"
      arg 3
      ext h₄
      -- enter [3, h] は arg 3; ext hと等しい。
      rw [Std.DHashMap.get_insert] -- if "boolean" == "natural"
      enter [3, h₅]
      rw [Std.DHashMap.get_insert] -- if "string" == "natural"
      enter [3, h₆]
      rw [Std.DHashMap.get_insert_self] -- ここでようやく123を取り出せた。
      --^ このレンマは挿入した値はそのまま取り出せるというもの。
      change (123 : Nat)
    rfl

  -- repeat を使って手間を減らす。
  example : s₁.get "natural" natural_exists = (123 : Nat) := by
      unfold s₁
      conv =>
        lhs
        repeat (
          first -- １つめの肢から成功するまで順に試す
          | rw [Std.DHashMap.get_insert_self]
          | rw [Std.DHashMap.get_insert]
            enter [3, h]
            --^ ここの h は名前の衝突が起こらないよう自動的に調整される。
        )
        change (123 : Nat)
      rfl

  -- simp を使って手間を減らす。
  -- しかし、なにをやっているのかはわからない。
  -- 既存のレンマを使いこなせるようにならなければいけなさそう。
  example : s₁.get "natural" natural_exists = (123 : Nat) := by
    unfold s₁
    conv =>
      lhs
      simp only
        [ Std.DHashMap.get_insert
        , reduceIte
        ]
    rfl

  -- もっと簡単にしてみる。ここまでくると何をやっているのかわからない。
  -- どんなことをしているのかは `simp` を `simp?` にしてInfoViewで確認できる。
  example : s₁.get "natural" natural_exists = (123 : Nat) := by
    simp? [ s₁, Std.DHashMap.get_insert ]
    -- Try this:
    --   [apply] simp only [s₁, Std.DHashMap.get_insert, String.reduceBEq,
    --                      Bool.false_eq_true, ↓reduceDIte,
    --                      Std.DHashMap.get_insert_self]

end hashmap_refined

補遺

今回の試みを通じて、直感主義論理に基づく証明とプログラミングの対応関係を教科書で目にした時際のトキメキは、学習の途上ではあるものの、感じる余裕はなかった。

依存ハッシュマップより先にiteとditeの違いをきちんと調べることが必要だったので、これも今後の課題としたい。とくに何番目の枝を狙うかというメカニズムの部分の理解が甘い。

基本的なレンマの習熟が必要そうだ。

TODO: 読む https://leanprover-community.github.io/mathlib4_docs/Init/SimpLemmas.html#or_self

依存ハッシュマップに関連するレンマの習熟も今後の課題になりそうだ。どこまで潜り込めばよいのか見当はつかない。

データ量が巨大になった場合のパフォーマンスは未確認。

動的言語のような依存ハッシュマップを型クラスと実装で再帰的に表現できないかと試みたがうまくいかなかった。推論を進めていく過程でどの分岐に該当するのか型チェッカが迷っていた。instance (priority := high)など、評価の優先度を変える仕組みもあるようだが、問題を解決できないままあきらめることとなった。

decideやnative_decideで、コンパイル時にハッシュマップを評価できれば簡単に値が取り出せて証明が自明になりそうだが、これもうまくいかなかった。native_decideには制限もあるようなので、詳細の学習は今後の課題としたい。
AIによると「key ∈ s という命題は Bool を返す計算（決定可能）に還元できるが、s.get ... = 123 という等式の証明には、get の引数に含まれる『証明項』の簡約が必要になるため、native_decide だけでは届かない壁がある」らしいが、よく理解できていない。

機会があればBatteries.Data.HashMapも試してみたい。