From 258bb22f0a5c145ba4b9c87a4ae6d5841bc8261d Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 4 Apr 2025 15:37:36 +0200 Subject: [PATCH] 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 | 22 +++++++++++++ src/Init/Data/Option/Lemmas.lean | 31 ++++++++++++++----- src/Init/Omega/Constraint.lean | 6 ++-- .../BVDecide/Frontend/Normalize/AC.lean | 4 +-- 4 files changed, 51 insertions(+), 12 deletions(-) diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index dc9f2f9d76..1e09ab31bd 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/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 diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index a7351c3d0b..2c27c0c850 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/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 diff --git a/src/Init/Omega/Constraint.lean b/src/Init/Omega/Constraint.lean index d04dff9bf0..542b5b5b98 100644 --- a/src/Init/Omega/Constraint.lean +++ b/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] diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean index b2682f7cf8..133f4e10a1 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean +++ b/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