import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesVstackset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Vstacktheorem matches_loop (a : Tensor ℝ [3]) (b : Tensor ℝ [3]) : Array.vstack a b = Loop.vstack a b := bya:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b = Loop.vstack a b funext ⟨i, j, u⟩a:Tensor ℝ [3]b:Tensor ℝ [3]i:Fin 2j:Fin 3u:Index []⊢ Array.vstack a b (i, j, u) = Loop.vstack a b (i, j, u) cases uunita:Tensor ℝ [3]b:Tensor ℝ [3]i:Fin 2j:Fin 3⊢ Array.vstack a b (i, j, PUnit.unit) = Loop.vstack a b (i, j, PUnit.unit) fin_cases iunit.«0»a:Tensor ℝ [3]b:Tensor ℝ [3]j:Fin 3⊢ Array.vstack a b ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit)unit.«1»a:Tensor ℝ [3]b:Tensor ℝ [3]j:Fin 3⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) <;>unit.«0»a:Tensor ℝ [3]b:Tensor ℝ [3]j:Fin 3⊢ Array.vstack a b ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit)unit.«1»a:Tensor ℝ [3]b:Tensor ℝ [3]j:Fin 3⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) fin_cases junit.«1».«0»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1».«1»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«1».«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0».«0»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«0».«1»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«0».«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«1».«0»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1».«1»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«1».«2»a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.vstack a b ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) rflAll goals completed! 🐙 theorem certificate (a : Tensor ℝ [3]) (b : Tensor ℝ [3]) : Jaxpr.Program.eval (.cons a (.cons b .nil)) Array.vstack_ir = Jaxpr.Program.eval (.cons a (.cons b .nil)) Loop.vstack_ir := bya:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Jaxpr.Program.eval (Jaxpr.Env.cons a (Jaxpr.Env.cons b Jaxpr.Env.nil)) Array.vstack_ir = Jaxpr.Program.eval (Jaxpr.Env.cons a (Jaxpr.Env.cons b Jaxpr.Env.nil)) Loop.vstack_ir rw [Array.vstack_translation_correct,a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b = Jaxpr.Program.eval (Jaxpr.Env.cons a (Jaxpr.Env.cons b Jaxpr.Env.nil)) Loop.vstack_ira:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b = Loop.vstack a b Loop.vstack_translation_correcta:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b = Loop.vstack a ba:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b = Loop.vstack a b]a:Tensor ℝ [3]b:Tensor ℝ [3]⊢ Array.vstack a b = Loop.vstack a b exact matches_loop a bAll goals completed! 🐙end JaxLean.Puzzles.Vstack