From 4447b703c8c1985866d5de6c64dff33c41e9b925 Mon Sep 17 00:00:00 2001
From: maokami <zerozerozero0216@gmail.com>
Date: Sun, 22 Dec 2024 19:13:32 +0900
Subject: [PATCH] feat: add multiqubit support with QState definition and
 Kronecker product

---
 VqcInLean/Basic.lean      |  1 +
 VqcInLean/Multiqubit.lean | 53 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 VqcInLean/Multiqubit.lean

diff --git a/VqcInLean/Basic.lean b/VqcInLean/Basic.lean
index 219f952..dfcf7be 100644
--- a/VqcInLean/Basic.lean
+++ b/VqcInLean/Basic.lean
@@ -1 +1,2 @@
 import VqcInLean.Qubit
+import VqcInLean.Multiqubit
diff --git a/VqcInLean/Multiqubit.lean b/VqcInLean/Multiqubit.lean
new file mode 100644
index 0000000..c990dce
--- /dev/null
+++ b/VqcInLean/Multiqubit.lean
@@ -0,0 +1,53 @@
+import VqcInLean.Qubit
+
+import Mathlib.Tactic
+import Mathlib.Data.Matrix.Kronecker
+
+open Complex Matrix Kronecker Qubit
+
+-- Multiqubit definition: 2ⁿx1 complex matrix
+structure QState (n : ℕ) where
+  mat : Matrix (Fin (2 ^ n)) (Fin 1) ℂ
+
+instance : Repr (QState n) where
+  reprPrec _ _ := s!"QState with {n} qubits"
+
+namespace Multiqubit
+
+-- Define coercion to Matrix
+instance : Coe (QState n) (Matrix (Fin (2 ^ n)) (Fin 1) ℂ) where
+  coe := QState.mat
+
+-- Make Qubit callable as a function
+instance : CoeFun (QState n) (λ _ => Fin n → Fin 1 → ℂ) where
+  coe ϕ := λ i j => ϕ.mat i j
+
+-- Coerce Qubit to QState 1
+instance : Coe Qubit (QState 1) where
+  coe q := { mat := q.mat }
+
+-- Define Kronecker product for QState
+@[simp]
+def kronecker (ϕ : QState n) (ψ : QState m) : QState (n + m) :=
+  -- Apply kronecker product to the underlying matrices
+  let product := ϕ.mat ⊗ₖ ψ.mat
+  -- Reindex the matrix to match the new dimensions
+  let reindexed := product.reindex finProdFinEquiv finProdFinEquiv
+  { mat := Eq.mp (by ring_nf) reindexed }
+
+-- Add notation for Kronecker product
+scoped infixl:100 " ⊗ₖ " => Multiqubit.kronecker
+
+def fromVector : {n : ℕ} → Vector ℕ n → QState n
+  | 0, _ => { mat := (1 : Matrix (Fin 1) (Fin 1) ℂ) } -- Identity for empty vector
+  | n + 1, v =>
+    let x := v.head
+    let xs := v.tail
+    let q : QState 1 := (qubit x : QState 1)
+    let rest : QState n := fromVector xs
+    Eq.mp (by simp [add_comm]) (q ⊗ₖ rest : QState (1 + n))
+
+macro "∣" xs:term,* "⟩" : term => do
+  `(fromVector (Vector.mk #[ $(xs),* ] rfl))
+
+#eval ∣0, 1, 0⟩