Tactic to deconstruct monadic syntax

Stream: new members

[McCoy R. Becker]

I'm working on a proof, and I have a hypothesis of the form:

h_eval : (do
    let t_eval ← none
    pure (Term.Abs t_eval)) =
  some t'

I'd like to collapse this to show a contradiction, but I'm not quite sure what to apply here. I tried simp at h_eval, but that made no progress.

[McCoy R. Becker]

Related -- is there an easy way to apply cases to syntax of this form (for e.g. t1_eval):

h_eval : (do
    let t1_eval ← eval n✝ [] a✝¹
    let t2_eval ← eval n✝ [] a✝
    eval n✝ [] (Term.App t1_eval t2_eval)) =
  some t'

[Mario Carneiro]

There is a simp lemma for this but it is hidden by bind. Try simp [bind]

[McCoy R. Becker]

No progress, unfortunately

[Mario Carneiro]

import Std?

[McCoy R. Becker]

ah, sorry -- simp [bind] at h_eval

[Mario Carneiro]

#mwe

[McCoy R. Becker]

I think I got it by applying simp [bind] to the hypothesis.

[McCoy R. Becker]

thanks for the MWE tip! I'll play around with the web editor later so I can be more helpful when asking Qs