Remove 20 ForMathlib declarations now in mathlib/core; rename lsbs → setWidth

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}

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]

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

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,18 +58,20 @@ 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
     induction 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]
 

Quantumlib/ForMathlib/Data/Complex/Basic.lean

@@ -20,20 +20,20 @@ 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
   rw [Complex.ext_iff] at h
   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]

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)

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]

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