Definitional eta for structures

[gebner]

This is not intended as a bug report or feature request, but merely as a discussion point since this has come up on Zulip several times and Sebastian asked me to write this up.

Frequently people run into issues in mathlib where they would like a definitional eta-rule for structures. Concretely, we are talking about a rule that would make the following example provable by rfl:

example (x : α × β) : x = (x.1, x.2) := rfl
-- and analogously for other structures than Prod

These issues often arise with wrapper types, for examples opposites in category theory, or additive/multiplicative which swaps plus and times. With these wrappers, you want to avoid definitional equalities to prevent e.g. the wrong type class being used (i.e., αᵒᵖ should not be definitionally equal to α). However turning these into single-field structures is painful partly because of the missing eta rules. In Lean 3 we often used irreducible definitions for this (with local attribute [semireducible] when eta was desired), but this is neither pretty nor available in Lean 4.

Concretely, the following are examples of definitional equalities that would be nice to have:

• s = { x | x ∈ s }
• op (unop x) = x
• to_dual (of_dual x) = x
• e.symm.symm = e

Relevant Zulip discussions (non-exhaustive):

• Sets and order_dual: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/with_top.20irreducible
• Sets and additive/multiplicative: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universe.20juggling
• Equivalences: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unexpected.20non-defeq
• Opposites in category theory: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.23538.20opposites

Other proof assistants that have eta for structures:

• Coq has it for records if you enable Set Primitive Projections.
• Agda

[gebner]

Please feel free to add additional concrete examples where eta for structures would be helpful.

[leodemoura]

@gebner Thanks for submitting the issue. We will try to add this issue soon. It would be great if the community could create a Lean 4 "test file" with the different use cases.

[javra]

I think another important example would be

example (x : PUnit) : x = () := rfl

which might spare us a lot of rewrites in auto-generated declarations.

[leodemoura]

@gebner I haven't tested the new feature much, but I added a few examples at d685c54
If you have time could you please take a look at the kernel modification at d685c54

[gebner]

Awesome! The main limitation I still see is that eta is not recursive. That is, the following fails:

example (x : Unit × α) : x = ((), x.2) := rfl -- fails

Something like this can easily happen with structure inheritance:

structure Equiv (α β : Type) where
  toFun : α → β
  inv : β → α
  -- ..

class TopologicalSpace (α : Type)

structure Homeomorph (α β : Type) [TopologicalSpace α] [TopologicalSpace β] extends Equiv α β where
  continuousToFun : True
  continuousInv : True

def Homeomorph.symm [TopologicalSpace α] [TopologicalSpace β] (f : Homeomorph α β) : Homeomorph β α where
  toFun := f.inv
  inv := f.toFun
  continuousToFun := f.continuousInv
  continuousInv := sorry

example [TopologicalSpace α] [TopologicalSpace β] (f : Homeomorph α β) :
  f.symm.symm = f := rfl -- fails

It also doesn't play well with proof irrelevance:

example (x : (_ : True ∨ False) ×' α) : x = ⟨Or.inl ⟨⟩, x.2⟩ := rfl -- fails

Unification is less strong than one might assume at first glance. But I think this is super low priority as it is extremely easy to work around (just write x instead of (y, z) whenever possible).

example (p : α × α → Prop) (h : ∀ x y, p (x, y)) : p z := h z.1 _   -- fails to unify

If you have time could you please take a look at the kernel modification at d685c54

The only thing that I'm missing is a check that both sides have the same type. But I don't see a way to exploit the missing check to derive anything strange.

[leodemoura]

@gebner Thanks for the detailed feedback. I will try to address the issues you pointed out above.

[gebner]

Okay, I'm almost out of ideas now.

When updating mathlib I found a few lemmas like this where I would've expected rfl to work as a proof:

example (x y : Unit) : x = y := rfl

Another somewhat important feature would be to reduce recursors even if the major premise is not a constructor:

def frob : Nat × Nat → Nat × Nat
  | (x, y) => (x + y, 42)

example (x : Nat × Nat) : (frob x).2 = 42 := rfl

In mathlib we try very hard to avoid pattern-matching on structures because it doesn't reduce in cases like this, and then use projections instead which is a lot more verbose. It would be cool if we could use the idiomatic solution (i.e, pattern-matching).

(I just wanted to mention these while the eta stuff is still fresh in your head. We can also postpone these features until we have had more experience with them in mathlib.)

[javra]

Just to add to @gebner's point: Making pattern matching more powerful in this way fits nicely with the shift towards more structured proof in Lean 4 vs Lean 3,

[leodemoura]

@gebner I added support for etaStruct at recursors. The frob example works now.

The support for example (x y : Unit) : x = y := rfl is still missing. I will add it later.