frustrating Type error

Stream: new members

[Andrew Souther]

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]

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]

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 χ) :=
sorry

[Kevin Buzzard]

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]

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 :=
sorry

[Andrew Souther]

Perfect, thank you!!