Zulip Chat Archive

Stream: new members

Topic: accessing fields on a type class


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Julian Berman (Dec 27 2020 at 23:43):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 27 2020 at 23:48):

Not ideal :(

view this post on Zulip Julian Berman (Dec 27 2020 at 23:48):

Is it still me doing something wrong/ideal declaring that

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Julian Berman (Dec 27 2020 at 23:52):

Aha .. ok trying that, thanks!

view this post on Zulip Adam Topaz (Dec 27 2020 at 23:52):

Matroids?

view this post on Zulip Julian Berman (Dec 27 2020 at 23:53):

Yeah.

view this post on Zulip Julian Berman (Dec 27 2020 at 23:55):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Julian Berman (Dec 28 2020 at 00:00):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Dec 28 2020 at 00:17):

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

view this post on Zulip Julian Berman (Dec 28 2020 at 00:18):

like, as the name?

view this post on Zulip Julian Berman (Dec 28 2020 at 00:18):

I mean you and Rota no?

view this post on Zulip Julian Berman (Dec 28 2020 at 00:18):

or is a pregeometry a looser condition

view this post on Zulip Adam Topaz (Dec 28 2020 at 00:19):

I think there are more finiteness conditions on matroids

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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