Make matrix reindex computable

Stream: new members

[Yunong Shi]

I am trying to convert Matrix (Fin 2 × Fin 2) (Fin 1 × Fin 1) ℂ) to (Matrix (Fin 4) (Fin 1) ℂ. However the converter needs to be set to "noncomputable", I am wondering what changes are needed in my Equiv proofs to make it computable?

Here is the code:

import Mathlib.Logic.Equiv.Fin
import Mathlib.Data.Matrix.Kronecker
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Basic

open Matrix
open Kronecker

theorem fin22Fin4Equiv: Fin (2 * 2) ≃ Fin 4
    where
  toFun x := match x with
    | ⟨0, _⟩ => 0
    | ⟨1, _⟩ => 1
    | ⟨2, _⟩ => 2
    | ⟨3, _⟩ => 3
  invFun x:= match x with
    | 0 => ⟨0, zero_lt_four⟩
    | 1 => ⟨1, by norm_num⟩
    | 2 => ⟨2, by norm_num⟩
    | 3 => ⟨3, by norm_num⟩
  left_inv := fun x => Fin.eq_of_veq <| by
    fin_cases x <;> simp <;> exact rfl
  right_inv := fun x => by
    fin_cases x <;> simp <;> exact rfl

theorem fin11Fin1Equiv: Fin (1 * 1) ≃ Fin 1
    where
  toFun x := match x with
    | ⟨0, _⟩ => 0
  invFun x:= match x with
    | 0 => ⟨0, zero_lt_one⟩
  left_inv := fun x => Fin.eq_of_veq <| by
    fin_cases x
    simp
  right_inv := fun x => by
    fin_cases x
    simp

-- This has to be set to noncomputable
abbrev convertMatrix_fin22Fin11Fin4Fin1 (M: Matrix (Fin 2 × Fin 2) (Fin 1 × Fin 1) ℂ): (Matrix (Fin 4) (Fin 1) ℂ) :=
    reindex (trans finProdFinEquiv fin22Fin4Equiv) (trans finProdFinEquiv fin11Fin1Equiv) M
````

[Kyle Miller]

It looks like you used theorem instead of def for your definitions.

[Matt Diamond]

yeah, it's a common mistake... equivalences aren't Propositions, they're data

[Yunong Shi]

Makes sense! Thanks!

[Eric Wieser]

You might be looking for docs#Fin.castIso, which gives you that Fin 4 and Fin (2*2) are isomorphic

[Eric Wieser]

(although in fact since 2*2=4 is true by definition you don't need it at all)