From 79e9822b1095caf51b3c58ada0d61bd4de721bc6 Mon Sep 17 00:00:00 2001 From: Ibrahim Mian Date: Wed, 26 Aug 2026 17:32:05 -0400 Subject: [PATCH] Delete the 20 ForMathlib declarations upstream already provides; rename lsbs->setWidth at use sites Verified against mathlib c1e30e17 (the lake-manifest revision) on leanprover/lean4:v4.30.0-rc2. One proof adjustment disclosed: weight_and_le's original proof relied on lsbs being opaque to simp; the setWidth version instantiates the induction hypothesis and closes with omega. Evidence that every deleted statement is derivable from mathlib/core alone: leanquantum-triage/evidence/Redundant.lean. --- Quantumlib/Data/Gate/Pauli/Defs.lean | 2 +- Quantumlib/Data/Gate/Pauli/Lemmas.lean | 6 +-- Quantumlib/ForMathlib/Data/BitVec/Basic.lean | 4 -- Quantumlib/ForMathlib/Data/BitVec/Lemmas.lean | 50 ++++--------------- Quantumlib/ForMathlib/Data/Complex/Basic.lean | 14 +++--- Quantumlib/ForMathlib/Data/Fin.lean | 9 ---- Quantumlib/ForMathlib/Data/Matrix/Basic.lean | 12 ----- .../ForMathlib/Data/Matrix/PowBitVec.lean | 4 +- .../ForMathlib/Data/Matrix/Unitary.lean | 37 -------------- 9 files changed, 23 insertions(+), 115 deletions(-) delete mode 100644 Quantumlib/ForMathlib/Data/Fin.lean diff --git a/Quantumlib/Data/Gate/Pauli/Defs.lean b/Quantumlib/Data/Gate/Pauli/Defs.lean index 735f364..f7d03b5 100644 --- a/Quantumlib/Data/Gate/Pauli/Defs.lean +++ b/Quantumlib/Data/Gate/Pauli/Defs.lean @@ -50,7 +50,7 @@ def cons (z x : Bool) (P : Pauli n) : Pauli (n + 1) := {P with z := P.z.cons z, x := P.x.cons x} def tail (P : Pauli (n + 1)) : Pauli n := - {P with z := P.z.lsbs, x := P.x.lsbs} + {P with z := P.z.setWidth n, x := P.x.setWidth n} def addPhase (a : ZMod 4) (P : Pauli n) := {P with m := P.m + a} diff --git a/Quantumlib/Data/Gate/Pauli/Lemmas.lean b/Quantumlib/Data/Gate/Pauli/Lemmas.lean index 8122d0e..aed7951 100644 --- a/Quantumlib/Data/Gate/Pauli/Lemmas.lean +++ b/Quantumlib/Data/Gate/Pauli/Lemmas.lean @@ -77,7 +77,7 @@ theorem mul_m (P Q : Pauli n) : theorem cons_msb_tail (P : Pauli (n + 1)) : P = cons P.z.msb P.x.msb P.tail := by - simp [cons, tail, BitVec.cons_msb_lsbs] + simp [cons, tail, BitVec.cons_msb_setWidth] theorem of_length_zero (P : Pauli 0) : ∃ m, P = {m := m, x := 0, z := 0} := by @@ -107,12 +107,12 @@ theorem cons_tail (P : Pauli n) a b : @[simp] theorem tail_z (P : Pauli (n + 1)) : - P.tail.z = P.z.lsbs := by + P.tail.z = P.z.setWidth n := by simp [tail] @[simp] theorem tail_x (P : Pauli (n + 1)) : - P.tail.x = P.x.lsbs := by + P.tail.x = P.x.setWidth n := by simp [tail] @[simp] diff --git a/Quantumlib/ForMathlib/Data/BitVec/Basic.lean b/Quantumlib/ForMathlib/Data/BitVec/Basic.lean index a165b2a..f906731 100644 --- a/Quantumlib/ForMathlib/Data/BitVec/Basic.lean +++ b/Quantumlib/ForMathlib/Data/BitVec/Basic.lean @@ -2,8 +2,6 @@ import Mathlib namespace BitVec -def lsbs (x : BitVec (w + 1)) : BitVec w := x.setWidth w - def foldl (x : BitVec w) (f : Bool → α → α) (init : α) : α := w.fold (fun i h acc => f x[i] acc) init @@ -16,6 +14,4 @@ def dot (x y : BitVec w) : Nat := def dotZ₂ (x y : BitVec w) : Bool := (x.dot y) % 2 == 1 -instance : Fintype (BitVec w) := Fintype.ofEquiv (Fin (2^w)) BitVec.equivFin.symm.toEquiv - end BitVec diff --git a/Quantumlib/ForMathlib/Data/BitVec/Lemmas.lean b/Quantumlib/ForMathlib/Data/BitVec/Lemmas.lean index c9d2393..d1785a0 100644 --- a/Quantumlib/ForMathlib/Data/BitVec/Lemmas.lean +++ b/Quantumlib/ForMathlib/Data/BitVec/Lemmas.lean @@ -7,38 +7,6 @@ import Mathlib.Tactic.Ring namespace BitVec -instance : Fintype (BitVec w) := - Fintype.ofEquiv (Fin (2 ^ w)) equivFin.toEquiv.symm - -theorem cons_msb_lsbs (x : BitVec (w + 1)) : - cons x.msb x.lsbs = x := by simp [lsbs] - -@[simp] -theorem lsbs_zero : - (0#(m + 1)).lsbs = 0#m := by simp [lsbs] - -@[simp] -theorem lsbs_cons (x : BitVec w) b : - (BitVec.cons b x).lsbs = x := by simp [lsbs] - -@[simp] -theorem lsbs_xor (x y : BitVec (w + 1)) : - (x ^^^ y).lsbs = x.lsbs ^^^ y.lsbs := by - simp [lsbs] - -@[simp] -theorem lsbs_or (x y : BitVec (w + 1)) : - (x ||| y).lsbs = x.lsbs ||| y.lsbs := by - simp [lsbs] - -@[simp] -theorem lsbs_and (x y : BitVec (w + 1)) : - (x &&& y).lsbs = x.lsbs &&& y.lsbs := by - simp [lsbs] - -theorem getElem_eq_msb (x : BitVec (w + 1)) : x[w] = x.msb := by - simp [BitVec.msb, ←getLsbD_eq_getElem, BitVec.getLsbD_eq_getMsbD] - @[simp] theorem cons_true_allOnes : cons true (allOnes m) = allOnes (m + 1) := by @@ -57,10 +25,10 @@ theorem foldl_cons {x : BitVec w} : foldl (cons b x) f a = f b (foldl x f a) := rw [dif_neg (by omega)] @[simp] -theorem lsbs_allOnes : - (allOnes (m + 1)).lsbs = allOnes m := by +theorem setWidth_allOnes : + (allOnes (m + 1)).setWidth m = allOnes m := by ext - simp [lsbs] + simp omega @[simp] @@ -90,10 +58,12 @@ theorem weight_and_le (x y : BitVec w) : case zero => simp [@BitVec.of_length_zero x, @BitVec.of_length_zero y] case succ w' ih => - rw [←cons_msb_lsbs x, ←cons_msb_lsbs y] + rw [←cons_msb_setWidth x, ←cons_msb_setWidth y] simp only [cons_and_cons] cases x.msb <;> cases y.msb - <;> simp [ih, Nat.le_succ_of_le, add_comm] + <;> simp only [Bool.and_self, Bool.and_true, Bool.and_false, + weight_cons, Bool.toNat_true, Bool.toNat_false] + <;> (have h := ih (x.setWidth w') (y.setWidth w'); omega) theorem weight_or (x y : BitVec w) : (x ||| y).weight = x.weight + y.weight - (x &&& y).weight := by @@ -101,7 +71,7 @@ theorem weight_or (x y : BitVec w) : case zero => simp [@BitVec.of_length_zero x, @BitVec.of_length_zero y] case succ w' ih => - rw [←cons_msb_lsbs x, ←cons_msb_lsbs y] + rw [←cons_msb_setWidth x, ←cons_msb_setWidth y] simp only [cons_and_cons, cons_or_cons, weight_cons, ih] cases x.msb <;> cases y.msb <;> simp only [ @@ -113,7 +83,7 @@ theorem weight_or (x y : BitVec w) : rw [Nat.sub_add_eq, add_comm 2, add_assoc _ 2, add_comm 2, ←add_assoc] symm calc - _ = (x.lsbs.weight + y.lsbs.weight + 1) - (x.lsbs &&& y.lsbs).weight := by + _ = ((x.setWidth w').weight + (y.setWidth w').weight + 1) - (x.setWidth w' &&& y.setWidth w').weight := by rw [add_assoc, Nat.add_sub_assoc, Nat.add_sub_assoc (k := 1) (by omega)] ring_nf rw [add_comm] @@ -176,7 +146,7 @@ theorem dotZ₂_xor_distrib_left (x y z : BitVec m) : case zero => simp [x.eq_nil] case succ m' ih => - rw [←cons_msb_lsbs x, ←cons_msb_lsbs y, ←cons_msb_lsbs z] + rw [←cons_msb_setWidth x, ←cons_msb_setWidth y, ←cons_msb_setWidth z] cases x.msb <;> cases y.msb <;> cases z.msb <;> simp [ih] diff --git a/Quantumlib/ForMathlib/Data/Complex/Basic.lean b/Quantumlib/ForMathlib/Data/Complex/Basic.lean index a490b0c..9b462cf 100644 --- a/Quantumlib/ForMathlib/Data/Complex/Basic.lean +++ b/Quantumlib/ForMathlib/Data/Complex/Basic.lean @@ -20,13 +20,6 @@ theorem sin_pi_div_four : Complex.sin (π / 4) = √2 / 2 := by _ = _ := by apply Complex.ext <;> simp -@[simp] -theorem exp_three_pi_div_two : Complex.exp (3 * ↑π / 2 * Complex.I) = -Complex.I := by - rw [show (3 : ℂ) = 2 + 1 by ring_nf, - add_mul, add_div, add_mul, - exp_add] - simp [exp_mul_I] - @[simp] theorem one_ne_neg_one : (1 : ℂ) ≠ -1 := by intros h @@ -34,6 +27,13 @@ theorem one_ne_neg_one : (1 : ℂ) ≠ -1 := by simp_all linarith +@[simp] +theorem exp_three_pi_div_two : Complex.exp (3 * ↑π / 2 * Complex.I) = -Complex.I := by + rw [show (3 : ℂ) = 2 + 1 by ring_nf, + add_mul, add_div, add_mul, + exp_add] + simp [exp_mul_I] + theorem neg_I_pow_eq_pow_mod (n : ℕ) : (-I) ^ n = (-I) ^ (n % 4) := by rw [neg_pow, neg_pow Complex.I, ←Complex.I_pow_eq_pow_mod] diff --git a/Quantumlib/ForMathlib/Data/Fin.lean b/Quantumlib/ForMathlib/Data/Fin.lean deleted file mode 100644 index 64a7915..0000000 --- a/Quantumlib/ForMathlib/Data/Fin.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Mathlib - -namespace Fin - -@[simp] -theorem add_neg (a b : Fin n) : a + -b = a - b := by - simp only [neg_def, add_def, Nat.add_mod_mod, sub_def, add_comm] - -end Fin diff --git a/Quantumlib/ForMathlib/Data/Matrix/Basic.lean b/Quantumlib/ForMathlib/Data/Matrix/Basic.lean index 39f9f90..5f8d3f0 100644 --- a/Quantumlib/ForMathlib/Data/Matrix/Basic.lean +++ b/Quantumlib/ForMathlib/Data/Matrix/Basic.lean @@ -10,18 +10,6 @@ abbrev CSquare n := CMatrix n n namespace Matrix -theorem conjTranspose_transpose_comm : ∀ (A : CMatrix m n), - Aᴴᵀ = Aᵀᴴ := by intros; rfl - -@[simp] -theorem pow_true [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : - M ^ true.toNat = M := by simp - -@[simp] -theorem pow_false [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : - M ^ false.toNat = 1 := by simp - end Matrix -def CMatrix.Commute (A B : CMatrix n n) : Prop := _root_.Commute A B def CMatrix.AntiCommute (A B : CMatrix n n) : Prop := A * B = -(B * A) diff --git a/Quantumlib/ForMathlib/Data/Matrix/PowBitVec.lean b/Quantumlib/ForMathlib/Data/Matrix/PowBitVec.lean index 95a807f..61d0737 100644 --- a/Quantumlib/ForMathlib/Data/Matrix/PowBitVec.lean +++ b/Quantumlib/ForMathlib/Data/Matrix/PowBitVec.lean @@ -14,7 +14,7 @@ def powBitVec (self : CMatrix m m) (x : BitVec n) : CMatrix (m ^ n) (m ^ n) := (finCongr <| by ring) (finCongr <| by ring) <| (self ^ x.msb.toNat) ⊗ - (powBitVec self x.lsbs : CMatrix (m ^ n') (m ^ n')) + (powBitVec self (x.setWidth n') : CMatrix (m ^ n') (m ^ n')) infix:80 " ^ᵥ " => powBitVec @@ -28,7 +28,7 @@ theorem powBitVec_zero (M : CMatrix n n) m : simp_rw [ powBitVec, BitVec.msb_zero, - BitVec.lsbs_zero, + BitVec.setWidth_zero, ih, Bool.toNat_false, pow_zero, Matrix.one_kron_one] diff --git a/Quantumlib/ForMathlib/Data/Matrix/Unitary.lean b/Quantumlib/ForMathlib/Data/Matrix/Unitary.lean index 9f9d883..591f880 100644 --- a/Quantumlib/ForMathlib/Data/Matrix/Unitary.lean +++ b/Quantumlib/ForMathlib/Data/Matrix/Unitary.lean @@ -7,43 +7,6 @@ namespace Matrix abbrev IsUnitary {n} (M : CSquare n) := M ∈ Matrix.unitaryGroup (Fin n) ℂ -theorem transpose_of_isUnitary : ∀ (M : CSquare n), - M.IsUnitary → Mᵀ.IsUnitary := by - intros M h - simp_rw [mem_unitaryGroup_iff'] - simp_rw [mem_unitaryGroup_iff] at h - simp only [star] at * - rw [←conjTranspose_transpose_comm, - ←transpose_mul, h, transpose_one] - -theorem conjTranspose_of_isUnitary : ∀ (M : CSquare n), - M.IsUnitary → Mᴴ.IsUnitary := by - intros M h - simp_rw [mem_unitaryGroup_iff'] - simp_rw [mem_unitaryGroup_iff] at h - simp only [star] at * - simpa - -theorem kron_of_isUnitary : ∀ (M₁ : CSquare m) (M₂ : CSquare n), - M₁.IsUnitary → M₂.IsUnitary → (M₁ ⊗ M₂).IsUnitary := by - intros M₁ M₂ h₁ h₂ - simp_rw [mem_unitaryGroup_iff', star] at * - rw [conjTranspose_kron, ←mul_kron_mul, h₁, h₂, one_kron_one] - -theorem mul_of_isUnitary : ∀ (M₁ M₂ : CSquare n), - M₁.IsUnitary → M₂.IsUnitary → (M₁ * M₂).IsUnitary := by - intros M₁ M₂ h₁ h₂ - simp_rw [mem_unitaryGroup_iff', star] at * - rw [conjTranspose_mul, mul_assoc, ←mul_assoc M₁ᴴ, h₁, one_mul, h₂] - -theorem smul_of_isUnitary : ∀ (c : ℂ) (M : CSquare n), - M.IsUnitary → c ∈ unitary ℂ → (c • M).IsUnitary := by - intros c M hM hc - simp_rw [mem_unitaryGroup_iff'] at hM ⊢ - rw [Unitary.mem_iff_self_mul_star] at hc - rw [star_smul, mul_smul, smul_mul, ←smul_assoc, smul_eq_mul, hc, hM] - simp - end Matrix