Zulip Chat Archive

Stream: general

Topic: optional arguments for tactics


Kevin Lacker (Dec 01 2020 at 17:38):

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 (Dec 01 2020 at 17:58):

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 (Dec 01 2020 at 17:58):

Does that make sense. (Me = meta noob)

Kevin Lacker (Dec 01 2020 at 18:02):

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 (Dec 01 2020 at 18:05):

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

Reid Barton (Dec 01 2020 at 18:05):

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

Kevin Lacker (Dec 01 2020 at 18:06):

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

Reid Barton (Dec 01 2020 at 18:06):

Instead, use another cfg : parse $ optional config

Mario Carneiro (Dec 01 2020 at 19:22):

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

Kevin Lacker (Dec 02 2020 at 17:08):

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 (Dec 02 2020 at 17:11):

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 (Dec 02 2020 at 17:14):

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 (Dec 02 2020 at 17:19):

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 (Dec 02 2020 at 17:22):

can i have two optional arguments at all

Yakov Pechersky (Dec 02 2020 at 17:22):

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 (Dec 02 2020 at 17:23):

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

Kevin Lacker (Dec 02 2020 at 17:23):

like rw {occs = occurences ...}

Kevin Lacker (Dec 02 2020 at 17:24):

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 (Dec 02 2020 at 17:25):

Sorry, one sec

Kevin Lacker (Dec 02 2020 at 17:27):

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

Kevin Lacker (Dec 02 2020 at 17:29):

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 (Dec 02 2020 at 17:30):

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 (Dec 02 2020 at 17:30):

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

Yakov Pechersky (Dec 02 2020 at 17:31):

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 (Dec 02 2020 at 17:31):

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

Kevin Lacker (Dec 02 2020 at 17:34):

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 (Dec 02 2020 at 17:35):

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

Kevin Lacker (Dec 02 2020 at 17:35):

yeah that definition is in tactic.interactive

Kevin Lacker (Dec 02 2020 at 17:49):

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 (Dec 02 2020 at 17:57):

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 (Dec 02 2020 at 17:58):

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

Kevin Lacker (Dec 02 2020 at 18:01):

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

Yakov Pechersky (Dec 02 2020 at 18:04):

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 (Dec 02 2020 at 18:04):

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

Yakov Pechersky (Dec 02 2020 at 18:04):

Mouse over on the two rewrite_search and rewrite_search!

Rob Lewis (Dec 02 2020 at 18:04):

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

Kevin Lacker (Dec 02 2020 at 18:05):

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

Rob Lewis (Dec 02 2020 at 18:05):

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

Kevin Lacker (Dec 02 2020 at 18:05):

oh, interesting

Rob Lewis (Dec 02 2020 at 18:06):

Er, wait, that's not quite it.

Rob Lewis (Dec 02 2020 at 18:07):

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

Rob Lewis (Dec 02 2020 at 18:07):

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

Kevin Lacker (Dec 02 2020 at 18:08):

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

Kevin Lacker (Dec 02 2020 at 18:09):

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 (Dec 02 2020 at 18:09):

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

Rob Lewis (Dec 02 2020 at 18:12):

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 (Dec 02 2020 at 18:13):

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

Rob Lewis (Dec 02 2020 at 18:14):

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 (Dec 02 2020 at 18:15):

that seems quite similar to have a second tactic called rewrite_search_using

Kevin Lacker (Dec 02 2020 at 18:15):

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

Rob Lewis (Dec 02 2020 at 18:17):

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 (Dec 02 2020 at 18:18):

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

Kevin Lacker (Dec 02 2020 at 18:19):

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

Rob Lewis (Dec 02 2020 at 18:21):

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 (Dec 02 2020 at 18:21):

hmm, I hate that more.

Kevin Lacker (Dec 02 2020 at 18:21):

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

Rob Lewis (Dec 02 2020 at 18:22):

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

Reid Barton (Dec 02 2020 at 18:23):

Kevin Lacker said:

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

simpa, convert

Rob Lewis (Dec 02 2020 at 18:24):

src#tactic.interactive.choose

Kevin Lacker (Dec 02 2020 at 18:25):

OK i'll look there

Kevin Lacker (Dec 02 2020 at 18:25):

thanks for the help folks

Rob Lewis (Dec 02 2020 at 19:51):

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 (Dec 02 2020 at 19:53):

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 (Dec 02 2020 at 19:53):

So needing to enclose it in a list makes sense.

Mario Carneiro (Dec 02 2020 at 23:28):

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

Mario Carneiro (Dec 02 2020 at 23:30):

oh, rob said this already

Mario Carneiro (Dec 02 2020 at 23:30):

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 (Dec 02 2020 at 23:33):

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 (Dec 02 2020 at 23:33):

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

Mario Carneiro (Dec 02 2020 at 23:37):

how come?

Mario Carneiro (Dec 02 2020 at 23:38):

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 (Dec 02 2020 at 23:39):

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 (Dec 02 2020 at 23:39):

I'm not sure I follow the latter argument

Rob Lewis (Dec 02 2020 at 23:39):

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

Rob Lewis (Dec 02 2020 at 23:40):

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

Mario Carneiro (Dec 02 2020 at 23:41):

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

Rob Lewis (Dec 02 2020 at 23:41):

Oh, wait, sorry

Rob Lewis (Dec 02 2020 at 23:41):

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

Mario Carneiro (Dec 02 2020 at 23:41):

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 (Dec 02 2020 at 23:42):

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 (Dec 02 2020 at 23:43):

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 (Dec 02 2020 at 23:43):

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

Mario Carneiro (Dec 02 2020 at 23:43):

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

Mario Carneiro (Dec 02 2020 at 23:44):

it's much more common than simp {config}

Rob Lewis (Dec 02 2020 at 23:45):

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

Mario Carneiro (Dec 02 2020 at 23:45):

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

Mario Carneiro (Dec 02 2020 at 23:48):

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 (Dec 02 2020 at 23:49):

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 (Dec 02 2020 at 23:52):

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 (Dec 02 2020 at 23:53):

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

Mario Carneiro (Dec 03 2020 at 00:57):

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 (Dec 03 2020 at 00:58):

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 (Dec 03 2020 at 01:08):

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 (Dec 03 2020 at 08:32):

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


Last updated: Dec 20 2023 at 11:08 UTC