Zulip Chat Archive

Stream: new members

Topic: What even is definitional equality in structures?

Mantas Baksys (Apr 06 2021 at 10:44):

After spending some time pondering the following issue and coming up with exactly nothing, I think's it's time to ask this question here :smiley: Below I post an example of a 'trivial' statement that I cannot close by refl, which baffles me.

import data.real.basic

structure dissection (a b : ) (S : finset ) :=
(N := S.card)
(mem_Icc:  x  S, a   x  x  b)
(mem_endpoints :  x  S, x = a   y  S, y = b)

lemma dissection_card_def {a b: } {S: finset } (D: dissection a b S) : D.N = S.card :=

I'm really lost why this happens (and what do I need to fix it), so I'll appreciate any help I get!

Scott Morrison (Apr 06 2021 at 10:57):

When you write N := S.card, you are not saying that "N is always S.card". You are only providing a default value.

Scott Morrison (Apr 06 2021 at 10:57):

Why is N even a field of dissection, rather than a separate def?

Mantas Baksys (Apr 06 2021 at 11:19):

Thanks @Scott Morrison , I'll define it separately. I wanted to define N inside dissection for elegance in notation (it's tiresome to always write S.card). But there's probably an easier way (and actually working) way to do this, I'm guessing.

Scott Morrison (Apr 06 2021 at 11:20):

Just def dissection.N (a b : ℝ) (S : finset ℝ) (D : dissection a b S) : nat := S.card.

Mantas Baksys (Apr 06 2021 at 11:30):

Thank you so much, @Scott Morrison. I'll just use def every time I want to say 'this is true by definition'. It's really obvious in hindsight, but surprisingly it wasn't at first.

Eric Wieser (Apr 06 2021 at 11:31):

def says "this is the definition", not "this is true"

Eric Wieser (Apr 06 2021 at 11:31):

Since the statement "nat is true" is nonsense

Mantas Baksys (Apr 06 2021 at 11:32):

Pardon my language, I completely agree @Eric Wieser .

Last updated: Dec 20 2023 at 11:08 UTC