## 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 :=
begin
sorry,
end


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