rename l r -> x y

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`
@@ -329,12 +329,12 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
 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,
 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
+    by_cases y.getLsb 0
     case pos hr =>
       simp only [hr, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
         hr, ofBool_true, ofNat_eq_ofNat]
@@ -345,10 +345,10 @@ theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) :
   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 hr : y.getLsb (s' + 1) <;> simp [hr]
     rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
 
 theorem getLsb_mul (x y : BitVec w) (i : Nat) :