## Stream: general

### Topic: Come on

#### Sebastien Gouezel (Feb 14 2021 at 09:21):

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 (Feb 14 2021 at 09:25):

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

#### Yury G. Kudryashov (Feb 14 2021 at 11:14):

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

#### Kevin Buzzard (Feb 14 2021 at 12:07):

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 (Feb 14 2021 at 12:55):

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

#### Ruben Van de Velde (Feb 14 2021 at 13:03):

"Let's assume that..."

#### Kevin Buzzard (Feb 14 2021 at 13:11):

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

#### Sebastian Ullrich (Feb 14 2021 at 14:35):

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 (Feb 14 2021 at 15:00):

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

#### Yakov Pechersky (Feb 14 2021 at 15:30):

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


Last updated: May 18 2021 at 17:44 UTC