import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesLinspaceset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Linspacetheorem matches_loop (start : Tensor ℝ []) (stop : Tensor ℝ []) : Array.linspace start stop = Loop.linspace start stop := bystart:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop = Loop.linspace start stop funext ⟨i, u⟩start:Tensor ℝ []stop:Tensor ℝ []i:Fin 3u:Index []⊢ Array.linspace start stop (i, u) = Loop.linspace start stop (i, u) cases uunitstart:Tensor ℝ []stop:Tensor ℝ []i:Fin 3⊢ Array.linspace start stop (i, PUnit.unit) = Loop.linspace start stop (i, PUnit.unit) fin_cases iunit.«0»start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.linspace start stop ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.linspace start stop ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.linspace start stop ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0»start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.linspace start stop ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.linspace start stop ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.linspace start stop ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) simp only [Array.linspace, Loop.linspace, Tensor.map, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_vector]unit.«2»start:Tensor ℝ []stop:Tensor ℝ []⊢ start () + (stop () - start ()) * ↑2 / 2 = if ⟨2, ⋯⟩ = 2 then start () + (stop () - start ()) * 2 / 2 else if ⟨2, ⋯⟩ = 1 then start () + (stop () - start ()) * 1 / 2 else if ⟨2, ⋯⟩ = 0 then start () + (stop () - start ()) * 0 / 2 else 0 all_goals norm_num [Fin.ext_iff, Bool.cond_decide, decide_eq_true_iff]All goals completed! 🐙 theorem certificate (start : Tensor ℝ []) (stop : Tensor ℝ []) : Jaxpr.Program.eval (.cons start (.cons stop .nil)) Array.linspace_ir = Jaxpr.Program.eval (.cons start (.cons stop .nil)) Loop.linspace_ir := bystart:Tensor ℝ []stop:Tensor ℝ []⊢ Jaxpr.Program.eval (Jaxpr.Env.cons start (Jaxpr.Env.cons stop Jaxpr.Env.nil)) Array.linspace_ir = Jaxpr.Program.eval (Jaxpr.Env.cons start (Jaxpr.Env.cons stop Jaxpr.Env.nil)) Loop.linspace_ir rw [Array.linspace_translation_correct,start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop = Jaxpr.Program.eval (Jaxpr.Env.cons start (Jaxpr.Env.cons stop Jaxpr.Env.nil)) Loop.linspace_irstart:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop = Loop.linspace start stop Loop.linspace_translation_correctstart:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop = Loop.linspace start stopstart:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop = Loop.linspace start stop]start:Tensor ℝ []stop:Tensor ℝ []⊢ Array.linspace start stop = Loop.linspace start stop exact matches_loop start stopAll goals completed! 🐙end JaxLean.Puzzles.Linspace