feat: Option lemmas (#8379)

This PR adds missing `Option` lemmas.

Also:

- generalize `bindM` from `Monad` to `Pure`
- change the `simp` normal form of both `<|>` and `Option.orElse` to
`Option.or`

Author: TwoFX

src/Init/Data/Option/Array.lean

@@ -11,6 +11,33 @@ import Init.Data.Option.List
 
 namespace Option
 
+@[simp, grind] theorem mem_toArray {a : α} {o : Option α} : a ∈ o.toArray ↔ o = some a := by
+  cases o <;> simp [eq_comm]
+
+@[simp, grind] theorem forIn'_toArray [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)) :
+    forIn' o.toArray b f = forIn' o b fun a m b => f a (by simpa using m) b := by
+  cases o <;> rfl
+
+@[simp, grind] theorem forIn_toArray [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
+    forIn o.toArray b f = forIn o b f := by
+  cases o <;> rfl
+
+@[simp, grind] theorem foldlM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
+    o.toArray.foldlM f a = o.elim (pure a) (fun b => f a b) := by
+  cases o <;> simp
+
+@[simp, grind] theorem foldrM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
+    o.toArray.foldrM f a = o.elim (pure a) (fun b => f b a) := by
+  cases o <;> simp
+
+@[simp, grind] theorem foldl_toArray (o : Option β) (a : α) (f : α → β → α) :
+    o.toArray.foldl f a = o.elim a (fun b => f a b) := by
+  cases o <;> simp
+
+@[simp, grind] theorem foldr_toArray (o : Option β) (a : α) (f : β → α → α) :
+    o.toArray.foldr f a = o.elim a (fun b => f b a) := by
+  cases o <;> simp
+
 @[simp]
 theorem toList_toArray {o : Option α} : o.toArray.toList = o.toList := by
   cases o <;> simp
@@ -23,4 +50,47 @@ theorem toArray_filter {o : Option α} {p : α → Bool} :
     (o.filter p).toArray = o.toArray.filter p := by
   rw [← toArray_toList, toList_filter, ← List.filter_toArray, toArray_toList]
 
+theorem toArray_bind {o : Option α} {f : α → Option β} :
+    (o.bind f).toArray = o.toArray.flatMap (Option.toArray ∘ f) := by
+  cases o <;> simp
+
+theorem toArray_join {o : Option (Option α)} : o.join.toArray = o.toArray.flatMap Option.toArray := by
+  simp [toArray_bind, ← bind_id_eq_join]
+
+theorem toArray_map {o : Option α} {f : α → β} : (o.map f).toArray = o.toArray.map f := by
+  cases o <;> simp
+
+theorem toArray_min [Min α] {o o' : Option α} :
+    (min o o').toArray = o.toArray.zipWith min o'.toArray := by
+  cases o <;> cases o' <;> simp
+
+@[simp]
+theorem size_toArray_le {o : Option α} : o.toArray.size ≤ 1 := by
+  cases o <;> simp
+
+theorem size_toArray_eq_ite {o : Option α} :
+    o.toArray.size = if o.isSome then 1 else 0 := by
+  cases o <;> simp
+
+@[simp]
+theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] ↔ o = none := by
+  cases o <;> simp
+
+@[simp]
+theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] ↔ o = some a := by
+  cases o <;> simp
+
+@[simp]
+theorem size_toArray_eq_zero_iff {o : Option α} :
+    o.toArray.size = 0 ↔ o = none := by
+  cases o <;> simp
+
+@[simp]
+theorem size_toArray_eq_one_iff {o : Option α} :
+    o.toArray.size = 1 ↔ o.isSome := by
+  cases o <;> simp
+
+theorem size_toArray_choice_eq_one [Nonempty α] : (choice α).toArray.size = 1 := by
+  simp
+
 end Option

src/Init/Data/Option/Attach.lean

@@ -8,11 +8,16 @@ module
 prelude
 import Init.Data.Option.Basic
 import Init.Data.Option.List
+import Init.Data.Option.Array
+import Init.Data.Array.Attach
 import Init.Data.List.Attach
 import Init.BinderPredicates
 
 namespace Option
 
+instance {o : Option α} : Subsingleton { x // o = some x } where
+  allEq a b := Subtype.ext (Option.some.inj (a.property.symm.trans b.property))
+
 /--
 Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
 `Option {x // P x}` is the same as the input `Option α`.
@@ -86,7 +91,7 @@ theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a,
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
 
-theorem attach_eq_some : ∀ (o : Option a) (x : {x // o = some x}), o.attach = some x
+theorem attach_eq_some : ∀ (o : Option α) (x : {x // o = some x}), o.attach = some x
   | none, ⟨x, h⟩ => by simp at h
   | some a, ⟨x, h⟩ => by simpa using h
 
@@ -123,20 +128,41 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
   cases o <;> cases x <;> simp
 
 @[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
-    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
-  cases o
-  · simp at h
-  · simp [get_some]
+    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ :=
+  Subsingleton.elim _ _
+
+@[simp] theorem getD_attach {o : Option α} {fallback} :
+    o.attach.getD fallback = fallback :=
+  Subsingleton.elim _ _
+
+@[simp] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
+    o.attach.get! = default :=
+  Subsingleton.elim _ _
 
 @[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a, o = some a → p a) (h : (o.attachWith p H).isSome) :
     (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
-  cases o
-  · simp at h
-  · simp [get_some]
+  cases o <;> simp
+
+@[simp] theorem getD_attachWith {p : α → Prop} {o : Option α} {h} {fallback} :
+    (o.attachWith p h).getD fallback =
+      ⟨o.getD fallback.1, by cases o <;> (try exact fallback.2) <;> exact h _ (by simp)⟩ := by
+  cases o <;> simp
 
 theorem toList_attach (o : Option α) :
-    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  cases o <;> simp [toList]
+    o.attach.toList = o.toList.attach.map fun x => ⟨x.1, by simpa using x.2⟩ := by
+  cases o <;> simp
+
+theorem toList_attachWith {p : α → Prop} {o : Option α} {h} :
+    (o.attachWith p h).toList = o.toList.attach.map fun x => ⟨x.1, h _ (by simpa using x.2)⟩ := by
+  cases o <;> simp
+
+theorem toArray_attach (o : Option α) :
+    o.attach.toArray = o.toArray.attach.map fun x => ⟨x.1, by simpa using x.2⟩ := by
+  cases o <;> simp
+
+theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
+    (o.attachWith p h).toArray = o.toArray.attach.map fun x => ⟨x.1, h _ (by simpa using x.2)⟩ := by
+  cases o <;> simp
 
 @[simp, grind =] theorem attach_toList (o : Option α) :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
@@ -203,6 +229,11 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
     · rintro ⟨h, rfl⟩
       simp [h]
 
+theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
+    (o.attachWith P h).filter q =
+      (o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
+  cases o <;> simp [filter_some] <;> split <;> simp
+
 theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
     o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
   cases o <;> simp [filter_some]
@@ -211,6 +242,64 @@ theorem toList_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     (o.pbind f).toList = o.attach.toList.flatMap (fun ⟨x, h⟩ => (f x h).toList) := by
   cases o <;> simp
 
+theorem toArray_pbind {o : Option α} {f : (a : α) → o = some a → Option β} :
+    (o.pbind f).toArray = o.attach.toArray.flatMap (fun ⟨x, h⟩ => (f x h).toArray) := by
+  cases o <;> simp
+
+theorem toList_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+    (o.pfilter p).toList = (o.toList.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pfilter_some, toList_some, List.attach_cons, List.attach_nil, List.map_nil]
+    split <;> rename_i h
+    · rw [List.filter_cons_of_pos h]; simp
+    · rw [List.filter_cons_of_neg h]; simp
+
+theorem toArray_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+    (o.pfilter p).toArray = (o.toArray.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [pfilter_some, toArray_some, List.attach_toArray, List.attachWith_mem_toArray,
+      List.attach_cons, List.attach_nil, List.map_nil, List.map_cons, List.size_toArray,
+      List.length_cons, List.length_nil, Nat.zero_add, List.filter_toArray', List.unattach_toArray]
+    split <;> rename_i h
+    · rw [List.filter_cons_of_pos h]; simp
+    · rw [List.filter_cons_of_neg h]; simp
+
+theorem toList_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a → β}
+    (h : ∀ a, o = some a → p a) :
+    (o.pmap f h).toList = o.attach.toList.map (fun x => f x.1 (h _ x.2)) := by
+  cases o <;> simp
+
+theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a → β}
+    (h : ∀ a, o = some a → p a) :
+    (o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
+  cases o <;> simp
+
+theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+    (o.pfilter p).attach =
+      o.attach.pbind fun x h => if h' : p x (by simp_all) then
+        some ⟨x.1, by simpa [pfilter_eq_some_iff] using ⟨_, h'⟩⟩ else none := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [attach_some, eq_mp_eq_cast, id_eq, pbind_some]
+    rw [attach_congr pfilter_some]
+    split <;> simp [*]
+
+theorem attach_guard {p : α → Bool} {x : α} :
+    (guard p x).attach = if h : p x then some ⟨x, by simp_all⟩ else none := by
+  simp only [guard_eq_ite]
+  split <;> simp [*]
+
+theorem attachWith_guard {q : α → Bool} {x : α} {P : α → Prop}
+    {h : ∀ a, guard q x = some a → P a} :
+    (guard q x).attachWith P h = if h' : q x then some ⟨x, h _ (by simp_all)⟩ else none := by
+  simp only [guard_eq_ite]
+  split <;> simp [*]
+
 /-! ## unattach
 
 `Option.unattach` is the (one-sided) inverse of `Option.attach`. It is a synonym for `Option.map Subtype.val`.
@@ -255,6 +344,29 @@ def unattach {α : Type _} {p : α → Prop} (o : Option { x // p x }) := o.map
     (o.attachWith p H).unattach = o := by
   cases o <;> simp
 
+theorem unattach_eq_some_iff {p : α → Prop} {o : Option { x // p x }} {x : α} :
+    o.unattach = some x ↔ ∃ h, o = some ⟨x, h⟩ :=
+  match o with
+  | none => by simp
+  | some ⟨y, h⟩ => by simpa using fun h' => h' ▸ h
+
+@[simp]
+theorem unattach_eq_none_iff {p : α → Prop} {o : Option { x // p x }} :
+    o.unattach = none ↔ o = none := by
+  cases o <;> simp
+
+theorem get_unattach {p : α → Prop} {o : Option { x // p x }} {h} :
+    o.unattach.get h = (o.get (by simpa using h)).1 := by
+  cases o <;> simp
+
+theorem toList_unattach {p : α → Prop} {o : Option { x // p x }} :
+    o.unattach.toList = o.toList.unattach := by
+  cases o <;> simp
+
+theorem toArray_unattach {p : α → Prop} {o : Option { x // p x }} :
+    o.unattach.toArray = o.toArray.unattach := by
+  cases o <;> simp
+
 /-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
 
 /--
@@ -279,4 +391,51 @@ and simplifies these to the function directly taking the value.
   · simp only [filter_some, hf, unattach_some]
     split <;> simp
 
+@[simp] theorem unattach_guard {p : α → Prop} {q : { x // p x } → Bool} {r : α → Bool}
+    (hq : ∀ x h, q ⟨x, h⟩ = r x) {x : { x // p x }} :
+    (guard q x).unattach = guard r x.1 := by
+  simp only [guard]
+  split <;> simp_all
+
+@[simp] theorem unattach_pfilter {p : α → Prop} {o : Option { x // p x }}
+    {f : (a : { x // p x }) → o = some a → Bool}
+    {g : (a : α) → o.unattach = some a → Bool} (hf : ∀ x h h', f ⟨x, h⟩ h' = g x (by simp_all)) :
+    (o.pfilter f).unattach = o.unattach.pfilter g := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [hf, pfilter_some, unattach_some]
+    split <;> simp
+
+@[simp] theorem unattach_merge {p : α → Prop} {f : { x // p x } → { x // p x } → { x // p x }}
+    {g : α → α → α} (hf : ∀ x h y h', (f ⟨x, h⟩ ⟨y, h'⟩).1 = g x y) {o o' : Option { x // p x }} :
+    (o.merge f o').unattach = o.unattach.merge g o'.unattach := by
+  cases o <;> cases o' <;> simp [*]
+
+theorem any_attach {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : o.attach.any q = o.any p := by
+  cases o <;> simp [*]
+
+theorem any_attachWith {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ x, o = some x → r x)
+    {q : { x // r x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : (o.attachWith r hr).any q = o.any p := by
+  cases o <;> simp [*]
+
+theorem any_unattach {p : α → Prop} {o : Option { x // p x }} {q : α → Bool} :
+    o.unattach.any q = o.any (q ∘ Subtype.val) := by
+  cases o <;> simp
+
+theorem all_attach {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : o.attach.all q = o.all p := by
+  cases o <;> simp [*]
+
+theorem all_attachWith {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ x, o = some x → r x)
+    {q : { x // r x } → Bool}
+    (h : ∀ x h, q ⟨x, h⟩ = p x) : (o.attachWith r hr).all q = o.all p := by
+  cases o <;> simp [*]
+
+theorem all_unattach {p : α → Prop} {o : Option { x // p x }} {q : α → Bool} :
+    o.unattach.all q = o.all (q ∘ Subtype.val) := by
+  cases o <;> simp
+
 end Option

src/Init/Data/Option/Basic.lean

@@ -102,11 +102,9 @@ From the perspective of `Option` as a collection with at most one element, the m
 is applied to the element if present, and the final result is empty if either the initial or the
 resulting collections are empty.
 -/
-@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
-  if let some a := o then
-    return (← f a)
-  else
-    return none
+@[inline] protected def bindM [Pure m] (f : α → m (Option β)) : Option α → m (Option β)
+  | none => pure none
+  | some a => f a
 
 /--
 Applies a function in some applicative functor to an optional value, returning `none` with no