## Stream: new members

### Topic: accessing fields on a type class

#### Julian Berman (Dec 27 2020 at 23:38):

What am I doing wrong syntactically here to try and use a field from a type class I'm including in another type class?

class cool (S : finset ℕ) := (property : ∀ s ∈ S, s = 37)

class thing (S : finset ℕ) :=
[cool : cool S]
(nonempty : S.nonempty)

lemma exists_37 {S} [T : thing S] : 37 ∈ S := begin
obtain ⟨s, hs⟩ := T.nonempty,
exact T.cool.property s hs,
end


Last line in the proof there -- how do I use the property from the first type class?

(I think I'm realizing I likely don't want a type class at all I want .. a Prop I guess, but still curious)

#### Adam Topaz (Dec 27 2020 at 23:42):

@cool.property _ _... would certainly work, but I think the standard thing is to make thing extend cool as opposed to making it a field, so you can then use exact cool.property

#### Julian Berman (Dec 27 2020 at 23:43):

Aha, ok, good to know, thanks -- that makes sense in my Real Code too I think.

#### Adam Topaz (Dec 27 2020 at 23:47):

import data.finset.basic

class cool (S : finset ℕ) := (property : ∀ s ∈ S, s = 37)

class thing (S : finset ℕ) extends cool S :=
(nonempty : S.nonempty)

lemma exists_37 {S} [T : thing S] : 37 ∈ S := begin
obtain ⟨s, hs⟩ := T.nonempty,
rwa ← cool.property s,
-- some metavars left :(
end


Not ideal :(

#### Julian Berman (Dec 27 2020 at 23:48):

Is it still me doing something wrong/ideal declaring that

#### Julian Berman (Dec 27 2020 at 23:50):

My real example is...

import data.finset

variables {E : Type*} [decidable_eq E]

class of_independent (𝓘 : finset (finset E)) :=
{nonempty : 𝓘.nonempty . tactic.exact_dec_trivial}
(hereditary {I J} (hI : I ∈ 𝓘) (hJ : J ⊆ I) : J ∈ 𝓘)
(augmentation {I J}
(hI : I ∈ 𝓘)
(hJ : J ∈ 𝓘)
(h_card : finset.card I < finset.card J) :
∃ j ∈ J \ I, insert j I ∈ 𝓘)

variable {𝓘  : finset (finset E)}

/-! The empty set is always an independent set. -/
lemma of_independent.empty_is_independent [M : of_independent 𝓘 ] : ∅ ∈ 𝓘 := begin
obtain ⟨S, hS⟩ := M.nonempty,
exact of_independent.hereditary hS (set.empty_subset (λ (a : E), a ∈ S.val)),
end


but I wanted to move hereditary to a type class so that I could talk about a set being hereditary regardless of whether I had an of_independent, and yeah having similar troubles to the slimmed down example when trying to reprove the lemma.

#### Adam Topaz (Dec 27 2020 at 23:52):

Nevermind. it's okay :)

import data.finset.basic

class cool (S : finset ℕ) :=
(property : ∀ s ∈ S, s = 37)

class thing (S : finset ℕ) extends cool S :=
(nonempty : S.nonempty)

lemma exists_37 {S} [T : thing S] : 37 ∈ S := begin
obtain ⟨s, hs⟩ := T.nonempty,
rwa ← cool.property _ hs,
end


#### Julian Berman (Dec 27 2020 at 23:52):

Aha .. ok trying that, thanks!

Matroids?

Yeah.

#### Julian Berman (Dec 27 2020 at 23:55):

Huh. I think it worked trivially with extends, so probably that's the right thing

#### Julian Berman (Dec 27 2020 at 23:55):

i.e.

import data.finset

variables {E : Type*} [decidable_eq E]

class hereditary (𝓘 : finset (finset E)) :=
(property {I J} (hI : I ∈ 𝓘) (hJ : J ⊆ I) : J ∈ 𝓘)

class of_independent (𝓘 : finset (finset E)) extends hereditary 𝓘 :=
{nonempty : 𝓘.nonempty . tactic.exact_dec_trivial}
(augmentation {I J}
(hI : I ∈ 𝓘)
(hJ : J ∈ 𝓘)
(h_card : finset.card I < finset.card J) :
∃ j ∈ J \ I, insert j I ∈ 𝓘)

variable {𝓘  : finset (finset E)}

/-! The empty set is always an independent set. -/
lemma of_independent.empty_is_independent [M : of_independent 𝓘 ] : ∅ ∈ 𝓘 := begin
obtain ⟨S, hS⟩ := M.nonempty,
exact hereditary.property hS (set.empty_subset (λ (a : E), a ∈ S.val)),
end


#### Julian Berman (Dec 28 2020 at 00:00):

Heh -- @Bryan Gin-ge Chen I set aside your repo for a bit to just screw around a little more, was getting tedious trying to figure out some things (because of my lean gaps)

#### Julian Berman (Dec 28 2020 at 00:00):

But will probably have to get back to it once I have a bit of fun.

#### Bryan Gin-ge Chen (Dec 28 2020 at 00:11):

No worries, that sounds a lot like why I set it aside myself. :wink:

I heard there was another attempt on matroids in Lean in progress, but I don't know how far along it is now.

#### Adam Topaz (Dec 28 2020 at 00:17):

Am I the only one who prefers combinatorial pregeometries? (The answer seems to be "yes")

#### Julian Berman (Dec 28 2020 at 00:18):

like, as the name?

#### Julian Berman (Dec 28 2020 at 00:18):

I mean you and Rota no?

#### Julian Berman (Dec 28 2020 at 00:18):

or is a pregeometry a looser condition

#### Adam Topaz (Dec 28 2020 at 00:19):

I think there are more finiteness conditions on matroids

#### Adam Topaz (Dec 28 2020 at 00:22):

But I'm mostly saying that I think the closure operator definition feels more natural to me as "the" definition. But I'm very far from being a combinatorist, so I'm probably in a small minority here.

#### Jesse Michael Han (Dec 28 2020 at 05:15):

Am I the only one who prefers combinatorial pregeometries? (The answer seems to be "yes")

i think model theorists prefer "pregeometry" and presenting matroids using closure operators

#### Bhavik Mehta (Dec 29 2020 at 18:05):

For those interested in closure operators, I've made: https://github.com/leanprover-community/mathlib/pull/5524, feel free to review!

Last updated: May 13 2021 at 00:41 UTC