import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesEyeset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Eyetheorem matches_loop : Array.eye (R := ℝ) = Loop.eye (R := ℝ) := by⊢ Array.eye = Loop.eye funext ⟨i, j, u⟩i:Fin 3j:Fin 3u:Index []⊢ Array.eye (i, j, u) = Loop.eye (i, j, u) cases uuniti:Fin 3j:Fin 3⊢ Array.eye (i, j, PUnit.unit) = Loop.eye (i, j, PUnit.unit) fin_cases iunit.«0»j:Fin 3⊢ Array.eye ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit) = Loop.eye ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit)unit.«1»j:Fin 3⊢ Array.eye ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) = Loop.eye ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit)unit.«2»j:Fin 3⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) <;>unit.«0»j:Fin 3⊢ Array.eye ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit) = Loop.eye ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit)unit.«1»j:Fin 3⊢ Array.eye ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) = Loop.eye ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit)unit.«2»j:Fin 3⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) fin_cases junit.«2».«0»⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«2».«1»⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2».«2»⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0».«0»⊢ Array.eye ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«0».«1»⊢ Array.eye ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«0».«2»⊢ Array.eye ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«1».«0»⊢ Array.eye ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1».«1»⊢ Array.eye ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«1».«2»⊢ Array.eye ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«2».«0»⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«2».«1»⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2».«2»⊢ Array.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.eye ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) simp only [Array.fn__where, Array.eye, Loop.eye, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_matrix]unit.«2».«2»⊢ (if decide True = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 ∧ ⟨2, ⋯⟩ = 2 then 1 else if ⟨2, ⋯⟩ = 1 ∧ ⟨2, ⋯⟩ = 1 then 1 else if ⟨2, ⋯⟩ = 0 ∧ ⟨2, ⋯⟩ = 0 then 1 else 0 all_goals norm_num [Fin.ext_iff, Bool.cond_decide, decide_eq_true_iff]All goals completed! 🐙 theorem certificate : Jaxpr.Program.eval .nil Array.eye_ir = Jaxpr.Program.eval .nil Loop.eye_ir := by⊢ Jaxpr.Program.eval Jaxpr.Env.nil Array.eye_ir = Jaxpr.Program.eval Jaxpr.Env.nil Loop.eye_ir rw [Array.eye_translation_correct,⊢ Array.eye = Jaxpr.Program.eval Jaxpr.Env.nil Loop.eye_ir⊢ Array.eye = Loop.eye Loop.eye_translation_correct⊢ Array.eye = Loop.eye⊢ Array.eye = Loop.eye]⊢ Array.eye = Loop.eye exact matches_loopAll goals completed! 🐙end JaxLean.Puzzles.Eye