lean4

lean4 copied to clipboard

In Lean 3 we had by have : stmt := proof; exact term which added stmt to the local context without leaving any trace behind. In Lean 4 have always generates a let_fun (both the term and tactic versions). This causes two problems. 1) It makes the theorem statements and goals harder to read because you see a large term. 2) Some metaprograms are confused by the extra "junk", e.g. rw fails to apply .

opaque f : Nat → True → Nat
axiom one : (have : True := (by simp); f 0 this) = 1
#check @one -- shows big term
example : f 0 ⟨⟩ = 1 := by simp only [one]
example : f 0 ⟨⟩ = 1 := by rw [one] -- fails (but should work)
example : f 0 ⟨⟩ = 1 ∧ True := by rw [← one] -- shows big term

theorem two (a b : Nat) :
    (let _ := Classical.propDecidable (a = b); if a = b then 0 else 1) =
      if a = b then 0 else 1 := by
  apply ite_congr <;> simp
-- same issues with local instances

(For local instances you usually want a let so that the instance reduces in the body.)

Expected: some nice syntax that allows declaration of local instances and proofs, but which elaborates to nothing.

Versions

July 17

Just mentioning this here because it came up on zulip. We could probably just resurrect the haveI and letI syntax in mathlib. Except that I is now short for "inline" instead of "instance". That is haveI := proof; term and letI : tc := inst; term elaborate term with an extra declaration in the local context, but then substitute it away instead of adding a (let_)fun.

In Lean 3 we had by have : stmt := proof; exact term which added stmt to the local context without leaving any trace behind.

We had users complaining that let and haves were vanishing, and we fixed it. It seems some users would complain if we eagerly inline the haves.

1. It makes the theorem statements and goals harder to read because you see a large term.

Is this a big problem? The user can clean the goal using dsimp or simp if they want. They may also decide to keep the have/let_fun.

2. Some metaprograms are confused by the extra "junk", e.g. rw fails to apply .

I think this should be viewed as a bug in these metaprograms, and we should fix it.

Just mentioning this here because it came up on zulip.

Thanks for documenting the issue here.

We could probably just resurrect the haveI and letI syntax in mathlib

I would try to fix the metaprograms first, and try to avoid haveI and letI.

-- same issues with local instances

For local instances, it seems it is defensible to inline eagerly since it is like a hint. Not sure.

-- same issues with local instances

For local instances, it seems it is defensible to inline eagerly since it is like a hint. Not sure.

@gebner What about this modification? I think it is a good one.

We had users complaining that let and haves were vanishing, and we fixed it. It seems some users would complain if we eagerly inline the haves. For local instances, it seems it is defensible to inline eagerly since it is like a hint. Not sure.

I think it is good to be consistent. Inlining some lets only is probably a recipe for confusion. (Also the question is when the inlining happens: we might only learn the type of the let after processing some postponed terms.)

Is this a big problem? The user can clean the goal using dsimp or simp if they want.

They are certainly undesirable in the sense that they make the goal harder to read. We don't want to see type ascriptions, open statements etc. in the goal either. Cleaning up with dsimp is a solution, but it shifts the burden to the user of the lemma. That is, if you use have in the theorem statement of foo, users will always dsimp after rw [foo].

They may also decide to keep the have/let_fun.

This is a similar issue as with the letification approach we discussed recently: some lets are intentional and you want to keep them (e.g. because they make the goal smaller and easier to read). Other lets are (such as the ones I'm talking about here) are only there for technical reasons where you needed to help the elaborator. Cleaning up only some of the lets is challenging.

I don't think there's anything we should or need to do about this in core at this moment. The haveI/letI syntax is trivial to implement in mathlib, and does exactly what it did in Lean 3 (great for porting!). We can revisit this when we have more experience. Putting a half-baked experimental solution in core doesn't help anyone at this point.