Suggest tactic bug ?

Stream: general

[Alice Laroche]

I have this MWE :

import data.finset

open finset

example (S : Type) (s : S) (a b : finset S) (h₁ : s ∉ a) (h₂ : b ⊆ a) : s ∉ b :=
begin
  suggest,
end

Suggest give three exact for this :

exact mt (h₂ s) h₁
exact not.imp h₁ (h₂ s)
exact not_imp_not.mpr (h₂ s) h₁

Problem no one work, they are all type mismatch

[Eric Wieser]

(h₂ s) should be h₂ in all of those

[Eric Wieser]

I'm guessing suggest is confused by the {{}} binders

[Alice Laroche]

That what i thought too, but it doesn't work neither

[Scott Morrison]

Unfortunately this is just a general class of "the pretty printer doesn't always round trip" deficiencies in Lean3. No one is going to do anything about this, but things look to be much better in Lean4.

[Scott Morrison]

There's nothing in suggest per se that could be changed to ameliorate this.

[Alice Laroche]

Meeeh.

[Scott Morrison]

The output of suggest is still useful: you can't just copy-paste, but it does tell you that those functions really can close the goal --- you're just going to have to work out the syntax yourself. :-)

[Scott Morrison]

They are not spurious results --- suggest really did find a term that solves the goal, it just printed badly.

[Floris van Doorn]

In this case you can replace (h₂ s) by (@h₂ s)