optional arguments for tactics

Stream: general

[Kevin Lacker]

I'm confused on how to make optional arguments for tactics to work. Right now I have two different tactics, one of them takes an extra argument, and I want to make them just one tactic with that extra argument being optional:

meta def rewrite_search (try_harder : parse $ optional (tk "!"))
  (cfg : config . pick_default) : tactic string :=
rewrite_search_target cfg []

meta def rewrite_search_with (try_harder : parse $ optional (tk "!")) (rs : parse rw_rules)
  (cfg : config . pick_default) : tactic string :=
rewrite_search_target cfg rs.rules

From the docs I thought I should just be able to add a (rs : parse (optional rw_rules)) to the arguments for rewrite_search, but that causes my existing code to mis-parse.

[Johan Commelin]

I think the optional will give you something of type option rw_rules, and so you can then match that with none or some rs.

[Johan Commelin]

Does that make sense. (Me = meta noob)

[Kevin Lacker]

It is just no longer able to parse correctly though. Like this no longer parses when I add another optional arg to rewrite_search:

private example : [[0], [0]] = [[4], [4]] := by rewrite_search

There is already one optional argument, maybe that is related?

[Johan Commelin]

maybe... I'm already way out of my depth

[Reid Barton]

These are interactive tactics? If so I don't think the . optional arguments are good to use

[Kevin Lacker]

yeah these are interactive tactics. i'll try dropping the . thing

[Reid Barton]

Instead, use another cfg : parse $ optional config

[Mario Carneiro]

the . is for using a tactic to produce the default. If it's just a value then you should use :=

[Kevin Lacker]

parse $ optional config doesn't seem to work - for this code:

meta def rewrite_search (try_harder : parse $ optional (tk "!"))
  (cfg : parse $ optional config) : tactic string :=
rewrite_search_target {} []

the "optional" is squiggled with the error:

82:18: type mismatch at application
  optional config
term
  config
has type
  Type : Type 1
but is expected to have type
  lean.parser ?m_1 : Type

82:18: don't know how to synthesize placeholder
context:
try_harder : parse (optional (tk "!"))
⊢ Type

The type of "config" is from:

meta structure config extends tactic.nth_rewrite.cfg :=
(max_iterations     : ℕ := 5000)
(explain            : bool := ff)
(explain_using_conv : bool := tt)

I don't really understand what any of this parser stuff is doing. I just want the tactic to take optional parameters of provided types, it seems like I shouldn't have to be doing any "parsing" at all.

[Kevin Lacker]

you know, I'm not even using this "try_harder" parse option. but removing that, it still doesn't work. simplified code:

meta def rewrite_search (cfg : parse $ optional config) : tactic string :=
rewrite_search_target {} []

with error:

81:40: type mismatch at application
  optional config
term
  config
has type
  Type : Type 1
but is expected to have type
  lean.parser ?m_1 : Type

81:40: don't know how to synthesize placeholder
context:
⊢ Type

it works with the . syntax though

[Kevin Lacker]

i can't really find documentation about the . syntax for optional arguments, or for using parse for optional arguments, so for both of them I am kind of just cutting and pasting from similar-looking code and trying to tweak til it works, rather than nicely understanding what it's doing

[Sebastian Ullrich]

Take a look at other tactics like simp that accept an optional last structure parameter: https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/library/init/meta/interactive.lean#L1210

[Kevin Lacker]

can i have two optional arguments at all

[Yakov Pechersky]

Also seen here in rewrite:

structure rewrite_cfg extends apply_cfg :=
(md            := reducible)
(symm          := ff)
(occs          := occurrences.all)

meta constant rewrite_core (h : expr) (e : expr) (cfg : rewrite_cfg := {}) : tactic (expr × expr × list expr)

meta def rewrite (h : expr) (e : expr) (cfg : rewrite_cfg := {}) : tactic (expr × expr × list expr) :=
do (new_t, prf, metas) ← rewrite_core h e cfg,
   try_apply_opt_auto_param cfg.to_apply_cfg metas,
   return (new_t, prf, metas)

[Yakov Pechersky]

Do you mean optional arguments like simp? or simp! or things like rw and rw {occs = occurences ...}?

