feat: Option.or (#4600)

Split from #4583

src/Init/Data/Option/Basic.lean

@@ -80,7 +80,9 @@ theorem map_id : (Option.map id : Option α → Option α) = id :=
   | none   => false
 
 /--
-Implementation of `OrElse`'s `<|>` syntax for `Option`.
+Implementation of `OrElse`'s `<|>` syntax for `Option`. If the first argument is `some a`, returns
+`some a`, otherwise evaluates and returns the second argument. See also `or` for a version that is
+strict in the second argument.
 -/
 @[always_inline, macro_inline] protected def orElse : Option α → (Unit → Option α) → Option α
   | some a, _ => some a
@@ -89,6 +91,12 @@ Implementation of `OrElse`'s `<|>` syntax for `Option`.
 instance : OrElse (Option α) where
   orElse := Option.orElse
 
+/-- If the first argument is `some a`, returns `some a`, otherwise returns the second argument.
+This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
+@[always_inline, macro_inline] def or : Option α → Option α → Option α
+  | some a, _ => some a
+  | none,   b => b
+
 @[inline] protected def lt (r : α → α → Prop) : Option α → Option α → Prop
   | none, some _     => True
   | some x,   some y => r x y

src/Init/Data/Option/Lemmas.lean

@@ -258,3 +258,46 @@ end
 @[simp] theorem toList_some (a : α) : (a : Option α).toList = [a] := rfl
 
 @[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
+
+@[simp] theorem or_some : (some a).or o = some a := rfl
+@[simp] theorem none_or : none.or o = o := rfl
+
+theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
+  cases o <;> rfl
+
+@[simp] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
+  cases o <;> rfl
+
+@[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
+  cases o <;> rfl
+
+@[simp] theorem or_eq_none : or o o' = none ↔ o = none ∧ o' = none := by
+  cases o <;> simp
+
+theorem or_eq_some : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by
+  cases o <;> simp
+
+theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
+  cases o₁ <;> cases o₂ <;> rfl
+instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
+
+@[simp]
+theorem or_none : or o none = o := by
+  cases o <;> rfl
+instance : Std.LawfulIdentity (or (α := α)) none where
+  left_id := @none_or _
+  right_id := @or_none _
+
+@[simp]
+theorem or_self : or o o = o := by
+  cases o <;> rfl
+instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
+
+theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
+  cases o <;> rfl
+
+theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by
+  cases o <;> rfl
+
+theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by
+  cases o <;> rfl