Zulip Chat Archive

Stream: general

Topic: Suggest tactic bug ?


Alice Laroche (Aug 20 2021 at 23:48):

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 (Aug 20 2021 at 23:55):

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

Eric Wieser (Aug 20 2021 at 23:55):

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

Alice Laroche (Aug 21 2021 at 00:04):

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

Scott Morrison (Aug 21 2021 at 00:10):

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 (Aug 21 2021 at 00:10):

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

Alice Laroche (Aug 21 2021 at 00:13):

Meeeh.

Scott Morrison (Aug 21 2021 at 00:15):

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 (Aug 21 2021 at 00:15):

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

Floris van Doorn (Aug 21 2021 at 04:55):

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


Last updated: Dec 20 2023 at 11:08 UTC