equality of objects

Stream: new members

[Winston Yin]

What's the best way to go about proving two objects with many fields are equal? Conversely, how do I obtain equality of fields from the equality of objects?

[Kevin Buzzard]

If you're making the objects yourself then you'd better make an ext lemma, perhaps by dumping @[ext] before the definition of your structure. If you're using a structure someone else has made then the ext lemma might already be there. If you want to make the ext lemma by hand then you might want to consider using cases to take your instances apart.

A simple example is the complex numbers, defined as two real numbers. I set them up in the complex number game, and in the 0th level I prove an ext lemma for them.

[Kevin Buzzard]

PS equality of fields from equality of objects comes for free. If h : s1 = s2 then s1.foo = s2.foo just by rewriting h and then using refl.

[Winston Yin]

I'm not sure why the latter doesn't work for me:

h: {to_submodule := s__to_submodule, smul_mem := s_smul_mem}.to_submodule.carrier = {to_submodule := t__to_submodule, smul_mem := t_smul_mem}.to_submodule.carrier
⊢ s__to_submodule = t__to_submodule

[Kevin Buzzard]

Can you post a #mwe ?

[Winston Yin]

One moment

[Eric Wieser]

injection h might close that goal?

[Winston Yin]

Nope...

[Winston Yin]

I'm trying to set up a set_like for a structure that extends submodules...

[Kevin Buzzard]

you can probably just use the ext tactic. All you know is that the carriers are equal and you want the submodules to be equal, but ext for submodules will do that.

[Kevin Buzzard]

I could be more helpful to you if you're more helpful to me though by setting up a MWE

[Eric Wieser]

Maybe exact set_like.coe_injective h

[Winston Yin]

Eric Wieser said:

Maybe exact set_like.coe_injective h

This worked. Thanks

[Winston Yin]

Although I'm looking at the proof of set_like.coe_injective for submodule, and it's so much simpler

[Eric Wieser]

Is your problem that you're not using old_structure_cmd?

[Eric Wieser]

Your proof has to fallback on the proof for submodule, but set_option old_structure_cmd true flattens everything out making that unnecessary.

[Winston Yin]

Eric Wieser said:

Is your problem that you're not using old_structure_cmd?

I suspected that might be the reason. Looks like I should use it

[Winston Yin]

Is there any way to set old_structure_cmd within a section only?

[Winston Yin]

Ah, looks like putting the option within a section ... end works as intended.