Proofs where cases are simplified away by contradiction

Stream: lean4

[Siddharth Bhat]

I have many proofs where I cases on a complicated inductive, and all but one case is eliminated from contradictions in the hypotheses. I wish to then automatically introduce the variables of the interesting inductive without having a nesting of case <case_name> <var1> <var2> ... <varN>. Is there some way to achieve this? What is the canonical way to write this proof in Lean?

Example proof, where I wish to avoid the case some ___ and the nesting that comes with it.

theorem example_thm (foo bar baz : Option Nat)
  (FOO: foo.isSome)
  (BAR: bar.isSome)
  (BAZ: baz.isSome) :
  ((do
    let a ← foo
    let b ← bar
    let c ← baz
    return (a+ b + c) : Option Nat) =
    (do
      let b ← bar
      let a ← foo
      let c ← baz
      return (a + b + c))) := by {
  simp[bind, Option.bind];
  cases FOO_VAL:foo <;> simp[FOO_VAL] at FOO; case some foo_val => {
    cases BAR_VAL:bar <;> simp[BAR_VAL] at BAR; case some bar_val => {
      cases BAZ_VAL:baz <;> simp[BAZ_VAL] at BAZ; case some baz_val => {
        simp[FOO_VAL, BAR_VAL, BAZ_VAL];
      }
    }
  }
}

[Adrien Champion]

How about

theorem example_thm
  (foo bar baz : Option Nat)
  -- -- unused
  -- (FOO: foo.isSome)
  -- (BAR: bar.isSome)
  -- (BAZ: baz.isSome)
: (
    ( do
      let a ← foo
      let b ← bar
      let c ← baz
      return (a + b + c)
    ) = ( do
      let b ← bar
      let a ← foo
      let c ← baz
      return (a + b + c)
  )
) := by
  simp [bind, Option.bind]
  cases foo <;> cases bar <;> simp

[Siddharth Bhat]

@Adrien Champion it works in this case, but in the proof I have, I really do need control over the name I introduce, since the proof is not immediately dispatched by simp.

[Eric Wieser]

This works;

theorem example_thm (foo bar baz : Option Nat)
  (FOO: foo.isSome)
  (BAR: bar.isSome)
  (BAZ: baz.isSome) :
  ((do
    let a ← foo
    let b ← bar
    let c ← baz
    return (a + b + c) : Option Nat) =
    (do
      let b ← bar
      let a ← foo
      let c ← baz
      return (a + b + c))) := by
  match foo, bar, baz with
  | some f, some b, some z =>
    simp [bind, Option.bind]

[Siddharth Bhat]

@Eric Wieser nice, thanks! What does match do in the unhandled case? does it automatically dispatch the contradiction?

[Eric Wieser]

Clearly it did so here, although I don't know exactly what type of contradiction it can and can't dispatch

[Eric Wieser]

My best guess is that it unfolded Option.isSome at all the hypotheses that depended on foo, bar, baz (reducing them to false = true), then did cases on those too