Come on

Stream: general

[Sebastien Gouezel]

Come on Lean :-)

type mismatch at application
  @approximates_linear_on.image_mem_nhds.{u_1 u_2 u_3} 𝕜 _inst_1 E _inst_2 _inst_3 F _inst_4 _inst_5 cs f s c f'
    f'symm
    hf
    x
    hs
term
  hs
has type
  @has_mem.mem.{u_2 u_2} (set.{u_2} E) (filter.{u_2} E) (@filter.has_mem.{u_2} E) s
    (@nhds.{u_2} E
       (@uniform_space.to_topological_space.{u_2} E
          (@metric_space.to_uniform_space'.{u_2} E (@normed_group.to_metric_space.{u_2} E _inst_2)))
       x)
but is expected to have type
  @has_mem.mem.{u_2 u_2} (set.{u_2} E) (filter.{u_2} E) (@filter.has_mem.{u_2} E) s
    (@nhds.{u_2} E
       (@uniform_space.to_topological_space.{u_2} E
          (@metric_space.to_uniform_space'.{u_2} E (@normed_group.to_metric_space.{u_2} E _inst_2)))
       x)

I'm sure I'll find a way to help Lean, but I am still amazed at how well it works like 99.9% of the time, and how sometimes it chokes for no reason I can spot.

[Sebastien Gouezel]

There were two things named s. So the stupid one here wasn't Lean ;-)

[Yury G. Kudryashov]

I think, lean (editor integration) should warn users when they have two variables with the same name in tactic context.

[Kevin Buzzard]

This occasionally catches me out too. I know there's some technical reason why it's hard to spot duplicate names but there are so many smart people here, there must be a trick. Recently I've started to try and be really principled about variable names, calling things hxS if they say x \in S rather than just h and this was partly the reason. I even try to name all variables after things like split_ifs rather than just getting a bunch of hs. I was rather proud when a student asked me in my class why they could not name a hypothesis h\notP because they even thought that lean demanded such principled choices. I think tactics like split_ifs should arguably fail if the user doesn't give variable names (I know the CS people will disagree but didn't someone say that this will be the default in lean 4?) and I'm wondering whether the system should tell us what to write here and generally try and keep us more honest with variable naming eg by checking for dupes. On a blackboard I can't just say "now introduce this nameless variable" and students and lecturers both get confused if lecturers call two things X. It should be banned!

[Eric Wieser]

But "now introduce this nameless hypothesis" is reasonably on a blackboard, right?

[Ruben Van de Velde]

"Let's assume that..."

[Kevin Buzzard]

If you're going to use it again you call it (*), right?

[Sebastian Ullrich]

Lean 4 suffixes shadowed variables with a cross:cross: to show It's Dead, Jim

I think tactics like split_ifs should arguably fail if the user doesn't give variable names (I know the CS people will disagree but didn't someone say that this will be the default in lean 4?)

By default, anonymously introduced hypotheses are inaccessible in Lean 4. They also get a cross (out of the door, line on the left).

[Kevin Buzzard]

There have been times with some tactics (rcases?) when I have been literally unable to name the variables it spits out :-/

[Yakov Pechersky]

For hypotheses spit out by things like split cases, french quotes have been useful in the cases where I don't want to worry about name tracking, or where restructuring of goals would have changed the auto-generated names anyway. So like:

/-- The second simplicial identity -/
lemma δ_comp_σ_of_le {n} {i : fin (n+2)} {j : fin (n+1)} (H : i ≤ j.cast_succ) :
  δ i.cast_succ ≫ σ j.succ = σ j ≫ δ i :=
begin
  ext k,
  dsimp [δ, σ, fin.succ_above, fin.pred_above],
  rcases i with ⟨i, _⟩,
  rcases j with ⟨j, _⟩,
  rcases k with ⟨k, _⟩,
  simp only [subtype.mk_le_mk, fin.cast_succ_mk] at H,
  simp with push_cast, -- `simp?` doesn't work here
  split_ifs,
  -- Hope for the best from `linarith`:
  all_goals { simp at *, try { linarith }, },
  -- Two of the goals need special handling:
  { have := nat.le_of_pred_lt ‹fin.cast_succ (fin.pred ⟨k, k_property⟩ _) < ⟨i, i_property⟩›,
    change k ≤ i at this,
    linarith, },
  { exact (nat.succ_pred_eq_of_pos (lt_of_le_of_lt (zero_le _) ‹j < k›)).symm, },
end