Using properties of classes

Stream: new members

[Andrew Souther]

Hello, I'm working on formalizing some ideas from Voting Theory. Here is a bit of context:
I have defined an election_profile as a structure consisting of a finset of candidates, a finset of voters, and an individual ordering Q that matches each voter to a ranking of the candidates. I have also defined a voting_method class. I am trying to prove a basic lemma about voting methods, but I am not sure how to "access" the properties of a class in a useful way. MWE:

import data.set.finite

structure election_profile (χ υ : Type*) :=
(cands : finset χ)
(voters : finset υ)
(Q : υ → χ → χ → Prop)

class voting_method {χ υ : Type*} (M : election_profile χ υ → finset χ) : Prop :=
(winners_subset : ∀ prof : election_profile χ υ, M prof ⊆ prof.cands)
(winners_nonempty : ∀ prof : election_profile χ υ, prof.cands.nonempty → (M prof).nonempty)

lemma voting_method_singleton {χ υ : Type*}  {prof : election_profile χ υ} {a : χ}
  (M : election_profile χ υ → finset χ) [hM : voting_method M] (h : prof.cands = {a}) :
  M prof = {a} :=
begin
  have : M prof ⊆ prof.cands := hM.winners_subset prof, -- doesn't work
end

[Andrew Souther]

A. Do you think that a class is a convenient way to define the idea of a voting method here?
B. If so, how can I better "access" the properties of this class in my proof?

[Heather Macbeth]

If you make voting_method a class, then in your assumptions you should say [voting_method M] rather than {hM : voting_method M} Sorry, I see you do this already

[Heather Macbeth]

And to get access to the two properties as lemmas, say something like

export voting_method (winners_subset, winners_nonempty)

[Andrew Souther]

Great, thank you! This didn't quite work, but removing the comma did the trick:

export voting_method (winners_subset winners_nonempty)

[Heather Macbeth]

Oops, yes!