goals accomplished, but tactic failed

Stream: general

[Stuart Presnell]

In the following #mwe, when I put the cursor at the end of the simp line I get goals accomplished in the Info View window, but I also get a red underline on end with the error tactic failed, result contains meta-variables. How is this proof both succeeding and failing?

import data.nat.factorization

open_locale big_operators

example (n : ℕ) : (∏ (p : ℕ) in n.factors.to_finset, p) ∣ n :=
begin
  rcases (decidable.eq_or_ne n 0) with rfl | hn0, { simp },
  convert multiset.to_finset_prod_dvd_prod,
  simp [nat.prod_factors hn0.bot_lt],
end

[Eric Rodriguez]

Does this happen if yoh turn it into a lemma?

[Stuart Presnell]

Yes it does

[Alex J. Best]

Tactics can modify the tactic state arbitrarily and so if they have bugs situations like this can occur. The kernel always has the final day on whether a proof is ok or not, so what you are seeing is a tactic thinking it took care of everything but the kernel saying some part of the proof is still missing. You can use the tactic recover to make goals for the metavariables. But if indeed this is a tactic bug it's probably worth minimizing and reporting

[Stuart Presnell]

Thanks. Appending recover reveals that what's missing is decidable_eq ℕ, which I guess was a goal generated by convert multiset.to_finset_prod_dvd_prod?

[Stuart Presnell]

On the way to minimising this, the following produces the same error, while changing convert to exact closes the goal with no problem.

import data.nat.factorization

open_locale big_operators

lemma test (L : list ℕ) : L.to_finset.prod id ∣ (L : multiset ℕ).prod :=
begin
  convert multiset.to_finset_prod_dvd_prod,
end

[Stuart Presnell]

Just to note that multiset.to_finset_prod_dvd_prod is something I added in #11693 that was merged yesterday. Is there any way this could be a problem that I've introduced, or is it purely a bug in convert that I've just turned up by chance?

[Eric Rodriguez]

no, definitely a bug in convert

[Eric Rodriguez]

or maybe in tactic.congr', actually

[Eric Rodriguez]

I think the middle line is the only thing that could go wrong:

  gs ← get_goals,
  set_goals [v],
  try (tactic.congr' n),
  gs' ← get_goals,
  set_goals $ gs' ++ gs

(lines 189-193 of congr.lean)

[Eric Rodriguez]

I'm going to try figure this out

[Eric Rodriguez]

also today I learned that convert supports ← to say that you want the equalities the other way round

[Eric Rodriguez]

if you want a solution, convert ... using 0 should fix it

[Eric Rodriguez]

I'm really not sure why but there you are

[Yaël Dillies]

I usually just fiddle the tactics until it works.

[Eric Rodriguez]

metaprogramming thread about this: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/.60convert.60.3A.20why.20does.20it.20use.20.60reflexivity.20transparency.2Enone.60.3F

[Stuart Presnell]

Huh, I didn't know about convert ... using ..., which isn't in the documentation for convert. What exactly does it do?

[Ruben Van de Velde]

"Don't go so deep"

[Eric Rodriguez]

convert seems to me (by a rough reading) to basically basically be "make the prop target = goal and try use congr to prove it". using controls the deepness of that congr

[Kyle Miller]

Stuart Presnell said:

convert ... using ..., which isn't in the documentation for convert

It's hidden in the last two sentences of tactic#convert

[Kyle Miller]

It would be nice if the tactic documentation would have the full syntax of each tactic -- this could be automatically generated from the type of an interactive tactic, right?

[Stuart Presnell]

Oh, so it is!

[Mario Carneiro]

import tactic.basic

open tactic
#eval do
  let name := `convert,
  (args, _) ← infer_type (expr.const (`tactic.interactive ++ name) []) >>= open_pis,
  fs ← args.mmap (λ arg, infer_type arg >>= interactive.param_desc),
  trace $ format.join (to_fmt name :: fs.map (λ f, " " ++ f))
-- convert ← expr (using n)?

[Mario Carneiro]

that is roughly what the C++ code is doing to show you the tactic description in the hover

[Stuart Presnell]

Eric Rodriguez said:

I'm going to try figure this out

Were you able to make any progress on tracking down this bug?

(Meanwhile I've found an alternative proof that doesn't use convert, but I'm still curious about what was going on here.)

[Eric Rodriguez]

It's to do with the reflexivity check in convert, but I'm still not too sure why...