squeeze_simp - match failed?!

Stream: metaprogramming / tactics

[Eric Rodriguez]

yeah, would much appreciate that. i'm currently really tempted to literally turn names into expr.const ffs which feels outstandingly wrong

[Eric Rodriguez]

hmm, so okay, if you write squeeze_simp [_root_.asda, int.asda] (using my MWE from above), you get that the simp_arg_list has exprs with the constructor local_const int.asda int.asda (...). So I tried replacing the resolve_name' in name.to_simp_args with get_local, but now there isn't a int.asda local; which makes sense, I guess, but then how did those original exprs appear?

[Arthur Paulino]

I just found the time to sit with the problem. First, just to check if we have the same ideas, how do you expect the tactic to react in this scenario?

Also, can a mod move this thread to #metaprogramming / tactics ?

[Eric Rodriguez]

hmm, it seems that in the simp_arg_list they are pexprs, but if I use get_local I have no choice but to get exprs. Is there any way to get pexprs?

[Eric Rodriguez]

I didn't know that was a stream!

[Eric Rodriguez]

The hope is that if you squeeze_simp when you have something like int.asda, _root_.asda in the used simpset, squeeze_simp doesn't just crash completely. currently I've got a semi-working thing that doesn't crash, but prints try this: simp only [asda, asda] so you have to guess namespaces

[Eric Rodriguez]

this also seems to work, but seems similarly wrong:

meta def name.to_simp_args (n : name) : tactic simp_arg_type :=
let h := @expr.local_const ff n n (default) (expr.var 1) in
do trace $ to_raw_fmt' h, return $ simp_arg_type.expr h

(ignore all the debugging stuff)

[Arthur Paulino]

But we're expecting it so say Try this: simp only [int.asda, asda, and_self], right?

[Arthur Paulino]

(even after open int)

[Eric Rodriguez]

yes, with a _root_ on the second asda because otherwise we'd get an overload resolution error

[Eric Rodriguez]

but honestly as long as it works, it's better than "match failed"

[Arthur Paulino]

I think name.to_simp_args will need more information

[Eric Rodriguez]

doesn't it have the tactic state by virtue of being a tactic monad?

[Arthur Paulino]

Right

[Arthur Paulino]

Eric Rodriguez said:

The hope is that if you squeeze_simp when you have something like int.asda, _root_.asda in the used simpset, squeeze_simp doesn't just crash completely. currently I've got a semi-working thing that doesn't crash, but prints try this: simp only [asda, asda] so you have to guess namespaces

How did you accomplish this?

[Eric Rodriguez]

you can see in my branch right now, but I just hand-craft the pexpr

[Arthur Paulino]

Oops, I forgot to change branches (I was on master :face_palm: )

[Arthur Paulino]

Alright, this is a good step. Now we need to do something about duplicated occurrences

[Arthur Paulino]

Actually I think this is the best approach:

a resolve_name' that will keep in the _root_

[Eric Rodriguez]

resolve_name is c++, is the issue

[Eric Rodriguez]

honestly, maybe my latest approach with declaring them as a local_const ff is the right approach; that's how they're going to be read in the context, and if they don't work as a local_const ff then they just won't work at all

[Eric Rodriguez]

maybe the only thing missing is to also add prepend_root_if_needed to the tactic format name

[Arthur Paulino]

yeah I was trying to write a resolve_name'' that incorporates prepend_root_if_needed

[Arthur Paulino]

and drop this line from squeeze_simp_core:

vs ← vs.mmap prepend_root_if_needed,

[Arthur Paulino]

@Eric Rodriguez maybe we can have more control this way?

