squeeze_simp - match failed?!

Stream: general

[Eric Rodriguez]

I guess this is because my current proof is "evil" and uses cast and such like, but see here in FLT-regular. I'm not attached enough to make a MWE; but this is mildly annoying. simp? reports a lemma which, when I actually try to put into the simp only, is reported as an invalid simplification lemma.

[Eric Rodriguez]

ok, this came up again, this time in a more pressing need; I tried to replace one of the conv blocks in file#ring_theory/polynomial/bernstein (line 338) with:

debug stuff

  replace h : ∑ i in finset.range (n + 1), ↑i * bernstein_polynomial R n i =
  (mv_polynomial.aeval e) ((pderiv tt) $ (x + y) ^ n) * X,
  begin
    rw [add_pow, (pderiv tt).map_sum, (mv_polynomial.aeval e).map_sum, finset.sum_mul],
    congr,
    simp [pderiv_mul, pderiv_tt_x, pderiv_tt_y, e, w],
  end,

but squeeze_simp again fails with the same error on this

[Eric Rodriguez]

non-squeezed simps in convs can die :(

[Johan Commelin]

I'm really sorry that simp? is so unreliable. I tried my best when implementing it in the C++, but I was very much out of my comfort zone. I don't know how to improve it.

[Eric Rodriguez]

Still definitely beats trying to figure it out from show_term!

[Ruben Van de Velde]

simp? is great, imo. I just wish it preserved at h

[Eric Rodriguez]

I've figured it out! Woop! It's to do with namespacing:

import tactic.squeeze

@[simp] lemma asda {a : ℕ} : 0 ≤ a := sorry

@[simp] lemma int.asda {a : ℤ} : 0 ≤ a := sorry

--open int

lemma tes {a : ℕ} {b : ℤ} : 0 ≤ a ∧ 0 ≤ b := by squeeze_simp

#print tes

Uncomment that open int, and the squeeze_simp will fail.

[Eric Rodriguez]

Should I open an issue for this?

[Eric Rodriguez]

I've never used the github issues for mathlib

[Arthur Paulino]

What happens if you rename one of the asda lemmas to asdas and then uncomment open int? (I'm not on my PC right now)
I suspect it's failing due to name ambiguity

[Eric Rodriguez]

exactly, this is the issue

[Eric Rodriguez]

i can't really rename polynomial.map_one and we have a global map_one, for instance

[Arthur Paulino]

Then simp works but squeeze_simp doesn't?

[Eric Rodriguez]

yeah

[Eric Rodriguez]

submitted as #11196

[Eric Rodriguez]

so there's been some progress on this; the reason we get match failed is on line 143 of squeeze.lean:

do some s ← get_proof_state_after (tac ff (user_args ++ simp_args)),

this essentially does simp only [some_args] in a separate tactic state, but this fails as in some_args you'll have the namespace clash and so the separate tactic state will have a namespace error

[Eric Rodriguez]

(thanks to Bhavik for discovering this). a suggested solution was to make a tactic that turns a name (e.g. map_zero) into all the possible names that it could be (so if it's unambigious, just [map_zero], else something like [_root_.map_zero, polynomial.map_zero] (I guess it should be checked that these are all simp lemmas/passed in). this can then replace each name in squeeze, and then it _should_ just work fine. however, I don't have the skills to code this :/

[Eric Rodriguez]

ok, so there's quite a bit of progress on this in #11659, but would really appreciate some meta help here. i put the below comment on GH, but copy-pasted for ease:

argh, I nearly got this to work, but I simply cannot figure out the last bit. I managed to know (well, guess) when a function is overloaded, and if it is, we prepend _root_ to its name, so that we don't get any namespace clashes. However, resolve_name' decides that it needs to strip the _root_, regardless; how do I get around this? Can I make a new resolve_name' that causes an overload on purpose so that it's forced to keep in _root_?

[Eric Rodriguez]

again, all I need is a resolve_name' that will keep in the _root_; i _think_ everything else works.

[Eric Rodriguez]

image.png ok, so if I manually write the pexprs then it does work, but render_simp_arg_list undoes some of the work and removes the namespacing

[Eric Rodriguez]

progress, I guess? would much appreciate any help

[Arthur Paulino]

@Eric Rodriguez I can try and help you tomorrow if you don't get it figured out by then :+1:

[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_

[Notification Bot]

This topic was moved by Mario Carneiro to #metaprogramming / tactics > squeeze_simp - match failed?!