Matrix simplification tactics

Stream: maths

[Anirudh Suresh]

I am trying to prove some Quantum lemmas on Lean.

import Mathlib
open scoped Matrix

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)) ℂ :=
(Matrix.kroneckerMap (fun (a:ℂ) (b:ℂ) => a*b) A B).reindex finProdFinEquiv finProdFinEquiv

infixl:80 " ⊗ " => tensor_product_2

@[reducible]
def ket0: Matrix (Fin 2) (Fin 1) ℂ :=  -- Assuming ℂ is the complex number type
  !![(1:ℂ);0]

@[reducible]
def ket1:Matrix (Fin 2) (Fin 1) ℂ  :=  -- Assuming ℂ is the complex number type
  !![0;1]

postfix:1024 "|0⟩" => ket0

postfix:1024 "|1⟩" => ket1
noncomputable def H_gate : Matrix (Fin 2) (Fin 2) ℂ :=
  let c := Complex.ofReal (1 / Real.sqrt 2)
  !![ c,  c;
      c, -c ]

def CNOT1 : Matrix (Fin 4) (Fin 4) ℂ :=
   !![1, 0, 0, 0;
      0, 1, 0, 0;
      0, 0, 0, 1;
      0, 0, 1, 0]

lemma sqrt_lemma_1 : (√2)⁻¹ * (√2)⁻¹ = 2⁻¹ := by {
  rw [← mul_inv]
  simp [Real.mul_self_sqrt]
}

theorem H_tensor_H_on_ket0_ket0 : (H_gate ⊗ H_gate) * (ket0 ⊗ ket0) = (1/2 : ℂ) • ((ket0 ⊗ ket0) + (ket0 ⊗ ket1) + (ket1 ⊗ ket0) + (ket1 ⊗ ket1)) :=by {
  ext (i : Fin (2 * 2)) j
  revert i j
  simp_rw [finProdFinEquiv.surjective.forall]
  rintro ⟨i1, i2⟩ ⟨j1, j2⟩
  have hj1:j1=0:=by {
    fin_cases j1
    simp
  }
  have hj2:j2=0:=by {
    fin_cases j2
    simp
  }
  rw [hj1,hj2]
  fin_cases i1; fin_cases i2;
  {
    simp [H_gate, ket0, ket1, tensor_product_2, Matrix.mul_apply, Matrix.kroneckerMap]
    simp [Fin.sum_univ_four]
    simp [finProdFinEquiv, Fin.divNat, Fin.modNat]
    let i : Fin 2 := ⟨(3 : ℕ) / 2, by norm_num⟩
    let j : Fin 2 := ⟨(3 : ℕ) % 2, by norm_num⟩
    have h1 : i = 1 := by dsimp [i]
    have h2 : j = 1 := by dsimp [j]
    conv_lhs=>enter [2,1,1,3];change(1)
    conv_lhs=>enter [2,1,2,3];change(1)
    simp
    conv_lhs=>enter [2,2,1,3];change(1)
    conv_lhs=>enter [2,2,2,3];change(1)
    simp
    norm_cast
    rw[sqrt_lemma_1]
    simp
  }
  {
    simp [H_gate, ket0, ket1, tensor_product_2, Matrix.mul_apply, Matrix.kroneckerMap]
    simp [Fin.sum_univ_four]
    simp [finProdFinEquiv, Fin.divNat, Fin.modNat]
    conv_lhs=>enter [2,1,1,3];change(1)
    conv_lhs=>enter [2,1,2,3];change(1)
    simp
    conv_lhs=>enter [2,1,2,1,3];change(1)
    conv_lhs=>enter [2,1,2,2,3];change(1)
    simp
    norm_cast
    rw[sqrt_lemma_1]
    simp
  }
  {
    fin_cases i2
    {
      simp [H_gate, ket0, ket1, tensor_product_2, Matrix.mul_apply, Matrix.kroneckerMap]
      simp [Fin.sum_univ_four]
      simp [finProdFinEquiv, Fin.divNat, Fin.modNat]
      conv_lhs=>enter [2,1,1,3];change(1)
      conv=>enter [1,2,2,1,3];change(1)
      simp
      norm_cast
      rw[sqrt_lemma_1]
      simp
    }
    {
      simp [H_gate, ket0, ket1, tensor_product_2, Matrix.mul_apply, Matrix.kroneckerMap]
      simp [Fin.sum_univ_four]
      simp [finProdFinEquiv, Fin.divNat, Fin.modNat]
      conv_lhs=>enter [2,1,1,3];change(1)
      conv=>enter [1,2,2,1,3];change(1)
      simp
      norm_cast
      rw[sqrt_lemma_1]
      simp
    }
  }

}

I am trying to prove the above theorem. However, it is an extremely long proof even though it is essentially a result of matrix operations. Is there any Lean tactic that can help me prove this faster without having to write so many lines of proof? This is a relatively simple thing to prove Mathematically so it is kinda annoying that it takes this much work in Lean.

[Frédéric Dupuis]

This might be a bit counterintuitive, but explicit numerical calculations with complex numbers like this is one of the worst places to start with Lean. None of the automation for numerics can handle complex numbers at the moment (norm_num can't deal with them at all, nor can simp +arith), so you're basically stuck doing everything manually. Starting out with more abstract arguments will almost certainly guarantee a better experience.

[Anirudh Suresh]

Would it be possible to unfold the complex number definition in Lean some way and then use the automation for the numerics?

[Yaël Dillies]

You could try using docs#Complex.ext and lemmas like docs#Complex.mul_re

[Frédéric Dupuis]

Sure, you can definitely get through the computations in this way. But if the goal was just to try something simple to get started, it's good to keep in mind that Lean is a very different beast from (say) Matlab, and this is definitely not what I would recommend!

[Bhavik Mehta]

lemma sqrt_lemma_2 : ((√2 : ℝ) : ℂ)⁻¹ * ((√2 : ℝ) : ℂ)⁻¹ = 2⁻¹ := by {
  norm_cast
  simp [sqrt_lemma_1]
}

theorem H_tensor_H_on_ket0_ket0 :
    (H_gate ⊗ H_gate) * (ket0 ⊗ ket0) = (1/2 : ℂ) • ((ket0 ⊗ ket0) + (ket0 ⊗ ket1) + (ket1 ⊗ ket0) + (ket1 ⊗ ket1)) := by
  ext (i : Fin (2 * 2)) j
  revert i j
  simp_rw [finProdFinEquiv.surjective.forall]
  simp [Fin.forall_fin_one, Fin.forall_fin_two, tensor_product_2]
  simp [Matrix.mul_apply, H_gate, Fintype.sum_prod_type, sqrt_lemma_2]

This works instead - there aren't really many complex number computations, it's really just matrix simplification in the right order. If you remove the sqrt_lemma_2 at the end, you'll see the only complex number result that's needed, the rest is just abstract comm ring stuff