by_cases and hygiene

Stream: mathlib4

[Kevin Buzzard]

I'm just updating all the tactic documentation in my course to Lean 4, and spotted this (something which is no doubt well-known): if h : P ∧ Q then cases h gives me inaccessible names left✝: P and right✝: Q, which as far as I know is expected behaviour and encourages users to supply names (which presumably leads to easier-to-maintain code). But by_cases P just gives me h: P in one goal and h: ¬P in the other (and makes any other hypothesis called h inaccessible). I thought we were moving away from this kind of behaviour. Is this just a case of an early tactic when we were more concerned with getting the port going than worrying about stuff like this? I want to tell my students "if you don't name hypotheses then don't expect to be able to use them explicitly later" and by_cases is a counterexample.

[Richard Copley]

(You probably already know there is also by_cases hP : P.)

[Kevin Buzzard]

Right, it's just that I'm having a hard time explaining why my students should use it!

[Adam Topaz]

Just make an example with some hypothesis named h which will become inaccessible if you use by_cases without an explicit name. I don’t know what the answer is but my guess is that the tactic was ported more or less directly from lean3 without regard for hygiene

[Adam Topaz]

Does by_contra have a similar behaviour?

[Alex J. Best]

Huh I thought the point of #8542 was that it fixed this, @Ruben Van de Velde ?

[Ruben Van de Velde]

That was certainly the goal, yeah

[Yaël Dillies]

Yes, this behavior should have changed, Kevin. Are you sure you're on the latest version?

[Kevin Buzzard]

Oh! I'm on "random mathlib from when I set up my course repo" and I couldn't upgrade because of the cache issue :-/

[Yaël Dillies]

Tough luck :(

[Mario Carneiro]

You know, it really doesn't take that long to compile enough of mathlib to make <project of interest> work, usually in the range 30 min - 1 hour

[Mario Carneiro]

sure it sucks but it's no reason to give up doing anything

[Kevin Buzzard]

I don't want to upgrade mathlib on my project because if there's a chance that it's not fixed by Monday then I'm in real trouble.

[Mario Carneiro]

Right now there is no difference between old mathlib and new mathlib in terms of cache effectiveness

[Mario Carneiro]

today they both fail, tomorrow (or whenever this is fixed) they both work

[Mario Carneiro]

if it's not fixed by monday you should precompile mathlib and put it in a zip file and send it to your students

[Ruben Van de Velde]

Kevin, this only works for you right now because for already have a cache on your own computer

[Kevin Buzzard]

I know all of this, and that's why I'm changing nothing right now. I am not going to be telling a class of students to download and unpack some zip file, unfortunately; that is way too high a bar for the kind of people I have to deal with. I am however confident that things will be fixed before Monday :-) I know this community too well.