do appears suddenly / List.ReduceOption_min_eq_min_join

Stream: new members

[Malvin Gattinger]

I was surprised to have the do notation appear "out of nowhere" here. Is there a reason for it / some automatic coercion going on?

theorem List.ReduceOption_min_weird [m : Min α] {l : List (Option α)} :
    l.reduceOption.min? = l.min? := by
  /- Why is the goal shown with do-notation like this?
  (do
  let a ← l.reduceOption.min?
    pure (some a)) =
  l.min?
  -/
  simp? -- simp only [Option.pure_def, Option.bind_eq_bind]
  -- (l.reduceOption.min?.bind fun a => some (some a)) = l.min?
  sorry

I guess there is some coercion happening because I then realised l.min? on the right side of the = actually would have a different type (Option Option _ instead of Option _). The theorem I want is probably this:

import Mathlib.Data.List.ReduceOption

theorem List.ReduceOption_min_eq_min_join [m : Min α] [Std.Associative m.min] {l : List (Option α)} :
    l.reduceOption.min? = l.min?.join := by
  induction l
  · simp_all [reduceOption]
  case cons head tail IH =>
    cases head
    · rw [List.reduceOption_cons_of_none]
      rw [IH]
      sorry
    · rw [List.reduceOption_cons_of_some]
      simp at *
      rw [IH]
      sorry

Is there something like this already in mathlib?

[Floris van Doorn]

The coercion seems to be caused by docs#Lean.Internal.coeM. I don't think this particular situation was intended (and probably that internal coercion should have lower priority than just applying Option.some.

Looking through Loogle, your lemma seems to not yet exist.

[Floris van Doorn]

Here is a proof:

import Mathlib.Data.List.ReduceOption

open List
variable {α : Type*} [m : Min α]

@[simp] theorem List.none_cons_min?_join :
    ∀ {l : List (Option α)}, (none::l).min?.join = l.min?.join
  | [] => by simp [min?]
  | none::l => by simp [min?]
  | some x::l => by simp [min?]

@[simp] theorem List.some_foldl_min :
    ∀ {l : List (Option α)}, some (foldl min x l.reduceOption) = foldl min (some x) l
  | [] => by simp
  | none::l => by simp [List.some_foldl_min]
  | some x::l => by simp [List.some_foldl_min]

theorem List.ReduceOption_min_eq_min_join :
    ∀ {l : List (Option α)}, l.reduceOption.min? = l.min?.join
  | [] => by simp
  | none::l => by rw [reduceOption_cons_of_none, none_cons_min?_join,
      l.ReduceOption_min_eq_min_join]
  | some x::l => by simp [min?]

[Floris van Doorn]

Not sure if they should be in Mathlib in this form.