swaitsandClaude Opus 5.5
a7f3cc09a9
check / check (push) Canceled after 0s
Members' shares of earnings are split cumulatively by largest remainder in the closes, the members' equity statement, the K-1 worksheet and the viewer, so a member's capital on a given day never moves by a cent when its month is later closed. Old closes replay as they were; the first P3 close carries any true-up. Feature members_cumulative. Kani and Lean proofs of the bounded drift; bookspec examples. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj
510 lines
23 KiB
Lean4
510 lines
23 KiB
Lean4
import Wanderbooks.Closing
|
||
|
||
/-!
|
||
# Apportioning: the parts sum to the whole, for any number of parts
|
||
|
||
Mirrors `crates/ledger-core/src/kernel.rs` `apportion`: each part is
|
||
first rounded down; the shortfall `s = whole - Σ parts` (not negative) is
|
||
`u` whole units plus a fraction `f` (`s = u * unit + f`, `u` below the
|
||
number of parts, else the function refuses). A part's *rank* is how many
|
||
parts are ahead of it: a strictly larger remainder, or an equal one at an
|
||
earlier index. A part of rank below `u` gets one unit; the part of rank 0
|
||
also gets the fraction.
|
||
|
||
Kani proves INVARIANT 1 for up to three parts. Here it holds for every
|
||
number of parts: the ranks are exactly `0, …, n-1` in some order (a strict
|
||
total order ranks a finite set without gaps or ties), so exactly `u` parts
|
||
get a unit and exactly one gets the fraction.
|
||
-/
|
||
|
||
namespace Wanderbooks.Apportion
|
||
|
||
/-- Part `j` is ahead of part `i` (the closure in `kernel::apportion`). -/
|
||
def ahead (r : Nat → Int) (j i : Nat) : Bool :=
|
||
decide (r j > r i) || (decide (r j = r i) && decide (j < i))
|
||
|
||
/-- A part's rank among `n` parts: the parts ahead of it. -/
|
||
def rank (r : Nat → Int) (n i : Nat) : Nat :=
|
||
((List.range n).filter (fun j => ahead r j i)).length
|
||
|
||
/-- What part `i` gets added: a unit if its rank is below `u`, and the
|
||
fraction too if its rank is 0. -/
|
||
def add (r : Nat → Int) (n u : Nat) (unit f : Int) (i : Nat) : Int :=
|
||
(if rank r n i < u then unit else 0) + (if rank r n i = 0 then f else 0)
|
||
|
||
theorem ahead_irrefl (r : Nat → Int) (i : Nat) : ahead r i i = false := by
|
||
simp [ahead]
|
||
|
||
theorem ahead_trans (r : Nat → Int) {a b c : Nat}
|
||
(h1 : ahead r a b = true) (h2 : ahead r b c = true) : ahead r a c = true := by
|
||
simp only [ahead, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at *
|
||
omega
|
||
|
||
theorem ahead_total (r : Nat → Int) {a b : Nat} (h : a ≠ b) :
|
||
ahead r a b = true ∨ ahead r b a = true := by
|
||
simp only [ahead, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq]
|
||
omega
|
||
|
||
theorem ahead_asymm (r : Nat → Int) {a b : Nat} (h : ahead r a b = true) :
|
||
ahead r b a = false := by
|
||
simp only [ahead, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at h
|
||
simp only [ahead, Bool.or_eq_false_iff, Bool.and_eq_false_imp, decide_eq_true_eq,
|
||
decide_eq_false_iff_not]
|
||
omega
|
||
|
||
/-- A filter by a weaker predicate is no longer. -/
|
||
theorem filter_length_le {p q : Nat → Bool} : ∀ (l : List Nat),
|
||
(∀ x ∈ l, p x = true → q x = true) → (l.filter p).length ≤ (l.filter q).length
|
||
| [], _ => by simp
|
||
| a :: t, sub => by
|
||
have ih := filter_length_le t (fun x hx => sub x (List.mem_cons_of_mem a hx))
|
||
have ha := sub a (List.mem_cons_self ..)
|
||
cases hpa : p a <;> cases hqa : q a <;> simp_all <;> omega
|
||
|
||
/-- ... and strictly shorter when some element passes only the weaker one. -/
|
||
theorem filter_length_lt {p q : Nat → Bool} : ∀ (l : List Nat),
|
||
(∀ x ∈ l, p x = true → q x = true) → (∃ x ∈ l, q x = true ∧ p x = false) →
|
||
(l.filter p).length < (l.filter q).length
|
||
| [], _, w => by simp at w
|
||
| a :: t, sub, w => by
|
||
have sub' : ∀ x ∈ t, p x = true → q x = true :=
|
||
fun x hx => sub x (List.mem_cons_of_mem a hx)
|
||
have le := filter_length_le t sub'
|
||
have ha := sub a (List.mem_cons_self ..)
|
||
obtain ⟨x, hx, hq, hp⟩ := w
|
||
rcases List.mem_cons.mp hx with rfl | hx'
|
||
· simp [hq, hp]
|
||
omega
|
||
· have := filter_length_lt t sub' ⟨x, hx', hq, hp⟩
|
||
cases hpa : p a <;> cases hqa : q a <;> simp_all <;> omega
|
||
|
||
/-- Being ahead means a strictly smaller rank. -/
|
||
theorem rank_lt_of_ahead (r : Nat → Int) {n a b : Nat} (ha : a < n)
|
||
(h : ahead r a b = true) : rank r n a < rank r n b := by
|
||
unfold rank
|
||
apply filter_length_lt
|
||
· intro x _ hx
|
||
exact ahead_trans r hx h
|
||
· exact ⟨a, List.mem_range.mpr ha, h, ahead_irrefl r a⟩
|
||
|
||
/-- Distinct parts have distinct ranks. -/
|
||
theorem rank_inj (r : Nat → Int) {n a b : Nat} (ha : a < n) (hb : b < n)
|
||
(h : rank r n a = rank r n b) : a = b := by
|
||
apply Classical.byContradiction
|
||
intro hne
|
||
rcases ahead_total r hne with h1 | h1
|
||
· have := rank_lt_of_ahead r ha h1; omega
|
||
· have := rank_lt_of_ahead r hb h1; omega
|
||
|
||
/-- Every rank is below the number of parts (a part isn't ahead of itself). -/
|
||
theorem rank_lt (r : Nat → Int) {n i : Nat} (hi : i < n) : rank r n i < n := by
|
||
unfold rank
|
||
have := (List.length_filter_lt_length_iff_exists (p := fun j => ahead r j i)
|
||
(l := List.range n)).mpr ⟨i, List.mem_range.mpr hi, by simp [ahead_irrefl]⟩
|
||
simpa using this
|
||
|
||
/-- A duplicate-free list inside another is no longer. -/
|
||
theorem nodup_length_le : ∀ (l m : List Nat), l.Nodup → (∀ x ∈ l, x ∈ m) →
|
||
l.length ≤ m.length
|
||
| [], _, _, _ => by simp
|
||
| a :: t, m, hn, hs => by
|
||
rw [List.nodup_cons] at hn
|
||
have ham : a ∈ m := hs a (by simp)
|
||
have ih := nodup_length_le t (m.erase a) hn.2 (fun x hx => by
|
||
have hxa : x ≠ a := fun e => hn.1 (e ▸ hx)
|
||
exact (List.mem_erase_of_ne hxa).mpr (hs x (by simp [hx])))
|
||
rw [List.length_erase_of_mem ham] at ih
|
||
have : 0 < m.length := List.length_pos_of_mem ham
|
||
simp
|
||
omega
|
||
|
||
/-- Mapping a duplicate-free list by a function injective on it keeps it
|
||
duplicate-free. -/
|
||
theorem nodup_map_of_inj {f : Nat → Nat} : ∀ (l : List Nat), l.Nodup →
|
||
(∀ a ∈ l, ∀ b ∈ l, f a = f b → a = b) → (l.map f).Nodup
|
||
| [], _, _ => by simp
|
||
| a :: t, hn, hi => by
|
||
rw [List.nodup_cons] at hn
|
||
rw [List.map_cons, List.nodup_cons]
|
||
refine ⟨?_, nodup_map_of_inj t hn.2 (fun x hx y hy => hi x (by simp [hx]) y (by simp [hy]))⟩
|
||
intro hm
|
||
obtain ⟨b, hb, hfb⟩ := List.mem_map.mp hm
|
||
have := hi a (by simp) b (by simp [hb]) hfb.symm
|
||
exact hn.1 (this ▸ hb)
|
||
|
||
/-- The ranks of `n` parts are `0, …, n-1` in some order. -/
|
||
theorem ranks_perm (r : Nat → Int) (n : Nat) :
|
||
((List.range n).map (rank r n)).Perm (List.range n) := by
|
||
let L := (List.range n).map (rank r n)
|
||
have nd : L.Nodup := nodup_map_of_inj _ List.nodup_range (fun a ha b hb h =>
|
||
rank_inj r (List.mem_range.mp ha) (List.mem_range.mp hb) h)
|
||
have sub : ∀ x ∈ L, x < n := by
|
||
intro x hx
|
||
obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hx
|
||
exact rank_lt r (List.mem_range.mp hi)
|
||
have len : L.length = n := by simp [L]
|
||
-- Pigeonhole: n distinct values below n are all of them.
|
||
have all : ∀ v < n, v ∈ L := by
|
||
intro v hv
|
||
apply Classical.byContradiction
|
||
intro hnot
|
||
have := nodup_length_le L ((List.range n).erase v) nd (fun x hx => by
|
||
have hxv : x ≠ v := fun e => hnot (e ▸ hx)
|
||
exact (List.mem_erase_of_ne hxv).mpr (List.mem_range.mpr (sub x hx)))
|
||
rw [List.length_erase_of_mem (List.mem_range.mpr hv), List.length_range] at this
|
||
omega
|
||
rw [List.perm_iff_count]
|
||
intro a
|
||
rw [List.Nodup.count nd, List.Nodup.count List.nodup_range]
|
||
by_cases ha : a < n
|
||
· simp [all a ha, List.mem_range.mpr ha]
|
||
· have h1 : a ∉ L := fun h => ha (sub a h)
|
||
simp [h1, List.mem_range, ha]
|
||
|
||
/-- Sums over permuted lists agree. -/
|
||
theorem perm_sum {l₁ l₂ : List Int} (h : l₁.Perm l₂) : l₁.sum = l₂.sum := by
|
||
induction h with
|
||
| nil => rfl
|
||
| cons x _ ih => simp [ih]
|
||
| swap x y l => simp; omega
|
||
| trans _ _ ih1 ih2 => exact ih1.trans ih2
|
||
|
||
/-- What the ranks `0, …, n-1` get, together: `u` units and the fraction. -/
|
||
theorem sum_by_rank (u : Nat) (unit f : Int) : ∀ n, 0 < n → u ≤ n →
|
||
((List.range n).map (fun v => (if v < u then unit else 0) + (if v = 0 then f else 0))).sum
|
||
= u * unit + f
|
||
| 0, h, _ => absurd h (by decide)
|
||
| 1, _, hu => by
|
||
rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hu with rfl | rfl <;> simp
|
||
| n + 2, _, hu => by
|
||
rw [List.range_succ, List.map_append, List.sum_append]
|
||
by_cases h : u ≤ n + 1
|
||
· rw [sum_by_rank u unit f (n + 1) (by omega) h]
|
||
have : ¬ (n + 1 < u) := by omega
|
||
simp [this]
|
||
· have hu' : u = n + 2 := by omega
|
||
subst hu'
|
||
have ih := sum_by_rank (n + 1) unit f (n + 1) (by omega) (Nat.le_refl _)
|
||
have eq : ((List.range (n + 1)).map
|
||
(fun v => (if v < n + 2 then unit else 0) + (if v = 0 then f else 0))) =
|
||
((List.range (n + 1)).map
|
||
(fun v => (if v < n + 1 then unit else 0) + (if v = 0 then f else 0))) := by
|
||
apply List.map_congr_left
|
||
intro v hv
|
||
have := List.mem_range.mp hv
|
||
simp [show v < n + 2 by omega, show v < n + 1 by omega]
|
||
rw [eq, ih]
|
||
have e : ((n + 2 : Nat) : Int) = ((n + 1 : Nat) : Int) + 1 := by omega
|
||
simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]
|
||
rw [e, Int.add_mul, Int.one_mul]
|
||
simp
|
||
omega
|
||
|
||
theorem sum_map_add (f g : Nat → Int) : ∀ (l : List Nat),
|
||
(l.map (fun i => f i + g i)).sum = (l.map f).sum + (l.map g).sum
|
||
| [] => by simp
|
||
| a :: t => by simp [sum_map_add f g t]; omega
|
||
|
||
/-- **INVARIANT 1, for any number of parts.** When the shortfall
|
||
`whole - Σ parts` is `u` units plus `f` (with `u` at most the number of
|
||
parts, as `apportion` requires before it changes anything), the parts
|
||
after apportioning sum to `whole` exactly. -/
|
||
theorem apportion_sum (parts r : Nat → Int) (n u : Nat) (unit f whole : Int)
|
||
(hn : 0 < n) (hu : u ≤ n)
|
||
(hs : whole - ((List.range n).map parts).sum = u * unit + f) :
|
||
((List.range n).map (fun i => parts i + add r n u unit f i)).sum = whole := by
|
||
rw [sum_map_add]
|
||
let g := fun v => (if v < u then unit else 0) + (if v = 0 then f else 0)
|
||
have h1 : (List.range n).map (add r n u unit f) = ((List.range n).map (rank r n)).map g := by
|
||
simp [List.map_map, add, g, Function.comp_def]
|
||
have h2 := perm_sum ((ranks_perm r n).map g)
|
||
have h3 := sum_by_rank u unit f n hn hu
|
||
show ((List.range n).map parts).sum + ((List.range n).map (add r n u unit f)).sum = whole
|
||
rw [h1, h2, h3]
|
||
omega
|
||
|
||
/-- The same, from the shortfall as `apportion` computes it: `u` whole
|
||
units by repeated subtraction (`s / unit`) and the rest (`s % unit`). -/
|
||
theorem apportion_sum_of_shortfall (parts r : Nat → Int) (n : Nat) (unit whole : Int)
|
||
(hn : 0 < n) (hunit : 0 < unit)
|
||
(hs : 0 ≤ whole - ((List.range n).map parts).sum)
|
||
(hu : ((whole - ((List.range n).map parts).sum) / unit).toNat ≤ n) :
|
||
let s := whole - ((List.range n).map parts).sum
|
||
((List.range n).map (fun i =>
|
||
parts i + add r n (s / unit).toNat unit (s % unit) i)).sum = whole := by
|
||
intro s
|
||
apply apportion_sum parts r n _ unit _ whole hn hu
|
||
have hq : 0 ≤ s / unit := Int.ediv_nonneg hs (Int.le_of_lt hunit)
|
||
rw [Int.toNat_of_nonneg hq]
|
||
have := Int.mul_ediv_add_emod s unit
|
||
rw [Int.mul_comm] at this
|
||
exact this.symm
|
||
|
||
/-! ## Bounded drift
|
||
|
||
With exact shares there is no sub-unit fraction: every amount is a whole
|
||
number of minor units (B-3) and every product `|T| × share` is exact
|
||
(`periods::allocate_cumulative` INVARIANT 4), so the remainders, scaled to
|
||
whole numbers below `m`, sum to whole units of `m`. Then a part that gets
|
||
a unit had a positive remainder, and every apportioned part is under one
|
||
unit from its exact share (rules.md B-13). -/
|
||
|
||
/-- Values in `[0, m)` that are zero wherever `p` fails sum to at most
|
||
`(m - 1)` per element where `p` holds. -/
|
||
theorem sum_le_count_mul (r : Nat → Int) (p : Nat → Bool) (m : Int) : ∀ (l : List Nat),
|
||
(∀ j ∈ l, 0 ≤ r j ∧ r j < m) → (∀ j ∈ l, p j = false → r j = 0) →
|
||
(l.map r).sum ≤ ((l.filter p).length : Int) * (m - 1)
|
||
| [], _, _ => by simp
|
||
| a :: t, hr, hz => by
|
||
have ih := sum_le_count_mul r p m t (fun j hj => hr j (List.mem_cons_of_mem a hj))
|
||
(fun j hj => hz j (List.mem_cons_of_mem a hj))
|
||
have ha := hr a (List.mem_cons_self ..)
|
||
simp only [List.map_cons, List.sum_cons, List.filter_cons]
|
||
cases hp : p a
|
||
· have := hz a (List.mem_cons_self ..) hp
|
||
simp only [Bool.false_eq_true, ↓reduceIte]
|
||
omega
|
||
· simp only [↓reduceIte, List.length_cons]
|
||
have e : (((t.filter p).length + 1 : Nat) : Int) * (m - 1)
|
||
= ((t.filter p).length : Int) * (m - 1) + (m - 1) := by
|
||
rw [Int.natCast_add, Int.add_mul, Int.natCast_one, Int.one_mul]
|
||
rw [e]
|
||
omega
|
||
|
||
/-- With remainders in `[0, m)` summing to exactly `u · m` (no sub-unit
|
||
fraction), every part ranked below `u` (so given a unit) has a positive
|
||
remainder. -/
|
||
theorem rem_pos_of_rank_lt (r : Nat → Int) (n u : Nat) (m : Int)
|
||
(hr : ∀ i < n, 0 ≤ r i ∧ r i < m)
|
||
(hs : ((List.range n).map r).sum = u * m)
|
||
{i : Nat} (hi : i < n) (hk : rank r n i < u) : 0 < r i := by
|
||
apply Classical.byContradiction
|
||
intro hneg
|
||
have hri : r i = 0 := by have := hr i hi; omega
|
||
-- Every part not ahead of `i` has a remainder no larger than `i`'s: 0.
|
||
have hz : ∀ j ∈ List.range n, ahead r j i = false → r j = 0 := by
|
||
intro j hj hna
|
||
have hj' := List.mem_range.mp hj
|
||
have hrj := hr j hj'
|
||
by_cases e : j = i
|
||
· subst e
|
||
exact hri
|
||
· rcases ahead_total r e with h | h
|
||
· rw [h] at hna
|
||
exact absurd hna (by decide)
|
||
· simp only [ahead, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at h
|
||
omega
|
||
have hle := sum_le_count_mul r (fun j => ahead r j i) m (List.range n)
|
||
(fun j hj => hr j (List.mem_range.mp hj)) hz
|
||
have hm : 0 < m := by have := hr i hi; omega
|
||
have hrank : ((List.range n).filter (fun j => ahead r j i)).length = rank r n i := rfl
|
||
rw [hrank, hs] at hle
|
||
have h1 : (rank r n i : Int) * (m - 1) ≤ ((u : Int) - 1) * (m - 1) :=
|
||
Int.mul_le_mul_of_nonneg_right (by omega) (by omega)
|
||
have h2 : ((u : Int) - 1) * (m - 1) = (u : Int) * m - u - m + 1 := by
|
||
simp only [Int.sub_mul, Int.mul_sub, Int.one_mul, Int.mul_one]
|
||
omega
|
||
omega
|
||
|
||
/-- **Bounded drift of one apportionment** (rules.md B-13): scaled by `m`,
|
||
each apportioned part (rounded down, plus its unit if any) is within one
|
||
unit of its exact share `parts i + r i / m`, when there is no sub-unit
|
||
fraction. -/
|
||
theorem apportion_drift (parts r : Nat → Int) (n u : Nat) (m : Int)
|
||
(hr : ∀ i < n, 0 ≤ r i ∧ r i < m)
|
||
(hs : ((List.range n).map r).sum = u * m) {i : Nat} (hi : i < n) :
|
||
-m < (parts i + add r n u 1 0 i) * m - (parts i * m + r i) ∧
|
||
(parts i + add r n u 1 0 i) * m - (parts i * m + r i) < m := by
|
||
have hri := hr i hi
|
||
unfold add
|
||
rw [ite_self, Int.add_zero]
|
||
by_cases hk : rank r n i < u
|
||
· have hpos := rem_pos_of_rank_lt r n u m hr hs hi hk
|
||
simp only [hk, ↓reduceIte]
|
||
rw [Int.add_mul, Int.one_mul]
|
||
omega
|
||
· simp only [hk, ↓reduceIte, Int.add_zero]
|
||
omega
|
||
|
||
/-- Σ c · f = c · Σ f. -/
|
||
theorem sum_map_mul_left (c : Int) (f : Nat → Int) : ∀ (l : List Nat),
|
||
(l.map (fun j => c * f j)).sum = c * (l.map f).sum
|
||
| [] => by simp
|
||
| a :: t => by simp [sum_map_mul_left c f t, Int.mul_add]
|
||
|
||
/-- Σ -f = -Σ f. -/
|
||
theorem sum_map_neg (f : Nat → Int) : ∀ (l : List Nat),
|
||
(l.map (fun j => -f j)).sum = -(l.map f).sum
|
||
| [] => by simp
|
||
| a :: t => by simp [sum_map_neg f t]; omega
|
||
|
||
/-- Values at most `c` sum to at most `c` per element. -/
|
||
theorem sum_le_length_mul (f : Nat → Int) (c : Int) : ∀ (l : List Nat),
|
||
(∀ j ∈ l, f j ≤ c) → (l.map f).sum ≤ (l.length : Int) * c
|
||
| [], _ => by simp
|
||
| a :: t, h => by
|
||
have ih := sum_le_length_mul f c t (fun j hj => h j (List.mem_cons_of_mem a hj))
|
||
have ha := h a (List.mem_cons_self ..)
|
||
simp only [List.map_cons, List.sum_cons, List.length_cons]
|
||
rw [Int.natCast_add, Int.add_mul, Int.natCast_one, Int.one_mul]
|
||
omega
|
||
|
||
/-- Nonnegative values have a nonnegative sum. -/
|
||
theorem sum_nonneg (f : Nat → Int) : ∀ (l : List Nat), (∀ j ∈ l, 0 ≤ f j) → 0 ≤ (l.map f).sum
|
||
| [], _ => by simp
|
||
| a :: t, h => by
|
||
have ih := sum_nonneg f t (fun j hj => h j (List.mem_cons_of_mem a hj))
|
||
have ha := h a (List.mem_cons_self ..)
|
||
simp only [List.map_cons, List.sum_cons]
|
||
omega
|
||
|
||
/-- Member `i`'s share of `x` rounded down to the unit: `x · w i / W`
|
||
(`periods::allocate_cumulative`'s floor; shares `w i / W`). -/
|
||
def floorW (w : Nat → Int) (W x : Int) (i : Nat) : Int := x * w i / W
|
||
|
||
/-- What rounding down took from it, scaled by `W`: `x · w i % W` (it
|
||
ranks the members as the Decimal remainder does). -/
|
||
def remW (w : Nat → Int) (W x : Int) (i : Nat) : Int := x * w i % W
|
||
|
||
/-- The whole units the floors fall short of `x`. -/
|
||
def shortW (w : Nat → Int) (W : Int) (n : Nat) (x : Int) : Nat :=
|
||
(x - ((List.range n).map (floorW w W x)).sum).toNat
|
||
|
||
/-- The model of `periods::allocate_cumulative`'s split of a gain (`x ≥
|
||
0`) at whole minor units: each floor, plus a unit to each of the members
|
||
with the largest remainders (ties to the earlier member). -/
|
||
def allocNat (w : Nat → Int) (W : Int) (n : Nat) (x : Int) (i : Nat) : Int :=
|
||
floorW w W x i + add (remW w W x) n (shortW w W n x) 1 0 i
|
||
|
||
/-- With the sign: a loss splits as the negation of the same gain
|
||
(`allocate_cumulative` scenario 3). -/
|
||
def allocW (w : Nat → Int) (W : Int) (n : Nat) (x : Int) (i : Nat) : Int :=
|
||
if x < 0 then -allocNat w W n (-x) i else allocNat w W n x i
|
||
|
||
/-- The floors and remainders of a gain, with shares `w i / W` summing to
|
||
one: the remainders sum to whole units, `W · (x − Σ floors)`, each in
|
||
`[0, W)`, and the floors fall short by fewer units than there are
|
||
members. -/
|
||
theorem remW_facts (w : Nat → Int) (W : Int) (n : Nat) (x : Int) (hW : 0 < W)
|
||
(hsum : ((List.range n).map w).sum = W) (hn : 0 < n) :
|
||
(∀ i < n, 0 ≤ remW w W x i ∧ remW w W x i < W) ∧
|
||
((List.range n).map (remW w W x)).sum = (shortW w W n x : Int) * W ∧
|
||
x - ((List.range n).map (floorW w W x)).sum = (shortW w W n x : Int) ∧
|
||
shortW w W n x ≤ n := by
|
||
have hW0 : W ≠ 0 := by omega
|
||
have bounds : ∀ i < n, 0 ≤ remW w W x i ∧ remW w W x i < W := fun i _ =>
|
||
⟨Int.emod_nonneg _ hW0, Int.emod_lt_of_pos _ hW⟩
|
||
-- x · w i = W · floor + rem, summed: x · W = W · Σ floors + Σ rems.
|
||
have each : ∀ i, x * w i = W * floorW w W x i + remW w W x i := fun i =>
|
||
(Int.mul_ediv_add_emod (x * w i) W).symm
|
||
have total : x * W = W * ((List.range n).map (floorW w W x)).sum
|
||
+ ((List.range n).map (remW w W x)).sum := by
|
||
have h1 : ((List.range n).map (fun j => x * w j)).sum = x * W := by
|
||
rw [sum_map_mul_left, hsum]
|
||
have h2 : ((List.range n).map (fun j => x * w j)).sum
|
||
= ((List.range n).map (fun j => W * floorW w W x j + remW w W x j)).sum := by
|
||
congr 1
|
||
apply List.map_congr_left
|
||
intro i _
|
||
exact each i
|
||
rw [← h1, h2, sum_map_add (fun j => W * floorW w W x j) (remW w W x), sum_map_mul_left]
|
||
let d := x - ((List.range n).map (floorW w W x)).sum
|
||
have hd : ((List.range n).map (remW w W x)).sum = W * d := by
|
||
show _ = W * (x - _)
|
||
rw [Int.mul_sub, Int.mul_comm W x]
|
||
omega
|
||
have rems_nonneg := sum_nonneg (remW w W x) (List.range n)
|
||
(fun j hj => (bounds j (List.mem_range.mp hj)).1)
|
||
have rems_lt := sum_le_length_mul (remW w W x) (W - 1) (List.range n)
|
||
(fun j hj => by have := (bounds j (List.mem_range.mp hj)).2; omega)
|
||
rw [List.length_range] at rems_lt
|
||
have d_nonneg : 0 ≤ d := by
|
||
apply Classical.byContradiction
|
||
intro h
|
||
have : W * d < 0 := Int.mul_neg_of_pos_of_neg hW (by omega)
|
||
omega
|
||
have d_lt : d < n := by
|
||
apply Classical.byContradiction
|
||
intro h
|
||
have h1 : (n : Int) * W ≤ d * W := Int.mul_le_mul_of_nonneg_right (by omega) (by omega)
|
||
have h2 : (n : Int) * (W - 1) = n * W - n := by
|
||
rw [Int.mul_sub, Int.mul_one]
|
||
rw [Int.mul_comm W d] at hd
|
||
omega
|
||
have hshort : (shortW w W n x : Int) = d := Int.toNat_of_nonneg d_nonneg
|
||
refine ⟨bounds, ?_, hshort.symm, ?_⟩
|
||
· rw [hshort, hd, Int.mul_comm]
|
||
· have : ((shortW w W n x : Nat) : Int) < n := by rw [hshort]; exact d_lt
|
||
omega
|
||
|
||
/-- **The split of a gain sums to it**, exactly. -/
|
||
theorem allocNat_sum (w : Nat → Int) (W : Int) (n : Nat) (x : Int) (hW : 0 < W)
|
||
(hsum : ((List.range n).map w).sum = W) (hn : 0 < n) :
|
||
((List.range n).map (allocNat w W n x)).sum = x := by
|
||
obtain ⟨_, _, hx, hu⟩ := remW_facts w W n x hW hsum hn
|
||
apply apportion_sum (floorW w W x) (remW w W x) n (shortW w W n x) 1 0 x hn hu
|
||
rw [hx]
|
||
omega
|
||
|
||
/-- **`allocate_cumulative`'s split sums to the amount**, gain or loss. -/
|
||
theorem allocW_sum (w : Nat → Int) (W : Int) (n : Nat) (x : Int) (hW : 0 < W)
|
||
(hsum : ((List.range n).map w).sum = W) (hn : 0 < n) :
|
||
((List.range n).map (allocW w W n x)).sum = x := by
|
||
unfold allocW
|
||
by_cases hx : x < 0
|
||
· simp only [hx, ↓reduceIte]
|
||
rw [sum_map_neg, allocNat_sum w W n (-x) hW hsum hn]
|
||
omega
|
||
· simp only [hx, ↓reduceIte]
|
||
exact allocNat_sum w W n x hW hsum hn
|
||
|
||
/-- **Bounded drift** (rules.md B-13): each member's part of an amount is
|
||
under one minor unit from their exact share, `|allocW x i · W − x · w i| <
|
||
W`, gain or loss. -/
|
||
theorem allocW_drift (w : Nat → Int) (W : Int) (n : Nat) (x : Int) (hW : 0 < W)
|
||
(hsum : ((List.range n).map w).sum = W) (hn : 0 < n) {i : Nat} (hi : i < n) :
|
||
-W < allocW w W n x i * W - x * w i ∧ allocW w W n x i * W - x * w i < W := by
|
||
have gain : ∀ y, 0 ≤ y →
|
||
-W < allocNat w W n y i * W - y * w i ∧ allocNat w W n y i * W - y * w i < W := by
|
||
intro y _
|
||
obtain ⟨hr, hs, _, _⟩ := remW_facts w W n y hW hsum hn
|
||
have h := apportion_drift (floorW w W y) (remW w W y) n (shortW w W n y) W hr hs hi
|
||
have e : floorW w W y i * W + remW w W y i = y * w i := by
|
||
rw [Int.mul_comm]
|
||
exact Int.mul_ediv_add_emod (y * w i) W
|
||
rw [e] at h
|
||
exact h
|
||
unfold allocW
|
||
by_cases hx : x < 0
|
||
· simp only [hx, ↓reduceIte]
|
||
have h := gain (-x) (by omega)
|
||
simp only [Int.neg_mul] at h ⊢
|
||
omega
|
||
· simp only [hx, ↓reduceIte]
|
||
exact gain x (by omega)
|
||
|
||
/-- **No member's running total is ever a minor unit from their exact
|
||
share**, after a cumulative close, whatever earlier closes gave them
|
||
(rules.md B-13; D-10): `Closing.trueUp` with `allocate_cumulative`'s
|
||
split (Kani `cumulative_close_never_drifts_a_unit_at_*` check the code on
|
||
small amounts). -/
|
||
theorem allocW_cumulative_drift (w : Nat → Int) (W : Int) (n : Nat) (hW : 0 < W)
|
||
(hsum : ((List.range n).map w).sum = W) (hn : 0 < n) (closed net : Int)
|
||
(given : Nat → Int) {i : Nat} (hi : i < n) :
|
||
-W < (given i + trueUp (allocW w W n) closed net given i) * W - (closed + net) * w i ∧
|
||
(given i + trueUp (allocW w W n) closed net given i) * W - (closed + net) * w i < W := by
|
||
rw [trueUp_running]
|
||
exact allocW_drift w W n (closed + net) hW hsum hn hi
|
||
|
||
/-- **A cumulative close hands out exactly its net** with
|
||
`allocate_cumulative`'s split, gain or loss, whatever the earlier closes
|
||
gave, as long as they gave what they closed. -/
|
||
theorem allocW_cumulative_total (w : Nat → Int) (W : Int) (n : Nat) (hW : 0 < W)
|
||
(hsum : ((List.range n).map w).sum = W) (hn : 0 < n) (closed net : Int)
|
||
(given : Nat → Int) (hg : ((List.range n).map given).sum = closed) :
|
||
((List.range n).map (trueUp (allocW w W n) closed net given)).sum = net :=
|
||
trueUp_total (allocW w W n) (List.range n) (fun x => allocW_sum w W n x hW hsum hn)
|
||
closed net given hg
|
||
|
||
end Wanderbooks.Apportion
|