import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesBucketizeset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Bucketizetheorem loop_spec (v boundaries : Tensor ℝ [3]) : Loop.bucketize v boundaries = fun i => if decide (v i ≥ boundaries (2, ())) then 3 else if decide (v i ≥ boundaries (1, ())) then 2 else if decide (v i ≥ boundaries (0, ())) then 1 else 0 := byv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries = fun i => if decide (v i ≥ boundaries (2, ())) = true then 3 else if decide (v i ≥ boundaries (1, ())) = true then 2 else if decide (v i ≥ boundaries (0, ())) = true then 1 else 0 funext ⟨i, u⟩v:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3u:Index []⊢ Loop.bucketize v boundaries (i, u) = if decide (v (i, u) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, u) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, u) ≥ boundaries (0, ())) = true then 1 else 0 cases uunitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3⊢ Loop.bucketize v boundaries (i, PUnit.unit) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 fin_cases iunit.«0»v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = if decide (v ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0unit.«1»v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = if decide (v ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0unit.«2»v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = if decide (v ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 <;>unit.«0»v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = if decide (v ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0unit.«1»v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = if decide (v ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0unit.«2»v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Loop.bucketize v boundaries ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = if decide (v ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 rflAll goals completed! 🐙 theorem matches_loop (v boundaries : Tensor ℝ [3]) : Array.bucketize v boundaries = Loop.bucketize v boundaries := byv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = Loop.bucketize v boundaries rw [loop_specv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = fun i => if decide (v i ≥ boundaries (2, ())) = true then 3 else if decide (v i ≥ boundaries (1, ())) = true then 2 else if decide (v i ≥ boundaries (0, ())) = true then 1 else 0v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = fun i => if decide (v i ≥ boundaries (2, ())) = true then 3 else if decide (v i ≥ boundaries (1, ())) = true then 2 else if decide (v i ≥ boundaries (0, ())) = true then 1 else 0]v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = fun i => if decide (v i ≥ boundaries (2, ())) = true then 3 else if decide (v i ≥ boundaries (1, ())) = true then 2 else if decide (v i ≥ boundaries (0, ())) = true then 1 else 0 funext ⟨i, u⟩v:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3u:Index []⊢ Array.bucketize v boundaries (i, u) = if decide (v (i, u) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, u) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, u) ≥ boundaries (0, ())) = true then 1 else 0 cases uunitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3⊢ Array.bucketize v boundaries (i, PUnit.unit) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 let cell (j : Fin 3) := if decide (v (i, ()) ≥ boundaries (j, ())) then (j.val : ℝ) + 1 else 0unitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0⊢ Array.bucketize v boundaries (i, PUnit.unit) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 change max (max (max (cell 0) (cell 0)) (cell 1)) (cell 2) = _unitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0⊢ max (max (max (cell 0) (cell 0)) (cell 1)) (cell 2) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 rw [max_selfunitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0⊢ max (max (cell 0) (cell 1)) (cell 2) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0unitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0⊢ max (max (cell 0) (cell 1)) (cell 2) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0]unitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0⊢ max (max (cell 0) (cell 1)) (cell 2) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 dsimp [cell]unitv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 by_cases h0 : v (i, ()) ≥ boundaries (0, ())posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 <;>posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 by_cases h1 : v (i, ()) ≥ boundaries (1, ())posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 <;>posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 by_cases h2 : v (i, ()) ≥ boundaries (2, ())posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())h2:v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())h2:¬v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 <;>posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())h2:v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())h2:¬v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())h2:v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())h2:¬v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())h2:v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:v (i, ()) ≥ boundaries (1, ())h2:¬v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0posv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())h2:v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0negv:Tensor ℝ [3]boundaries:Tensor ℝ [3]i:Fin 3cell:Fin 3 → ℝ := fun j => if decide (v (i, ()) ≥ boundaries (j, ())) = true then ↑↑j + 1 else 0h0:¬v (i, ()) ≥ boundaries (0, ())h1:¬v (i, ()) ≥ boundaries (1, ())h2:¬v (i, ()) ≥ boundaries (2, ())⊢ max (max (if decide (v (i, ()) ≥ boundaries (0, ())) = true then ↑0 + 1 else 0) (if decide (v (i, ()) ≥ boundaries (1, ())) = true then ↑1 + 1 else 0)) (if decide (v (i, ()) ≥ boundaries (2, ())) = true then 2 + 1 else 0) = if decide (v (i, PUnit.unit) ≥ boundaries (2, ())) = true then 3 else if decide (v (i, PUnit.unit) ≥ boundaries (1, ())) = true then 2 else if decide (v (i, PUnit.unit) ≥ boundaries (0, ())) = true then 1 else 0 norm_num [h0, h1, h2]All goals completed! 🐙 theorem certificate (v : Tensor ℝ [3]) (boundaries : Tensor ℝ [3]) : Jaxpr.Program.eval (.cons v (.cons boundaries .nil)) Array.bucketize_ir = Jaxpr.Program.eval (.cons v (.cons boundaries .nil)) Loop.bucketize_ir := byv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Jaxpr.Program.eval (Jaxpr.Env.cons v (Jaxpr.Env.cons boundaries Jaxpr.Env.nil)) Array.bucketize_ir = Jaxpr.Program.eval (Jaxpr.Env.cons v (Jaxpr.Env.cons boundaries Jaxpr.Env.nil)) Loop.bucketize_ir rw [Array.bucketize_translation_correct,v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = Jaxpr.Program.eval (Jaxpr.Env.cons v (Jaxpr.Env.cons boundaries Jaxpr.Env.nil)) Loop.bucketize_irv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = Loop.bucketize v boundaries Loop.bucketize_translation_correctv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = Loop.bucketize v boundariesv:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = Loop.bucketize v boundaries]v:Tensor ℝ [3]boundaries:Tensor ℝ [3]⊢ Array.bucketize v boundaries = Loop.bucketize v boundaries exact matches_loop v boundariesAll goals completed! 🐙end JaxLean.Puzzles.Bucketize