[Kevin Lacker]

like rw {occs = occurences ...}

[Kevin Lacker]

simp? could just be a separate function from simp entirely, right? so the "optional argument" there is just messing with the parser to do something you could do straightforwardly

[Yakov Pechersky]

Sorry, one sec

[Kevin Lacker]

OK, this lets me use the := method and avoid the .. Great success.

[Kevin Lacker]

that brings me back to the original question, though, of how to add an optional argument with (rs : parse (optional rw_rules)). That still does not appear to work. This code compiles fine but then it causes anything that just uses by rewrite_search to fail to parse:

meta def rewrite_search (rs : parse $ optional rw_rules) (cfg : config := {}) : tactic string :=
rewrite_search_target cfg []

Is that fundamentally illegitimate in Lean, to have multiple optional arguments? Or is there some other way to do it

[Yakov Pechersky]

meta def rewrite_search (try_harder : parse $ optional (tk "!"))
  (cfg : config := {}) : tactic string :=
rewrite_search_target
{ max_iterations := match try_harder with | none := 5000 | some _ := 100000 end, ..cfg } []

[Yakov Pechersky]

there's some issue with the definition, but I don't have all your code

[Yakov Pechersky]

But you parse in the optional flags, and then map or const_map them how you will. There's probably a neater way to do it

[Kevin Lacker]

there's no flags here, just a list and a config structure

[Kevin Lacker]

so basically when rewrite_search is defined as above, and I have code like:

lemma test_linear_path : h 0 = h 4 := by rewrite_search

constants a b c d e : ℚ

The "constants" line shows an error: 68:1: invalid expression, unexpected token

[Yakov Pechersky]

Did you define an interactive tactic to go along with your tactic?

[Kevin Lacker]

yeah that definition is in tactic.interactive

[Kevin Lacker]

OK, here's a simpler repro. AFAICT the optional parsing just does not work with the rw_rules type.

The tactic:

meta def rewrite_search (rs : parse $ optional rw_rules) : tactic string :=
rewrite_search_target {} []

The code that fails to parse:

private example : [[1], [1]] = [[7], [7]] := by rewrite_search

constants f g : ℕ → ℕ → ℕ → ℕ

The error is on the "constants" - 37:1: invalid expression, unexpected token - but it seems to just happen anywhere immediately after the rewrite_search tactic. Like the optional-parsing is failing to find the supposedly-optional thing, and then failing. This code works if I just delete the (rs : parse $ optional rw_rules) block.

[Rob Lewis]

I haven't followed most of this thread and I'm gonna look at the PR soon, but meta def rewrite_search (rs : parse $ optional rw_rules) : tactic string looks fishy. Is this in the tactic.interactive namespace? Then it should be tactic unit, not tactic string. If it is in tactic.interactive, try the example outside of that namespace. If it isn't in tactic.interactive I wouldn't expect the parsing to work at all.

[Kevin Lacker]

it is in tactic.interactive. it works fine without this optional arg parsing stuff.

[Kevin Lacker]

it is actually returning a string here. but I think that part is working fine.

[Yakov Pechersky]

This works:

import tactic.nth_rewrite

namespace tactic

namespace rewrite_search

meta structure config extends tactic.nth_rewrite.cfg :=
(max_iterations     : ℕ := 5000)
(explain            : bool := ff)
(explain_using_conv : bool := tt)

meta def core (cfg : config := {}) (l : list ℕ) : tactic (list string) :=
do
  msgs ← pure (to_string <$> l),
  trace msgs,
  pure msgs

end rewrite_search

meta def rewrite_search (cfg : tactic.rewrite_search.config := {}) : tactic unit :=
(if cfg.max_iterations = 5000
  then tactic.rewrite_search.core cfg [0, 1, 2, 3, 4]
  else tactic.rewrite_search.core cfg [1000000])
  >> skip

namespace interactive
open lean.parser interactive

meta def rewrite_search (try_harder : parse $ optional (tk "!"))
  (cfg : rewrite_search.config := {}) : tactic unit :=
tactic.rewrite_search { max_iterations := match try_harder with | none := 5000 | some _ := 100000 end,
..cfg }

