LeanMachineLearning

Learning.action_stepsUntilπŸ”—

Lemma

No docstring.

πŸ”—theorem
Learning.action_stepsUntil.{u_1, u_3} {𝓐 : Type u_1} {Ξ© : Type u_3}
  [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {m : β„•} {Ο‰ : Ξ©} (hm : m β‰  0)
  (h_exists : βˆƒ s, pullCount A a (s + 1) Ο‰ = m) :
  A (ENat.toNat (stepsUntil A a m Ο‰)) Ο‰ = a
Learning.action_stepsUntil.{u_1, u_3}
  {𝓐 : Type u_1} {Ξ© : Type u_3}
  [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐}
  {m : β„•} {Ο‰ : Ξ©} (hm : m β‰  0)
  (h_exists :
    βˆƒ s, pullCount A a (s + 1) Ο‰ = m) :
  A (ENat.toNat (stepsUntil A a m Ο‰)) Ο‰ =
    a

Code

lemma action_stepsUntil (hm : m β‰  0) (h_exists : βˆƒ s, pullCount A a (s + 1) Ο‰ = m) :
    A (stepsUntil A a m Ο‰).toNat Ο‰ = a
Proof
by
  classical
  simp only [stepsUntil_eq_dite, h_exists, ↓reduceDIte, ENat.toNat_natCast]
  have h_spec := Nat.find_spec h_exists
  have h_spec' n := Nat.find_min h_exists (m := n)
  by_cases h_zero : Nat.find h_exists = 0
  Β· simp only [h_zero, zero_add, not_lt_zero, IsEmpty.forall_iff, implies_true] at *
    by_contra h_ne
    rw [← zero_add 1, pullCount_eq_pullCount_of_action_ne h_ne] at h_spec
    simp only [pullCount_zero] at h_spec
    exact hm h_spec.symm
  have h_pos : 0 < Nat.find h_exists := Nat.pos_of_ne_zero h_zero
  by_contra h_ne
  refine h_spec' (Nat.find h_exists - 1) ?_ ?_
  Β· simp [h_pos]
  rw [Nat.sub_add_cancel (by omega)]
  rwa [← pullCount_eq_pullCount_of_action_ne]
  exact h_ne

Actions: Source Β· Open Issue

Meaning last changed in v4.34.0-rc1-3-g2cf8f3b (2026-08-20).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file Β· open it in the Lean web editor.

Dependency graph

Audit surface: 2 project declarations, 27 external constants

βœ“ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.