Creating a tactic

Stream: lean4

[Anirudh Suresh]

I am trying to create my own tactic as shown in my code but I am facing one issue

import Mathlib
import Quantum.Essential_math_lemmas
import Lean.Elab.Tactic
open scoped Matrix
open Lean Elab Tactic

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]

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

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

elab "two_qubit_lemma_tactic" : tactic => do
  evalTactic (← `(tactic|
    ext (i : Fin (2 * 2)) j;
    revert i j;
    simp_rw [finProdFinEquiv.surjective.forall];
    rintro ⟨i1, i2⟩ ⟨j1, j2⟩;
    have hj1 : j1 = 0 := Subsingleton.elim _ _;
    have hj2 : j2 = 0 := Subsingleton.elim _ _;
    rw [hj1, hj2];
    have h32 : (⟨((3 : Fin 4) : ℕ) / 2, by decide⟩ : Fin 2) = 1 := rfl;
    have h32_2 : (⟨((3 : Fin 4) : ℕ) % 2, by decide⟩ : Fin 2) = 1 := rfl;
    simp [H_gate, CNOT1, CNOT2, SWAP, tensor_product_2, Matrix.mul_apply, Matrix.kroneckerMap,
          Fin.sum_univ_four, finProdFinEquiv, Fin.divNat, Fin.modNat, h32, h32_2, Matrix.vecCons_const];
    fin_cases i1 <;> fin_cases i2 <;> simp
  ))

theorem SWAP_CNOT_SWAP (q1 q2 : Matrix (Fin 2) (Fin 1) ℂ) : (SWAP * CNOT1 * SWAP) * (tensor_product_2 q1 q2) = CNOT2 * (tensor_product_2 q1 q2):= by
  {
      two_qubit_lemma_tactic
  }

In the SWAP_CNOT_SWAP theorem, the tactic solves the goal too early and thus, gives an error. How can I change my tactic definition so that the tactic doesnt do anything if the goal is solved.

[Mario Carneiro]

the simple fix is to replace every occurrence of ; in the tactic by <;>