import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesBincountset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Bincounttheorem matches_loop (a : Tensor Int32 [3]) : Array.bincount (R := ℝ) a = Loop.bincount (R := ℝ) a := bya:Tensor Int32 [3]⊢ Array.bincount a = Loop.bincount a funext ⟨i, u⟩a:Tensor Int32 [3]i:Fin 3u:Index []⊢ Array.bincount a (i, u) = Loop.bincount a (i, u) cases uunita:Tensor Int32 [3]i:Fin 3⊢ Array.bincount a (i, PUnit.unit) = Loop.bincount a (i, PUnit.unit) fin_cases iunit.«0»a:Tensor Int32 [3]⊢ Array.bincount a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.bincount a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»a:Tensor Int32 [3]⊢ Array.bincount a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.bincount a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»a:Tensor Int32 [3]⊢ Array.bincount a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.bincount a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0»a:Tensor Int32 [3]⊢ Array.bincount a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.bincount a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»a:Tensor Int32 [3]⊢ Array.bincount a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.bincount a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»a:Tensor Int32 [3]⊢ Array.bincount a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.bincount a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) simp only [Array.fn__where, Array.bincount, Loop.fn__where, Loop.loop_masked_sum, Loop.bincount, Tensor.map, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Fin.sum_univ_succ]unit.«2»a:Tensor Int32 [3]⊢ (if decide (↑(a (0, ())).toInt = ↑2) = true then 1 else 0) + ((if decide (↑(a (Fin.succ 0, ())).toInt = ↑2) = true then 1 else 0) + ((if decide (↑(a ((Fin.succ 0).succ, ())).toInt = ↑2) = true then 1 else 0) + ∑ x, if decide (↑(a (x.succ.succ.succ, ())).toInt = ↑2) = true then 1 else 0)) = if ⟨2, ⋯⟩ = 2 then ((0 + if decide (↑(a (⟨0 + 1 * ↑0, ⋯⟩, ())).toInt = 2) = true then 1 else 0) + if decide (↑(a (⟨1 + 1 * ↑0, ⋯⟩, ())).toInt = 2) = true then 1 else 0) + if decide (↑(a (⟨2 + 1 * ↑0, ⋯⟩, ())).toInt = 2) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then ((0 + if decide (↑(a (⟨0 + 1 * ↑0, ⋯⟩, ())).toInt = 1) = true then 1 else 0) + if decide (↑(a (⟨1 + 1 * ↑0, ⋯⟩, ())).toInt = 1) = true then 1 else 0) + if decide (↑(a (⟨2 + 1 * ↑0, ⋯⟩, ())).toInt = 1) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then ((0 + if decide (↑(a (⟨0 + 1 * ↑0, ⋯⟩, ())).toInt = 0) = true then 1 else 0) + if decide (↑(a (⟨1 + 1 * ↑0, ⋯⟩, ())).toInt = 0) = true then 1 else 0) + if decide (↑(a (⟨2 + 1 * ↑0, ⋯⟩, ())).toInt = 0) = true then 1 else 0 else 0 all_goals norm_num [Fin.ext_iff, Bool.cond_decide, decide_eq_true_iff]unit.«2»a:Tensor Int32 [3]⊢ (if ↑(a (0, ())).toInt = 2 then 1 else 0) + ((if ↑(a (1, ())).toInt = 2 then 1 else 0) + if ↑(a (2, ())).toInt = 2 then 1 else 0) = ((if ↑(a (0, ())).toInt = 2 then 1 else 0) + if ↑(a (1, ())).toInt = 2 then 1 else 0) + if ↑(a (⟨2, ⋯⟩, ())).toInt = 2 then 1 else 0 all_goals simp []unit.«2»a:Tensor Int32 [3]⊢ (if ↑(a (0, ())).toInt = 2 then 1 else 0) + ((if ↑(a (1, ())).toInt = 2 then 1 else 0) + if ↑(a (2, ())).toInt = 2 then 1 else 0) = ((if ↑(a (0, ())).toInt = 2 then 1 else 0) + if ↑(a (1, ())).toInt = 2 then 1 else 0) + if ↑(a (2, ())).toInt = 2 then 1 else 0 all_goals ringAll goals completed! 🐙 theorem certificate (a : Tensor Int32 [3]) : Jaxpr.Program.eval (.cons a .nil) Array.bincount_ir = Jaxpr.Program.eval (.cons a .nil) Loop.bincount_ir := bya:Tensor Int32 [3]⊢ Jaxpr.Program.eval (Jaxpr.Env.cons a Jaxpr.Env.nil) Array.bincount_ir = Jaxpr.Program.eval (Jaxpr.Env.cons a Jaxpr.Env.nil) Loop.bincount_ir rw [Array.bincount_translation_correct,a:Tensor Int32 [3]⊢ Array.bincount a = Jaxpr.Program.eval (Jaxpr.Env.cons a Jaxpr.Env.nil) Loop.bincount_ira:Tensor Int32 [3]⊢ Array.bincount a = Loop.bincount a Loop.bincount_translation_correcta:Tensor Int32 [3]⊢ Array.bincount a = Loop.bincount aa:Tensor Int32 [3]⊢ Array.bincount a = Loop.bincount a]a:Tensor Int32 [3]⊢ Array.bincount a = Loop.bincount a exact matches_loop aAll goals completed! 🐙end JaxLean.Puzzles.Bincount