Zulip Chat Archive

Stream: new members

Topic: frustrating Type error

Andrew Souther (Dec 19 2021 at 14:56):

I am working to formalize this paper from Voting Theory. A few weeks ago, Kyle Miller helped me write a rough draft for the definition of the voting system Stable Voting. Now, I'm trying to prove that Stable Voting satisfies certain properties.

Here is a bit of background on my context. An election_profile is a structure containing a finset of candidates, a finset of voters, and an individual preference ordering Q that matches each voter to a ranking of candidates. stable_voting is a voting system. That means it takes an election profile as an input, and it outputs another finset of winning candidates. "Stability for Winners" is a property that some voting systems have. I'm trying to show that stable_voting satisfies this property.

I tried to state the theorem that is_stable_for_winners stable_voting, but I am getting a "don't know how to synthesize placeholder" error. Here is an mwe, with the error at the bottom of the file.

Andrew Souther (Dec 19 2021 at 14:58):

I am hoping this is a simple issue with the way I set up my variables in the beginning of the file. However, on top of some help with this problem, I would appreciate some general advice about what this problem means, and how I can keep my code organized to avoid it.

Kevin Buzzard (Dec 19 2021 at 15:03):

Lean can't guess chi and upsilon. You can just help it by using type ascription, e.g.

theorem sv_stable_for_winners :
  is_stable_for_winners (stable_voting : election_profile χ υ  finset χ) :=

Kevin Buzzard (Dec 19 2021 at 15:05):

Alternatively you could make chi and upsilon explicit in stable_voting or elsewhere. Whether you want to do this depends on whether stable_voting is typically used by itself or whether mostly it will be instantly evaluated at some term of type election_profile χ υ

Kevin Buzzard (Dec 19 2021 at 15:06):

Here's how to make the variables explicit for is_stable_for_winners (and further definitions):

def is_stable (M : election_profile χ υ  finset χ)
  (prof : election_profile χ υ) (a: χ) : Prop :=
let prof_without (b : χ) : election_profile χ υ :=
  prof.cands.erase b, prof.voters, prof.Q in
 b  prof.cands, margin_pos prof.voters prof.Q a b  a  M (prof_without b)

variables (χ) (υ)

/- "Stability for winners" is a property that certain voting systems satisfy. -/
def is_stable_for_winners (M : election_profile χ υ  finset χ) : Prop :=
 (prof: election_profile χ υ),
( x, is_stable M prof x)   a  (M prof), is_stable M prof a

theorem sv_stable_for_winners :
  is_stable_for_winners χ υ stable_voting :=

Andrew Souther (Dec 19 2021 at 15:18):

Perfect, thank you!!

Last updated: Dec 20 2023 at 11:08 UTC