Implis, Level 13: explain why 'by_cases a : A' does not work

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪

https://adam.math.hhu.de

Apache License 2.0

16 stars 9 forks source link

Implis, Level 13: explain why 'by_cases a : A' does not work #20

Closed TentativeConvert closed 4 months ago

TentativeConvert commented 4 months ago

Add branches with these commands, and add hints to these branches.

After 'intro a', there's already an assumption called a, so using a in by_cases a : A will rename the existing assumption in an inaccessible way.
Using by cases A will likewise produce inaccesible assumption.

joneugster commented 4 months ago

first point is currently not possible. Hint does not care if variables/hypothesis are accessible or not. (although, I guess I could look into implementing such a feature if desired.)
second point is IMO a bug in Lean and I'll file an issue/PR about by_cases ignoring set_option tactic.hygienic false. (Zulip)

TentativeConvert commented 4 months ago

Ah, I forgot that branches catch different proof states and not different commands/tactics.

But two students made a mistake in this step, out of a very small sample size. So at least there should be a hint saying not to use by_cases a : A after intro a. OR, perhaps there should be some explanation earlier about naming assumptions and possible pitfalls.

joneugster commented 4 months ago

I added a fixed by_cases tactic to the game that deals with both cases:

if a already exists, by_cases a : A will create a Hypothesis a_1 : A.
by cases A will create a hyp h : A (or h_1 : A if h already exists.)

I'm trying to get this upstreamed, but since by_cases is now in Core Lean, PR's might not be as welcome as in Mathlib/Std.

(but even if we keep the modified tactic in the game, besides better naming, it should be the same as the original one, so that should be no issue to the player)