concatenating and the tactic monad

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

this question belongs in the "New members metaprogramming" stream.

I feel very uneasy about tactic and I may have gotten in a weird place to ask this question unwillingly.

I would like confirmation/correction about whether the definition below does what I think it does.

meta def cat (l : tactic expr)  (m : tactic (list expr)) : tactic (list expr) :=
l >>= (λ e, m)

Does this mean "take the expr in l, concatenate it with the list in m and produce a list that is one longer, inside the tactic monad"?

Many of these concepts are well below my level of reasonable confidence for me to be sure or even know how to check in some examples.
For instance, what is the role of the "irrelevant" λ e?

Thanks!

[Henrik Böving]

Do you understand the general idea of a monad? If not you might want to take a look at simple ones such as option or list in order to grasp the concept.

[Damiano Testa]

I may have a too general idea of a monad. I am usually able to get by with option and list. I struggle specifically with tactic, though (and have been playing with it for about a week, so I do not really have much experience at all).

[Henrik Böving]

Okay, in that case: The tactic monad is basically a state monad that allows you to indicate that an operation failed in addition. This means that the bind operation will execute the left hand side (in this case l) which:

1. might change the state
2. might throw an error which will prevent the next (right hand side) computation from getting executed and instead give back the error as a result

the right hand side then gets passed the value that the first computation returned, in this case an expr and is allowed to execute whatever to return a list expr in this case.

So effectively what you are doing here is:

1. execute tactic l, if it fails return instantly with a failure
2. if it doesnt fail tactic l might have changed the tactic state
3. pass the result (the expr) of tactic l as a parameter e to your lambda that may return some expression of type tactic (list expr). Note that this computation will already be happening with the updated state. In this specific case you are simply choosing to ignoree
4. the lambda then just returns m but evaluated with the state that l returned so this computation is different from just returning m due to the eventual error and state change of l

[Damiano Testa]

Ok, this clarifies somewhat. Here is what I am trying to do.

[Damiano Testa]

I have a list of "user-provided" exprs and a list of exprs that lean found in some expr. The user wants to get lean to match the exprs that it gives to lean with a sublist of the exprs that lean produces.

[Damiano Testa]

for instance, lean computes [a, b, c] and the user want to obtain b.

[Damiano Testa]

So, they pass [b], but, because of how things go with pretty-printing and all, they may not be an exact match, but may only unify to the same thing.

[Damiano Testa]

So, I try to get lean to try to unify each element of [a, b, c] with the b that the user provides and, as soon as it matches, lean then uses the b that lean had, instead of the one that the user had provided.

[Damiano Testa]

So far, I am able to get this to work.

[Damiano Testa]

My problem starts when the user passes more than one input. Then, I want lean to find matches different from the matches that it already found.

[Damiano Testa]

Now, if I were not in a monad-mess, I would simply recursively do the match on the initial element of the list, and then call the recursion with some list.erase (matched element). Except that the matched element is now in tactic expr and not in expr and I am entangled!

[Damiano Testa]

(The error part that you mention is also very relevant, since I am throwing errors if a match for the user provided expr is not found and I want the computation to stop there and Lean to say that it did not find a match)

[Damiano Testa]

Here is the code that I have so far. Maybe it makes things appear clearer.

import tactic.core

namespace tactic

meta def cat (l : tactic expr)  (m : tactic (list expr)) : tactic (list expr) :=
l >>= (λ e, m)

