chore: name variables in Data/BitVec consistently

src/Init/Data/BitVec/Basic.lean

@@ -42,8 +42,8 @@ Bitvectors have decidable equality. This should be used via the instance `Decida
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
-def BitVec.decEq (a b : BitVec n) : Decidable (a = b) :=
-  match a, b with
+def BitVec.decEq (x y : BitVec n) : Decidable (x = y) :=
+  match x, y with
   | ⟨n⟩, ⟨m⟩ =>
     if h : n = m then
       isTrue (h ▸ rfl)
@@ -69,9 +69,9 @@ protected def ofNat (n : Nat) (i : Nat) : BitVec n where
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
-/-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a
+/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
 (zero-cost) wrapper around a `Nat`. -/
-protected def toNat (a : BitVec n) : Nat := a.toFin.val
+protected def toNat (x : BitVec n) : Nat := x.toFin.val
 
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
@@ -123,18 +123,18 @@ section getXsb
 @[inline] def getMsb (x : BitVec w) (i : Nat) : Bool := i < w && getLsb x (w-1-i)
 
 /-- Return most-significant bit in bitvector. -/
-@[inline] protected def msb (a : BitVec n) : Bool := getMsb a 0
+@[inline] protected def msb (x : BitVec n) : Bool := getMsb x 0
 
 end getXsb
 
 section Int
 
 /-- Interpret the bitvector as an integer stored in two's complement form. -/
-protected def toInt (a : BitVec n) : Int :=
-  if 2 * a.toNat < 2^n then
-    a.toNat
+protected def toInt (x : BitVec n) : Int :=
+  if 2 * x.toNat < 2^n then
+    x.toNat
   else
-    (a.toNat : Int) - (2^n : Nat)
+    (x.toNat : Int) - (2^n : Nat)
 
 /-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
 protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLt (i % (Int.ofNat (2^n))).toNat (by
@@ -215,7 +215,7 @@ instance : Neg (BitVec n) := ⟨.neg⟩
 /--
 Return the absolute value of a signed bitvector.
 -/
-protected def abs (s : BitVec n) : BitVec n := if s.msb then .neg s else s
+protected def abs (x : BitVec n) : BitVec n := if x.msb then .neg x else x
 
 /--
 Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation
@@ -262,12 +262,12 @@ sdiv 5#4 -2 = -2#4
 sdiv (-7#4) (-2) = 3#4
 ```
 -/
-def sdiv (s t : BitVec n) : BitVec n :=
-  match s.msb, t.msb with
-  | false, false => udiv s t
-  | false, true  => .neg (udiv s (.neg t))
-  | true,  false => .neg (udiv (.neg s) t)
-  | true,  true  => udiv (.neg s) (.neg t)
+def sdiv (x y : BitVec n) : BitVec n :=
+  match x.msb, y.msb with
+  | false, false => udiv x y
+  | false, true  => .neg (udiv x (.neg y))
+  | true,  false => .neg (udiv (.neg x) y)
+  | true,  true  => udiv (.neg x) (.neg y)
 
 /--
 Signed division for bit vectors using SMTLIB rules for division by zero.
@@ -276,40 +276,40 @@ Specifically, `smtSDiv x 0 = if x >= 0 then -1 else 1`
 
 SMT-Lib name: `bvsdiv`.
 -/
-def smtSDiv (s t : BitVec n) : BitVec n :=
-  match s.msb, t.msb with
-  | false, false => smtUDiv s t
-  | false, true  => .neg (smtUDiv s (.neg t))
-  | true,  false => .neg (smtUDiv (.neg s) t)
-  | true,  true  => smtUDiv (.neg s) (.neg t)
+def smtSDiv (x y : BitVec n) : BitVec n :=
+  match x.msb, y.msb with
+  | false, false => smtUDiv x y
+  | false, true  => .neg (smtUDiv x (.neg y))
+  | true,  false => .neg (smtUDiv (.neg x) y)
+  | true,  true  => smtUDiv (.neg x) (.neg y)
 
 /--
 Remainder for signed division rounding to zero.
 
 SMT_Lib name: `bvsrem`.
 -/
-def srem (s t : BitVec n) : BitVec n :=
-  match s.msb, t.msb with
-  | false, false => umod s t
-  | false, true  => umod s (.neg t)
-  | true,  false => .neg (umod (.neg s) t)
-  | true,  true  => .neg (umod (.neg s) (.neg t))
+def srem (x y : BitVec n) : BitVec n :=
+  match x.msb, y.msb with
+  | false, false => umod x y
+  | false, true  => umod x (.neg y)
+  | true,  false => .neg (umod (.neg x) y)
+  | true,  true  => .neg (umod (.neg x) (.neg y))
 
 /--
 Remainder for signed division rounded to negative infinity.
 
 SMT_Lib name: `bvsmod`.
 -/
