Zulip Chat Archive

Stream: general

Topic: Unexpected non-defeq


Heather Macbeth (Jul 09 2021 at 16:50):

I was surprised to learn that for an equiv e : α ≃ β, it is not true that e.symm.symm is definitionally equal to e, even though each of their data fields is definitionally equal:

import data.equiv.basic

variables {α β : Type*}

example (e : α  β) : e.symm.symm = e := rfl -- fails

There is a trick to get around this, which @Frédéric Dupuis showed me: I can define an equiv e.self which is a field-by-field copy of e, and this is definitionally equal to e.symm.symm.

def equiv.self (e : α  β) : α  β :=
{ to_fun := e.to_fun,
  inv_fun := e.inv_fun,
  left_inv := e.left_inv,
  right_inv := e.right_inv }

example (e : α  β) : e.self = e := rfl -- fails
example (e : α  β) : e.symm.symm = e.self := rfl -- works

Heather Macbeth (Jul 09 2021 at 16:52):

I would like to understand this better -- why are e.self and e not definitionally equal? Is this somehow fundamental to the axioms of Lean? And is this trick to get around it the canonical workaround?

Johan Commelin (Jul 09 2021 at 16:52):

@Heather Macbeth This is the so-called eta-rule. And in Lean it doesn't count as defeq. There are pragmatical reasons to exclude it, because otherwise the typechecker goes crazy. But that's about all I know about this.

Kevin Buzzard (Jul 09 2021 at 17:06):

eta for pi types is definitional, but not for inductive types. In other words, (lam x, f x) is defeq to f, but e.symm.symm is not defeq to e. I have no idea why this design decision was made.

@[simp] theorem eta :  z : , complex.mk z.re z.im = z
| a, b := rfl

(so the proof is "cases, refl" rather than "refl")

Heather Macbeth (Jul 09 2021 at 17:14):

This gave me a good search term for past conversations, which I am busily reading, thanks.

To put my basic question rather naively: Suppose I went through mathlib and I changed every occurence of an equiv e to e.self (according to this equiv.self definition I wrote above). What would break?

Bhavik Mehta (Jul 09 2021 at 17:17):

Heather Macbeth said:

I would like to understand this better -- why are e.self and e not definitionally equal? Is this somehow fundamental to the axioms of Lean? And is this trick to get around it the canonical workaround?

I think the canonical work around is either to use cases, refl or ext, refl to prove it, or use simp to simplify it (after the equality lemma exists, which it does for symm_symm)

Eric Wieser (Jul 09 2021 at 19:51):

Am I right in thinking that coe_fn e = coe_fn e.symm.symm is true by refl?

Eric Wieser (Jul 09 2021 at 19:53):

Do Coq or Agda allow the eta rule in determining defeq?

Bhavik Mehta (Jul 09 2021 at 20:43):

Eric Wieser said:

Am I right in thinking that coe_fn e = coe_fn e.symm.symm is true by refl?

Yes, because coe_fn on equivs is to_fun, and as Heather mentions, the to_fun components are equal by rfl

Nathaniel Yazdani (Jul 15 2021 at 10:01):

For those interested, the nLab --- generally a good though sometimes quite technical resource for
learning about type theory --- gives the following summary (lightly edited by me for clarity)
of why a dependent type theory like Lean's or Coq's typically omits a definitional η-expansion rule:

Coq versions 8.3 and prior do not implement definitional η-expansion, but versions 8.4 and higher
do implement it for dependent product types (i.e., function types). Even in Coq v8.4 and later,
η-expansion is not implemented for other types, such as inductive and coinductive types...
since definitonal η-expansion for the identity type forces us into extensional dependent type theory.

...if “equality” refers to the identity type in a dependent type theory, then η-expansion for an
inductively defined type is provable as an equality. This includes the identity type itself, but this
propositional form of η-expansion does not imply extensionality of the identity type because
the identity type itself must be incorporated in stating the equivalence.

By the way, I think that a dependent type theory can have definitonal η-conversion for a carefully
restricted class of inductive types without becoming extensional, but don't quote me on that :-)

Coincidentally, the absence of definitional η-expansion for inductive types (in Coq, not Lean) was
a major pain in the butt intellectual challenge in a recent research paper to which I contributed:
Proof Repair across Type Equivalences, §4.1.

Patrick Massot (Jul 15 2021 at 10:46):

Your "edit for clarity" removed the crucial part: "This is a good thing for homotopy type theory, since η-equivalence for identity types forces us into extensional type theory". So we don't need to read what extensional type theory means since it's not relevant to us.

Johan Commelin (Jul 15 2021 at 10:49):

Well, maybe it should be... it would mean that motive is not type correct is no longer a wall of steel that cannot move.

Patrick Massot (Jul 15 2021 at 10:49):

Is that an answer to my message?

Johan Commelin (Jul 15 2021 at 10:50):

Yes. Currently Lean doesn't support extensional type theory. But it's something that maybe should be part of the "ideal" proof assistant.

Patrick Massot (Jul 15 2021 at 10:52):

But I didn't say definitional eta or extensional type theory isn't relevant to us. I said the explanation from nlab about why eta is bad is not relevant to us.

Jannis Limperg (Jul 15 2021 at 10:52):

Nathaniel Yazdani said:

By the way, I think that a dependent type theory can have definitonal η-conversion for a carefully
restricted class of inductive types without becoming extensional, but don't quote me on that :-)

