swaitsandClaude Opus 5.5
3609bf065e
The money arithmetic every invariant rests on now lives in one kernel,
ledger-core/src/kernel.rs: signing a line, totals, net, per-account
movements, reversal, normal balances, trial-balance columns, closing
lines, and the rounding plug for member splits. It is generic over a
checked `Amount` trait. The engine runs it on Decimal (validate,
movements, reverse_entry, account_balance, close_period_to, allocate,
trial_balance): there is one copy of the arithmetic, and it is the one
under proof.
Three layers, docs/verification.md maps every law to its proofs:
- Kani (src/proofs.rs): 17 harnesses prove the kernel at i64 for every
input up to 4 lines over 3 accounts. An entry is accepted exactly
when it is two or more positive, in-range lines whose debits equal
credits; accepted entries net to zero; grouping by account loses
nothing; a reversal mirrors and cancels its original; trial-balance
columns balance iff the books net to zero; closing lines zero their
accounts and a close balances however the net is split; the plug
makes parts sum to the whole. No panics, no overflow. kani::cover!
shows the proofs are not vacuous.
- Lean 4 (verify/lean): 24 headline theorems for books of any size. The
ledger is a state machine (add account, draft, post, reverse, open,
close), and in every reachable state the books net to zero, the trial
balance balances (as of any date), and the accounting equation holds.
Posting only appends ("posted is forever"), closed periods are
frozen, a close zeroes revenue and expenses and credits exactly the net
income, and period statements add up. Audit.lean shows standard axioms
only, no sorry.
- Bridge (tests/kernel_bridge.rs): the Decimal and i64 kernels agree.
What the proofs found (each one missed by every test, fuzzer, and
mutant):
- The engine accepted negative line amounts; only MCP refused them. Now
NegativeAmountLine: direction is the side's job.
- Summing lines near Decimal::MAX panicked. Lines are now capped at one
quadrillion and ten decimal places (AmountOutOfRange), which keeps
every realistic sum exact, and the kernel's sums are checked.
- FX conversion (foreign_amount * fx_rate) could panic the same way; it
is now a checked multiply.
- Kani itself: 0.68 mis-models symbolic-length copy_from_slice
(model-checking/kani#4904) and reported a reversal that doesn't net to
zero. The counterexample, replayed natively, passes, and a 15-line
standalone crate reproduces the bug. Harnesses avoid bulk copies, and
a should_panic canary will flag the upstream fix.
`just prove` runs it all (Kani memory- and time-capped, fails on an
unsatisfiable cover or a non-standard Lean axiom). AGENTS.md now makes
formal coverage part of every core change.
Also, docs: GnuCash is *an* oracle, never *the* oracle (Stephen). The
spec is accounting principles, proved. Golden files are recomputed from
principles. External implementations (GnuCash, the old Sheet, QBO/Xero)
are cross-checks whose disagreements get adjudicated, never obeyed.
docs/oracle.md gains "Who is right"; AGENTS, README, architecture,
roadmap, parity, and STATUS are reworded to match.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX
447 lines
19 KiB
Lean4
447 lines
19 KiB
Lean4
import Wanderbooks.Closing
|
||
|
||
/-!
|
||
# The ledger as a state machine
|
||
|
||
The engine's command surface (`Ledger`), modelled as the steps it allows:
|
||
add an account, start a draft, post, reverse, open a period, close one.
|
||
Each step carries the checks the engine makes before it mutates. The
|
||
theorems below hold in *every* state reachable from empty books, by any
|
||
sequence of commands, of any length.
|
||
|
||
Mirrors `Ledger::add_account`, `try_create_entry`, `post_entry`,
|
||
`reverse_entry`, `create_period`, and `close_period_to`.
|
||
-/
|
||
|
||
namespace Wanderbooks
|
||
|
||
/-- A journal entry: its id, its date (a day number), its lines. -/
|
||
structure Entry where
|
||
id : Nat
|
||
date : Nat
|
||
lines : List Line
|
||
deriving DecidableEq
|
||
|
||
/-- Every line of some entries, in order. -/
|
||
def allLines : List Entry → List Line
|
||
| [] => []
|
||
| e :: es => e.lines ++ allLines es
|
||
|
||
theorem allLines_append (xs ys : List Entry) : allLines (xs ++ ys) = allLines xs ++ allLines ys := by
|
||
induction xs with
|
||
| nil => rfl
|
||
| cons x xs ih => simp [allLines, ih]
|
||
|
||
theorem mem_allLines {l : Line} {es : List Entry} : l ∈ allLines es ↔ ∃ e ∈ es, l ∈ e.lines := by
|
||
induction es with
|
||
| nil => simp [allLines]
|
||
| cons e es ih => simp [allLines, ih]
|
||
|
||
/-- **Any collection of balanced entries nets to zero**: all of them, those
|
||
dated through some day, those in some period, any filter at all. -/
|
||
theorem net_allLines (es : List Entry) (h : ∀ e ∈ es, net e.lines = 0) : net (allLines es) = 0 := by
|
||
induction es with
|
||
| nil => rfl
|
||
| cons e es ih =>
|
||
simp only [allLines, net_append, h e (by simp), ih (fun x hx => h x (by simp [hx]))]
|
||
rfl
|
||
|
||
/-- An accounting period: inclusive day range, open or closed. -/
|
||
structure Period where
|
||
id : Nat
|
||
start : Nat
|
||
stop : Nat
|
||
closed : Bool
|
||
deriving DecidableEq
|
||
|
||
/-- Whether a day falls in a period. -/
|
||
def Period.contains (p : Period) (d : Nat) : Bool := decide (p.start ≤ d ∧ d ≤ p.stop)
|
||
|
||
/-- The books: chart, posted entries in posting order, drafts, periods. -/
|
||
structure Ledger where
|
||
chart : Chart
|
||
posted : List Entry
|
||
drafts : List Entry
|
||
periods : List Period
|
||
|
||
/-- Empty books. -/
|
||
def Ledger.empty : Ledger := ⟨[], [], [], []⟩
|
||
|
||
/-- Whether a closed period contains a day. -/
|
||
def Ledger.closedOn (L : Ledger) (d : Nat) : Prop :=
|
||
∃ p ∈ L.periods, p.closed = true ∧ p.contains d = true
|
||
|
||
/-- Entries dated on or before a day. -/
|
||
def through (d : Nat) (es : List Entry) : List Entry := es.filter (fun e => decide (e.date ≤ d))
|
||
|
||
/-- Mark one period closed. -/
|
||
def closeIn (p : Period) (ps : List Period) : List Period :=
|
||
ps.map (fun q => if q = p then { q with closed := true } else q)
|
||
|
||
/-- The closing entry for period `p` crediting targets `ts`, if there is
|
||
anything to close. -/
|
||
def closingFor (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) : List Entry :=
|
||
if closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) = [] then []
|
||
else [⟨id, p.stop, closingEntry (nominalCodes L.chart) ts (allLines (through p.stop L.posted))⟩]
|
||
|
||
/-- What the engine allows. -/
|
||
inductive Step : Ledger → Ledger → Prop
|
||
/-- `add_account`: codes are unique. -/
|
||
| addAccount (L : Ledger) (a : Nat) (t : AccountType) (h : a ∉ codes L.chart) :
|
||
Step L { L with chart := (a, t) :: L.chart }
|
||
/-- `try_create_entry` (and lines added to it): not in a closed period. -/
|
||
| draft (L : Ledger) (e : Entry) (h : ¬ L.closedOn e.date) :
|
||
Step L { L with drafts := e :: L.drafts }
|
||
/-- `post_entry`: a draft, acceptable, on known accounts, not in a closed
|
||
period. Appends to the log. -/
|
||
| post (L : Ledger) (e : Entry) (hd : e ∈ L.drafts) (ha : Accepted e.lines)
|
||
(hk : ∀ l ∈ e.lines, l.account ∈ codes L.chart) (hc : ¬ L.closedOn e.date) :
|
||
Step L { L with posted := L.posted ++ [e], drafts := L.drafts.filter (· ≠ e) }
|
||
/-- `reverse_entry`: a posted entry's lines, sides flipped, posted on a
|
||
day not in a closed period. -/
|
||
| reverse (L : Ledger) (e : Entry) (he : e ∈ L.posted) (r : Entry)
|
||
(hr : r.lines = reversal e.lines) (hc : ¬ L.closedOn r.date) :
|
||
Step L { L with posted := L.posted ++ [r] }
|
||
/-- `create_period`: periods open. -/
|
||
| openPeriod (L : Ledger) (p : Period) (h : p.closed = false) :
|
||
Step L { L with periods := p :: L.periods }
|
||
/-- `close_period_to`: an open period with no drafts in it, whose last day
|
||
is in no other closed period, with no later period closed, crediting the
|
||
net income to equity targets (not themselves revenue or expense) in
|
||
parts that sum to it. -/
|
||
| close (L : Ledger) (p : Period) (hp : p ∈ L.periods) (hopen : p.closed = false)
|
||
(hdrafts : ∀ d ∈ L.drafts, p.contains d.date = false)
|
||
(hother : ∀ q ∈ L.periods, q.closed = true → q.contains p.stop = false)
|
||
(hlater : ∀ q ∈ L.periods, q.closed = true → q.stop ≤ p.stop)
|
||
(ts : List (Nat × Int))
|
||
(hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
|
||
(hsum : total (ts.map Prod.snd)
|
||
= net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted))))
|
||
(id : Nat) :
|
||
Step L { L with posted := L.posted ++ closingFor L p ts id, periods := closeIn p L.periods }
|
||
|
||
/-- States reachable from empty books. -/
|
||
inductive Reachable : Ledger → Prop
|
||
| empty : Reachable Ledger.empty
|
||
| step {L L' : Ledger} : Reachable L → Step L L' → Reachable L'
|
||
|
||
/-- What holds in every reachable state. -/
|
||
structure Inv (L : Ledger) : Prop where
|
||
distinct : Distinct (codes L.chart)
|
||
accepted : ∀ e ∈ L.posted, Accepted e.lines
|
||
known : ∀ e ∈ L.posted, ∀ l ∈ e.lines, l.account ∈ codes L.chart
|
||
draftsOpen : ∀ d ∈ L.drafts, ¬ L.closedOn d.date
|
||
|
||
theorem closedOn_closeIn (L : Ledger) (p : Period) (d : Nat) :
|
||
({ L with periods := closeIn p L.periods } : Ledger).closedOn d →
|
||
L.closedOn d ∨ (p ∈ L.periods ∧ p.contains d = true) := by
|
||
rintro ⟨q, hq, hc, hd⟩
|
||
simp only [closeIn, List.mem_map] at hq
|
||
obtain ⟨q', hq', rfl⟩ := hq
|
||
by_cases e : q' = p
|
||
· subst e; right; simp at hd; exact ⟨hq', by simpa [Period.contains] using hd⟩
|
||
· left; simp [e] at hc hd; exact ⟨q', hq', hc, hd⟩
|
||
|
||
theorem closingFor_lines (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) :
|
||
∀ e ∈ closingFor L p ts id,
|
||
e.date = p.stop ∧ e.lines = closingEntry (nominalCodes L.chart) ts
|
||
(allLines (through p.stop L.posted))
|
||
∧ closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) ≠ [] := by
|
||
intro e he
|
||
unfold closingFor at he
|
||
split at he
|
||
· simp at he
|
||
· simp at he; subst he; exact ⟨rfl, rfl, by assumption⟩
|
||
|
||
/-- **Every step preserves the invariant.** -/
|
||
theorem Step.inv {L L' : Ledger} (s : Step L L') (h : Inv L) : Inv L' := by
|
||
cases s with
|
||
| addAccount a t ha =>
|
||
exact ⟨⟨ha, h.distinct⟩, h.accepted,
|
||
fun e he l hl => List.mem_cons_of_mem _ (h.known e he l hl), h.draftsOpen⟩
|
||
| draft e hc =>
|
||
refine ⟨h.distinct, h.accepted, h.known, ?_⟩
|
||
intro d hd
|
||
cases hd with
|
||
| head => exact hc
|
||
| tail _ hd => exact h.draftsOpen d hd
|
||
| post e hd ha hk hc =>
|
||
refine ⟨h.distinct, ?_, ?_, ?_⟩
|
||
· intro x hx
|
||
simp only [List.mem_append, List.mem_singleton] at hx
|
||
rcases hx with hx | rfl
|
||
· exact h.accepted x hx
|
||
· exact ha
|
||
· intro x hx
|
||
simp only [List.mem_append, List.mem_singleton] at hx
|
||
rcases hx with hx | rfl
|
||
· exact h.known x hx
|
||
· exact hk
|
||
· intro d hd
|
||
exact h.draftsOpen d ((List.mem_filter.1 hd).1)
|
||
| reverse e he r hr hc =>
|
||
refine ⟨h.distinct, ?_, ?_, h.draftsOpen⟩
|
||
· intro x hx
|
||
simp only [List.mem_append, List.mem_singleton] at hx
|
||
rcases hx with hx | rfl
|
||
· exact h.accepted x hx
|
||
· rw [hr, accepted_reversal_iff]; exact h.accepted e he
|
||
· intro x hx
|
||
simp only [List.mem_append, List.mem_singleton] at hx
|
||
rcases hx with hx | rfl
|
||
· exact h.known x hx
|
||
· intro l hl
|
||
rw [hr] at hl
|
||
simp only [reversal, List.mem_map] at hl
|
||
obtain ⟨l', hl', rfl⟩ := hl
|
||
exact h.known e he l' hl'
|
||
| openPeriod p hp =>
|
||
refine ⟨h.distinct, h.accepted, h.known, ?_⟩
|
||
rintro d hd ⟨q, hq, hc, hdq⟩
|
||
cases hq with
|
||
| head => simp [hp] at hc
|
||
| tail _ hq => exact h.draftsOpen d hd ⟨q, hq, hc, hdq⟩
|
||
| close p hp hopen hdrafts hother hlater ts hts hsum id =>
|
||
refine ⟨h.distinct, ?_, ?_, ?_⟩
|
||
· intro x hx
|
||
simp only [List.mem_append] at hx
|
||
rcases hx with hx | hx
|
||
· exact h.accepted x hx
|
||
· obtain ⟨-, hl, hne⟩ := closingFor_lines L p ts id x hx
|
||
rw [hl]; exact closingEntry_accepted _ _ _ hsum hne
|
||
· intro x hx
|
||
simp only [List.mem_append] at hx
|
||
rcases hx with hx | hx
|
||
· exact h.known x hx
|
||
· obtain ⟨-, hl, -⟩ := closingFor_lines L p ts id x hx
|
||
intro l hl'
|
||
rw [hl] at hl'
|
||
simp only [closingEntry, List.mem_append] at hl'
|
||
rcases hl' with hl' | hl'
|
||
· exact nominalCodes_sub _ _ (closings_account _ _ l hl')
|
||
· obtain ⟨y, hy, e⟩ := equityLines_account ts l hl'
|
||
rw [e]; exact (hts y hy).1
|
||
· intro d hd hcl
|
||
rcases closedOn_closeIn L p d.date hcl with hcl | ⟨-, hc⟩
|
||
· exact h.draftsOpen d hd hcl
|
||
· simp [hdrafts d hd] at hc
|
||
|
||
/-- **The invariant holds in every reachable state.** -/
|
||
theorem Reachable.inv {L : Ledger} (r : Reachable L) : Inv L := by
|
||
induction r with
|
||
| empty => exact ⟨trivial, by simp [Ledger.empty], by simp [Ledger.empty], by simp [Ledger.empty]⟩
|
||
| step _ s ih => exact s.inv ih
|
||
|
||
/-! ## The books always balance -/
|
||
|
||
/-- **The books net to zero**: in every reachable state, the posted lines'
|
||
debits equal their credits. -/
|
||
theorem Reachable.books_net_zero {L : Ledger} (r : Reachable L) : net (allLines L.posted) = 0 :=
|
||
net_allLines _ (fun e he => (r.inv.accepted e he).net_zero)
|
||
|
||
/-- The same through any day: the books as of any date balance too. -/
|
||
theorem Reachable.net_zero_through {L : Ledger} (r : Reachable L) (d : Nat) :
|
||
net (allLines (through d L.posted)) = 0 :=
|
||
net_allLines _ (fun e he => (r.inv.accepted e ((List.mem_filter.1 he).1)).net_zero)
|
||
|
||
theorem Reachable.covers {L : Ledger} (r : Reachable L) (es : List Entry)
|
||
(hs : ∀ e ∈ es, e ∈ L.posted) : ∀ l ∈ allLines es, l.account ∈ codes L.chart := by
|
||
intro l hl
|
||
obtain ⟨e, he, hl⟩ := mem_allLines.1 hl
|
||
exact r.inv.known e (hs e he) l hl
|
||
|
||
/-- **The trial balance balances**, in every reachable state. -/
|
||
theorem Reachable.trial_balance {L : Ledger} (r : Reachable L) :
|
||
tbDebits (allLines L.posted) (codes L.chart) = tbCredits (allLines L.posted) (codes L.chart) :=
|
||
trial_balance_balances _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero
|
||
|
||
/-- **The trial balance as of any date balances.** -/
|
||
theorem Reachable.trial_balance_through {L : Ledger} (r : Reachable L) (d : Nat) :
|
||
tbDebits (allLines (through d L.posted)) (codes L.chart)
|
||
= tbCredits (allLines (through d L.posted)) (codes L.chart) :=
|
||
trial_balance_balances _ _ r.inv.distinct
|
||
(r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)
|
||
|
||
/-- **The accounting equation holds**, in every reachable state:
|
||
Assets = Liabilities + Equity + (Revenue - Expenses). -/
|
||
theorem Reachable.accounting_equation {L : Ledger} (r : Reachable L) :
|
||
let ls := allLines L.posted
|
||
typeTotal .asset ls L.chart
|
||
= typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
|
||
+ (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
|
||
Wanderbooks.accounting_equation _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero
|
||
|
||
/-- **The balance sheet as of any date balances.** -/
|
||
theorem Reachable.accounting_equation_through {L : Ledger} (r : Reachable L) (d : Nat) :
|
||
let ls := allLines (through d L.posted)
|
||
typeTotal .asset ls L.chart
|
||
= typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
|
||
+ (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
|
||
Wanderbooks.accounting_equation _ _ r.inv.distinct
|
||
(r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)
|
||
|
||
/-! ## Posted is forever -/
|
||
|
||
/-- **Posting only appends.** No step edits, reorders, or removes a posted
|
||
entry. -/
|
||
theorem Step.extends {L L' : Ledger} (s : Step L L') : ∃ t, L'.posted = L.posted ++ t := by
|
||
cases s with
|
||
| addAccount => exact ⟨[], by simp⟩
|
||
| draft => exact ⟨[], by simp⟩
|
||
| post e => exact ⟨[e], rfl⟩
|
||
| reverse e _ r => exact ⟨[r], rfl⟩
|
||
| openPeriod => exact ⟨[], by simp⟩
|
||
| close p _ _ _ _ _ ts _ _ id => exact ⟨closingFor L p ts id, rfl⟩
|
||
|
||
/-- Any number of steps. -/
|
||
inductive Steps : Ledger → Ledger → Prop
|
||
| refl (L : Ledger) : Steps L L
|
||
| tail {L M N : Ledger} : Steps L M → Step M N → Steps L N
|
||
|
||
/-- **Posted is forever**: after any sequence of commands, the old log is
|
||
a prefix of the new one. Every posted entry keeps its place and its
|
||
lines. -/
|
||
theorem Steps.extends {L L' : Ledger} (s : Steps L L') : ∃ t, L'.posted = L.posted ++ t := by
|
||
induction s with
|
||
| refl => exact ⟨[], by simp⟩
|
||
| tail _ s ih =>
|
||
obtain ⟨t, ht⟩ := ih
|
||
obtain ⟨u, hu⟩ := s.extends
|
||
exact ⟨t ++ u, by rw [hu, ht, List.append_assoc]⟩
|
||
|
||
/-! ## Closed periods are frozen -/
|
||
|
||
/-- Entries dated in a period. -/
|
||
def within (p : Period) (es : List Entry) : List Entry := es.filter (fun e => p.contains e.date)
|
||
|
||
theorem within_append (p : Period) (xs ys : List Entry) :
|
||
within p (xs ++ ys) = within p xs ++ within p ys := List.filter_append ..
|
||
|
||
/-- A closed period stays closed. -/
|
||
theorem Step.keeps_closed {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
|
||
(hc : q.closed = true) : q ∈ L'.periods := by
|
||
cases s with
|
||
| openPeriod p _ => exact List.mem_cons_of_mem _ hq
|
||
| close p _ hopen =>
|
||
have : q ≠ p := fun e => by subst e; simp [hopen] at hc
|
||
exact List.mem_map.2 ⟨q, hq, by simp [this]⟩
|
||
| _ => exact hq
|
||
|
||
/-- **A step never changes what a closed period contains.** -/
|
||
theorem Step.frozen {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
|
||
(hc : q.closed = true) : within q L'.posted = within q L.posted := by
|
||
have nothing : ∀ e : Entry, ¬ L.closedOn e.date → within q [e] = [] := by
|
||
intro e he
|
||
simp only [within, List.filter_cons, List.filter_nil]
|
||
split
|
||
· exact absurd ⟨q, hq, hc, by assumption⟩ he
|
||
· rfl
|
||
cases s with
|
||
| post e _ _ _ hcl => rw [within_append, nothing e hcl, List.append_nil]
|
||
| reverse e _ r _ hcl => rw [within_append, nothing r hcl, List.append_nil]
|
||
| close p hp hopen hdrafts hother hlater ts hts hsum id =>
|
||
rw [within_append]
|
||
have : within q (closingFor L p ts id) = [] := by
|
||
unfold closingFor
|
||
split
|
||
· rfl
|
||
· simp only [within, List.filter_cons, List.filter_nil]
|
||
rw [hother q hq hc]; rfl
|
||
rw [this, List.append_nil]
|
||
| _ => rfl
|
||
|
||
/-- **Closed periods are frozen**: once a period is closed, no sequence of
|
||
commands adds, removes, or changes an entry dated in it. -/
|
||
theorem Steps.frozen {L L' : Ledger} (s : Steps L L') (q : Period) (hq : q ∈ L.periods)
|
||
(hc : q.closed = true) : within q L'.posted = within q L.posted ∧ q ∈ L'.periods := by
|
||
induction s with
|
||
| refl => exact ⟨rfl, hq⟩
|
||
| tail _ s ih =>
|
||
obtain ⟨h1, h2⟩ := ih
|
||
exact ⟨(s.frozen q h2 hc).trans h1, s.keeps_closed q h2 hc⟩
|
||
|
||
/-! ## Closing -/
|
||
|
||
/-- **After a close, every revenue and expense account is zero through the
|
||
period's last day.** (The trial balance still balances: the close is a
|
||
step, and `Reachable.trial_balance` covers every step.) -/
|
||
theorem close_zeroes {L : Ledger} (r : Reachable L) (p : Period)
|
||
(ts : List (Nat × Int)) (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
|
||
(id : Nat) (a : Nat) (ha : a ∈ nominalCodes L.chart) :
|
||
movement a (allLines (through p.stop (L.posted ++ closingFor L p ts id))) = 0 := by
|
||
have hd := nominalCodes_distinct _ r.inv.distinct
|
||
have hta : ∀ x ∈ ts, x.1 ≠ a := fun x hx e => (hts x hx).2 (e ▸ ha)
|
||
rw [through, List.filter_append, ← through, allLines_append]
|
||
unfold closingFor
|
||
split
|
||
· rename_i hnil
|
||
simp only [List.filter_nil, allLines, List.append_nil]
|
||
exact closings_eq_nil _ _ hnil a ha
|
||
· simp only [List.filter_cons, Nat.le_refl, decide_true, ite_true, List.filter_nil, allLines,
|
||
List.append_nil]
|
||
exact closingEntry_zeroes _ ts _ hd a ha hta
|
||
|
||
/-- **A close credits equity with exactly the period's net income**:
|
||
revenue minus expenses through its last day, split among the targets. -/
|
||
theorem close_credits_net_income (L : Ledger) (p : Period) (ts : List (Nat × Int))
|
||
(hsum : total (ts.map Prod.snd)
|
||
= net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) :
|
||
let ls := allLines (through p.stop L.posted)
|
||
total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart := by
|
||
intro ls
|
||
rw [hsum, net_closings_is_net_income]
|
||
|
||
/-! ## Period statements add up -/
|
||
|
||
/-- Entries dated after day `b`, through day `c`. -/
|
||
def between (b c : Nat) (es : List Entry) : List Entry :=
|
||
es.filter (fun e => decide (b < e.date ∧ e.date ≤ c))
|
||
|
||
theorem movement_split (a b c : Nat) (h : b ≤ c) (es : List Entry) :
|
||
movement a (allLines (through c es))
|
||
= movement a (allLines (through b es)) + movement a (allLines (between b c es)) := by
|
||
induction es with
|
||
| nil => rfl
|
||
| cons e es ih =>
|
||
simp only [through, between] at ih ⊢
|
||
by_cases h1 : e.date ≤ b
|
||
· have h2 : e.date ≤ c := by omega
|
||
have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
|
||
rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_pos (by simpa using h1),
|
||
List.filter_cons_of_neg (by simpa using h3)]
|
||
simp only [allLines, movement_append, ih]; omega
|
||
· by_cases h2 : e.date ≤ c
|
||
· have h3 : b < e.date ∧ e.date ≤ c := by omega
|
||
rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
|
||
List.filter_cons_of_pos (by simpa using h3)]
|
||
simp only [allLines, movement_append, ih]; omega
|
||
· have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
|
||
rw [List.filter_cons_of_neg (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
|
||
List.filter_cons_of_neg (by simpa using h3)]
|
||
exact ih
|
||
|
||
theorem typeTotal_split (t : AccountType) (x y z : List Line)
|
||
(h : ∀ a, movement a x = movement a y + movement a z) (c : Chart) :
|
||
typeTotal t x c = typeTotal t y c + typeTotal t z c := by
|
||
induction c with
|
||
| nil => rfl
|
||
| cons p c ih =>
|
||
obtain ⟨a, t'⟩ := p
|
||
simp only [typeTotal, h a, ih]
|
||
split
|
||
· cases t' <;> simp [balance, AccountType.normal, signed] <;> omega
|
||
· omega
|
||
|
||
/-- **Period statements add up**: every account type's total (so revenue,
|
||
expenses, and net income) through day `c` is its total through day `b`
|
||
plus its total for the days after `b` through `c`. A year's P&L is the sum
|
||
of its months'. -/
|
||
theorem statements_add_up (t : AccountType) (b c : Nat) (h : b ≤ c) (es : List Entry)
|
||
(chart : Chart) :
|
||
typeTotal t (allLines (through c es)) chart
|
||
= typeTotal t (allLines (through b es)) chart
|
||
+ typeTotal t (allLines (between b c es)) chart :=
|
||
typeTotal_split t _ _ _ (fun a => movement_split a b c h es) chart
|
||
|
||
end Wanderbooks
|