suggest and show_term give incorrect suggestions

[ghost]

Uncomment each block of code one at a time:

import data.real.basic
import data.set.basic


-- library_search fails
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   library_search
-- end

-- This passes
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   tauto,
-- end

-- Try this: exact Exists.intro (λ (a : ℝ), a = a) rfl
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   suggest
-- end

-- Try this: exact Exists.intro (λ (a : ℝ), a = a) rfl
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   show_term {tauto}
-- end

-- Using exact Exists.intro (λ (a : ℝ), a = a) rfl
-- causes type mismatch at application
-- example : ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s :=
-- begin
--   exact Exists.intro (λ (a : ℝ), a = a) rfl
-- end

The full type mismatch error message is:

type mismatch at application
  Exists.intro (λ (a : ℝ), a = a) rfl
term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  ∀ (r : ℝ), r ∈ λ (a : ℝ), a = a
state:
⊢ ∃ (s : set ℝ), ∀ (r : ℝ), r ∈ s

[shingtaklam1324]

Is this the same issue as #3093 and leanprover-community/lean#394 ?

[ghost]

@shingtaklam1324 I suspect that the causes of those issues might be the same as the cause of this issue, but this issue is nevertheless different.

[eric-wieser]

Can you include the full error message in this issue?

[alexjbest]

Apologies I posted in the wrong thread and misclicked.

[shingtaklam1324]

I think suggest and show_term are doing what is expected, but Lean is not. This is different to the issue I linked, and is more of a general "Lean's pretty printer does not round trip" issue.

Here is a mathlib free reproduction of the issue

lemma p : ∀ {a : ℕ}, a = a := @rfl nat

#print p
/-
theorem p : ∀ {a : ℕ}, a = a :=
rfl
-/

lemma q : ∀ {a : ℕ}, a = a := rfl -- doesn't work

[bryangingechen]

While this is unlikely to be fixed before we change to Lean 4, it may be worth leaving this open to serve as a reference for others who run into this issue.

Actually, I suggest we document these limitations better in our tactic docs and then we can close this issue when that's done.

[BoltonBailey]

Here is another manifestation that seems similar, with suggest and library_search! returning exacts that don't typecheck. Is this the same thing?

import data.nat.interval

open finset

example : monotone (@card (finset ℕ)) :=
begin
  -- suggest, -- Try this: exact card_le_of_subset ...
  -- library_search, -- fails
  -- library_search!, -- Try this: exact card_le_of_subset
  -- exact card_le_of_subset, -- Invalid type ascription
  exact @card_le_of_subset _, -- works
end