Grace/Cumulus/Combinatorics/Ballot.g17
Open in Workbench Download source
Imports
List · BinomialMore
Declarations
Source
12345678910module Grace.Cumulus.Combinatorics.Ballot11import List12import BinomialMore13141516def zeroVotes (xs : Set) : Set := listCount{2}(0, xs)17def oneVotes (xs : Set) : Set := listCount{2}(1, xs)1819theorem zero.in_two20 shows 0 ∈ 221proof22 typecheck2324theorem one.in_two25 shows 1 ∈ 226proof27 typecheck2829theorem zeroVotes.nil30 shows zeroVotes([]) = 031proof32 unfold zeroVotes33 exact listCount.nil at 2, 03435theorem oneVotes.nil36 shows oneVotes([]) = 037proof38 unfold oneVotes39 exact listCount.nil at 2, 14041theorem zeroVotes.natural (xs : List(2))42 shows Nat(zeroVotes(xs))43proof44 unfold zeroVotes45 exact listCount.natural at 2, 0, xs with *4647theorem oneVotes.natural (xs : List(2))48 shows Nat(oneVotes(xs))49proof50 unfold oneVotes51 exact listCount.natural at 2, 1, xs with *5253theorem zeroVotes.cons_zero (ys : List(2))54 shows zeroVotes(0 :: ys) = zeroVotes(ys) + 155proof56 have zeroIn := zero.in_two57 have natural := listCount.natural at 2, 0, ys with *58 unfold zeroVotes59 rw listCount.cons_self60 ring6162theorem oneVotes.cons_zero (ys : List(2))63 shows oneVotes(0 :: ys) = oneVotes(ys)64proof65 have zeroIn := zero.in_two66 have different := one.ne_zero67 unfold oneVotes68 exact listCount.cons_other with zeroIn, different6970theorem zeroVotes.cons_one (ys : List(2))71 shows zeroVotes(1 :: ys) = zeroVotes(ys)72proof73 have oneIn := one.in_two74 have different := zero.ne_one75 unfold zeroVotes76 exact listCount.cons_other with oneIn, different7778theorem oneVotes.cons_one (ys : List(2))79 shows oneVotes(1 :: ys) = oneVotes(ys) + 180proof81 have oneIn := one.in_two82 have natural := listCount.natural at 2, 1, ys with *83 unfold oneVotes84 rw listCount.cons_self85 ring868788theorem zeroVotes.add_ones (xs : List(2))89 shows zeroVotes(xs) + oneVotes(xs) = length{2}(xs)90proof91 induction xs92 | List.nil =>93 rw [zeroVotes.nil, oneVotes.nil, length.nil]94 compute95 | List.cons(x, tail) using ih =>96 have element : x ∈ 2 by assumption97 have zerosNat := zeroVotes.natural at tail with *98 have onesNat := oneVotes.natural at tail with *99 rw length.cons100 have alternatives := membership.two.forward with element101 cases alternatives with isZero | isOne102 . rw [isZero, zeroVotes.cons_zero, oneVotes.cons_zero, ← ih]103 ring104 . rw [isOne, zeroVotes.cons_one, oneVotes.cons_one, ← ih]105 ring106107def ballots (n : Nat) → Set108 | zero => {List.nil}109 | succ(k) => consImage(0, ballots(k)) ∪ consImage(1, ballots(k))110111theorem ballots.zero112 shows ballots(0) = {List.nil}113proof114 simp [ballots]115116theorem ballots.succ (k : Nat)117 shows ballots(succ(k)) = consImage(0, ballots(k)) ∪ consImage(1, ballots(k))118proof119 simp [ballots]120121theorem ballots.membership (n : Nat) (xs : Set)122 shows xs ∈ ballots(n) ↔ List(2, xs) ∧ length{2}(xs) = n123proof124 induction n generalizing xs125 | zero =>126 intro xs127 rw ballots.zero128 constructor129 . intro hx130 have equal := singleton.membership.forward with hx131 rw equal132 constructor133 . typecheck134 . exact length.nil at 2135 . intro hx136 obtain ⟨list, zero⟩ := hx137 have equal := length.eq_zero at 2, xs with list, zero138 rw equal139 apply singleton.membership.backward140 rfl141 | succ(k) using ih =>142 intro xs143 rw ballots.succ144 have zeroIn := zero.in_two145 have oneIn := one.in_two146 constructor147 . intro hx148 have split := union2.membership.forward with hx149 cases split with inZero | inOne150 . obtain ⟨ys, hy, shape⟩ := consImage.membership.forward with inZero151 have parts := ih with ys152 obtain ⟨list, len⟩ := parts.forward with hy153 rw ← shape154 constructor155 . typecheck156 . rw [length.cons, len]157 rfl158 . obtain ⟨ys, hy, shape⟩ := consImage.membership.forward with inOne159 have parts := ih with ys160 obtain ⟨list, len⟩ := parts.forward with hy161 rw ← shape162 constructor163 . typecheck164 . rw [length.cons, len]165 rfl166 . intro hx167 obtain ⟨list, len⟩ := hx168 have shape := List.cases at 2, xs with *169 cases shape with isNil | isCons170 . rw [isNil, length.nil] at len171 exfalso172 arith173 . obtain ⟨x, hx2, tail, tailList, xsShape⟩ := isCons174 rw [xsShape, length.cons] at len175 have tailLen := Naturals.injective.succ with len176 have parts := ih with tail177 have tailIn := parts.backward with ⟨tailList, tailLen⟩178 apply union2.membership.backward179 have alternatives := membership.two.forward with hx2180 cases alternatives with isZero | isOne181 . left182 apply consImage.membership.backward183 witness tail184 constructor185 . exact tailIn186 . rw [xsShape, isZero]187 rfl188 . right189 apply consImage.membership.backward190 witness tail191 constructor192 . exact tailIn193 . rw [xsShape, isOne]194 rfl195196theorem ballots.finite (n : Nat)197 shows Finite(ballots(n))198proof199 induction n200 | zero =>201 rw ballots.zero202 exact Finite.singleton at List.nil203 | succ(k) using ih =>204 rw ballots.succ205 have left := consImage.finite at 0, ballots(k) with ih206 have right := consImage.finite at 1, ballots(k) with ih207 exact Finite.union with left, right208209210211212predicate AheadBy (k xs : Set) :=213 ∀ ys, List(2, ys) → ListPrefix(2, ys, xs) → ys ≠ [] →214 oneVotes(ys) < zeroVotes(ys) + k215216predicate AlwaysAhead (xs : Set) :=217 ∀ ys, List(2, ys) → ListPrefix(2, ys, xs) → ys ≠ [] →218 oneVotes(ys) < zeroVotes(ys)219220theorem AlwaysAhead.iff (xs : Set)221 shows AlwaysAhead(xs) ↔ AheadBy(0, xs)222proof223 constructor224 . intro ahead225 unfold AlwaysAhead at ahead226 unfold AheadBy227 intros ys list prefix nonempty228 have bound := ahead with ys, list, prefix, nonempty229 have zerosNat := zeroVotes.natural at ys with *230 have shape : zeroVotes(ys) + 0 = zeroVotes(ys) := add.right_unit at zeroVotes(ys)231 rw shape232 exact bound233 . intro ahead234 unfold AheadBy at ahead235 unfold AlwaysAhead236 intros ys list prefix nonempty237 have bound := ahead with ys, list, prefix, nonempty238 have zerosNat := zeroVotes.natural at ys with *239 have shape : zeroVotes(ys) + 0 = zeroVotes(ys) := add.right_unit at zeroVotes(ys)240 rw shape at bound241 exact bound242243theorem AheadBy.nil (k : Nat)244 shows AheadBy(k, [])245proof246 unfold AheadBy247 intros ys list prefix nonempty248 obtain ⟨zs, zsList, equal⟩ := prefix249 symm at equal250 have parts := append.eq_nil with equal251 exfalso252 exact nonempty with parts.left253254theorem AheadBy.cons_zero (k : Nat) (ys : List(2))255 shows AheadBy(k, 0 :: ys) ↔ AheadBy(k + 1, ys)256proof257 have zeroIn := zero.in_two258 constructor259 . intro ahead260 unfold AheadBy at ahead261 unfold AheadBy262 intros zs list prefix nonempty263 have prefixCons := ListPrefix.cons with zeroIn, prefix264 have nonemptyCons := List.cons_ne_nil at 2, 0, zs with *265 have consList : List(2, 0 :: zs) by typecheck266 have bound := ahead with 0 :: zs, consList, prefixCons, nonemptyCons267 rw [oneVotes.cons_zero, zeroVotes.cons_zero] at bound268 have zerosNat := zeroVotes.natural at zs with *269 have shape : zeroVotes(zs) + 1 + k = zeroVotes(zs) + (k + 1) by ring270 rw shape at bound271 exact bound272 . intro ahead273 unfold AheadBy at ahead274 unfold AheadBy275 intros zs list prefix nonempty276 have shape := List.cases at 2, zs with *277 cases shape with isNil | isCons278 . exfalso279 exact nonempty with isNil280 . obtain ⟨z, hz, tail, tailList, zsShape⟩ := isCons281 rw zsShape at prefix282 obtain ⟨rest, restList, consShape, tailPrefix⟩ :=283 ListPrefix.of_cons with hz, prefix284 obtain ⟨zIs, ysIs⟩ := List.inductive.injective.cons with consShape285 rw ← ysIs at tailPrefix286 rw [zsShape, ← zIs, oneVotes.cons_zero, zeroVotes.cons_zero]287 have zerosNat := zeroVotes.natural at tail with *288 have onesNat := oneVotes.natural at tail with *289 have tailShape := List.cases at 2, tail with *290 cases tailShape with tailNil | tailCons291 . rw [tailNil, oneVotes.nil, zeroVotes.nil]292 arith293 . obtain ⟨w, hw, more, moreList, tailIs⟩ := tailCons294 have tailNonempty : tail ≠ []295 rw tailIs296 exact List.cons_ne_nil at 2, w, more with *297 have bound := ahead with tail, tailList, tailPrefix, tailNonempty298 have reshape : zeroVotes(tail) + (k + 1) = zeroVotes(tail) + 1 + k by ring299 rw reshape at bound300 exact bound301302theorem AheadBy.cons_one (k : Nat) (ys : List(2))303 shows AheadBy(k + 2, 1 :: ys) ↔ AheadBy(k + 1, ys)304proof305 have oneIn := one.in_two306 constructor307 . intro ahead308 unfold AheadBy at ahead309 unfold AheadBy310 intros zs list prefix nonempty311 have prefixCons := ListPrefix.cons with oneIn, prefix312 have nonemptyCons := List.cons_ne_nil at 2, 1, zs with *313 have consList : List(2, 1 :: zs) by typecheck314 have bound := ahead with 1 :: zs, consList, prefixCons, nonemptyCons315 rw [oneVotes.cons_one, zeroVotes.cons_one] at bound316 have zerosNat := zeroVotes.natural at zs with *317 have onesNat := oneVotes.natural at zs with *318 arith319 . intro ahead320 unfold AheadBy at ahead321 unfold AheadBy322 intros zs list prefix nonempty323 have shape := List.cases at 2, zs with *324 cases shape with isNil | isCons325 . exfalso326 exact nonempty with isNil327 . obtain ⟨z, hz, tail, tailList, zsShape⟩ := isCons328 rw zsShape at prefix329 obtain ⟨rest, restList, consShape, tailPrefix⟩ :=330 ListPrefix.of_cons with hz, prefix331 obtain ⟨zIs, ysIs⟩ := List.inductive.injective.cons with consShape332 rw ← ysIs at tailPrefix333 rw [zsShape, ← zIs, oneVotes.cons_one, zeroVotes.cons_one]334 have zerosNat := zeroVotes.natural at tail with *335 have onesNat := oneVotes.natural at tail with *336 have tailShape := List.cases at 2, tail with *337 cases tailShape with tailNil | tailCons338 . rw [tailNil, oneVotes.nil, zeroVotes.nil]339 arith340 . obtain ⟨w, hw, more, moreList, tailIs⟩ := tailCons341 have tailNonempty : tail ≠ []342 rw tailIs343 exact List.cons_ne_nil at 2, w, more with *344 have bound := ahead with tail, tailList, tailPrefix, tailNonempty345 arith346347theorem AheadBy.not_cons_one (k : Nat) (ys : List(2))348 requires low : k ≤ 1349 shows ¬AheadBy(k, 1 :: ys)350proof351 have oneIn := one.in_two352 intro ahead353 unfold AheadBy at ahead354 have prefixNil := ListPrefix.nil at 2, ys with *355 have prefixOne := ListPrefix.cons with oneIn, prefixNil356 have nonempty := List.cons_ne_nil at 2, 1, [] with *357 have oneList : List(2, 1 :: []) by typecheck358 have bound := ahead with 1 :: [], oneList, prefixOne, nonempty359 have nilList : List(2, []) by typecheck360 have onesOne := oneVotes.cons_one at [] with nilList361 have zerosOne := zeroVotes.cons_one at [] with nilList362 rw [onesOne, zerosOne, oneVotes.nil, zeroVotes.nil] at bound363 arith364365366367def leadSequences (k a b : Nat) : Set :=368 { xs ∈ ballots(a + b) | zeroVotes(xs) = a ∧ oneVotes(xs) = b ∧ AheadBy(k, xs) }369370def ballotSequences (a b : Nat) : Set :=371 { xs ∈ ballots(a + b) | zeroVotes(xs) = a ∧ AlwaysAhead(xs) }372373theorem leadSequences.finite (k a b : Nat)374 shows Finite(leadSequences(k, a, b))375proof376 have subset : leadSequences(k, a, b) ⊆ ballots(a + b)377 intros xs hx378 have parts := leadSequences.membership.forward with hx379 exact parts.left380 exact Finite.subset with (ballots.finite at a + b), subset381382theorem ballotSequences.finite (a b : Nat)383 shows Finite(ballotSequences(a, b))384proof385 have subset : ballotSequences(a, b) ⊆ ballots(a + b)386 intros xs hx387 have parts := ballotSequences.membership.forward with hx388 exact parts.left389 exact Finite.subset with (ballots.finite at a + b), subset390391392393def headZero (k a b : Nat) : Set :=394 { xs ∈ leadSequences(k, a, b) | ∃ ys, 0 :: ys = xs }395396def headOne (k a b : Nat) : Set :=397 { xs ∈ leadSequences(k, a, b) | ∃ ys, 1 :: ys = xs }398399theorem headZero.subset (k a b : Nat)400 shows headZero(k, a, b) ⊆ leadSequences(k, a, b)401proof402 intros xs hx403 have parts := headZero.membership.forward with hx404 exact parts.left405406theorem headOne.subset (k a b : Nat)407 shows headOne(k, a, b) ⊆ leadSequences(k, a, b)408proof409 intros xs hx410 have parts := headOne.membership.forward with hx411 exact parts.left412413414theorem leadSequences.split (k a b : Nat)415 requires positive : 0 < a + b416 shows cardinality(leadSequences(k, a, b)) =417 cardinality(headZero(k, a, b)) + cardinality(headOne(k, a, b))418proof419 have finite := leadSequences.finite at k, a, b420 have zeroSubset := headZero.subset at k, a, b421 have oneSubset := headOne.subset at k, a, b422 have finiteZero := Finite.subset with finite, zeroSubset423 have finiteOne := Finite.subset with finite, oneSubset424 have disjoint : Disjoint(headZero(k, a, b), headOne(k, a, b))425 apply Disjoint.iff.backward426 intros xs hx inOne427 have zeroParts := headZero.membership.forward with hx428 have oneParts := headOne.membership.forward with inOne429 obtain ⟨ys, ysShape⟩ := zeroParts.right430 obtain ⟨zs, zsShape⟩ := oneParts.right431 rw ← ysShape at zsShape432 obtain ⟨headEqual, tailEqual⟩ :=433 List.inductive.injective.cons with zsShape434 exact one.ne_zero with headEqual435 have union : leadSequences(k, a, b) = headZero(k, a, b) ∪ headOne(k, a, b)436 ext xs437 constructor438 . intro hx439 have parts := leadSequences.membership.forward with hx440 obtain ⟨list, len⟩ := ballots.membership.forward with parts.left441 have shape := List.cases at 2, xs with *442 apply union2.membership.backward443 cases shape with isNil | isCons444 . exfalso445 rw [isNil, length.nil] at len446 arith447 . obtain ⟨x, hx2, tail, tailList, xsShape⟩ := isCons448 have alternatives := membership.two.forward with hx2449 cases alternatives with isZero | isOne450 . left451 apply headZero.membership.backward452 constructor453 . exact hx454 . witness tail455 rw [xsShape, isZero]456 rfl457 . right458 apply headOne.membership.backward459 constructor460 . exact hx461 . witness tail462 rw [xsShape, isOne]463 rfl464 . intro hx465 have split := union2.membership.forward with hx466 unfold Subset at zeroSubset467 unfold Subset at oneSubset468 cases split with inZero | inOne469 . exact zeroSubset with xs, inZero470 . exact oneSubset with xs, inOne471 rw union472 exact cardinality.union_disjoint with finiteZero, finiteOne, disjoint473474475476theorem headZero.succ (k a b : Nat)477 shows headZero(k, a + 1, b) = consImage(0, leadSequences(k + 1, a, b))478proof479 have zeroIn := zero.in_two480 ext xs481 constructor482 . intro hx483 have parts := headZero.membership.forward with hx484 obtain ⟨ys, ysShape⟩ := parts.right485 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=486 leadSequences.membership.forward with parts.left487 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots488 rw ← ysShape at list489 obtain ⟨headIn, ysList⟩ := List.cons_parts with list490 rw ← ysShape at len491 rw ← ysShape at zerosIs492 rw ← ysShape at onesIs493 rw ← ysShape at ahead494 rw [length.cons] at len495 rw zeroVotes.cons_zero at zerosIs496 rw oneVotes.cons_zero at onesIs497 have iff := AheadBy.cons_zero at k, ys with *498 have zerosNat := zeroVotes.natural at ys with *499 apply consImage.membership.backward500 witness ys501 constructor502 . apply leadSequences.membership.backward503 refine ⟨?_, ?_, ?_, ?_⟩504 . apply ballots.membership.backward505 constructor506 . exact ysList507 . have shape : a + 1 + b = succ(a + b) by ring508 rw shape at len509 exact Naturals.injective.succ with len510 . exact add.right_cancel at zeroVotes(ys), a, 1 with zerosIs511 . exact onesIs512 . exact iff.forward with ahead513 . exact ysShape514 . intro hx515 obtain ⟨ys, hy, ysShape⟩ := consImage.membership.forward with hx516 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=517 leadSequences.membership.forward with hy518 obtain ⟨ysList, len⟩ := ballots.membership.forward with inBallots519 have iff := AheadBy.cons_zero at k, ys with *520 apply headZero.membership.backward521 constructor522 . apply leadSequences.membership.backward523 rw ← ysShape524 refine ⟨?_, ?_, ?_, ?_⟩525 . apply ballots.membership.backward526 constructor527 . typecheck528 . rw [length.cons, len]529 ring530 . rw [zeroVotes.cons_zero, zerosIs]531 rfl532 . rw oneVotes.cons_zero533 exact onesIs534 . exact iff.backward with ahead535 . witness ys536 exact ysShape537538theorem headZero.zero (k b : Nat)539 shows headZero(k, 0, b) = ∅540proof541 ext xs542 constructor543 . intro hx544 exfalso545 have parts := headZero.membership.forward with hx546 obtain ⟨ys, ysShape⟩ := parts.right547 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=548 leadSequences.membership.forward with parts.left549 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots550 rw ← ysShape at list551 obtain ⟨headIn, ysList⟩ := List.cons_parts with list552 rw [← ysShape, zeroVotes.cons_zero] at zerosIs553 have zerosNat := zeroVotes.natural at ys with *554 arith555 . intro hx556 exact empty.subset at headZero(k, 0, b) with xs, hx557558559theorem headOne.succ (k a b : Nat)560 shows headOne(k + 2, a, b + 1) = consImage(1, leadSequences(k + 1, a, b))561proof562 have oneIn := one.in_two563 ext xs564 constructor565 . intro hx566 have parts := headOne.membership.forward with hx567 obtain ⟨ys, ysShape⟩ := parts.right568 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=569 leadSequences.membership.forward with parts.left570 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots571 rw ← ysShape at list572 obtain ⟨headIn, ysList⟩ := List.cons_parts with list573 rw ← ysShape at len574 rw ← ysShape at zerosIs575 rw ← ysShape at onesIs576 rw ← ysShape at ahead577 rw [length.cons] at len578 rw zeroVotes.cons_one at zerosIs579 rw oneVotes.cons_one at onesIs580 have iff := AheadBy.cons_one at k, ys with *581 have onesNat := oneVotes.natural at ys with *582 apply consImage.membership.backward583 witness ys584 constructor585 . apply leadSequences.membership.backward586 refine ⟨?_, ?_, ?_, ?_⟩587 . apply ballots.membership.backward588 constructor589 . exact ysList590 . have shape : a + (b + 1) = succ(a + b) by ring591 rw shape at len592 exact Naturals.injective.succ with len593 . exact zerosIs594 . exact add.right_cancel at oneVotes(ys), b, 1 with onesIs595 . exact iff.forward with ahead596 . exact ysShape597 . intro hx598 obtain ⟨ys, hy, ysShape⟩ := consImage.membership.forward with hx599 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=600 leadSequences.membership.forward with hy601 obtain ⟨ysList, len⟩ := ballots.membership.forward with inBallots602 have iff := AheadBy.cons_one at k, ys with *603 apply headOne.membership.backward604 constructor605 . apply leadSequences.membership.backward606 rw ← ysShape607 refine ⟨?_, ?_, ?_, ?_⟩608 . apply ballots.membership.backward609 constructor610 . typecheck611 . rw [length.cons, len]612 ring613 . rw zeroVotes.cons_one614 exact zerosIs615 . rw [oneVotes.cons_one, onesIs]616 rfl617 . exact iff.backward with ahead618 . witness ys619 exact ysShape620621622theorem headOne.low (k a b : Nat)623 requires low : k ≤ 1624 shows headOne(k, a, b) = ∅625proof626 ext xs627 constructor628 . intro hx629 exfalso630 have parts := headOne.membership.forward with hx631 obtain ⟨ys, ysShape⟩ := parts.right632 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=633 leadSequences.membership.forward with parts.left634 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots635 rw ← ysShape at list636 obtain ⟨headIn, ysList⟩ := List.cons_parts with list637 rw ← ysShape at ahead638 have blocked := AheadBy.not_cons_one at k, ys with *639 exact blocked with ahead640 . intro hx641 exact empty.subset at headOne(k, a, b) with xs, hx642643theorem headOne.zero (k a : Nat)644 shows headOne(k, a, 0) = ∅645proof646 ext xs647 constructor648 . intro hx649 exfalso650 have parts := headOne.membership.forward with hx651 obtain ⟨ys, ysShape⟩ := parts.right652 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=653 leadSequences.membership.forward with parts.left654 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots655 rw ← ysShape at list656 obtain ⟨headIn, ysList⟩ := List.cons_parts with list657 rw [← ysShape, oneVotes.cons_one] at onesIs658 have onesNat := oneVotes.natural at ys with *659 arith660 . intro hx661 exact empty.subset at headOne(k, a, 0) with xs, hx662663664theorem leadSequences.nil (k : Nat)665 shows leadSequences(k, 0, 0) = {[]}666proof667 have nilList : List(2, []) by typecheck668 have shape : (0:N) + 0 = 0 by compute669 ext xs670 constructor671 . intro hx672 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=673 leadSequences.membership.forward with hx674 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots675 rw shape at len676 have equal := length.eq_zero at 2, xs with list, len677 rw equal678 apply singleton.membership.backward679 rfl680 . intro hx681 have equal := singleton.membership.forward with hx682 rw equal683 apply leadSequences.membership.backward684 refine ⟨?_, zeroVotes.nil, oneVotes.nil, AheadBy.nil at k⟩685 apply ballots.membership.backward686 rw [shape, length.nil]687 exact ⟨nilList, rfl⟩688689theorem leadSequences.nil_count (k : Nat)690 shows cardinality(leadSequences(k, 0, 0)) = 1691proof692 rw leadSequences.nil693 exact cardinality.singleton at []694695696697698theorem leadSequences.closed_form (n k a b : Nat)699 requires total : a + b = n700 requires bound : b ≤ a + k701 shows cardinality(leadSequences(k + 1, a, b)) + (n choose (a + k + 1)) =702 n choose a703proof704 induction n generalizing k a b705 | zero =>706 intros k a b kNat aNat bNat total bound707 obtain ⟨aZero, bZero⟩ := add.eq_zero at b, a with total708 rw [aZero, bZero, leadSequences.nil_count]709 have shape : (0:N) + k + 1 = succ(k) by ring710 rw [shape, choose.zero_left, choose.zero_right]711 compute712 | succ(m) using ih =>713 intros k a b kNat aNat bNat total bound714 have positive : 0 < a + b by arith715 have split := leadSequences.split at k + 1, a, b with positive716 have aShape := natural.zero_or_successor with aNat717 have bShape := natural.zero_or_successor with bNat718 have kShape := natural.zero_or_successor with kNat719 cases aShape with aZero | aSucc720 . 721 rw aZero at total722 rw aZero at bound723 rw aZero at split724 rw aZero725 cases bShape with bZero | bSucc726 . exfalso727 rw bZero at total728 arith729 . obtain ⟨b2, b2Nat, rfl⟩ := bSucc730 cases kShape with kZero | kSucc731 . exfalso732 rw kZero at bound733 arith734 . obtain ⟨k2, k2Nat, rfl⟩ := kSucc735 have mIs : b2 = m736 have shape : (0:N) + succ(b2) = succ(b2) :=737 add.left_unit at succ(b2)738 rw shape at total739 exact Naturals.injective.succ with total740 have zeroCount : cardinality(headZero(succ(k2) + 1, 0, succ(b2))) = 0741 rw headZero.zero742 exact cardinality.empty743 have oneShape : headOne(succ(k2) + 1, 0, succ(b2)) =744 consImage(1, leadSequences(k2 + 1, 0, b2))745 have kForm : succ(k2) + 1 = k2 + 2 by ring746 have bForm : succ(b2) = b2 + 1 by ring747 rw [kForm, bForm]748 exact headOne.succ at k2, 0, b2749 have oneCount : cardinality(headOne(succ(k2) + 1, 0, succ(b2))) =750 cardinality(leadSequences(k2 + 1, 0, b2))751 rw oneShape752 exact consImage.cardinality with753 (leadSequences.finite at k2 + 1, 0, b2)754 have zeroNat : Nat(0) by typecheck755 have total2 : (0:N) + b2 = m756 rw ← mIs757 exact add.left_unit at b2758 have bound2 : b2 ≤ 0 + k2 by arith759 have inner := ih with k2, 0, b2, k2Nat, zeroNat, b2Nat, total2, bound2760 have vanish : m choose (0 + k2 + 1) = 0761 have form : (0:N) + k2 + 1 = succ(k2) by ring762 have le : m ≤ k2 by arith763 rw form764 exact choose.vanishes with le765 have vanishNext : succ(m) choose (0 + succ(k2) + 1) = 0766 have form : (0:N) + succ(k2) + 1 = succ(succ(k2)) by ring767 have le : succ(m) ≤ succ(k2) by arith768 rw form769 exact choose.vanishes with le770 have cardNat := cardinality.nat with771 (leadSequences.finite at k2 + 1, 0, b2)772 rw [vanish, choose.zero_right] at inner773 rw [split, zeroCount, oneCount, vanishNext, choose.zero_right]774 ring [inner]775 . obtain ⟨a2, a2Nat, rfl⟩ := aSucc776 cases bShape with bZero | bSucc777 . 778 rw bZero at total779 rw bZero at bound780 rw bZero at split781 rw bZero782 have saNat : Nat(succ(a2)) by typecheck783 have mIs : a2 = m784 have shape : succ(a2) + 0 = succ(a2) := add.right_unit at succ(a2)785 rw shape at total786 exact Naturals.injective.succ with total787 have oneCount : cardinality(headOne(k + 1, succ(a2), 0)) = 0788 rw headOne.zero789 exact cardinality.empty790 have zeroShape : headZero(k + 1, succ(a2), 0) =791 consImage(0, leadSequences(k + 1 + 1, a2, 0))792 have aForm : succ(a2) = a2 + 1 by ring793 rw aForm794 exact headZero.succ at k + 1, a2, 0795 have zeroCount : cardinality(headZero(k + 1, succ(a2), 0)) =796 cardinality(leadSequences(k + 1 + 1, a2, 0))797 rw zeroShape798 exact consImage.cardinality with799 (leadSequences.finite at k + 1 + 1, a2, 0)800 have zeroNat : Nat(0) by typecheck801 have kNat2 : Nat(k + 1) by typecheck802 have total2 : a2 + 0 = m803 rw ← mIs804 exact add.right_unit at a2805 have bound2 : 0 ≤ a2 + (k + 1) by arith806 have inner := ih with k + 1, a2, 0, kNat2, a2Nat, zeroNat, total2,807 bound2808 have vanish : m choose (a2 + (k + 1) + 1) = 0809 have form : a2 + (k + 1) + 1 = succ(a2 + (k + 1)) by ring810 have le : m ≤ a2 + (k + 1) by arith811 rw form812 exact choose.vanishes with le813 have vanishNext : succ(m) choose (succ(a2) + k + 1) = 0814 have form : succ(a2) + k + 1 = succ(succ(a2) + k) by ring815 have le : succ(m) ≤ succ(a2) + k by arith816 rw form817 exact choose.vanishes with le818 have diagonal : m choose a2 = 1819 rw mIs820 exact choose.diagonal at m821 have diagonalNext : succ(m) choose succ(a2) = 1822 rw mIs823 exact choose.diagonal at succ(m)824 have cardNat := cardinality.nat with825 (leadSequences.finite at k + 1 + 1, a2, 0)826 rw [vanish, diagonal] at inner827 rw [split, zeroCount, oneCount, vanishNext, diagonalNext]828 ring [inner]829 . obtain ⟨b2, b2Nat, rfl⟩ := bSucc830 cases kShape with kZero | kSucc831 . 832 rw kZero at bound833 rw kZero at split834 rw kZero835 have mIs : a2 + succ(b2) = m836 have shape : succ(a2) + succ(b2) = succ(a2 + succ(b2)) by ring837 rw shape at total838 exact Naturals.injective.succ with total839 have oneCount : cardinality(headOne(0 + 1, succ(a2), succ(b2))) = 0840 have low : (0:N) + 1 ≤ 1 by arith841 have empty := headOne.low at 0 + 1, succ(a2), succ(b2) with low842 rw empty843 exact cardinality.empty844 have zeroShape : headZero(0 + 1, succ(a2), succ(b2)) =845 consImage(0, leadSequences(0 + 1 + 1, a2, succ(b2)))846 have aForm : succ(a2) = a2 + 1 by ring847 rw aForm848 exact headZero.succ at 0 + 1, a2, succ(b2)849 have zeroCount : cardinality(headZero(0 + 1, succ(a2), succ(b2))) =850 cardinality(leadSequences(0 + 1 + 1, a2, succ(b2)))851 rw zeroShape852 exact consImage.cardinality with853 (leadSequences.finite at 0 + 1 + 1, a2, succ(b2))854 have oneNat : Nat(0 + 1) by typecheck855 have sbNat : Nat(succ(b2)) by typecheck856 have bound2 : succ(b2) ≤ a2 + (0 + 1) by arith857 have inner := ih with 0 + 1, a2, succ(b2), oneNat, a2Nat, sbNat, mIs,858 bound2859 have pascalA : succ(m) choose succ(a2) =860 (m choose a2) + (m choose succ(a2)) := choose.succ_succ at m, a2861 have pascalB : succ(m) choose (succ(a2) + 0 + 1) =862 (m choose succ(a2)) + (m choose succ(succ(a2)))863 have form : succ(a2) + 0 + 1 = succ(succ(a2)) by ring864 rw form865 exact choose.succ_succ at m, succ(a2)866 have innerForm : a2 + (0 + 1) + 1 = succ(succ(a2)) by ring867 rw innerForm at inner868 have cardNat := cardinality.nat with869 (leadSequences.finite at 0 + 1 + 1, a2, succ(b2))870 have firstNat := choose.natural at m, a2871 have secondNat := choose.natural at m, succ(a2)872 have thirdNat := choose.natural at m, succ(succ(a2))873 rw [split, zeroCount, oneCount, pascalB, pascalA]874 ring [inner]875 . 876 obtain ⟨k2, k2Nat, rfl⟩ := kSucc877 have mIs : a2 + succ(b2) = m878 have shape : succ(a2) + succ(b2) = succ(a2 + succ(b2)) by ring879 rw shape at total880 exact Naturals.injective.succ with total881 have mIs2 : succ(a2) + b2 = m882 have shape : succ(a2) + succ(b2) = succ(succ(a2) + b2) by ring883 rw shape at total884 exact Naturals.injective.succ with total885 have zeroShape : headZero(succ(k2) + 1, succ(a2), succ(b2)) =886 consImage(0, leadSequences(succ(k2) + 1 + 1, a2, succ(b2)))887 have aForm : succ(a2) = a2 + 1 by ring888 rw aForm889 exact headZero.succ at succ(k2) + 1, a2, succ(b2)890 have zeroCount :891 cardinality(headZero(succ(k2) + 1, succ(a2), succ(b2))) =892 cardinality(leadSequences(succ(k2) + 1 + 1, a2, succ(b2)))893 rw zeroShape894 exact consImage.cardinality with895 (leadSequences.finite at succ(k2) + 1 + 1, a2, succ(b2))896 have oneShape : headOne(succ(k2) + 1, succ(a2), succ(b2)) =897 consImage(1, leadSequences(k2 + 1, succ(a2), b2))898 have kForm : succ(k2) + 1 = k2 + 2 by ring899 have bForm : succ(b2) = b2 + 1 by ring900 rw [kForm, bForm]901 exact headOne.succ at k2, succ(a2), b2902 have oneCount :903 cardinality(headOne(succ(k2) + 1, succ(a2), succ(b2))) =904 cardinality(leadSequences(k2 + 1, succ(a2), b2))905 rw oneShape906 exact consImage.cardinality with907 (leadSequences.finite at k2 + 1, succ(a2), b2)908 have kNat2 : Nat(succ(k2) + 1) by typecheck909 have sbNat : Nat(succ(b2)) by typecheck910 have saNat : Nat(succ(a2)) by typecheck911 have bound0 : succ(b2) ≤ a2 + (succ(k2) + 1) by arith912 have bound1 : b2 ≤ succ(a2) + k2 by arith913 have inner0 := ih with succ(k2) + 1, a2, succ(b2), kNat2, a2Nat,914 sbNat, mIs, bound0915 have inner1 := ih with k2, succ(a2), b2, k2Nat, saNat, b2Nat, mIs2,916 bound1917 have pascalA : succ(m) choose succ(a2) =918 (m choose a2) + (m choose succ(a2)) := choose.succ_succ at m, a2919 have pascalB : succ(m) choose (succ(a2) + succ(k2) + 1) =920 (m choose (succ(a2) + k2 + 1)) +921 (m choose succ(succ(a2) + k2 + 1))922 have form : succ(a2) + succ(k2) + 1 = succ(succ(a2) + k2 + 1)923 ring924 rw form925 exact choose.succ_succ at m, succ(a2) + k2 + 1926 have innerForm : a2 + (succ(k2) + 1) + 1 = succ(succ(a2) + k2 + 1)927 ring928 rw innerForm at inner0929 have cardNat0 := cardinality.nat with930 (leadSequences.finite at succ(k2) + 1 + 1, a2, succ(b2))931 have cardNat1 := cardinality.nat with932 (leadSequences.finite at k2 + 1, succ(a2), b2)933 have firstNat := choose.natural at m, a2934 have secondNat := choose.natural at m, succ(a2)935 have thirdNat := choose.natural at m, succ(a2) + k2 + 1936 have fourthNat := choose.natural at m, succ(succ(a2) + k2 + 1)937 rw [split, zeroCount, oneCount, pascalB, pascalA]938 ring [inner0, inner1]939940941942theorem ballotSequences.eq (a b : Nat)943 shows ballotSequences(a + 1, b) = consImage(0, leadSequences(1, a, b))944proof945 have zeroIn := zero.in_two946 have form : (0:N) + 1 = 1 by compute947 ext xs948 constructor949 . intro hx950 obtain ⟨inBallots, zerosIs, ahead⟩ :=951 ballotSequences.membership.forward with hx952 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots953 have shape := List.cases at 2, xs with *954 cases shape with isNil | isCons955 . exfalso956 rw [isNil, length.nil] at len957 arith958 . obtain ⟨x, hx2, tail, tailList, xsShape⟩ := isCons959 have iff := AlwaysAhead.iff at xs960 have aheadBy := iff.forward with ahead961 rw xsShape at aheadBy962 have alternatives := membership.two.forward with hx2963 cases alternatives with isZero | isOne964 . rw isZero at xsShape965 rw isZero at aheadBy966 rw xsShape at len967 rw xsShape at zerosIs968 rw [length.cons] at len969 rw zeroVotes.cons_zero at zerosIs970 have zerosNat := zeroVotes.natural at tail with *971 have onesNat := oneVotes.natural at tail with *972 have tailLen : length{2}(tail) = a + b973 have reshape : a + 1 + b = succ(a + b) by ring974 rw reshape at len975 exact Naturals.injective.succ with len976 have tailZeros : zeroVotes(tail) = a :=977 add.right_cancel at zeroVotes(tail), a, 1 with zerosIs978 have tailOnes : oneVotes(tail) = b979 have sum := zeroVotes.add_ones at tail with *980 rw [tailLen, tailZeros] at sum981 exact add.left_cancel at oneVotes(tail), b, a with sum982 have consIff := AheadBy.cons_zero at 0, tail with *983 have tailAhead := consIff.forward with aheadBy984 rw form at tailAhead985 apply consImage.membership.backward986 witness tail987 constructor988 . apply leadSequences.membership.backward989 refine ⟨?_, tailZeros, tailOnes, tailAhead⟩990 apply ballots.membership.backward991 exact ⟨tailList, tailLen⟩992 . symm993 exact xsShape994 . exfalso995 rw isOne at aheadBy996 have low : (0:N) ≤ 1 by arith997 have blocked := AheadBy.not_cons_one at 0, tail with *998 exact blocked with aheadBy999 . intro hx1000 obtain ⟨ys, hy, ysShape⟩ := consImage.membership.forward with hx1001 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=1002 leadSequences.membership.forward with hy1003 obtain ⟨ysList, len⟩ := ballots.membership.forward with inBallots1004 rw ← form at ahead1005 have consIff := AheadBy.cons_zero at 0, ys with *1006 have consAhead := consIff.backward with ahead1007 have iff := AlwaysAhead.iff at 0 :: ys1008 apply ballotSequences.membership.backward1009 rw ← ysShape1010 refine ⟨?_, ?_, iff.backward with consAhead⟩1011 . apply ballots.membership.backward1012 constructor1013 . typecheck1014 . rw [length.cons, len]1015 ring1016 . rw [zeroVotes.cons_zero, zerosIs]1017 rfl1018101910201021theorem ballotSequences.count_succ (a b : Nat)1022 requires le : b ≤ a1023 shows cardinality(ballotSequences(a + 1, b)) + ((a + b) choose (a + 1)) =1024 (a + b) choose a1025proof1026 have zeroNat : Nat(0) by typecheck1027 have total : a + b = a + b by rfl1028 have bound : b ≤ a + 0 by arith1029 have closed := leadSequences.closed_form at a + b, 0, a, b with total, bound1030 have formK : (0:N) + 1 = 1 by compute1031 have formA : a + 0 + 1 = a + 1 by ring1032 rw [formK, formA] at closed1033 rw [ballotSequences.eq, consImage.cardinality]1034 exact closed1035103610371038def orderings (a b : Nat) : Set := { xs ∈ ballots(a + b) | zeroVotes(xs) = a }10391040theorem orderings.finite (a b : Nat)1041 shows Finite(orderings(a, b))1042proof1043 have subset : orderings(a, b) ⊆ ballots(a + b)1044 intros xs hx1045 have parts := orderings.membership.forward with hx1046 exact parts.left1047 exact Finite.subset with (ballots.finite at a + b), subset10481049theorem ballotSequences.subset_orderings (a b : Nat)1050 shows ballotSequences(a, b) ⊆ orderings(a, b)1051proof1052 intros xs hx1053 obtain ⟨inBallots, zerosIs, ahead⟩ :=1054 ballotSequences.membership.forward with hx1055 apply orderings.membership.backward1056 exact ⟨inBallots, zerosIs⟩10571058theorem oneVotes.prefix_le (ys xs : List(2))1059 requires prefix : ListPrefix(2, ys, xs)1060 shows oneVotes(ys) ≤ oneVotes(xs)1061proof1062 have le := ListPrefix.count_le at 2, 1, ys, xs with prefix1063 unfold oneVotes1064 exact le10651066theorem orderings.eq (a b : Nat)1067 shows orderings(a, b) = leadSequences(b + 1, a, b)1068proof1069 ext xs1070 constructor1071 . intro hx1072 obtain ⟨inBallots, zerosIs⟩ := orderings.membership.forward with hx1073 obtain ⟨list, len⟩ := ballots.membership.forward with inBallots1074 have onesIs : oneVotes(xs) = b1075 have sum := zeroVotes.add_ones at xs with *1076 rw [len, zerosIs] at sum1077 exact add.left_cancel at oneVotes(xs), b, a with sum1078 apply leadSequences.membership.backward1079 refine ⟨inBallots, zerosIs, onesIs, ?_⟩1080 unfold AheadBy1081 intros ys ysList prefix nonempty1082 have le := oneVotes.prefix_le with prefix1083 have zerosNat := zeroVotes.natural at ys with *1084 have onesNat := oneVotes.natural at ys with *1085 rw onesIs at le1086 arith1087 . intro hx1088 obtain ⟨inBallots, zerosIs, onesIs, ahead⟩ :=1089 leadSequences.membership.forward with hx1090 apply orderings.membership.backward1091 exact ⟨inBallots, zerosIs⟩10921093theorem orderings.count (a b : Nat)1094 shows cardinality(orderings(a, b)) = (a + b) choose a1095proof1096 have total : a + b = a + b by rfl1097 have bound : b ≤ a + b by arith1098 have closed := leadSequences.closed_form at a + b, b, a, b with total, bound1099 have vanish : (a + b) choose (a + b + 1) = 01100 have reflexive : a + b ≤ a + b by arith1101 have shape : a + b + 1 = succ(a + b) by ring1102 rw shape1103 exact choose.vanishes with reflexive1104 have cardNat := cardinality.nat with (leadSequences.finite at b + 1, a, b)1105 rw [vanish, add.right_unit] at closed1106 rw orderings.eq1107 exact closed110811091110theorem ballot.count (a b : Nat)1111 requires lead : b < a1112 shows (a + b) * cardinality(ballotSequences(a, b)) =1113 (a - b) * ((a + b) choose a)1114proof1115 have aShape := natural.zero_or_successor at a with *1116 cases aShape with aZero | aSucc1117 . exfalso1118 rw aZero at lead1119 arith1120 . obtain ⟨a2, a2Nat, rfl⟩ := aSucc1121 have le : b ≤ a2 by arith1122 have form : succ(a2) = a2 + 1 by ring1123 rw form1124 have count := ballotSequences.count_succ with le1125 have absorb : (a2 + 1) * ((a2 + 1 + b) choose (a2 + 1)) =1126 (a2 + 1 + b) * ((a2 + b) choose a2)1127 have shape : a2 + 1 + b = a2 + b + 1 by ring1128 rw shape1129 exact choose.absorption_at at a2 + b, a21130 have finite := ballotSequences.finite at a2 + 1, b1131 have cardNat := cardinality.nat with finite1132 have xNat := choose.natural at a2 + b, a2 + 11133 have cNat := choose.natural at a2 + 1 + b, a2 + 11134 have main : (a2 + 1 + b) * cardinality(ballotSequences(a2 + 1, b)) +1135 b * ((a2 + 1 + b) choose (a2 + 1)) =1136 (a2 + 1) * ((a2 + 1 + b) choose (a2 + 1))1137 have bShape := natural.zero_or_successor at b with *1138 cases bShape with bZero | bSucc1139 . rw bZero at count1140 rw bZero at absorb1141 rw bZero1142 have vanish : (a2 + 0) choose (a2 + 1) = 01143 have reflexive : a2 ≤ a2 by arith1144 have shape : a2 + 0 = a2 := add.right_unit at a21145 have shapeOne : a2 + 1 = succ(a2) := add.right_one at a21146 rw [shape, shapeOne]1147 exact choose.vanishes with reflexive1148 rw [absorb, ← count, vanish]1149 ring1150 . obtain ⟨b2, b2Nat, rfl⟩ := bSucc1151 have complement : succ(b2) * ((a2 + 1 + succ(b2)) choose (a2 + 1)) =1152 (a2 + 1 + succ(b2)) * ((a2 + succ(b2)) choose (a2 + 1))1153 have le2 : a2 + 1 ≤ a2 + succ(b2) by arith1154 have comp := choose.absorption_complement at a2 + succ(b2), a2 + 11155 with le21156 have diff : a2 + succ(b2) - (a2 + 1) = b21157 have shape : a2 + succ(b2) = a2 + 1 + b2 by ring1158 rw shape1159 exact sub.add_left at b2, a2 + 11160 have coefficient : b2 + 1 = succ(b2) by ring1161 have shape : a2 + 1 + succ(b2) = a2 + succ(b2) + 1 by ring1162 rw [diff, coefficient] at comp1163 rw shape1164 exact comp1165 rw [absorb, ← count, complement]1166 ring1167 have le2 : b ≤ a2 + 1 by arith1168 have split := mul.split_sub at a2 + 1, b, (a2 + 1 + b) choose (a2 + 1)1169 with le21170 rw split at main1171 exact add.right_cancel at1172 (a2 + 1 + b) * cardinality(ballotSequences(a2 + 1, b)),1173 (a2 + 1 - b) * ((a2 + 1 + b) choose (a2 + 1)),1174 b * ((a2 + 1 + b) choose (a2 + 1)) with main1175