Making records definitionally equal

Stream: general

[Adrian Marti]

I have been working on a category theory formalization in Lean 4 and I am trying to make it so that the opposite of the opposite of a category is definitionally equal to the original category (in Agda this idea apparently works). The reason for this, is that it seems pretty inconvenient to dualize theorems by replacing categories by their opposites if we don't have a definitional equality.

In any case, the issue can be illustrated with the following code:

-- The code is in Lean 4, but similar code should
-- behave the same way in Lean 3
structure Tuple where
  first: Nat
  second: Nat

def Tuple.flip (x: Tuple) : Tuple := { first := x.2, second := x.1 }

variable (x: Tuple)

-- fails
def flipflip : Tuple.flip (Tuple.flip x) = x := rfl
-- Eta rule fails
def p : { first := x.1, second := x.2 } = x := rfl

I would like Tuple.flip (Tuple.flip x) to be definitionally equal to x, but that seems to fail because Lean does not seem to have an eta rule for records. This seems to be precisely the issue I am running into with my opposite categories.

I also tried to define flip by pattern matching, but I ran into a similar issue:

def Tuple.flip' (x: Tuple) : Tuple :=
  match x with
  | ⟨n,m⟩ => ⟨m,n⟩

-- fails since passing the record constructor to the recursion
-- does not reduce to the identity
def flipflip' : Tuple.flip' (Tuple.flip' x) = x := rfl

Is there some trick I am missing to make this work or am I better off giving up on this idea?

[Johan Commelin]

I will just point out that currently in mathlib opposite (opposite X) is not defeq to X, even for things like rings, preorders, etc... We provide isomorphisms instead.
If I recall correctly, the reason is that type class inference got mightily confused if we didn't put up a strong barrier.

[Adrian Marti]

I guess that typeclass inference won't be an issue for me, since I am experimenting with bundled structures and unification hints, but it is still nice to know how things currently work in mathlib.

[David Wärn]

I think you can't do this since Lean doesn't have eta for records/structures? The mathlib style is to not rely too much on def eqs. But even of you want to use def eqs here, you might be fine since any reasonable definition involving a category C will unfold to something only mentioning projections, and the double opposite doesn't do anything to these projections

[Kevin Buzzard]

Does Agda have eta for records/structures?

[Kevin Buzzard]

PS @Adrian Marti your link is not to a URL or an upload, so doesn't work for me.

[Eric Wieser]

@Johan Commelin , you're wrong, opposite (opposite X) = X is true by rfl

[Eric Wieser]

Because src#opposite is a def not a structure with one field

[Johan Commelin]

Ooh, I thought we transitioned to a structure recently...

[Nathaniel Yazdani]

Yep, Agda indeed has definitional η-conversion for records, which coincidentally came up in another recent thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unexpected.20non-defeq/near/246077975

[Johan Commelin]

This only happened for additive and multiplicative maybe?

[Eric Wieser]

Additive and multiplicative are the ones you're thinking of, but the transition didn't happen for the same reason

[Johan Commelin]

Hmm, I guess I missed some discussions then

[Eric Wieser]

Polynomial _did_ make the transition, but that's because definitional roundtripping between finsupp and polynomial isn't nearly as important

[Eric Wieser]

I think @Gabriels Herculean PR to change additive / multiplicative is still open, but there was a Zulip thread where Mario and I expressed opposition

[Eric Wieser]

And of course it's now stale

[Adrian Marti]

Kevin Buzzard said:

PS Adrian Marti your link is not to a URL or an upload, so doesn't work for me.

Fixed

[Adam Topaz]

Eric Wieser said:

Johan Commelin , you're wrong, opposite (opposite X) = X is true by rfl

I'm not sure what this is supposed to mean? (opposite.op a).unop = a is true by rfl, but opposite.op is a function that goes from a type T to T\op, so opposite.op (opposite.op a) has type T\op\op...

[Eric Rodriguez]

I guess this is what's meant:

import data.opposite

local attribute [semireducible] opposite

example {A : Type} : opposite A = A := rfl

this is absolute abuse though

[Adam Topaz]

local attribute [semireducible] opposite :scared:

[Eric Rodriguez]

yeah strong do-not-try-this-at-home here

[Johan Commelin]

But without that attribute, does the proof break? Because I think that is what I had in mind...

[Eric Rodriguez]

I couldn't make it work without it, no. I needed to unfold

[Eric Wieser]

I must have been in a section with that attribute set when I last saw opposite. I think the statement is still true without the attribute, but you have to use rw instead of rfl

[Eric Wieser]

Also opposite X = X is clearly evil and it's nice to pretend that only opposite (opposite X) = X is true!