have tactic footgun

Stream: lean4

[Floris van Doorn]

The have tactic is an enormous footgun for new users, since if you write have : <some type> := ... (i.e. not a proposition but data), then the value of the data is forgotten. This is especially problematic if the type is a class, since it can then be used without the user realizing.

Typical example:

example (n m : Nat) : True := by
  have h1 : n + m = m + n := Nat.add_comm n m
  have : Add Nat := inferInstance
  -- many other steps
  have : n + m = m + n := h1 -- error

This is treacherous, since the offending have can occur many lines before the error.

Suggestion: have x? : T := _ will emit a warning if T is a type . We add have! which has the current behavior of have. The warning suggests switching to either let or have!.

Alternative suggestion: only emit the warning when T is a type and a class.

[Jireh Loreaux]

I think it should warn on any type, not just classes.

[Eric Wieser]

I think if we're going to make have! the only way to silence the warning, we may as well be aggressive about when we warn

[Eric Wieser]

(we probably would need haveI! and haveI'! to match)

[Kevin Buzzard]

I see this problem year after year with my undergraduates (the most recent being this week).

[Floris van Doorn]

lean4#3559

[Floris van Doorn]

Eric Wieser said:

(we probably would need haveI! and haveI'! to match)

What is haveI'?

[Floris van Doorn]

Oh, I see that have' is like have but turns all remaining metavariables into subgoals? That sounds useful!

[Kyle Miller]

Some technical considerations for figuring out how to implement this:

The have h : T := v tactic is a macro that expands out to essentially refine let_fun h : T := v; ?_. To implement this, I suppose we need to somehow tell let_fun that T is a Prop.

One way to handle this, which probably wouldn't yield great error messages, is to have it use let_fun h : (T : Prop) := v; ?_. That makes it be an error rather than a warning though, and it doesn't give a way to suggest have!.

Another is to create some a new construct that can surface a warning if some condition on a metavariable isn't met, once there's enough information to make a judgment.

Like, maybe it would look like

assert_is_a_prop% ?m := T
  | "The `have` tactic does not preserve the value of the new local hypothesis. \
     You likely want to use `let` instead. \
     Otherwise, if this is your intent, you can use `have!`.";
let_fun h : %m := v; ?_

Then, once the body of assert_is_a_prop% is complete, it does the check and emits the warning if needed.

[Kyle Miller]

Incidentally, I wonder if we should have a parser that handles !/? variants of tactics (and now, potentially, terms), so that we can avoid needing macros for both variants. Maybe we could make it so that simp! parses so that the resulting Syntax is the same as simp !?

[Jannis Limperg]

Can't you just implement have as an elab and do the Prop check there? (I generally find macros that expand into a bunch of magic suspect.)