Proof in Lean 4 formalization of circuits

Stream: maths

[Anirudh Suresh]

import Mathlib
import Lean
open Lean Elab Tactic
open Matrix
open ComplexConjugate
open Lean.Elab
open Lean.Elab.Tactic
open Lean.Meta

def I (n:ℕ) : Matrix (Fin n) (Fin n) ℂ := 1

@[reducible]
def Square (n : ℕ) := Matrix (Fin n) (Fin n) ℂ

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

def flip_bit (n : ℕ) (i : ℕ) : ℕ := n ^^^ (1 <<< i)

def swap_bit (k i j : ℕ) : ℕ :=
  let bi := (k >>> i) % 2
  let bj := (k >>> j) % 2
  if bi = bj then
    k
  else
    -- flip the two differing bits
    flip_bit (flip_bit k i) j

lemma swap_indices{i j dim:ℕ} {a b: Fin (2^dim)} (g:Square 2) (swap_cond : i < dim ∧ j < dim ∧ i ≠ j):
(I (2 ^ i) ⊗ g ⊗ I (2 ^ (dim - 1 - i))) (Fin.cast (by sorry) ((swap_bit (a.val) (dim - 1 - i) (dim - 1 - j)):Fin (2^dim)))
    (Fin.cast (by sorry) ((swap_bit (b.val) (dim - 1 - i) (dim - 1 - j)):Fin (2^i*2*2^(dim-1-i)))) =
  (I (2 ^ j) ⊗ g ⊗ I (2 ^ (dim - 1 - j))) (Fin.cast (by sorry) a) (Fin.cast (by sorry) b):= by {

}

I'm working on a Lean 4 formalization of quantum circuits and need help with a proof about swapping gate positions in tensor products. The lemma swap_indices proves that applying a 2×2 gate g at position i in an n-qubit system produces the same result as applying the same gate at position j, but with the input/output indices appropriately swapped using bit manipulation. Unfolding the definitions just yet does not seem to help much in this case. What would be the best approach to complete this proof?

[Aaron Liu]

Do you really need a Fin (a * b)? Can you get by with Fin a × Fin b?

[Aaron Liu]

What's the reason for having Fin (a * b)? What's the reason for having Fin at all? How about {ι : Type*} [Fintype ι]?

[Aaron Liu]

your code does not typecheck on the web server, probably because they got rid of the Nat to Fin coercion

[Anirudh Suresh]

Aaron Liu said:

Do you really need a Fin (a * b)? Can you get by with Fin a × Fin b?

Wont it be a problem with Fin a x Fin b especially when we have multiple tensor products which would result in the index having type tuple?

[Eric Wieser]

Tuple types are easier to work with than Fin (a * b * c * d)

[Anirudh Suresh]

But wont it be inconvenient especially when I would want to do a matrix multiplication right after a tensor product but the index types dont match. With Fin (a*b), this seemed more convenient.

[Anirudh Suresh]

import Mathlib
import Lean
open Lean Elab Tactic
open Matrix
open ComplexConjugate
open Lean.Elab
open Lean.Elab.Tactic
open Lean.Meta

def I (n:ℕ) : Matrix (Fin n) (Fin n) ℂ := 1

@[reducible]
def Square (n : ℕ) := Matrix (Fin n) (Fin n) ℂ

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

def flip_bit (n : ℕ) (i : ℕ) : ℕ := n ^^^ (1 <<< i)

def swap_bit (k i j : ℕ) : ℕ :=
  let bi := (k >>> i) % 2
  let bj := (k >>> j) % 2
  if bi = bj then
    k
  else
    -- flip the two differing bits
    flip_bit (flip_bit k i) j

lemma swap_indices{i j dim:ℕ} {a b: Fin (2^dim)} (g:Square 2) (swap_cond : i < dim ∧ j < dim ∧ i ≠ j) (h1:(swap_bit (a.val) (dim - 1 - i) (dim - 1 - j))<2^dim) (h2:(swap_bit (b.val) (dim - 1 - i) (dim - 1 - j))<2^i*2*2^(dim-1-i)):
(I (2 ^ i) ⊗ g ⊗ I (2 ^ (dim - 1 - i))) (Fin.cast (by sorry) (Fin.mk (swap_bit (a.val) (dim - 1 - i) (dim - 1 - j)) h1))
    (Fin.cast (by sorry) (Fin.mk (swap_bit (b.val) (dim - 1 - i) (dim - 1 - j)) h2)) =
  (I (2 ^ j) ⊗ g ⊗ I (2 ^ (dim - 1 - j))) (Fin.cast (by sorry) a) (Fin.cast (by sorry) b):= by {

}

I have made changes to remove the typechecking errors

Also, in my current setup, I’ve already defined a lot of things using Fin (a * b) (and similar higher-dimensional versions like Fin (a * b * c)), so changing this now would require substantial refactoring across many parts of the project.

Given that, is there still a way to proceed with the proof using Fin (a * b) as it is? I do see the merits of switching to tuple-based indexing for the long run, but for now, I’d really appreciate any help in getting things to work with the current definitions.