Zulip Chat Archive

Stream: general

Topic: Come on


view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Feb 14 2021 at 09:25):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Feb 14 2021 at 12:55):

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

view this post on Zulip Ruben Van de Velde (Feb 14 2021 at 13:03):

"Let's assume that..."

view this post on Zulip Kevin Buzzard (Feb 14 2021 at 13:11):

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

view this post on Zulip 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).

view this post on Zulip 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 :-/

view this post on Zulip 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