import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesTriuset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Triutheorem matches_loop : Array.triu (R := ℝ) = Loop.triu (R := ℝ) := by⊢ Array.triu = Loop.triu funext ⟨i, j, u⟩i:Fin 3j:Fin 3u:Index []⊢ Array.triu (i, j, u) = Loop.triu (i, j, u) cases uuniti:Fin 3j:Fin 3⊢ Array.triu (i, j, PUnit.unit) = Loop.triu (i, j, PUnit.unit) fin_cases iunit.«0»j:Fin 3⊢ Array.triu ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit) = Loop.triu ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit)unit.«1»j:Fin 3⊢ Array.triu ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) = Loop.triu ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit)unit.«2»j:Fin 3⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) <;>unit.«0»j:Fin 3⊢ Array.triu ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit) = Loop.triu ((fun i => i) ⟨0, ⋯⟩, j, PUnit.unit)unit.«1»j:Fin 3⊢ Array.triu ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit) = Loop.triu ((fun i => i) ⟨1, ⋯⟩, j, PUnit.unit)unit.«2»j:Fin 3⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, j, PUnit.unit) fin_cases junit.«2».«0»⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«2».«1»⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2».«2»⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0».«0»⊢ Array.triu ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«0».«1»⊢ Array.triu ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«0».«2»⊢ Array.triu ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«1».«0»⊢ Array.triu ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1».«1»⊢ Array.triu ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«1».«2»⊢ Array.triu ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«2».«0»⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«2».«1»⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2».«2»⊢ Array.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.triu ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩, PUnit.unit) simp only [Array.fn__where, Array.triu, Loop.triu, Tensor.scalar, Tensor.reindex, Tensor.scatterSet_matrix]unit.«2».«2»⊢ (if decide (↑2 ≤ ↑2) = true then 1 else 0) = if ⟨2, ⋯⟩ = 2 ∧ ⟨2, ⋯⟩ = 2 then 1 else if ⟨2, ⋯⟩ = 1 ∧ ⟨2, ⋯⟩ = 2 then 1 else if ⟨2, ⋯⟩ = 1 ∧ ⟨2, ⋯⟩ = 1 then 1 else if ⟨2, ⋯⟩ = 0 ∧ ⟨2, ⋯⟩ = 2 then 1 else if ⟨2, ⋯⟩ = 0 ∧ ⟨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.triu_ir = Jaxpr.Program.eval .nil Loop.triu_ir := by⊢ Jaxpr.Program.eval Jaxpr.Env.nil Array.triu_ir = Jaxpr.Program.eval Jaxpr.Env.nil Loop.triu_ir rw [Array.triu_translation_correct,⊢ Array.triu = Jaxpr.Program.eval Jaxpr.Env.nil Loop.triu_ir⊢ Array.triu = Loop.triu Loop.triu_translation_correct⊢ Array.triu = Loop.triu⊢ Array.triu = Loop.triu]⊢ Array.triu = Loop.triu exact matches_loopAll goals completed! 🐙end JaxLean.Puzzles.Triu