# 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: Aug 03 2023 at 10:10 UTC