meta def name.to_simp_args' (n : name) : tactic simp_arg_type :=
do x ← resolve_name' n,
return $ match x with
  | expr.macro m l := -- m and l might add in some useful info?
    -- simp_arg_type.expr $ pexpr.mk_field_macro (@expr.const ff n []) `_root
    -- simp_arg_type.expr (@expr.macro ff m ([`_root_, n].map (λ n', to_pexpr $ mk_local n')))
    simp_arg_type.expr (@expr.const ff (`_root_ ++ n) [])
  | _ :=
    simp_arg_type.expr (@expr.const ff n [])
  end

[Eric Rodriguez]

ooh, maybe this is the right way. maybe we can make it a function that is resolve_name' usually, but in the case of an overload it just prepends _root_?

[Arthur Paulino]

oof, I'm stuck

[Eric Rodriguez]

what's the issue?

[Arthur Paulino]

Okay, this approach won't help.
When tracing (@expr.const ff (_root_ ++ n) [])` it prints:

_root_.int.asda
_root_.asda
_root_.and_self

Each of those is the consumed by simp_arg_type.expr : pexpr → simp_arg_type
Then, right after that, when tracing the results, it says:

[asda, asda, and_self]

So I believe something is happening inside simp_arg_type.expr that's getting rid of _root_ without mercy

[Arthur Paulino]

I'm resetting my branch to the state where you left it at

[Eric Rodriguez]

that's just the pretty printer

[Arthur Paulino]

Hm

[Eric Rodriguez]

if you change the has_to_string instance to use to_raw_fmt, you'll see that it's still the right place

[Eric Rodriguez]

we do need to fight it at the end, but again I think even just getting asda, asda is an improvement over a crash

[Eric Rodriguez]

especially because at that point Lean will throw all the possible overloads at you and you can start to figure it out

[Eric Rodriguez]

it'd be nice to not have to do that but the pp works in mysterious ways

[Arthur Paulino]

Maybe simp_arg_type needs something like dotted_expr?

[Eric Rodriguez]

the issue isn't simp_arg_type, it's expr's to_string

[Arthur Paulino]

but how would we indicate that to_string is not supposed to strip _root_?

[Eric Rodriguez]

make a custom to_string, I think

[Arthur Paulino]

In C?

[Arthur Paulino]

What if prepend_root_if_needed returns tactic (name × bool) indicating which ones needed the prepend?

[Eric Rodriguez]

i was thinking that and think it's a good idea

[Eric Rodriguez]

I was hoping we could swap the pp in mk_suggestion for a different method so we don't have to worry about this

[Eric Rodriguez]

but >>= is not one of the two monadic operators I know

[Arthur Paulino]

I'm gonna brb, please let me know if this works

[Eric Rodriguez]

image.png hmm, I think you're right that we just need to keep track of root independently

[Eric Rodriguez]

I think the fix can be two-fold - keep track of _root_ independently, and use to_string instead of pp

[Eric Rodriguez]

i'll try this in a little bit and see what happens

[Arthur Paulino]

Use to_string then the bool returns true, right? Otherwise use pp

[Eric Rodriguez]

no, pp also cuts off the int. (presumably because it's open)

[Arthur Paulino]

Ah, right

[Arthur Paulino]

Wait, I think it worked?
image.png

[Eric Rodriguez]

omg! this is great news! what did you end up doing?

[Arthur Paulino]

This is weird, I didn't do anything different from https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/squeeze_simp.20-.20match.20failed.3F!/near/269490059

[Eric Rodriguez]

ooh, I changed the to_string to to_raw_fmt for debugging

[Eric Rodriguez]

I should've checked it without that!!

[Arthur Paulino]

wanna push? you solved it haha

[Eric Rodriguez]

no dw you were a massive help^^ I've got another branch open right now, too, so it'd be a massive pain ;b

[Arthur Paulino]

This is the exact git diff:

$ git diff
diff --git a/src/tactic/squeeze.lean b/src/tactic/squeeze.lean
index 20bad3d651..fa4bf57038 100644
--- a/src/tactic/squeeze.lean
+++ b/src/tactic/squeeze.lean
@@ -80,7 +80,7 @@ run_cmd squeeze_loc_attr.set ``squeeze_loc_attr_carrier none tt
 list entirely if it is empty. -/
 meta def render_simp_arg_list : list simp_arg_type → tactic format
 | [] := pure ""
-| args := (++) " " <$> to_line_wrap_format <$> args.mmap pp
+| args := (++) " " <$> to_line_wrap_format <$> pure (args.map to_string)

 /-- Emit a suggestion to the user. If inside a `squeeze_scope` block,
 the suggestions emitted through `mk_suggestion` will be aggregated so that

:joy:

[Arthur Paulino]

Just that

[Arthur Paulino]

I am also going to document why pp was problematic in the docstring of render_simp_arg_list

[Kevin Buzzard]

Wanna try #3097 next?

[Eric Rodriguez]

oh, christ, I always assumed simp lemmas were order independent... i'll have a dig. also huge thanks to Rob for the metaprogramming in Lean stuff, I would've never gotten my head around this without him

[Arthur Paulino]

Makes sense?

Patch: pp was changed to to_string because it was getting rid of prefixes
that would be necessary for some disambiguations.

[Alex J. Best]

For #3097 maybe squeeze simp could just check its output works (either in the sense of not failing or in the sense of giving the same result as the original simp call), seeing as this should be a simp only it may well be fast enough, and otherwise apply a random permutation and try again.

[Eric Rodriguez]

ahh, bogosort ;b

[Arthur Paulino]

#11659 should be ready for review already :octopus:

[Eric Rodriguez]

@Kevin Buzzard, do you know if the issue can happen with non-rfl lemmas?

[Eric Rodriguez]

it may be a bit easier to debug it that way

[Arthur Paulino]

If we want squeeze_simp to try harder, maybe we can't do much better than trying every permutation?

[Arthur Paulino]

I think we could continue the conversation about the other issue here and ask a mod to move that thread to this stream as well

[Kevin Buzzard]

I don't know anything, I just keep track of times when squeeze_simp fails because this causes problems for my students!

[Arthur Paulino]

The fix is ready for review #11696
@Rob Lewis can you also take a look at this one? :pray:

[Rob Lewis]

I'll find time later today!

[Julian Berman]

OT: Arthur you are quite inspiring :)