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

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

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

Perfect, thank you!!

Last updated: Dec 20 2023 at 11:08 UTC