Merge pull request Verified-zkEVM#1187 from Verified-zkEVM/cleanup/divn4doubleaddback-anon

refactor: anonymize 7 unused have bindings across 4 files (Verified-zkEVM#694)

Author: pirapira

EvmAsm/Evm64/EvmWordArith/DivN4DoubleAddback.lean

@@ -88,22 +88,22 @@ theorem hq_over_from_second_carry_one (q : Word) {v0 v1 v2 v3 u0 u1 u2 u3 : Word
   --   val256(u) + (2 - q) * val256(v) ≥ 1  (signed arithmetic)
   --   val256(u) ≥ (q - 2) * val256(v)  (Nat subtraction handles q < 2 trivially)
   -- Hence u/v ≥ q - 2, i.e., q ≤ u/v + 2.
-  have hq_v_le_plus : q.toNat * val256 v0 v1 v2 v3 ≤
+  have : q.toNat * val256 v0 v1 v2 v3 ≤
       val256 u0 u1 u2 u3 + 2 * val256 v0 v1 v2 v3 := by nlinarith
   -- (q - 2) * v ≤ u
-  have hqm2_le : (q.toNat - 2) * val256 v0 v1 v2 v3 ≤ val256 u0 u1 u2 u3 := by
+  have : (q.toNat - 2) * val256 v0 v1 v2 v3 ≤ val256 u0 u1 u2 u3 := by
     rcases Nat.lt_or_ge q.toNat 2 with hq_lt | hq_ge
     · -- q < 2: q - 2 = 0, trivial
       have : q.toNat - 2 = 0 := by omega
       rw [this]; simp
     · -- q ≥ 2
-      have hq_split : q.toNat * val256 v0 v1 v2 v3 =
+      have : q.toNat * val256 v0 v1 v2 v3 =
           (q.toNat - 2) * val256 v0 v1 v2 v3 + 2 * val256 v0 v1 v2 v3 := by
         have : q.toNat = (q.toNat - 2) + 2 := by omega
         nlinarith
       linarith
   -- u/v ≥ q - 2
-  have hdiv_ge : val256 u0 u1 u2 u3 / val256 v0 v1 v2 v3 ≥ q.toNat - 2 := by
+  have : val256 u0 u1 u2 u3 / val256 v0 v1 v2 v3 ≥ q.toNat - 2 := by
     exact Nat.le_div_iff_mul_le hv_pos |>.mpr (by linarith [Nat.mul_comm (q.toNat - 2) (val256 v0 v1 v2 v3)])
   omega
 

EvmAsm/Evm64/EvmWordArith/DivRemainderBound.lean

@@ -105,7 +105,7 @@ theorem mulsub_addback_correct {uVal vVal qNat rAbVal : Nat}
     (hge : uVal / vVal + 1 ≤ qNat) :
     qNat - 1 = uVal / vVal ∧ rAbVal < vVal := by
   have := Nat.zero_le (uVal / vVal)
-  have hq1 : qNat ≥ 1 := by omega
+  have : qNat ≥ 1 := by omega
   have heq : uVal = (qNat - 1) * vVal + rAbVal := by omega
   have hge' : uVal / vVal ≤ qNat - 1 := by omega
   exact remainder_lt_of_ge_floor hv heq hge'

EvmAsm/Evm64/EvmWordArith/MulSubChain.lean

@@ -97,7 +97,7 @@ theorem mulsub_correction_eq (u_nat v_nat r_nat qNat : Nat)
     (hchain : u_nat + 2^256 = r_nat + qNat * v_nat)
     (hq : 0 < qNat) :
     u_nat + 2^256 = (r_nat + v_nat) + (qNat - 1) * v_nat := by
-  have hq1 : qNat = 1 + (qNat - 1) := by omega
+  have : qNat = 1 + (qNat - 1) := by omega
   nlinarith [show qNat * v_nat = v_nat + (qNat - 1) * v_nat by nlinarith]
 
 end EvmWord

EvmAsm/Evm64/EvmWordArith/Val256ModBridge.lean

@@ -55,7 +55,7 @@ theorem val256_ms_un_eq_val256_mod_max_skip
   -- compare with `Nat.div_add_mod` to conclude.
   rw [hq] at hmulsub
   have := Nat.div_add_mod (val256 a0 a1 a2 a3) (val256 b0 b1 b2 b3)
-  have hmulcomm : val256 b0 b1 b2 b3 * (val256 a0 a1 a2 a3 / val256 b0 b1 b2 b3) =
+  have : val256 b0 b1 b2 b3 * (val256 a0 a1 a2 a3 / val256 b0 b1 b2 b3) =
       (val256 a0 a1 a2 a3 / val256 b0 b1 b2 b3) * val256 b0 b1 b2 b3 := Nat.mul_comm _ _
   omega