Computational canonicity and unfolding

Stream: general

[Pedro Minicz]

Lean sometimes forces you to unfold definitions. Some tactics, like rw, may fail a given goal, but succeed in a definitionally equal term after unfolding. I've noticed this since I've migrated from Coq (I am by no means an "expert" Coq user) that some goals in Lean need unfold or dsimp there Coq made me expect them to "just work."

While listening to the "Every proof assistant: Cubical Agda" talk (can be found here), around 10 minutes in, the speaker explains that one of the drawbacks of adding axioms such as funext is that you break canonicity and, therefore, proofs may become longer because of the necessity of manual unfolding among other things. This is quite interesting. Between Agda, Coq, and Lean, Lean is the only one that actively uses such axioms, that is, while one can postulate funext and friends in Agda and Coq, it is "not encouraged", while in Lean funext, propext, and choice are in the prelude.

My question is: has the "embracing" of axioms influenced how Lean treats expressions modulo beta-reduction/unfolding?

[Patrick Massot]

I'm pretty sure this is only a performance choice for rw. We do have tactics that see through definitions. That's one of the reason to use simp_rw for instance.