Type matching in Lean 4

Stream: lean4

[Anirudh Suresh]

lemma tensor_assoc {m n o p q r:ℕ} (A:Matrix (Fin m) (Fin n) ℂ ) (B:Matrix (Fin o) (Fin p) ℂ ) (C:Matrix (Fin q) (Fin r) ℂ ):
tensor_product_2 (tensor_product_2 A B) C = tensor_product_2 A (tensor_product_2 B C) :=
by{
  sorry
}

I am trying to prove the associativity of tensor products that I defined myself. However, I am facing an issue when it comes to the type matching.

image.png

Lean's type checker is not able to detect that " Matrix (Fin (m * (o * q))) (Fin (n * (p * r))) ℂ" is equivalent to "Matrix (Fin (m * o * q)) (Fin (n * p * r)) ℂ". Is there a way to fix this type mismatch or is there something that can be done to tell Lean's type checker to assume the types are the same or to ignore this type mismatch?

[suhr]

Could you provide an #mwe?

[Aaron Liu]

You can use docs#HEq, which says that the types are the same, and if you cast along the equivalence induced by the equality then the values are also the same.

[Aaron Liu]

I would recommend defining an associator to help cast between your types

[Anirudh Suresh]

import Mathlib.Data.Vector
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
open scoped Matrix
open ComplexConjugate


@[reducible]
def tensor_product_2 {m n o p: ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m*o)) (Fin (n*p)) ℂ :=
sorry

lemma tensor_assoc {m n o p q r:ℕ} (A:Matrix (Fin m) (Fin n) ℂ ) (B:Matrix (Fin o) (Fin p) ℂ ) (C:Matrix (Fin q) (Fin r) ℂ ):
tensor_product_2 (tensor_product_2 A B) C = tensor_product_2 A (tensor_product_2 B C) :=
by{
  sorry
}

[Anirudh Suresh]

Aaron Liu said:

I would recommend defining an associator to help cast between your types

What exactly do you mean by an associator?

[Robert Maxton]

Unfortunately, multiplication of scalars is not definitionally associative, only propositionally associative -- m * (o * q) = m*o * q only propositionally, the proof requires induction and isn't a simple application of the definition. As a result, the types Matrix Fin (m * (o * q)) ... and Matrix Fin (m * o * q) ... are a priori different types, and applying the proof of associativity of multiplication to convert between them amounts to a typecast.

[Aaron Liu]

Anirudh Suresh said:

Aaron Liu said:

I would recommend defining an associator to help cast between your types

What exactly do you mean by an associator?

A function that converts between (a * b) * c and a * (b * c). For example, docs#Equiv.prodAssoc or docs#Equiv.sumAssoc.

[Robert Maxton]

Casting itself is simple enough, but arbitrary casts can be hard to work with later, because Lean doesn't expose the implementation details of its underlying representation for types; as a result, if all you know is that two types are equal, there's no general way of reducing that equality into more specific terms. For example, it is not the case that, if the function types α → β₁ and α → β₂ are equal, then β₁ = β₂ in all possible internal representations for those types (indeed in some cases injectivity of type construction must fail), and so if you need the equality of the βs to you have to require that as a separate hypothesis.

[Robert Maxton]

Using your own cast function mitigates this by implicitly adding structure to your casts, allowing you to extract that kind of information by taking advantage of features in your specific use case

[suhr]

You can apply an band-aid:

import Mathlib.Data.Vector.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
open scoped Matrix
open ComplexConjugate

@[reducible]
def tensor_product_2 {m n o p: ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m*o)) (Fin (n*p)) ℂ :=
sorry

lemma tensor_assoc {m n o p q r:ℕ} (A:Matrix (Fin m) (Fin n) ℂ ) (B:Matrix (Fin o) (Fin p) ℂ ) (C:Matrix (Fin q) (Fin r) ℂ ):
tensor_product_2 (tensor_product_2 A B) C = (Nat.mul_assoc m o q) ▸ (Nat.mul_assoc n p r) ▸ tensor_product_2 A (tensor_product_2 B C) :=
by{
  sorry
}

But I suspect playing with types will hurt in the long run.

[Eric Wieser]

Perhaps docs#Matrix.kronecker_assoc is relevant here, which uses docs#Matrix.reindex