recursive function on finset

Stream: new members

[Andrew Souther]

I am trying to define voting systems in Lean, so that I can formalize theorems about these voting systems. I am hoping to define recursive voting systems like Instant Runoff Voting which iteratively remove candidates until a winner is chosen.

In particular, I am working to define "Simple Stable Voting" in Lean. Here is the paper I am looking at, and here is a description of the voting system from that paper:

I have sketched up a rough framework for defining this kind of voting system in Lean (mwe with more explanation):

import data.set.finite

structure election_profile (χ υ : Type*) :=
(candidates : finset χ)
(voters : finset υ)
(ballots : υ → χ → χ → Prop)


def simple_stable_voting {χ υ : Type*} : election_profile χ υ → finset χ := λ prof,
begin
  cases prof with X V Rᵢ,
  sorry,
end

I figure I will need to perform some kind of induction on the finset X. I have tried to read through Chapter 8 on recursion and induction in TPIL, and I think I understand how to define simple recursive functions on natural numbers, but I have no clue where to start when it comes to defining a recursive function on a finset.

[Andrew Souther]

I assume I will need to handle three cases. If the set of candidates is empty, then the function outputs a junk value (the empty set) because you can't pick a winner from 0 candidates. If there is one candidate, then the function should output a finset with only that candidate as a winner. Then, I need to perform some kind of recursion on this base case to handle further cases.

[Mario Carneiro]

You probably want to induct on the size of the finset

[Mario Carneiro]

Normally you could use docs#finset.induction but in this case you want to remove a particular element from the set (the losing candidate) in the recursive call

[Andrew Souther]

Hm, let's say I define n to be the size of X like this: n : ℕ := X.card. How can I actually induct on that natural number in this case? Like I understand how to use the induction tactic or apply the finset.induction_on lemma when I am trying to prove a proposition, but I don't understand how to use these things so well when I'm trying to define a function

[Andrew Souther]

For example, Lean doesn't like this because Lean fails to create a new goal:

def simple_stable_voting {χ υ : Type*} : election_profile χ υ → finset χ := λ prof,
begin
  cases prof with X V Rᵢ,
  set n : ℕ := X.card with hX,
  induction n with n hn,
  sorry,
end

[Yaël Dillies]

Random idea, but maybe you can first define the voting system on list?

[Andrew Souther]

Like handle a list of candidates instead of a finset of candidates, because list is a more primitive object, so induction might be a bit easier?

[Andrew Souther]

Maybe that could be a good first step to wrap my head around this stuff.

[Mario Carneiro]

let/set screws up induction because it doesn't know how to deal with let variables in the context. Use generalize instead:

def simple_stable_voting {χ υ : Type*} : election_profile χ υ → finset χ := λ prof,
begin
  cases prof with X V Rᵢ,
  generalize h : X.card = n,
  induction n with n hn generalizing X,
  sorry,
end

[Andrew Souther]

Exciting, thank you Mario!!! I will play with this and see if it turns out fruitful.

[Andrew Souther]

Actually, another quick question. Is there an easy way to split off the X.card=0 case AND the X.card=1 case before proceeding with the recursion? Similar to this example in TPIL:

open nat

def sub2 : ℕ → ℕ
| zero            := 0
| (succ zero)     := 0
| (succ (succ a)) := a

[Kevin Buzzard]

You can do cases n with d just before the induction and you'll be left with n=0 and n=succ(d), and then you can do cases d with t and you'll be left with the cases d=0 and d=succ(t).

[Eric Wieser]

Andrew Souther said:

Like handle a list of candidates instead of a finset of candidates, because list is a more primitive object, so induction might be a bit easier?

Yes. Once you do this, you then have to prove your algorithm doesn't depend on the order the list was in, and then you can make it a function on multisets.

[Notification Bot]

Andrew Souther has marked this topic as unresolved.

[Andrew Souther]

Is it ok to unresolve? Or is it encouraged to open a new conversation?

[Andrew Souther]

I just want to ask further questions about the definition Kyle posted above

[Kevin Buzzard]

back in the old days (last month or so) it was impossible to resolve questions, and I think half of us are still just ignoring this feature. So just keep going.

[Andrew Souther]

I am just trying to prove some simple lemmas using this definition, get a sense what the difficulties are, so perhaps that can inform a cleaner definition going forward.

First, I am trying to prove that when there is only one candidate, simple_stable_voting simply outputs the set of candidates. This is the second "case" in teh recursive definition of the function.

