batteries
batteries copied to clipboard
leanprover-community
refactor: avoid relying on rfl's behavior on ground terms
rfl for ground terms will reduce at transparency .all, even if the current transparency is .default. Maybe it's prudent to not rely on this corner case, and have more explicit proofs.
I understand where this is coming from but I'm skeptical of simp as a replacement since that is a much more complex tactic. Maybe we need an enhanced rfl-like tactic that doesn't draw in all the simp lemmas?
I guess I mean a tactic that would locally unseal some defs but not use simp lemmas. Maybe it could even try to figure out what defs to unseal without user prompt.
Yes, this PR is a mit premature, I should first figure out if this rfl behavior is intended or accidental.
Using simp isn't unreasonable in the sense that the other half of that proof is also rewriting. But I am more hesitant to rely on DefEqs of irreducible definitions than others :-)
Marking as draft for now.
I don't think these two changes are problematic by themselves. I'm mostly questioning the general strategy of replacing rfl by simp, especially now that defs by wf are irreducible by default. It seems to me that rfl is the wrong tool for reasons you mention but simp is also the wrong tool for different reasons. These are the tools we currently have and the "right tool" appears to be missing, probably because there was not much need before now.
To be more specific about my (currently purely theoretical) vision is for an eqn tactic that attempts to prove an equality using "defining equations". In most cases, these "defining equations" would simply be the actual definition (i.e. what rfl does) but in the case of irreducible defs, these would be more like specifications which have more to do with the intended meaning than the actual implementation.
Note that the equations used by eqn are not always simp lemmas. In fact, some would be really bad simp lemmas. But eqn is cannot be used to simplify a goal, so that is not a problem. In a sense, eqn would be orthogonal to simp, using overlapping but ultimately completely different set of rules.
Anyway, this discussion should probably be elsewhere.
Ah, I see what you are getting at: An evaluator of ground terms that uses the equations as specified, but not necessarily as elaborated (which suffers at least for well-founded definitions).
A good approximation to that is rw [foo] or simp [foo] where foo is the function name, what's missing doing that for any function, and not applying other simp rules, I guess.
I’m working on https://github.com/leanprover/lean4/pull/3772 again, so I expect his will be needed soon. I’d wager that simp [last] is reasonable style, at least with the idioms and tactics with have.
I still don't think simp is the right choice as a general replacement for rfl here since it doesn't have the same behavior as rfl at all. How about having rfl [foo, bar] that locally changes the reducibility of foo and bar before rfl?