Combining do notation and tactic mode?

Stream: new members

[aron]

Is it possible to use do notation in tactic mode?

I have a few functions that a) take some proofs as input and b) return a state monad. I'd like to use the refine tactic so I can call the function whilst providing the required proofs later, but it doesn't look like I can use do and by in the same block. Which means I have to manually thread the state through each function, which gets quite finicky.

Is it possible to use tactics and do notation in the same block? If not, what would be the best way to thread a state through a series of computations in a by tactic block?

[Kevin Buzzard]

exact takes you back into term mode and presumably you can use do there

[aron]

ah nice, yeah that worked!
Screenshot 2025-02-23 at 20.10.13.png

[Kyle Miller]

Watch out though; using tactics like rw when you're defining functions like this can cause them to be difficult to prove things about, or cause them to not be reducible (causing rfl or decide to fail for example).

It would be better to stay in term mode, and put the rewrites inside the haves (which are still valid in term mode). This keeps the casts that rw produces inside the proofs, where they won't cause any trouble.

[aron]

is there a way to do that without duplicating these 4 lines at the top that are used in the definitions of both okUnif and errUnif?
Screenshot 2025-02-23 at 20.21.19.png

[Kyle Miller]

You could put each rewrite into the corresponding have, like have prf1_empty := by rw [...]; exact ...