Zulip Chat Archive
Stream: general
Topic: Unexpected nondefeq
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 fieldbyfield 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 socalled etarule. 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
ande
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 equiv
s 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 etaconversion 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 sayx : α'
. 
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 wellknown 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 idtype 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 "etalike for the eliminator [eq.rec]".
Last updated: Aug 03 2023 at 10:10 UTC