Agda has eta for most structure types ("records" in their terminology), including something like this equiv type. So it's certainly possible.

Johan Commelin (Jul 15 2021 at 10:52):

@Patrick Massot Aha, then I misunderstood your message. Sorry.

Patrick Massot (Jul 15 2021 at 10:53):

That's what I guessed. Sorry about that unclear message.

Jannis Limperg (Jul 15 2021 at 10:57):

Nathaniel's quote still applies, though, if you replace "for homotopy type theory" with "for any type theory that wants to be intensional", which includes Lean. So the explanation is relevant.

Gabriel Ebner (Jul 15 2021 at 11:04):

I believe the comment in the ncatlab explanation about "extensional type theory" refers (confusingly) not to a type theory with an extensionality rule (which allows you to derive definitional equality from propositional equality), but instead to a type theory where a = b is a subsingleton...

Gabriel Ebner (Jul 15 2021 at 11:06):

Eta for equality is indeed not helpful in HoTT (just like axiom K, but I don't know if there is a difference between the two). For Lean this consideration is absolutely irrelevant though.

David Wärn (Jul 15 2021 at 11:16):

What does eta for the identity type mean? Any h : a = b is def eq to rfl : a = a? But this only makes sense if a is def eq to b?

Jannis Limperg (Jul 15 2021 at 11:28):

Gabriel Ebner said:

I believe the comment in the ncatlab explanation about "extensional type theory" refers (confusingly) not to a type theory with an extensionality rule (which allows you to derive definitional equality from propositional equality), but instead to a type theory where a = b is a subsingleton...

Ah! In that case I retract my previous statement and claim the opposite. (This saying works better in German.) The Agda remark still applies though.

Nathaniel Yazdani (Jul 15 2021 at 13:17):

@Patrick Massot Lean's type theory is based closely on CiC, which is very much intensional. Also, the quote from nLab really does use "extensional type theory" to mean "a dependent type theory with equality reflection," as the term is conventionally understood in PL research. Since my modest (IMO) paraphrasing of that nLab subsection --- which was just meant to reduce unfamiliar jargon for those not already experts in type theory --- elicited an unexpected degree of controversy, I will simply point to the relevant subsection of nLab's article on the identity type: identity type § extensionality and η-conversion

Nathaniel Yazdani (Jul 15 2021 at 13:25):

Of course, I find a simpler reference just after sending my last message; the last paragraph of extensional type theory § definitional extensionality reads as follows, verbatim:

A different, also equivalent, way of presenting definitionally extensional type theory is with a definitional eta-conversion rule for the identity types; see here.

Kyle Miller (Jul 15 2021 at 16:49):

I found the entry in the Stanford Encyclopedia of Philosophy on extensional type theory to be illuminating.

In Lean, it seems like it would mean the following two things (the second of which is already the case):

  • If {α α' : Type*} (h : α = α') (x : α), then there would be some way to say x : α'.

  • lemma eq_eq_irrel {α : Type*} {a a' : α} (h h' : a = a') : h = h' := rfl

If I understand it correctly, the first thing lets you avoid heq-hell, but at the cost of losing an algorithm for decidable typechecking.

Gabriel Ebner (Jul 15 2021 at 16:51):

Yes, precisely.

Kyle Miller (Jul 15 2021 at 17:00):

@Gabriel Ebner Oh, now I understand what you and @David Wärn were saying. In extensional type theory, you assert that eta for the identity type makes sense. The h : a = b implies a is formally defeq to b.

Gabriel Ebner (Jul 15 2021 at 17:00):

Maybe to make the situation clear to the casual readers here: the example Nathaniel has posted shows that we cannot have full eta for eq without getting into extensional type theory. (This also applies to other GADTs.) Another way to think about this we cannot even prove an eta theorem---∀ x : a = b, x = eq.refl ???---for eq (so why would we expect it to hold definitionally).

However we can still add eta for structures (like the equiv that Heather complained about in the beginning of the thread). The biggest hurdle I see here is that we would need to teach the kernel about structures (because it doesn't even know what a projection is at the moment).

David Wärn (Jul 15 2021 at 17:18):

One of Nathaniel's links, https://ncatlab.org/nlab/show/identity+type#EtaConversion explains eta for the identity type. Actually this form of eta doesnt look like "x = eq.refl...", rather it says something like "any (dependent) function out of an identity type is def eq to something obtained from eq.rec". Iiuc the well-known versions of eta for structures and functions is a specialisation of this general form of eta, applied to the identity function. What's surprising is that while eta for identity holds "propositionally" in intensional type theory, if you make it def eq then you get extensional type theory. This is explained in the link above; the idea is that the two functions out of the id-type which return first and second endpoints are def eq on the base case (rfl), so are defeq assuming eta.

David Wärn (Jul 15 2021 at 17:19):

But indeed this seems irrelevant for the original discussion about eta for structures

Yaël Dillies (Jul 15 2021 at 18:07):

(I would translate it by "I take everything back and declare the opposite" :wink:)

Gabriel Ebner (Jul 15 2021 at 18:09):

Ok, after reading (the relevant part of) Streicher's thesis, I finally understand it. To use Streicher's terminology: "uniqueness of elimination implies the reflection rule".

Calling uniqueness of elimination the eta rule for equality really stretches the meaning of these words though. Even Streicher only calls it an "eta-like for the eliminator [eq.rec]".


Last updated: Dec 20 2023 at 11:08 UTC