end interactive


variable (h : ℕ → ℕ)

lemma test_linear_path : h 0 = h 4 := by rewrite_search

lemma test_linear_path' : h 0 = h 4 := by rewrite_search!

[Rob Lewis]

Ahah, I take it back, I see what's going on.

[Yakov Pechersky]

Mouse over on the two rewrite_search and rewrite_search!

[Rob Lewis]

optional rw_rules doesn't make sense, because the rw_rules parser always succeeds.

[Kevin Lacker]

@Yakov Pechersky your example isn't using an optional rw_rules though, which is the sticking point

[Rob Lewis]

If there's no argument given you get an empty rw_rules object.

[Kevin Lacker]

oh, interesting

[Rob Lewis]

Er, wait, that's not quite it.

[Rob Lewis]

rw_rules looks for a list [...] or an expression.

[Rob Lewis]

When it sees constant it thinks that's the beginning of an expression.

[Kevin Lacker]

lean syntax does not seem to be a natural fit for optional arguments to functions

[Kevin Lacker]

if the answer here is like, optionally parsing a rw_rules just isn't simple so don't do it, I can live with that. but a PR reviewer asked for it and it seems reasonable abstractly so I would like to do it if it's straightforward ;-)

[Kevin Lacker]

bc right now there's just two identical tactics but one has this argument and one doesn't

[Rob Lewis]

Expressions can't contain constant, but I think the interactive parser doesn't know that, so it thinks parsing succeeded? But I'm not completely sure what's going on there.

[Rob Lewis]

The easy fix would be to prefix the optional rw_rules with a keyword like using

[Rob Lewis]

So rewrite_search using [....] works, and if you write using without giving a rw_rule you deserve an error. rewrite_search without using won't even try to parse a rw_rule so it won't complain about the following token.

[Kevin Lacker]

that seems quite similar to have a second tactic called rewrite_search_using

[Kevin Lacker]

but either way, TLDR I just shouldn't expect (parse $ optional rw_rules) to work

[Rob Lewis]

Kevin Lacker said:

that seems quite similar to have a second tactic called rewrite_search_using

I mean, yes, except you're not duplicating code? Lots and lots of tactics take optional arguments this way.

[Kevin Lacker]

it isn't duplicating code, you just have both of them call a helper function

[Kevin Lacker]

but i am happy to stylistically adhere to the practices of other tactics

[Rob Lewis]

If you really hate it you can just use the brackets part of rw_rules.

optional ((tk "[" *>
 rw_rules_t.mk <$> sep_by (skip_info (tk ",")) (set_goal_info_pos $ rw_rule_p (parser.pexpr 0))
               <*> (some <$> cur_pos <* set_goal_info_pos (tk "]"))))