-def smod (s t : BitVec m) : BitVec m :=
-  match s.msb, t.msb with
-  | false, false => umod s t
+def smod (x y : BitVec m) : BitVec m :=
+  match x.msb, y.msb with
+  | false, false => umod x y
   | false, true =>
-    let u := umod s (.neg t)
-    (if u = .zero m then u else .add u t)
+    let u := umod x (.neg y)
+    (if u = .zero m then u else .add u y)
   | true, false =>
-    let u := umod (.neg s) t
-    (if u = .zero m then u else .sub t u)
-  | true, true => .neg (umod (.neg s) (.neg t))
+    let u := umod (.neg x) y
+    (if u = .zero m then u else .sub y u)
+  | true, true => .neg (umod (.neg x) (.neg y))
 
 end arithmetic
 
@@ -373,8 +373,8 @@ end relations
 
 section cast
 
-/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
-@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m := .ofNatLt i.toNat (eq ▸ i.isLt)
+/-- `cast eq x` embeds `x` into an equal `BitVec` type. -/
+@[inline] def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLt x.toNat (eq ▸ x.isLt)
 
 @[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
     cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
@@ -391,20 +391,20 @@ Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to
 new bitvector of size `len`. If `start + len > n`, then the vector will be zero-padded in the
 high bits.
 -/
-def extractLsb' (start len : Nat) (a : BitVec n) : BitVec len := .ofNat _ (a.toNat >>> start)
+def extractLsb' (start len : Nat) (x : BitVec n) : BitVec len := .ofNat _ (x.toNat >>> start)
 
 /--
 Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
 yield a new bitvector of size `hi - lo + 1`.
 
 SMT-Lib name: `extract`.
 -/
-def extractLsb (hi lo : Nat) (a : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ a
+def extractLsb (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ x
 
 /--
 A version of `zeroExtend` that requires a proof, but is a noop.
 -/
-def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n)  : BitVec w :=
+def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
   x.toNat#'(by
     apply Nat.lt_of_lt_of_le x.isLt
     exact Nat.pow_le_pow_of_le_right (by trivial) le)
@@ -413,8 +413,8 @@ def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n)  : BitVec w :=
 `shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
 needing to compute `x % 2^(2+n)`.
 -/
-def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) :=
-  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by
+def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) :=
+  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w + m) := by
         simp [Nat.shiftLeft_eq, Nat.pow_add]
         apply Nat.mul_lt_mul_of_pos_right p
         exact (Nat.two_pow_pos m)
@@ -502,36 +502,36 @@ instance : Complement (BitVec w) := ⟨.not⟩
 
 /--
 Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is
-equivalent to `a * 2^s`, modulo `2^n`.
+equivalent to `x * 2^s`, modulo `2^n`.
 
 SMT-Lib name: `bvshl` except this operator uses a `Nat` shift value.
 -/
-protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := BitVec.ofNat n (a.toNat <<< s)
+protected def shiftLeft (x : BitVec n) (s : Nat) : BitVec n := BitVec.ofNat n (x.toNat <<< s)
 instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩
 
 /--
 (Logical) right shift for bit vectors. The high bits are filled with zeros.
-As a numeric operation, this is equivalent to `a / 2^s`, rounding down.
+As a numeric operation, this is equivalent to `x / 2^s`, rounding down.
 
 SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value.
 -/
-def ushiftRight (a : BitVec n) (s : Nat) : BitVec n :=
-  (a.toNat >>> s)#'(by
-  let ⟨a, lt⟩ := a
+def ushiftRight (x : BitVec n) (s : Nat) : BitVec n :=
+  (x.toNat >>> s)#'(by
+  let ⟨x, lt⟩ := x
   simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)]
-  rw [←Nat.mul_one a]
+  rw [←Nat.mul_one x]
   exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1))
 
 instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩
 
 /--
 Arithmetic right shift for bit vectors. The high bits are filled with the
 most-significant bit.
-As a numeric operation, this is equivalent to `a.toInt >>> s`.
+As a numeric operation, this is equivalent to `x.toInt >>> s`.
 
 SMT-Lib name: `bvashr` except this operator uses a `Nat` shift value.
 -/
-def sshiftRight (a : BitVec n) (s : Nat) : BitVec n := .ofInt n (a.toInt >>> s)
+def sshiftRight (x : BitVec n) (s : Nat) : BitVec n := .ofInt n (x.toInt >>> s)
 
 instance {n} : HShiftLeft  (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩
 instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x >>> y.toNat⟩

src/Init/Data/BitVec/Bitblast.lean

@@ -289,18 +289,18 @@ theorem sle_eq_carry (x y : BitVec w) :
 A recurrence that describes multiplication as repeated addition.
 Is useful for bitblasting multiplication.
 -/
-def mulRec (l r : BitVec w) (s : Nat) : BitVec w :=
-  let cur := if r.getLsb s then (l <<< s) else 0
+def mulRec (x y : BitVec w) (s : Nat) : BitVec w :=
+  let cur := if y.getLsb s then (x <<< s) else 0
   match s with
   | 0 => cur
-  | s + 1 => mulRec l r s + cur
+  | s + 1 => mulRec x y s + cur
 
-theorem mulRec_zero_eq (l r : BitVec w) :
-    mulRec l r 0 = if r.getLsb 0 then l else 0 := by
+theorem mulRec_zero_eq (x y : BitVec w) :
+    mulRec x y 0 = if y.getLsb 0 then x else 0 := by
   simp [mulRec]
 
-theorem mulRec_succ_eq (l r : BitVec w) (s : Nat) :
-    mulRec l r (s + 1) = mulRec l r s + if r.getLsb (s + 1) then (l <<< (s + 1)) else 0 := rfl
+theorem mulRec_succ_eq (x y : BitVec w) (s : Nat) :
+    mulRec x y (s + 1) = mulRec x y s + if y.getLsb (s + 1) then (x <<< (s + 1)) else 0 := rfl
 
 /--
 Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
@@ -326,29 +326,29 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
     by_cases hi : x.getLsb i <;> simp [hi] <;> omega
 
 /--
-Recurrence lemma: multiplying `l` with the first `s` bits of `r` is the
-same as truncating `r` to `s` bits, then zero extending to the original length,
+Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
+same as truncating `y` to `s` bits, then zero extending to the original length,
 and performing the multplication. -/
-theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) :
-    mulRec l r s = l * ((r.truncate (s + 1)).zeroExtend w) := by
+theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
+    mulRec x y s = x * ((y.truncate (s + 1)).zeroExtend w) := by
   induction s
   case zero =>
     simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
-    by_cases r.getLsb 0
-    case pos hr =>
-      simp only [hr, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
-        hr, ofBool_true, ofNat_eq_ofNat]
+    by_cases y.getLsb 0
+    case pos hy =>
+      simp only [hy, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
+        ofBool_true, ofNat_eq_ofNat]
       rw [zeroExtend_ofNat_one_eq_ofNat_one_of_lt (by omega)]
       simp
-    case neg hr =>
-      simp [hr, zeroExtend_one_eq_ofBool_getLsb_zero]
+    case neg hy =>
+      simp [hy, zeroExtend_one_eq_ofBool_getLsb_zero]
   case succ s' hs =>
     rw [mulRec_succ_eq, hs]
     have heq :
-      (if r.getLsb (s' + 1) = true then l <<< (s' + 1) else 0) =
-        (l * (r &&& (BitVec.twoPow w (s' + 1)))) := by
+      (if y.getLsb (s' + 1) = true then x <<< (s' + 1) else 0) =
+        (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
       simp only [ofNat_eq_ofNat, and_twoPow]
-      by_cases hr : r.getLsb (s' + 1) <;> simp [hr]
+      by_cases hy : y.getLsb (s' + 1) <;> simp [hy]
     rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
 
 theorem getLsb_mul (x y : BitVec w) (i : Nat) :

src/Init/Data/BitVec/Lemmas.lean

@@ -23,7 +23,7 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
   simp only [BitVec.ofNat, Fin.ofNat', lt, Nat.mod_eq_of_lt]
 
 /-- Prove equality of bitvectors in terms of nat operations. -/
-theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
+theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
@@ -228,12 +228,12 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 /-! ### toInt/ofInt -/
 
 /-- Prove equality of bitvectors in terms of nat operations. -/
-theorem toInt_eq_toNat_cond (i : BitVec n) :
-    i.toInt =
-      if 2*i.toNat < 2^n then
-        (i.toNat : Int)
+theorem toInt_eq_toNat_cond (x : BitVec n) :
+    x.toInt =
+      if 2*x.toNat < 2^n then
+        (x.toNat : Int)
       else
-        (i.toNat : Int) - (2^n : Nat) :=
+        (x.toNat : Int) - (2^n : Nat) :=
   rfl
 
 theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false ↔ 2 * x.toNat < 2^w := by
@@ -260,13 +260,13 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
     omega
 
 /-- Prove equality of bitvectors in terms of nat operations. -/
-theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
+theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
   simp [toInt_eq_toNat_cond] at eq
   apply eq_of_toNat_eq
   revert eq
-  have _ilt := i.isLt
-  have _jlt := j.isLt
+  have _xlt := x.isLt
+  have _ylt := y.isLt
   split <;> split <;> omega
 
 theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt ↔ x = y :=
@@ -869,15 +869,15 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
     (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
   rfl
 
-@[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
-    getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
+@[simp] theorem getLsb_append {x : BitVec n} {y : BitVec m} :
+    getLsb (x ++ y) i = bif i < m then getLsb y i else getLsb x (i - m) := by
   simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
-@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
-    getMsb (v ++ w) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by
+@[simp] theorem getMsb_append {x : BitVec n} {y : BitVec m} :
+    getMsb (x ++ y) i = bif n ≤ i then getMsb y (i - n) else getMsb x i := by
   simp [append_def]
   by_cases h : n ≤ i
   · simp [h]