using `←` inside a list of `pexpr`

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

while working on a tactic sort_summands (#13483) to reorder sums, Arthur Paulino and I would like to use ← as an optional identifier for whether to move a term to the left of to the right.

Thus, I would like something like

example {f g h : ℕ} : f + g + h = 0 :=
begin
  sort_summands g,  -- works, and the goal changes to `f + h + g = 0`
  sort_summands [← g],  -- currently does not work,
  -- we would like it to mean that the goal changes to `g + f + h`
end

[Damiano Testa]

Is it possible to get Lean to accept the extra token ← and then do a case split, depending on whether it is present or not?

I wanted something similar to how simp [lemma] and simp [-lemma] work, except using - does not really work, since there might be a - in the pexpr in this context.

[Arthur Paulino]

An important remark is that we're using parse pexpr_list_or_texpr? so that's not a list of identifiers like we usually see with simp [⋯] or rw [⋯]

[Kyle Miller]

Have you taken a look at the source for docs#tactic.simp_arg_list or docs#tactic.interactive.rw_rules? You could use these as inspiration to make your own tactic.sort_summands_arg_list.

[Arthur Paulino]

We found those and Damiano started to investigate it. I don't know what he was able to achieve tho

[Damiano Testa]

Honestly, I tried, but am somewhat overwhelmed by parser and rules...

[Mario Carneiro]

import tactic.core
setup_tactic_parser

meta def opt_list_of {α : Type} (p : parser α) : parser (list α) :=
list_of p <|> list.ret <$> p <|> return []

meta def sort_summands_arg (prec : nat) : parser (bool × pexpr) :=
(do tk "<-", e ← parser.pexpr prec, return (tt, e)) <|>
(do e ← parser.pexpr prec, return (ff, e))

meta def tactic.interactive.foo
  (args : parse (
    list_of (sort_summands_arg 0) <|>
    list.ret <$> (sort_summands_arg tac_rbp) <|>
    return [])) : tactic unit :=
tactic.trace args

example : true := begin
  foo [a, ← b],
  foo ← b,
  foo ← b <|> skip,
  foo,
end

[Damiano Testa]

Mario, thank you so much! I think that I can take it from here.

[Damiano Testa]

I only have one problem: my computer seems to have to work a lot on the file that only contains your code and Lean breaks as soon as I change anything...

[Damiano Testa]

In fact, even if I do not touch anything at all, after some noise from the computer, Lean says

Error updating: excessive memory consumption detected at 'whnf'
(potential solution: increase memory consumption threshold).Try again.
No info found.

[Damiano Testa]

Sorry for the noise: I had some issues with my oleans. Everything is fast now!

[Damiano Testa]

What is the significance of prec : nat?

[Kyle Miller]

It's for setting the parsing precedence (also known as binding power for a Pratt parser) for parser.pexpr. When you're parsing something inside a list, it's in a precedence-0 context, but when you're not parsing inside a list, you need to respect the precedence for arguments to a tactic -- that precedence is given by tac_rbp (tactic right binding power). By giving parser.pexpr higher binding power, it will be less greedy in how far it will parse, and in particular it won't parse past a token of higher left binding power I believe.

[Damiano Testa]

Kyle, thank you very much for the explanation! It makes more sense now!

[Kyle Miller]

If you take a look at the source for pexpr_list_or_texpr, you can see that Mario's code is sort of swapping out parser.pexpr for sort_summands_arg, which is a wrapper around parser.pexpr to optionally parse the <-. All the binding powers are the same.

[Eric Wieser]

As another notation suggestion, sort_summands [.., g] vs sort_summands [g, ..], might be a nice notation for "sort to start" vs "sort to end"

[Eric Wieser]

Or even sort_summands g + _, vs sort_summands _ + g, but maybe that's trying to be too clever

[Damiano Testa]

Eric, in your first suggestion you mean that .., is part of what gets consumed by the parser? I would like to be able to give simultaneously conditions on which terms go to the left and which ones go to the right, so maybe something like

sort_summands [g1,...,gn <some_separator> h1,...,hm]

though I think that I prefer the arrow, since it is very used in mathlib and clearly tells you where the term goes.

Also, I like the fact that you do not need to input the terms in a sorted list: you can add each term and decide for each term whether it goes left or right.

[Damiano Testa]

Kyle, it is indeed much clearer now! I had been staring at those definitions for quite some time, but there was too much extra noise and unknowns for me, that I could not find my way around them. Now it is all starting to lock into place!

[Eric Wieser]

Under my suggested spelling that would be:

sort_summands [g1,h1,...,gn,hn]  -- goal changes to `g1 + h1 + _ + gn + hn`

[Eric Wieser]

though I think that I prefer the arrow, since it is very used in mathlib and clearly tells you where the term goes.

It's not that clear to me; what does [a, b, ← c, ← d] mean? Does c end up right of d or left of d?

[Damiano Testa]

Oh, [a, b, ← c, ← d] for me means to the left there are [c, d] and to the right [a, b].

[Damiano Testa]

I view the arrow as attached to each term and, if present, it tells you that the term goes all the way to the left.

[Damiano Testa]

So, the default behaviour is that an explicitly given term moves to the right. You can change this by using the arrow.

[Damiano Testa]

I like your suggestion as well. Now that I feel bold with the use of the parser, I may even go as far as saying that I can implement both! :wink:

[Damiano Testa]

I am stuck between expr and pexpr, which I really do not understand. Is there a way to convert a pexpr to an expr?

The reason is that the code for sort_summands works with exprs, but what Mario gave me uses pexprs. I tried changing Mario's pexprs to exprs, but parser.pexpr prec at the end of sort_summands_arg gets in the way...

[Damiano Testa]

If I simply try to convert a pe : pexpr to an expr I get the unpleasant goal tt = ff. :upside_down:

[Yakov Pechersky]

docs#tactic.to_expr

[Damiano Testa]

This seems to produce a tactic expr, whereas I seem to want an actual expr...

[Damiano Testa]

(I am very aware that I probably took a wrong turn somewhere, so what you are suggesting may also be a solution. I am just unable to use it.)

[Arthur Paulino]

It produces an expr but it runs in the tactic monad

[Damiano Testa]

Arthur, does this mean that I can use it or that I cannot use it?

[Yakov Pechersky]

Do you have a list of pexpr? Then you can run list.mmap tactic.to_expr to get tactic (list pexpr). Damiano, are you inside do notation?

[Damiano Testa]

I am inside do notation, yes.

[Arthur Paulino]

You can use it, but you just need to use the right syntax and functions for monadic computation. Can you point to the code?

[Yakov Pechersky]

Basically, my_expr <- to_expr my_pexpr

[Yakov Pechersky]

Instead of walrus assignment :=

[Damiano Testa]

currently, my code is in a messy state. However, I am trying to use what Mario gave me (which uses pexprs), to what we had (which uses pexprs). I'll try with Yakov's mmap and otherwise I'll see if I can write a #we, if not an actual #mwe!

[Arthur Paulino]

This is how I coded the conversion from a list of pexpr to a list of expr:

l : list expr ← (l.get_or_else []).mmap to_expr

[Damiano Testa]

Ok, this is promising. I have a pair of lists of pexprs that I want to convert into a pair of lists of exprs. I can probably do it, but if someone has a quick way of solving this, I'd be grateful!

[Damiano Testa]

here is my state:

args: parse interactive.sort_pexpr_list_or_texpr
locat: parse location
sort_summands: tactic unit
ll: list pexpr × list pexpr
_match: parse location → tactic unit
⊢ list expr × list expr

[Damiano Testa]

I want ll to merge with the goal.

[Arthur Paulino]

do
  a ← ll.1.mmap to_expr,
  b ← ll.2.mmap to_expr,
  (a, b)

[Arthur Paulino]

(untested)

[Damiano Testa]

I think that it might have worked! At least I progressed with the conversion a few extra lines!

Thank you so much!