or whatever (maybe don't inline it though). You won't be able to write by rewrite_search foo but you can do by rewrite_search [foo].

[Kevin Lacker]

hmm, I hate that more.

[Kevin Lacker]

what is another tactic that happily uses a "using" keyword that I can copy off its design

[Rob Lewis]

Note that this is the same syntax as simp (you can't write by simp foo, has to be by simp [foo])

[Reid Barton]

Kevin Lacker said:

what is another tactic that happily uses a "using" keyword that I can copy off its design

simpa, convert

[Rob Lewis]

src#tactic.interactive.choose

[Kevin Lacker]

OK i'll look there

[Kevin Lacker]

thanks for the help folks

[Rob Lewis]

After reviewing the PR, I think there's a better solution here.

Define

private meta def rw_search_parser : lean.parser (pexpr × bool) :=
do flipped ← optional $ tk "←",
   e ← lean.parser.pexpr 0,
   return (e, flipped.is_some)

/-- Search for a chain of rewrites to prove an equation or iff statement. -/
meta def rewrite_search (args : parse (optional (list_of rw_search_parser))) (cfg : config := {}) : tactic unit :=
rewrite_search_target cfg (args.get_or_else []) $> ()

Now rewrite_search_target is getting a list of pexpr × bools instead of a list of rw_rules. But you never used the rw_rules as rw_rules, you converted them into expr × bool immediately. You need to propagate that change through a few functions but it isn't hard.

[Rob Lewis]

This allows you to write by rewrite_search and by rewrite_search [a, b, c]. You can't write by rewrite_search a. But I'm not inclined to allow that anyway. rw_search is closer to simp than rw. Even if you only give it a single extra rule, morally you're giving it a singleton set of rules. That rule can be used multiple times.

[Rob Lewis]

So needing to enclose it in a list makes sense.

[Mario Carneiro]

This is the reason why simp has required brackets around its arguments while rw doesn't, btw

[Mario Carneiro]

oh, rob said this already

[Mario Carneiro]

Actually, I think it might be possible to write a parser that only allows the config if the brackets are provided, but lets you leave off the brackets if you don't provide a config

[Rob Lewis]

Mario Carneiro said:

Actually, I think it might be possible to write a parser that only allows the config if the brackets are provided, but lets you leave off the brackets if you don't provide a config

Possible, but I wouldn't bother

[Rob Lewis]

In fact, I'd prefer that you not bother!

[Mario Carneiro]

how come?

[Mario Carneiro]

is it just the churn of changing simp, or is it the regression in writing simp [] {config_opt := ...} instead of simp {config_opt := ...}

[Rob Lewis]

It's a more complicated parser and more work to describe the available syntax options, and semantically it doesn't make a ton of sense.

[Mario Carneiro]

I'm not sure I follow the latter argument

[Rob Lewis]

I was talking about rewrite_search foo {...} vs rewrite_search [foo] {...}

[Rob Lewis]

May have misinterpreted what you meant about simp, I didn't know you needed [] in your example.

[Mario Carneiro]

you would in the suggested change, because the {...} would be treated as a simp lemma otherwise

[Rob Lewis]

Oh, wait, sorry

[Rob Lewis]

I read you right the first time and misread the second time

[Mario Carneiro]

I suppose you could check for a { but I'm not sure if it's possible to do that, roll back by one token and then parse it as an expr

[Mario Carneiro]

the major limitation is that lean's parser does not do backtracking, so you have to sometimes write parsers in a weird way

[Rob Lewis]

Allowing simp foo saves you two characters in an edge case in exchange for a more complicated parser. And you have a simp set anyway, semantically it makes sense that you're adding a set (/list) to it, so, [a].

[Rob Lewis]

Wasn't even thinking of the simp [] {} case, but that's another argument.

[Mario Carneiro]

I don't think simp [one_lemma] is an edge case

[Mario Carneiro]

it's much more common than simp {config}

[Rob Lewis]

Given how often simp is called, it wouldn't surprise me if the more complicated parser even had a visible performance impact.

[Mario Carneiro]

6950 hits for simp [, 2478 for simp [one_word], 39 for simp {

[Mario Carneiro]

I don't have a really good understanding of parser performance behavior. There is an extra eval_expr to get the config but this seems to be a pretty uncommon option anyway

[Mario Carneiro]

My guess is that it would not be visible in the benchmark over the noise, but probably we would have to test to find out

[Mario Carneiro]

I remember reporting this "inconsistency" between simp and rw back in the day to leo et al, and being told about the parser limitations preventing this. I have since become better at writing parsers

[Mario Carneiro]

the cfg currently comes at a really weird place though, after everything including the with attrs... and at pos

[Mario Carneiro]

Well, I managed to find a lean bug while mocking this up:

import tactic

namespace tactic.interactive
setup_tactic_parser

meta def test : parse texpr? → tactic unit := λ _, trivial

end tactic.interactive

example : true := by test . -- ok
example : true := by test   -- works, but...
example -- invalid expression, unexpected token
  : true := by test .

[Mario Carneiro]

It appears that the optional texpr parser will crash badly if it sees a command keyword instead of just failing by the usual channels. It still works to parse what it was supposed to, the tactic continues and everything, but it throws an error on the token while it's at it

[Mario Carneiro]

Here's a repro in pure lean:

example (x : ℕ) : x = x := by transitivity -- this error is expected
example : true := trivial -- this one is not

[Kevin Lacker]

nice. yeah missing by rewrite_search a is not a big loss. i'll implement this suggestion in the PR