I have found that finish does the job, but I want to be more explicit:

import data.set.finite
import tactic

structure election_profile (χ υ : Type*) :=
(candidates : finset χ)
(cpos : 0 < candidates.card)
(voters : finset υ)
(vpos : 0 < voters.card)
(ballots : υ → χ → χ → Prop)

instance {α : Type*} (s : finset α) : decidable s.nonempty :=
begin
  rw ←finset.card_pos,
  apply_instance,
end

def simple_stable_voting' {χ υ : Type*} (voters : finset υ) (ballots : υ → χ → χ → Prop)
  [decidable_eq χ]
  [∀ v, decidable_rel (ballots v)] :
  Π (n : ℕ) (candidates : finset χ) (hn : candidates.card = n) (cpos : 0 < n), finset χ
| 0 _ _ cpos := (nat.not_lt_zero _ cpos).elim
| 1 candidates _ _ := candidates
| (n+2) cands hn cpos :=
let
  -- whether c wins when candidate rem is removed
  still_wins (c rem : χ) (rem_prop : rem ∈ cands) : Prop :=
    c ∈ simple_stable_voting' (n+1) (cands.erase rem)
          (by { rw [finset.card_erase_of_mem, hn]; simp [rem_prop], })
          (by omega),
  -- the margin for candidate c vs c'
  margin (c c' : χ) : ℤ :=
    (voters.filter (λ v, ballots v c c')).card - (voters.filter (λ v, ballots v c' c)).card,
  -- the set of pairs (c, c') of candidates such that when c' is removed, c is a winner.
  viable : finset (χ × χ) := finset.image coe $
    (cands.product cands).attach.filter (λ (p : cands.product cands),
      still_wins p.1.1 p.1.2 (by { cases p, simp at p_property, exact p_property.2, })),
  -- find the maximal margin (using 0 if viable is somehow empty)
  best_margin : ℤ := if hn : viable.nonempty then viable.sup' hn (λ p, margin p.1 p.2) else 0
in finset.image prod.fst $ viable.filter (λ p, margin p.1 p.2 = best_margin)

def simple_stable_voting {χ υ : Type*} (prof : election_profile χ υ)
  [decidable_eq χ] [∀ v, decidable_rel (prof.ballots v)] : finset χ :=
simple_stable_voting' prof.voters prof.ballots prof.candidates.card prof.candidates rfl prof.cpos

lemma ssv_singleton {χ υ : Type*} (prof : election_profile χ υ) (hcands : prof.candidates.card = 1)
  [decidable_eq χ] [∀ v, decidable_rel (prof.ballots v)] :
  simple_stable_voting prof = prof.candidates :=
by unfold simple_stable_voting; finish

[Andrew Souther]

After unfolding simple_stable_voting, how can I actually use hcands to convince Lean we are on that second case of the definition where the number of candidates equals 1?

[Kevin Buzzard]

lemma ssv_singleton {χ υ : Type*} (prof : election_profile χ υ) (hcands : prof.candidates.card = 1)
  [decidable_eq χ] [∀ v, decidable_rel (prof.ballots v)] :
  simple_stable_voting prof = prof.candidates :=
begin
  unfold simple_stable_voting,
  simp [simple_stable_voting', hcands],
end

[Kevin Buzzard]

simp only works too. You're dancing around "motive is not type correct" here if you try to do it manually.

[Kevin Buzzard]

#print prefix simple_stable_voting' gives you access to the things the simplifier knows and which it's hiding from you; looks like simple_stable_voting'._main.equations._eqn_2 is what you want.

[Kevin Buzzard]

You have some complex inductive definition, it's usually best to let the simplifier deal with these foundational issues.

[Kevin Buzzard]

lemma ssv_singleton {χ υ : Type*} (prof : election_profile χ υ) (hcands : prof.candidates.card = 1)
  [decidable_eq χ] [∀ v, decidable_rel (prof.ballots v)] :
  simple_stable_voting prof = prof.candidates :=
begin
  unfold simple_stable_voting,
  convert simple_stable_voting'._main.equations._eqn_2 prof.voters prof.ballots _ hcands (dec_trivial),
  simp only [hcands],
  congr',
end

[Kevin Buzzard]

If you instead of simp only [hcands] you write show_term {simp only [hcands]} you can see the explicit argument it finds. Oh -- refl works instead of congr'.