chore: deprecate Option.merge and Option.liftOrGet in favor of Option.zipWith (#7818)

This PR deprecates `Option.merge` and `Option.liftOrGet` in favor of
`Option.zipWith`.

src/Init/Data/Option/Basic.lean

@@ -209,12 +209,33 @@ The value is `some (fn a b)` if the inputs are `some a` and `some b`. Otherwise,
 equivalent to `Option.orElse`: if only one input is `some x`, then the value is `some x`, and if
 both are `none`, then the value is `none`.
 
+Examples:
+ * `Option.zipWith (· + ·) none (some 3) = some 3`
+ * `Option.zipWith (· + ·) (some 2) (some 3) = some 5`
+ * `Option.zipWith (· + ·) (some 2) none = some 2`
+ * `Option.zipWith (· + ·) none none = none`
+-/
+def zipWith (fn : α → α → α) : Option α → Option α → Option α
+  | none  , none   => none
+  | some x, none   => some x
+  | none  , some y => some y
+  | some x, some y => some <| fn x y
+
+/--
+Applies a function to a two optional values if both are present. Otherwise, if one value is present,
+it is returned and the function is not used.
+
+The value is `some (fn a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
+equivalent to `Option.orElse`: if only one input is `some x`, then the value is `some x`, and if
+both are `none`, then the value is `none`.
+
 Examples:
  * `Option.merge (· + ·) none (some 3) = some 3`
  * `Option.merge (· + ·) (some 2) (some 3) = some 5`
  * `Option.merge (· + ·) (some 2) none = some 2`
  * `Option.merge (· + ·) none none = none`
 -/
+@[deprecated zipWith (since := "2025-04-04")]
 def merge (fn : α → α → α) : Option α → Option α → Option α
   | none  , none   => none
   | some x, none   => some x
@@ -307,6 +328,7 @@ Examples:
  * `Option.liftOrGet (· + ·) (some 2) none = some 2`
  * `Option.liftOrGet (· + ·) none none = none`
 -/
+@[deprecated zipWith (since := "2025-04-04")]
 def liftOrGet (f : α → α → α) : Option α → Option α → Option α
   | none, none => none
   | some a, none => some a

src/Init/Data/Option/Lemmas.lean

@@ -429,21 +429,38 @@ theorem guard_eq_map (p : α → Prop) [DecidablePred p] :
 theorem guard_def (p : α → Prop) {_ : DecidablePred p} :
     Option.guard p = fun x => if p x then some x else none := rfl
 
-theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
-    ∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂
+theorem zipWith_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
+    ∀ o₁ o₂, zipWith f o₁ o₂ = o₁ ∨ zipWith f o₁ o₂ = o₂
   | none, none => .inl rfl
   | some _, none => .inl rfl
   | none, some _ => .inr rfl
-  | some a, some b => by have := h a b; simp [liftOrGet] at this ⊢; exact this
+  | some a, some b => by have := h a b; simp [zipWith] at this ⊢; exact this
 
-@[simp] theorem liftOrGet_none_left {f} {b : Option α} : liftOrGet f none b = b := by
+@[simp] theorem zipWith_none_left {f} {b : Option α} : zipWith f none b = b := by
   cases b <;> rfl
 
-@[simp] theorem liftOrGet_none_right {f} {a : Option α} : liftOrGet f a none = a := by
+@[simp] theorem zipWith_none_right {f} {a : Option α} : zipWith f a none = a := by
   cases a <;> rfl
 
-@[simp] theorem liftOrGet_some_some {f} {a b : α} :
-  liftOrGet f (some a) (some b) = f a b := rfl
+@[simp] theorem zipWith_some_some {f} {a b : α} :
+  zipWith f (some a) (some b) = f a b := rfl
+
+@[deprecated zipWith_eq_or_eq (since := "2025-04-04")]
+theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
+    ∀ o₁ o₂, zipWith f o₁ o₂ = o₁ ∨ zipWith f o₁ o₂ = o₂ :=
+  zipWith_eq_or_eq h
+
+@[deprecated zipWith_none_left (since := "2025-04-04")]
+theorem liftOrGet_none_left {f} {b : Option α} : zipWith f none b = b :=
+  zipWith_none_left
+
+@[deprecated zipWith_none_right (since := "2025-04-04")]
+theorem liftOrGet_none_right {f} {a : Option α} : zipWith f a none = a :=
+  zipWith_none_right
+
+@[deprecated zipWith_some_some (since := "2025-04-04")]
+theorem liftOrGet_some_some {f} {a b : α} : zipWith f (some a) (some b) = f a b :=
+  zipWith_some_some
 
 @[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 

src/Init/Omega/Constraint.lean

@@ -166,13 +166,13 @@ theorem combo_sat (a) (w₁ : c₁.sat x₁) (b) (w₂ : c₂.sat x₂) :
 
 /-- The conjunction of two constraints. -/
 def combine (x y : Constraint) : Constraint where
-  lowerBound := Option.merge max x.lowerBound y.lowerBound
-  upperBound := Option.merge min x.upperBound y.upperBound
+  lowerBound := Option.zipWith max x.lowerBound y.lowerBound
+  upperBound := Option.zipWith min x.upperBound y.upperBound
 
 theorem combine_sat : (c : Constraint) → (c' : Constraint) → (t : Int) →
     (c.combine c').sat t = (c.sat t ∧ c'.sat t) := by
   rintro ⟨_ | l₁, _ | u₁⟩ <;> rintro ⟨_ | l₂, _ | u₂⟩ t
-    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le, Option.merge] at *
+    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le, Option.zipWith] at *
   · rw [And.comm]
   · rw [← and_assoc, And.comm (a := l₂ ≤ t), and_assoc]
   · rw [and_assoc]

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean

@@ -290,8 +290,8 @@ def canonicalizeWithSharing (P : Expr) (lhs rhs : Expr) : SimpM Simp.Step := do
     -- of `lCoeff_{old}` are zero iff `lExpr` contains only neutral elements,
     -- we default to `lNew` being some canonical neutral element if both
     -- `commonExpr?` and `lNew?` are `none`.
-    let lNew := Option.merge (mkApp2 op.toExpr) commonExpr? lNew? |>.getD op.neutralElement
-    let rNew := Option.merge (mkApp2 op.toExpr) commonExpr? rNew? |>.getD op.neutralElement
+    let lNew := Option.zipWith (mkApp2 op.toExpr) commonExpr? lNew? |>.getD op.neutralElement
+    let rNew := Option.zipWith (mkApp2 op.toExpr) commonExpr? rNew? |>.getD op.neutralElement
 
     let oldExpr := mkApp2 P lhs rhs
     let expr := mkApp2 P lNew rNew