-- adapted from Arthur's code
meta def _root_.expr.unify_with (e e' : expr) : tactic bool :=
succeeds $ unify e e'

-- adapted from `tactic.op_induction.is_opposite` in `data.opposite`
/--  Given `e : expr` and `l : list expr`, find the first expression in `l` that unifies with `e`.
Fail if no such hypothesis exist in the local context. -/
meta def _root_.expr.find_in (e : expr) (lc : list expr) : tactic expr :=
do
  pe ← pp e,
  h :: _ ← lc.mfilter $ e.unify_with | fail format!"No {pe} found",
  return h

meta def _root_.list.to_arg_list_cat : list expr → list expr → tactic (list expr)
| [] sl := return []
| (e::es) sl := do
  ma ← (e.find_in sl),
  cat (pure ma) (_root_.list.to_arg_list_cat es (sl.erase ma))

end tactic

[Damiano Testa]

I hoped that list.to_arg_list_cat would take an element of the first list, checked whether it could be unified with an element of the second list.

• If not, throw an error.
• If it unifies to ma, then append ma to the new list, and repeat the matching with the remaining elements of the first list and the second list without ma.

I do not think that this is what that function does, though.

[Damiano Testa]

So, reading again your answer, it seems that e in λ e is what I would like to remove from m?
I don't know, I am very confused.

[Damiano Testa]

Let me try again with a question.

Is it possible to extract a bool from a tactic bool?

[Damiano Testa]

From the discussion above, I understand that the tactic bool may have failed, in which case I would extract nothing. Otherwise, I probably can read off the value of the bool? If I wanted to do this, how would I go about it?

[Henrik Böving]

let mybool <- mytactic

for the rest of your question my meta programming experience in lean 3 is too limited im afraid

[Damiano Testa]

Thank you: I feel that I understood something from what you said, but I am still confused by a lot of basic questions.

[Damiano Testa]

Some small amount of testing seems to indicate that this might be a solution to the question that I asked. I leave it here, in case someone can either check it or needs it!

import tactic.move_add

open tactic

/-- A `tactic bool` computing whether the user-input `e` unifies with `e'`. -/
meta def expr.unify_with (e e' : expr) : tactic bool :=
succeeds $ unify e e'

/-- A `tactic expr` that either finds the first entry of `lc` that unifies with `e` or fails. -/
meta def expr.find_in (e : expr) (lc : list expr) : tactic expr :=
do
  pe ← pp e,
  h :: _ ← lc.mfilter $ e.unify_with | fail format!"No {pe} found",
  return h

/-- A `tactic (list expr)` that either finds a sublist of its second argument`sl` that unifies
entry-wise with its first argument or fails. -/
meta def list.to_arg_list_cat : list expr → list expr → tactic (list expr)
| [] sl := return []
| (e::es) sl := do
  ma ← (e.find_in sl),
  nl ← (list.to_arg_list_cat es (sl.erase ma)),
  functor.map (λ (T : expr), nl.cons T) (return ma)

[Damiano Testa]

Henrik, thank you for your explanation: what you said definitely helped me make progress!

[Damiano Testa]

If I understand correctly, when you are inside a do block, Lean displays in the infoview types without tactic, but I am supposed to think that they are all implicitly tactic.
If this is so, then that was part of my confusion!
If that is not so, then I am confused at a deeper level.

[Kevin Buzzard]

I think the whole point of a monad is that you cannot escape it! You can't get a nat from a list nat because the list might be empty.

[Henrik Böving]

I don't know about the Lean 3 specifics but this is most certainly not the case in Lean 4, could you show what makes you think so?

[Damiano Testa]

Kevin, I see your point, but you could assign 0 to every list. I was worried that someone would have answered this to my questions, but luckily the community here is too nice to do so!

[Kevin Buzzard]

Well you can get a bool from a tactic bool because you can just use tt! That's what you didn't want me to say, right? :-)

[Damiano Testa]

Indeed, this is what I was lucky enough to not have received as a first answer! :stuck_out_tongue_wink:

[Damiano Testa]

Anyway, I think that what I have above is correct: it works inside the monad, extracts what seems to work in a dubious case and does not leave the monad!

[Kevin Buzzard]

So your tactic bool term could be made from tt or ff or it could represent some kind of failure.

[Damiano Testa]

Yes, and the failure is passed on to the tactic (list expr): you either get a list expr or you fail, since you failed at one of the steps that was building your list.

[Damiano Testa]

Now that I (think that I) have solved this question, it all seems much simpler than I thought at the beginning.

[Damiano Testa]

Henrik, I had read about this failure thing, but it was not until you explained it that I actually internalized it. Thank you again!

[Damiano Testa]

Regarding "not leaving the monad", I can imagine that there are silly kinds of monads, like the identity monad, where you can enter and leave at will. However, I would also agree with Kevin that "most" monads are of the kind that you cannot leave. The ones that have been mentioned in this stream seem to be this trap-like kind of monad:

• list, you can leave, if the list is not [],
• option, you can leave, if you are not none,
• tactic, you can leave, if you did not produce an error.

At least, this is my understanding of it!

[Damiano Testa]

In fact, when dealing with polynomials, in mathlib there are the degree, taking values in option nat and the nat_degree, taking values in nat and assigning 0 to none. I was at the beginning completely unable to work with the option nat-valued degree, but now I think that a lot of the difficulties of working with nat_degree arise from the "weird" assignment of 0 : nat as the degree of 0 : R[X].

[Henrik Böving]

So your concept of "leaving" isnt exactly correct here, what you are referring to as leaving is the bind operation you see if you have a code like this:

let x <- myMonadicComputation
return (somePureComputation x)

what this compiles to is:

myMonadicComputation >>= (fun x -> return (somePureComputation x)

so you are actually never leaving the monad you are making use of the bind operator in a syntactically nice way that makes it seem like you are leaving but you are in fact always there.

Now there is actually a way to turn e.g. a tactic expr into just an expr or an error. After all not all parts of the Lean compiler live in the tactic moand right?

If we take a look at the definition of the tactic monad in we can see that its a

state → result state α

where state is the tactic state and α is whatever is "stored inside the monad" so if you really want to escape the monad all you have to do is provide a state to this function and it will give you back either an error or a state coupled with an α at which point you have truly escaped. The provider of this state is the Lean compiler who constructs the initial tactic state from other information when you open a tactic

[Damiano Testa]

Yes, I think that we probably all mean the same thing, but put the emphasis on different parts. I would consider the lingering possibility that an error is produced as "you have not left the monad, you were simply lucky enough that you were not bitten by it". On the other hand, if what you are interested in is the outcome of the computation, and you get a result, it is immaterial that something else could have failed!

[Reid Barton]

Damiano Testa said:

Is it possible to extract a bool from a tactic bool?

How about "Is it possible to extract a unit from a tactic unit?" Now the answer "Sure, just use unit.star" isn't even that silly, because what else could you get? But you are throwing away the effects of the tactic, which might be introducing a variable or running the simplifier. It is not just about success or failure.

[Damiano Testa]

Reid, I agree. It is also how I feel about degree → nat_degree for polynomials. At some level, it is not wrong to assign degree 0 to the zero polynomial, but, even though it is constant, the zero polynomial is a different constant than the other constant polynomials!