Why do we need kernel reduction

Stream: general

[Chris Hughes]

The library_search thread made me think about this question. I'm not sure exactly what the question is.

Why should we resort to adding an axiom for structural eta, when it's already provable.

Definitional reduction could also I guess in principle be a tactic that applied all the reduction rules and produced a proof term containing the reduction steps.

Is it inevitable that tactics and interface can never be as good as a definitional reduction rule? When you rely on definitional reduction, you're forced to stay somewhat close to the axioms. It feels like a major limitation to me that for example we need both option and roption just for slightly different definitional equality properties. There are plenty of things that I want to treat like the same thing but will never be axioms. Can they ever be as good as axioms?

[Johan Commelin]

The major benefit of defeq is that it is invisible. Hence it allows you to write short code, which is often more readable. Wednesday I gave a Lean talk in front of an audience of pure mathematicians that had never seen Lean before. They thought it was really cool. But the immediate question was: "You are writing

have key_fact : some_prop,
{ a simple proof }

Can't the a simple proof be hidden away?"
Defeq and kernel reduction is one way that we are currently able to hide such "trivial proofs". I'm not saying it is the best way. Tactics could provide these trivial proofs, but with the current state of things, that would give even more "trivial proofs" that make mathematicians wonder "why am I even writing this proof?"...

[Johan Commelin]

Sorry, somehow a duplicate got posted.

[Kevin Buzzard]

With the natural number game I completely hid the concept of definitional equality. At the end of it, mathematicians are writing rw zero_add and rw add_zero and have no idea that one is a theorem and one is defeq. Because the concept "doesn't exist" in mathematics (a concept can have three definitions, as long as they're all logically equivalent; the advantage of this approach is that far more things are true "by definition"; I think the question "yes but which one is the actual definition?" barely makes sense to a mathematician) means that this question is firmly an implementation issue. Isn't the trick to make each simple proof a one-line tactic? I don't care if it's refl or simp. And then who cares about defeq? There's also the issue that computer scientists point out again and again that what a mathematician means by "simple" can range from refl to omega/linarith/ring, which all look simple to mathematicians and which computer scientists (correctly) point out have a hugely different amount of computational content to refl.