Zulip Chat Archive

Stream: general

Topic: Computational canonicity and unfolding

Pedro Minicz (Sep 24 2020 at 14:11):

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 (Sep 24 2020 at 14:13):

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.

Last updated: Dec 20 2023 at 11:08 UTC