accessing fields on a type class

Stream: new members

[Julian Berman]

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]

@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]

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

[Adam Topaz]

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

[Adam Topaz]

Not ideal :(

[Julian Berman]

Is it still me doing something wrong/ideal declaring that

[Julian Berman]

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]

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]

Aha .. ok trying that, thanks!

[Adam Topaz]

Matroids?

[Julian Berman]

Yeah.

[Julian Berman]

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

[Julian Berman]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Julian Berman]

like, as the name?

[Julian Berman]

I mean you and Rota no?

[Julian Berman]

or is a pregeometry a looser condition

[Adam Topaz]

I think there are more finiteness conditions on matroids

[Adam Topaz]

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]

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]

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