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 https://github.com/leanprover/lean4/commit/d685c545b46b5d026475789d77be031bfb64f88d If you have time could you please take a look at the kernel modification at https://github.com/leanprover/lean4/commit/d685c545b46b5d026475789d77be031bfb64f88d

[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.

[leodemoura]

@gebner I have also added a etaStruct flag at Meta.Config and Meta.Simp.Config. It is useful for disabling "eta for structures" in tactic mode.

[gebner]

The change introduced a regression where unifying Fin.mk ?n ?h and Fin.mk n h no longer assigns ?h := h. :cry:

theorem Fin.ext_iff : (Fin.mk m h₁ : Fin k) = Fin.mk n h₂ ↔ m = n :=
  Fin.mk.injEq _ _ _ _ ▸ Iff.rfl

example : (Fin.mk m h₁ : Fin k) = Fin.mk n h₂ := by
  apply Fin.ext_iff.2
  -- should only generate one goal (i.e., fill in h₁ and h₂ via unification)

example : (Fin.mk m h₁ : Fin k) = Fin.mk n h₂ := by
  simp
  -- should simplify to m = n

[leodemoura]

@gebner Pushed a fix for the Fin issue. We might have other nasty interactions in unification constraints containing metavariables.

[gebner]

The last commit fixed all issues I could find.

We had a small temporary regression in binport after the initial eta commit, where the import failed because the Lean 3 and Lean 4 versions of the Div Nat instance were no longer defeq. But with the current nightly this is fixed now.