import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesHeavisideset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Heaviside theorem matches_loop (a : Tensor ℝ [3]) (b : Tensor ℝ [3]) : Array.heaviside a b = Loop.heaviside a b := bya:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b = Loop.heaviside a b funext ⟨i, u⟩a:Tensor ℝ [3]b:Tensor ℝ [3]i:Fin 3u:Index []⊢ Array.heaviside a b (i, u) = Loop.heaviside a b (i, u) cases uunita:Tensor ℝ [3]b:Tensor ℝ [3]i:Fin 3⊢ Array.heaviside a b (i, PUnit.unit) = Loop.heaviside a b (i, PUnit.unit) fin_cases iunit.«0»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.heaviside a b ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.heaviside a b ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.heaviside a b ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.heaviside a b ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.heaviside a b ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.heaviside a b ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, This simp argument is unused: Tensor.map Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.concatenate, Tensor.sumFirst, Tensor.reduceSum, Fin.sum_univ_succ, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Tensor.mapunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, This simp argument is unused: Tensor.map₂ Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.concatenate, Tensor.sumFirst, Tensor.reduceSum, Fin.sum_univ_succ, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Tensor.map₂unit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, This simp argument is unused: Tensor.scatterSet_matrix Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.concatenate, Tensor.sumFirst, Tensor.reduceSum, Fin.sum_univ_succ, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Tensor.scatterSet_matrixunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, This simp argument is unused: Tensor.concatenate Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.sumFirst, Tensor.reduceSum, Fin.sum_univ_succ, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Tensor.concatenateunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, This simp argument is unused: Tensor.sumFirst Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.concatenate, Tensor.reduceSum, Fin.sum_univ_succ, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Tensor.sumFirstunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, This simp argument is unused: Tensor.reduceSum Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.concatenate, Tensor.sumFirst, Fin.sum_univ_succ, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Tensor.reduceSumunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, This simp argument is unused: Fin.sum_univ_succ Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.concatenate, Tensor.sumFirst, Tensor.reduceSum, Bool.cond_decide] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Fin.sum_univ_succunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0, This simp argument is unused: Bool.cond_decide Hint: Omit it from the simp argument list. [apply] simp only [Array.fn__where, Array.fn__where_2, Array.heaviside, Loop.fn__where, Loop.fn__where_2, Loop.heaviside, Tensor.map, Tensor.map₂, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector, Tensor.scatterSet_matrix, Tensor.concatenate, Tensor.sumFirst, Tensor.reduceSum, Fin.sum_univ_succ] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Bool.cond_decideunit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0]unit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if decide (a (⟨2, ⋯⟩, ()) > 0) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 then if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨2 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨2 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 1 then if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨1 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨1 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else if ⟨2, ⋯⟩ = 0 then if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) = 0) = true then b (⟨0 + 1 * ↑0, ⋯⟩, ()) else if decide (a (⟨0 + 1 * ↑0, ⋯⟩, ()) > 0) = true then 1 else 0 else 0 all_goals norm_num [Fin.ext_iff]unit.«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ (if decide (a (⟨2, ⋯⟩, ()) = 0) = true then b (⟨2, ⋯⟩, ()) else if 0 < a (⟨2, ⋯⟩, ()) then 1 else 0) = if a (⟨2, ⋯⟩, ()) = 0 then b (⟨2, ⋯⟩, ()) else if 0 < a (⟨2, ⋯⟩, ()) then 1 else 0 all_goals exact if_congr decide_eq_true_iff rfl rflAll goals completed! 🐙 theorem certificate (a : Tensor ℝ [3]) (b : Tensor ℝ [3]) : Jaxpr.Program.eval (.cons a (.cons b .nil)) Array.heaviside_ir = Jaxpr.Program.eval (.cons a (.cons b .nil)) Loop.heaviside_ir := bya:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Jaxpr.Program.eval (Jaxpr.Env.cons a (Jaxpr.Env.cons b Jaxpr.Env.nil)) Array.heaviside_ir = Jaxpr.Program.eval (Jaxpr.Env.cons a (Jaxpr.Env.cons b Jaxpr.Env.nil)) Loop.heaviside_ir rw [Array.heaviside_translation_correct,a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b = Jaxpr.Program.eval (Jaxpr.Env.cons a (Jaxpr.Env.cons b Jaxpr.Env.nil)) Loop.heaviside_ira:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b = Loop.heaviside a b Loop.heaviside_translation_correcta:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b = Loop.heaviside a ba:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b = Loop.heaviside a b]a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.heaviside a b = Loop.heaviside a b exact matches_loop a bAll goals completed! 🐙end JaxLean.Puzzles.Heaviside