From f034b0d45b5da4f514b1dcb7e07e6531c62df88a Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Thu, 29 Oct 2026 12:33:54 -0600 Subject: [PATCH] feat(bookspec): the five laws as Lean theorems (P13 step 4) The first edition's five laws (debits equal credits; the accounting equation; the trial balance balances; net income articulates to equity; the cash-flow sections sum to the change in cash) are theorems in bookspec/lean, ported from verify/lean (Basic, Entry, Statements, Closing, Ledger under namespace Bookspec) and restated by name in Laws.lean, each a statement about every reachable state of the books. Audit.lean prints their axioms; the checker's lean.rs test fails on a sorry, a law not audited, or any axiom beyond propext, Quot.sound and Classical.choice. Money is Int, the exact count of the smallest unit: every law is a law of addition, so the model is faithful to exact decimals. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp --- checker/tests/lean.rs | 93 +++++ lean/.gitignore | 1 + lean/Audit.lean | 14 + lean/Bookspec.lean | 2 + lean/Bookspec/Basic.lean | 165 ++++++++ lean/Bookspec/Closing.lean | 451 ++++++++++++++++++++++ lean/Bookspec/Entry.lean | 117 ++++++ lean/Bookspec/Laws.lean | 62 +++ lean/Bookspec/Ledger.lean | 562 ++++++++++++++++++++++++++++ lean/Bookspec/Statements.lean | 683 ++++++++++++++++++++++++++++++++++ lean/lake-manifest.json | 6 + lean/lakefile.toml | 5 + lean/lean-toolchain | 1 + 13 files changed, 2162 insertions(+) create mode 100644 checker/tests/lean.rs create mode 100644 lean/.gitignore create mode 100644 lean/Audit.lean create mode 100644 lean/Bookspec.lean create mode 100644 lean/Bookspec/Basic.lean create mode 100644 lean/Bookspec/Closing.lean create mode 100644 lean/Bookspec/Entry.lean create mode 100644 lean/Bookspec/Laws.lean create mode 100644 lean/Bookspec/Ledger.lean create mode 100644 lean/Bookspec/Statements.lean create mode 100644 lean/lake-manifest.json create mode 100644 lean/lakefile.toml create mode 100644 lean/lean-toolchain diff --git a/checker/tests/lean.rs b/checker/tests/lean.rs new file mode 100644 index 0000000..78517bc --- /dev/null +++ b/checker/tests/lean.rs @@ -0,0 +1,93 @@ +//! The five laws are Lean theorems in `bookspec/lean` (P13 step 4), with +//! no assumption beyond Lean's standard axioms. + +use std::path::{Path, PathBuf}; +use std::process::Command; + +const LAWS: [&str; 5] = [ + "law_debits_equal_credits", + "law_accounting_equation", + "law_trial_balance", + "law_net_income_articulates", + "law_cash_flow_is_change_in_cash", +]; + +fn lean_dir() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("../lean") +} + +/// Every law is stated in `Laws.lean`, audited in `Audit.lean`, and no +/// file of the library says `sorry`. +#[test] +fn the_five_laws_are_stated_and_audited() { + let laws = std::fs::read_to_string(lean_dir().join("Bookspec/Laws.lean")).unwrap(); + let audit = std::fs::read_to_string(lean_dir().join("Audit.lean")).unwrap(); + for law in LAWS { + assert!(laws.contains(&format!("theorem {law}")), "{law} is stated"); + assert!( + audit.contains(&format!("#print axioms {law}")), + "{law} is audited" + ); + } + for entry in std::fs::read_dir(lean_dir().join("Bookspec")).unwrap() { + let path = entry.unwrap().path(); + let text = std::fs::read_to_string(&path).unwrap(); + for (i, line) in text.lines().enumerate() { + let code = line.split("--").next().unwrap(); + assert!( + !code + .split(|c: char| !c.is_alphanumeric() && c != '_') + .any(|w| w == "sorry"), + "{}:{}: sorry", + path.display(), + i + 1 + ); + } + } +} + +/// With Lean installed, the library builds and every law depends only on +/// `propext`, `Quot.sound` and `Classical.choice`. Without it the test +/// says so and passes: `mise install` provides Lean (`just prove` is +/// where the machine is known to have it). +#[test] +fn the_laws_use_standard_axioms_only() { + let built = Command::new("lake") + .arg("build") + .current_dir(lean_dir()) + .output(); + let Ok(built) = built else { + eprintln!("lake is not installed: the Lean build is not checked here"); + return; + }; + assert!( + built.status.success(), + "lake build:\n{}", + String::from_utf8_lossy(&built.stdout) + ); + let out = Command::new("lake") + .args(["env", "lean", "Audit.lean"]) + .current_dir(lean_dir()) + .output() + .unwrap(); + let text = String::from_utf8_lossy(&out.stdout); + assert!(out.status.success(), "audit:\n{text}"); + for law in LAWS { + let line = text + .lines() + .find(|l| l.contains(&format!("Bookspec.{law}'"))) + .unwrap_or_else(|| panic!("{law} is not audited:\n{text}")); + for axiom in line + .split('[') + .nth(1) + .unwrap() + .trim_end_matches(']') + .split(", ") + { + assert!( + ["propext", "Quot.sound", "Classical.choice"].contains(&axiom.trim()), + "{law}: axiom {axiom}" + ); + } + } +} diff --git a/lean/.gitignore b/lean/.gitignore new file mode 100644 index 0000000..01f8cdb --- /dev/null +++ b/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/lean/Audit.lean b/lean/Audit.lean new file mode 100644 index 0000000..d528d73 --- /dev/null +++ b/lean/Audit.lean @@ -0,0 +1,14 @@ +import Bookspec + +/-! Each of the five laws' axioms are printed, and must be only Lean's +standard three (`propext`, `Quot.sound`, `Classical.choice`) or fewer. No +`sorryAx`, nothing assumed. `bookspec/checker/tests/lean.rs` reads this +file's output shape; run it with `lake env lean Audit.lean`. -/ + +open Bookspec + +#print axioms law_debits_equal_credits +#print axioms law_accounting_equation +#print axioms law_trial_balance +#print axioms law_net_income_articulates +#print axioms law_cash_flow_is_change_in_cash diff --git a/lean/Bookspec.lean b/lean/Bookspec.lean new file mode 100644 index 0000000..14fd6c2 --- /dev/null +++ b/lean/Bookspec.lean @@ -0,0 +1,2 @@ +import Bookspec.Laws +import Bookspec.Ledger diff --git a/lean/Bookspec/Basic.lean b/lean/Bookspec/Basic.lean new file mode 100644 index 0000000..ce4becd --- /dev/null +++ b/lean/Bookspec/Basic.lean @@ -0,0 +1,165 @@ +/-! +# Lines, sides, and nets + +The vocabulary of double entry. Money is `Int`: an exact count of the +smallest unit the books use. Any finite set of exact decimals (what the +engine stores) scales to integers without loss, and every law here is a +law of addition, so `Int` is a faithful model. + +Mirrors `crates/ledger-core/src/kernel.rs` (`flip`, `signed`, `net`, +`totals`) and `account.rs` (`Side`, `AccountType`, `normal_side`). +-/ + +namespace Bookspec + +/-- Debit or credit. -/ +inductive Side where + | debit + | credit + deriving DecidableEq, Repr + +/-- The other side (`kernel::flip`). -/ +def Side.flip : Side → Side + | .debit => .credit + | .credit => .debit + +@[simp] theorem Side.flip_flip (s : Side) : s.flip.flip = s := by + cases s <;> rfl + +theorem Side.flip_ne (s : Side) : s.flip ≠ s := by + cases s <;> simp [Side.flip] + +/-- The five account types. -/ +inductive AccountType where + | asset + | liability + | equity + | revenue + | expense + deriving DecidableEq, Repr + +/-- The side that increases an account (`AccountType::normal_side`). -/ +def AccountType.normal : AccountType → Side + | .asset | .expense => .debit + | .liability | .equity | .revenue => .credit + +/-- A line's signed amount: `+a` for a debit, `-a` for a credit +(`kernel::signed`). -/ +def signed : Side → Int → Int + | .debit, a => a + | .credit, a => -a + +@[simp] theorem signed_debit (a : Int) : signed .debit a = a := rfl +@[simp] theorem signed_credit (a : Int) : signed .credit a = -a := rfl + +theorem signed_flip (s : Side) (a : Int) : signed s.flip a = -signed s a := by + cases s <;> simp [Side.flip] + +/-- One journal line. -/ +structure Line where + account : Nat + side : Side + amount : Int + deriving DecidableEq, Repr + +/-- A line's signed amount. -/ +def Line.signed (l : Line) : Int := Bookspec.signed l.side l.amount + +/-- The net of some lines: debits minus credits (`kernel::net`). -/ +def net : List Line → Int + | [] => 0 + | l :: ls => l.signed + net ls + +/-- Total debits. -/ +def debits : List Line → Int + | [] => 0 + | l :: ls => (if l.side = .debit then l.amount else 0) + debits ls + +/-- Total credits. -/ +def credits : List Line → Int + | [] => 0 + | l :: ls => (if l.side = .credit then l.amount else 0) + credits ls + +@[simp] theorem net_nil : net [] = 0 := rfl +@[simp] theorem net_cons (l : Line) (ls : List Line) : net (l :: ls) = l.signed + net ls := rfl + +theorem net_append (xs ys : List Line) : net (xs ++ ys) = net xs + net ys := by + induction xs with + | nil => simp + | cons x xs ih => simp only [List.cons_append, net_cons, ih]; omega + +/-- The net is debits minus credits. -/ +theorem net_eq_debits_sub_credits (ls : List Line) : net ls = debits ls - credits ls := by + induction ls with + | nil => rfl + | cons l ls ih => + obtain ⟨a, s, m⟩ := l + cases s <;> simp [net, debits, credits, Line.signed, signed, ih] <;> omega + +/-- A sum over a list of account codes. -/ +def sumOver (f : Nat → Int) : List Nat → Int + | [] => 0 + | a :: as => f a + sumOver f as + +@[simp] theorem sumOver_nil (f : Nat → Int) : sumOver f [] = 0 := rfl +@[simp] theorem sumOver_cons (f : Nat → Int) (a : Nat) (as : List Nat) : + sumOver f (a :: as) = f a + sumOver f as := rfl + +theorem sumOver_add (f g : Nat → Int) (as : List Nat) : + sumOver (fun a => f a + g a) as = sumOver f as + sumOver g as := by + induction as with + | nil => rfl + | cons a as ih => simp only [sumOver_cons, ih]; omega + +theorem sumOver_neg (f : Nat → Int) (as : List Nat) : + sumOver (fun a => -f a) as = -sumOver f as := by + induction as with + | nil => rfl + | cons a as ih => simp only [sumOver_cons, ih]; omega + +theorem sumOver_zero (as : List Nat) : sumOver (fun _ => 0) as = 0 := by + induction as with + | nil => rfl + | cons a as ih => simp [ih] + +theorem sumOver_congr (f g : Nat → Int) (as : List Nat) (h : ∀ a ∈ as, f a = g a) : + sumOver f as = sumOver g as := by + induction as with + | nil => rfl + | cons a as ih => + simp only [sumOver_cons] + rw [h a (by simp), ih (fun b hb => h b (by simp [hb]))] + +/-- No code repeats (a chart's codes are unique). -/ +def Distinct : List Nat → Prop + | [] => True + | a :: as => a ∉ as ∧ Distinct as + +/-- Summing an indicator over codes that do not include `k` gives zero. -/ +theorem sumOver_indicator_absent (k : Nat) (x : Int) (as : List Nat) (h : k ∉ as) : + sumOver (fun a => if k = a then x else 0) as = 0 := by + induction as with + | nil => rfl + | cons a as ih => + have hka : k ≠ a := fun e => h (e ▸ List.mem_cons_self ..) + have hk : k ∉ as := fun hm => h (List.mem_cons_of_mem _ hm) + simp [hka, ih hk] + +/-- Summing an indicator over distinct codes that include `k` picks out +exactly one term. -/ +theorem sumOver_indicator (k : Nat) (x : Int) (as : List Nat) (hd : Distinct as) + (hk : k ∈ as) : sumOver (fun a => if k = a then x else 0) as = x := by + induction as with + | nil => simp at hk + | cons a as ih => + obtain ⟨ha, hd⟩ := hd + by_cases e : k = a + · subst e + simp [sumOver_indicator_absent k x as ha] + · have : k ∈ as := by + cases hk with + | head => exact absurd rfl e + | tail _ h => exact h + simp [e, ih hd this] + +end Bookspec diff --git a/lean/Bookspec/Closing.lean b/lean/Bookspec/Closing.lean new file mode 100644 index 0000000..c9ffca5 --- /dev/null +++ b/lean/Bookspec/Closing.lean @@ -0,0 +1,451 @@ +import Bookspec.Statements + +/-! +# Closing a period, and splitting the net + +Mirrors `kernel::closing_line`, `kernel::credit_line`, `kernel::plug_last`, +`periods::allocate`, and `Ledger::close_period_to` (income closing, net to +one equity account or split among members). +-/ + +namespace Bookspec + +/-- The line that zeroes an account with movement `m`: the opposite side, +same amount; nothing for zero (`kernel::closing_line`). It is also the +line that credits `m` to an account (`kernel::credit_line`). -/ +def closingLine (a : Nat) (m : Int) : List Line := + if 0 < m then [⟨a, .credit, m⟩] else if m < 0 then [⟨a, .debit, -m⟩] else [] + +theorem net_closingLine (a : Nat) (m : Int) : net (closingLine a m) = -m := by + unfold closingLine + split + · simp [Line.signed] + · split <;> simp [Line.signed] <;> omega + +theorem movement_closingLine (b a : Nat) (m : Int) : + movement b (closingLine a m) = if b = a then -m else 0 := by + by_cases e : b = a + · subst e + rcases (by omega : 0 < m ∨ m < 0 ∨ m = 0) with h | h | h + · simp [closingLine, h, Line.signed] + · have : ¬ 0 < m := by omega + simp [closingLine, h, this, Line.signed] + · simp [closingLine, h] + · have e' : ¬ a = b := fun x => e x.symm + unfold closingLine + split <;> (try split) <;> simp [e'] + +theorem closingLine_pos (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, 0 < l.amount := by + unfold closingLine + split + · simp; omega + · split + · simp; omega + · simp + +theorem closingLine_account (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, l.account = a := by + unfold closingLine + split + · simp + · split <;> simp + +theorem closingLine_eq_nil (a : Nat) (m : Int) : closingLine a m = [] ↔ m = 0 := by + unfold closingLine + split + · simp; omega + · split + · simp; omega + · simp; omega + +/-- The closing lines for some accounts: one per account with a nonzero +movement. -/ +def closings (as : List Nat) (ls : List Line) : List Line := + match as with + | [] => [] + | a :: as => closingLine a (movement a ls) ++ closings as ls + +theorem net_closings (as : List Nat) (ls : List Line) : + net (closings as ls) = -sumOver (fun a => movement a ls) as := by + induction as with + | nil => rfl + | cons a as ih => simp only [closings, net_append, net_closingLine, ih, sumOver_cons]; omega + +theorem movement_closings (b : Nat) (as : List Nat) (ls : List Line) (hd : Distinct as) : + movement b (closings as ls) = if b ∈ as then -movement b ls else 0 := by + induction as with + | nil => simp [closings] + | cons a as ih => + obtain ⟨ha, hd⟩ := hd + simp only [closings, movement_append, movement_closingLine, ih hd] + by_cases e : b = a + · subst e; simp [ha] + · simp [e] + +theorem closings_pos (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, 0 < l.amount := by + induction as with + | nil => simp [closings] + | cons a as ih => + intro l hl + simp only [closings, List.mem_append] at hl + cases hl with + | inl h => exact closingLine_pos _ _ l h + | inr h => exact ih l h + +theorem closings_account (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, l.account ∈ as := by + induction as with + | nil => simp [closings] + | cons a as ih => + intro l hl + simp only [closings, List.mem_append] at hl + cases hl with + | inl h => rw [closingLine_account _ _ l h]; simp + | inr h => exact List.mem_cons_of_mem _ (ih l h) + +/-- Nothing to close means every closed account was already at zero. -/ +theorem closings_eq_nil (as : List Nat) (ls : List Line) (h : closings as ls = []) : + ∀ a ∈ as, movement a ls = 0 := by + induction as with + | nil => simp + | cons a as ih => + simp only [closings, List.append_eq_nil_iff] at h + intro b hb + cases hb with + | head => exact (closingLine_eq_nil _ _).1 h.1 + | tail _ hb => exact ih h.2 b hb + +/-! ## The net to equity -/ + +/-- The sum of some amounts. -/ +def total : List Int → Int + | [] => 0 + | x :: xs => x + total xs + +/-- Lines crediting each target its part (`kernel::credit_line` per +member). -/ +def equityLines : List (Nat × Int) → List Line + | [] => [] + | (t, c) :: ts => closingLine t c ++ equityLines ts + +theorem net_equityLines (ts : List (Nat × Int)) : + net (equityLines ts) = -total (ts.map Prod.snd) := by + induction ts with + | nil => rfl + | cons x ts ih => + obtain ⟨t, c⟩ := x + simp only [equityLines, net_append, net_closingLine, ih, List.map_cons, total]; omega + +theorem movement_equityLines_absent (b : Nat) (ts : List (Nat × Int)) + (h : ∀ x ∈ ts, x.1 ≠ b) : movement b (equityLines ts) = 0 := by + induction ts with + | nil => rfl + | cons x ts ih => + obtain ⟨t, c⟩ := x + have ht : b ≠ t := fun e => h (t, c) (by simp) e.symm + simp only [equityLines, movement_append, movement_closingLine, ht, ite_false, + ih (fun y hy => h y (List.mem_cons_of_mem _ hy))] + rfl + +theorem equityLines_pos (ts : List (Nat × Int)) : ∀ l ∈ equityLines ts, 0 < l.amount := by + induction ts with + | nil => simp [equityLines] + | cons x ts ih => + obtain ⟨t, c⟩ := x + intro l hl + simp only [equityLines, List.mem_append] at hl + cases hl with + | inl h => exact closingLine_pos _ _ l h + | inr h => exact ih l h + +theorem equityLines_account (ts : List (Nat × Int)) : + ∀ l ∈ equityLines ts, ∃ x ∈ ts, l.account = x.1 := by + induction ts with + | nil => simp [equityLines] + | cons x ts ih => + obtain ⟨t, c⟩ := x + intro l hl + simp only [equityLines, List.mem_append] at hl + cases hl with + | inl h => exact ⟨(t, c), by simp, closingLine_account _ _ l h⟩ + | inr h => + obtain ⟨y, hy, e⟩ := ih l h + exact ⟨y, List.mem_cons_of_mem _ hy, e⟩ + +theorem equityLines_eq_nil (ts : List (Nat × Int)) (h : equityLines ts = []) : + total (ts.map Prod.snd) = 0 := by + induction ts with + | nil => rfl + | cons x ts ih => + obtain ⟨t, c⟩ := x + simp only [equityLines, List.append_eq_nil_iff] at h + simp only [List.map_cons, total, (closingLine_eq_nil _ _).1 h.1, ih h.2]; rfl + +/-- The closing entry: zero the closed accounts, credit the net to the +targets. -/ +def closingEntry (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) : List Line := + closings as ls ++ equityLines ts + +/-- **A closing entry balances** when the targets' parts sum to the net +of the closing lines (the net income), however that net was split. -/ +theorem closingEntry_net (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) + (hsum : total (ts.map Prod.snd) = net (closings as ls)) : + net (closingEntry as ts ls) = 0 := by + rw [closingEntry, net_append, net_equityLines, hsum]; omega + +/-- **A closing entry zeroes every account it closes.** -/ +theorem closingEntry_zeroes (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) + (hd : Distinct as) (b : Nat) (hb : b ∈ as) (ht : ∀ x ∈ ts, x.1 ≠ b) : + movement b (ls ++ closingEntry as ts ls) = 0 := by + rw [movement_append, closingEntry, movement_append, movement_closings b as ls hd, + movement_equityLines_absent b ts ht] + simp only [hb, ite_true]; omega + +/-- **A non-empty closing entry is acceptable**: two or more lines, every +amount positive, debits equal to credits. -/ +theorem closingEntry_accepted (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) + (hsum : total (ts.map Prod.snd) = net (closings as ls)) (hne : closings as ls ≠ []) : + Accepted (closingEntry as ts ls) := by + refine ⟨?_, ?_, ?_⟩ + · rw [closingEntry, List.length_append] + match hc : closings as ls with + | [] => exact absurd hc hne + | [l] => + have hl : 0 < l.amount := closings_pos as ls l (by rw [hc]; simp) + have hnet : net (closings as ls) ≠ 0 := by + rw [hc]; obtain ⟨a, s, m⟩ := l + cases s <;> simp [Line.signed] at hl ⊢ <;> omega + have : equityLines ts ≠ [] := fun h => hnet (hsum ▸ equityLines_eq_nil ts h) + have : 1 ≤ (equityLines ts).length := by + cases h : equityLines ts with + | nil => exact absurd h this + | cons _ _ => simp + simp; omega + | _ :: _ :: _ => simp; omega + · intro l hl + simp only [closingEntry, List.mem_append] at hl + cases hl with + | inl h => exact closings_pos as ls l h + | inr h => exact equityLines_pos ts l h + · have := closingEntry_net as ts ls hsum + rw [net_eq_debits_sub_credits] at this; omega + +/-! ## Net income -/ + +/-- The chart's revenue and expense codes: what a close zeroes. -/ +def nominalCodes : Chart → List Nat + | [] => [] + | (a, t) :: c => if t = .revenue ∨ t = .expense then a :: nominalCodes c else nominalCodes c + +theorem nominalCodes_sub (c : Chart) : ∀ a ∈ nominalCodes c, a ∈ codes c := by + induction c with + | nil => simp [nominalCodes] + | cons x c ih => + obtain ⟨a, t⟩ := x + intro b hb + simp only [nominalCodes] at hb + split at hb + · cases hb with + | head => simp + | tail _ h => exact List.mem_cons_of_mem _ (ih b h) + · exact List.mem_cons_of_mem _ (ih b hb) + +theorem nominalCodes_distinct (c : Chart) (hd : Distinct (codes c)) : Distinct (nominalCodes c) := by + induction c with + | nil => trivial + | cons x c ih => + obtain ⟨a, t⟩ := x + obtain ⟨ha, hd⟩ := hd + simp only [nominalCodes] + split + · exact ⟨fun h => ha (nominalCodes_sub c a h), ih hd⟩ + · exact ih hd + +/-- **The net a close credits to equity is the period's net income**: +revenue balances minus expense balances. -/ +theorem net_closings_is_net_income (c : Chart) (ls : List Line) : + net (closings (nominalCodes c) ls) = typeTotal .revenue ls c - typeTotal .expense ls c := by + rw [net_closings] + induction c with + | nil => rfl + | cons x c ih => + obtain ⟨a, t⟩ := x + cases t <;> simp [nominalCodes, typeTotal, balance, AccountType.normal, signed] at ih ⊢ <;> omega + +/-! ## Splitting among members -/ + +/-- Make rounded parts sum to the whole: the last becomes the whole minus +the others (`kernel::plug_last`). -/ +def plugLast (whole : Int) : List Int → List Int + | [] => [] + | [_] => [whole] + | p :: q :: rest => p :: plugLast (whole - p) (q :: rest) + +/-- **An allocation's parts sum to the whole, exactly**, however the +other parts were rounded. -/ +theorem plugLast_total (whole : Int) (ps : List Int) (h : ps ≠ []) : + total (plugLast whole ps) = whole := by + induction ps generalizing whole with + | nil => exact absurd rfl h + | cons p rest ih => + match rest, ih with + | [], _ => show total [whole] = whole; simp [total] + | q :: rest, ih => + simp only [plugLast, total] + have := ih (whole - p) (by simp) + omega + +theorem plugLast_length (whole : Int) (ps : List Int) : (plugLast whole ps).length = ps.length := by + induction ps generalizing whole with + | nil => rfl + | cons p rest ih => + match rest, ih with + | [], _ => rfl + | q :: rest, ih => simp only [plugLast, List.length_cons]; rw [ih]; rfl + +/-- Only the last part changes. -/ +theorem plugLast_keeps (whole : Int) (ps : List Int) : + (plugLast whole ps).dropLast = ps.dropLast := by + induction ps generalizing whole with + | nil => rfl + | cons p rest ih => + match rest, ih with + | [], _ => rfl + | q :: rest, ih => + have hne : plugLast (whole - p) (q :: rest) ≠ [] := by + intro h + have := plugLast_length (whole - p) (q :: rest) + rw [h] at this; simp at this + rw [show plugLast whole (p :: q :: rest) = p :: plugLast (whole - p) (q :: rest) from rfl, + List.dropLast_cons_of_ne_nil hne, ih, List.dropLast_cons_cons] + +/-! ## Cumulative member closes + +A run of members closes under the run rule of 2026-10-13 to P3 +(`CloseTo::MembersRun`, journaled `"cumulative"`; rules.md B-13) gives each +member, at each close, their allocation of the run's total so far minus +their allocation of the total before it. `alloc` is any allocation of an +amount to members (member `i` gets `alloc x i`), such as +`periods::allocate`. -/ + +/-- What one close gives member `i`: `before` is the run's total before +it, `net` what it closes. -/ +def closePart (alloc : Int → Nat → Int) (before net : Int) (i : Nat) : Int := + alloc (before + net) i - alloc before i + +/-- What a run of closes with these nets, starting after `before`, gives +member `i` in all. -/ +def runPart (alloc : Int → Nat → Int) : Int → List Int → Nat → Int + | _, [], _ => 0 + | before, net :: rest, i => closePart alloc before net i + runPart alloc (before + net) rest i + +/-- **A run telescopes**: member `i`'s total from a run is their allocation +of everything the run closed, less their allocation of where it started. +From an empty start (`alloc 0 = 0`), it is exactly their allocation of +the run's total, so its rounding is one allocation's rounding, never a +sum of them. -/ +theorem runPart_telescopes (alloc : Int → Nat → Int) (before : Int) (nets : List Int) (i : Nat) : + runPart alloc before nets i = alloc (before + nets.sum) i - alloc before i := by + induction nets generalizing before with + | nil => simp [runPart] + | cons n rest ih => + simp only [runPart, closePart, ih, List.sum_cons] + rw [show before + n + rest.sum = before + (n + rest.sum) by omega] + omega + +/-- A sum of differences is the difference of the sums. -/ +theorem sum_map_sub (f g : Nat → Int) (ms : List Nat) : + (ms.map (fun i => f i - g i)).sum = (ms.map f).sum - (ms.map g).sum := by + induction ms with + | nil => simp + | cons m ms ih => simp only [List.map_cons, List.sum_cons, ih]; omega + +/-- **Each close hands out exactly its net** when every allocation sums +to its amount (`periods::allocate` does: `kernel::apportion`). -/ +theorem closePart_total (alloc : Int → Nat → Int) (members : List Nat) + (sums : ∀ x, (members.map (alloc x)).sum = x) (before net : Int) : + (members.map (closePart alloc before net)).sum = net := by + have h := sum_map_sub (alloc (before + net)) (alloc before) members + unfold closePart + rw [h, sums, sums] + omega + +/-! ## Members closes counted from a count's start (P3) + +The rule since P3 (`CloseTo::Members`, rules.md B-13; D-10): a close gives +member `i` their allocation of everything the count has closed (`closed` +before it, plus its `net`), less what the count's earlier closes gave them +(`given i`), whatever rule those closes were made under +(`periods::allocate_cumulative`, `kernel::apportion_cumulative`). The run +rule of 2026-10-13 (`CloseTo::MembersRun`, `closePart`) is the special case +where the earlier closes gave exactly the allocation. -/ + +/-- What a cumulative close gives member `i`. -/ +def trueUp (alloc : Int → Nat → Int) (closed net : Int) (given : Nat → Int) (i : Nat) : Int := + alloc (closed + net) i - given i + +/-- **A cumulative close hands out exactly its net**, whatever rule the +earlier closes used, as long as they handed out what they closed. -/ +theorem trueUp_total (alloc : Int → Nat → Int) (members : List Nat) + (sums : ∀ x, (members.map (alloc x)).sum = x) (closed net : Int) (given : Nat → Int) + (hg : (members.map given).sum = closed) : + (members.map (trueUp alloc closed net given)).sum = net := by + have h := sum_map_sub (alloc (closed + net)) given members + unfold trueUp + rw [h, sums, hg] + omega + +/-- **A running total is one allocation**: after the close, what the count +has given member `i` is their allocation of everything it closed, so its +rounding is one allocation's, never a sum of them. -/ +theorem trueUp_running (alloc : Int → Nat → Int) (closed net : Int) (given : Nat → Int) + (i : Nat) : given i + trueUp alloc closed net given i = alloc (closed + net) i := by + unfold trueUp + omega + +/-- The run rule is the special case `given = alloc closed`. -/ +theorem closePart_eq_trueUp (alloc : Int → Nat → Int) (before net : Int) (i : Nat) : + closePart alloc before net i = trueUp alloc before net (alloc before) i := rfl + +/-- **Bounded drift, for any history**: when every allocation is under one +unit from exact (scaled by `W`, the shares being `w i / W`), so is every +member's running total after a cumulative close, whatever the earlier +closes gave (`Apportion.allocW_drift` supplies the hypothesis). -/ +theorem cumulative_drift (alloc : Int → Nat → Int) (w : Nat → Int) (W : Int) + (hd : ∀ x i, -W < alloc x i * W - x * w i ∧ alloc x i * W - x * w i < W) + (closed net : Int) (given : Nat → Int) (i : Nat) : + -W < (given i + trueUp alloc closed net given i) * W - (closed + net) * w i ∧ + (given i + trueUp alloc closed net given i) * W - (closed + net) * w i < W := by + rw [trueUp_running] + exact hd _ _ + +/-- The statement of members' equity's share of the earnings `U` not yet +closed, as of a day: what the count's next close would give of them, its +allocation of `closed + U` less its allocation of `closed` (D-38; P3 review +R-1: never the true-up a close hasn't posted). -/ +def unclosedShare (alloc : Int → Nat → Int) (closed U : Int) (i : Nat) : Int := + alloc (closed + U) i - alloc closed i + +/-- **Closing a period moves a member's capital on a day by exactly the +true-up the close posts** (D-38, R-1): before, their capital `cap` plus +their share of the unclosed `U`; after closing `net` of it, `cap` plus the +close's part plus their share of the rest. The difference is +`alloc closed i - given i`. -/ +theorem statement_after_close (alloc : Int → Nat → Int) (cap closed net U : Int) + (given : Nat → Int) (i : Nat) : + cap + trueUp alloc closed net given i + unclosedShare alloc (closed + net) (U - net) i + = cap + unclosedShare alloc closed U i + (alloc closed i - given i) := by + unfold trueUp unclosedShare + rw [show closed + net + (U - net) = closed + U by omega] + omega + +/-- **A member's capital on a day never moves when its period is closed** +(D-38), once the count's closes gave what the cumulative rule gives +(`given = alloc closed`: every count the rule began, and every count after +its first close that posts). -/ +theorem statement_unmoved_by_close (alloc : Int → Nat → Int) (cap closed net U : Int) + (i : Nat) : + cap + trueUp alloc closed net (alloc closed) i + unclosedShare alloc (closed + net) (U - net) i + = cap + unclosedShare alloc closed U i := by + rw [statement_after_close] + omega + +end Bookspec diff --git a/lean/Bookspec/Entry.lean b/lean/Bookspec/Entry.lean new file mode 100644 index 0000000..8edb3f8 --- /dev/null +++ b/lean/Bookspec/Entry.lean @@ -0,0 +1,117 @@ +import Bookspec.Basic + +/-! +# Entries: acceptance, movements, reversals + +Mirrors `kernel::check_lines`, `kernel::movements`, `kernel::reversal`, +and `JournalEntry::validate`. +-/ + +namespace Bookspec + +/-- What the engine accepts (the arithmetic of `JournalEntry::validate`, +i.e. `kernel::check_lines`): two or more lines, every amount positive, +debits equal to credits. (Range, account, and currency checks are not +arithmetic laws and are left out of the model.) -/ +def Accepted (ls : List Line) : Prop := + 2 ≤ ls.length ∧ (∀ l ∈ ls, 0 < l.amount) ∧ debits ls = credits ls + +/-- **Every accepted entry nets to zero.** -/ +theorem Accepted.net_zero {ls : List Line} (h : Accepted ls) : net ls = 0 := by + rw [net_eq_debits_sub_credits]; have := h.2.2; omega + +/-- Net movement of account `a` over some lines. -/ +def movement (a : Nat) : List Line → Int + | [] => 0 + | l :: ls => (if l.account = a then l.signed else 0) + movement a ls + +@[simp] theorem movement_nil (a : Nat) : movement a [] = 0 := rfl +@[simp] theorem movement_cons (a : Nat) (l : Line) (ls : List Line) : + movement a (l :: ls) = (if l.account = a then l.signed else 0) + movement a ls := rfl + +theorem movement_append (a : Nat) (xs ys : List Line) : + movement a (xs ++ ys) = movement a xs + movement a ys := by + induction xs with + | nil => simp + | cons x xs ih => simp only [List.cons_append, movement_cons, ih]; omega + +/-- **Movements partition the net.** Summed over a chart's distinct codes +that cover every line's account, the per-account movements add up to the +net of the lines: grouping by account loses and invents nothing. -/ +theorem sum_movements (as : List Nat) (hd : Distinct as) : + ∀ ls : List Line, (∀ l ∈ ls, l.account ∈ as) → + sumOver (fun a => movement a ls) as = net ls := by + intro ls + induction ls with + | nil => intro _; simpa using sumOver_zero as + | cons l ls ih => + intro hcov + simp only [movement_cons, net_cons] + rw [sumOver_add, ih (fun m hm => hcov m (List.mem_cons_of_mem _ hm)), + sumOver_indicator l.account l.signed as hd (hcov l (List.mem_cons_self ..))] + +/-- So the movements of an accepted entry sum to zero. -/ +theorem Accepted.movements_sum_zero {ls : List Line} (h : Accepted ls) (as : List Nat) + (hd : Distinct as) (hcov : ∀ l ∈ ls, l.account ∈ as) : + sumOver (fun a => movement a ls) as = 0 := by + rw [sum_movements as hd ls hcov, h.net_zero] + +/-! ## Reversals -/ + +/-- A line with its side flipped. -/ +def Line.reverse (l : Line) : Line := { l with side := l.side.flip } + +/-- A reversing entry's lines (`kernel::reversal`). -/ +def reversal (ls : List Line) : List Line := ls.map Line.reverse + +theorem Line.reverse_signed (l : Line) : l.reverse.signed = -l.signed := by + simp [Line.reverse, Line.signed, signed_flip] + +theorem net_reversal (ls : List Line) : net (reversal ls) = -net ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + simp only [net_cons, ih, Line.reverse_signed]; omega + +theorem movement_reversal (a : Nat) (ls : List Line) : + movement a (reversal ls) = -movement a ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + simp only [movement_cons, ih, Line.reverse_signed] + by_cases h : l.account = a <;> simp [Line.reverse, h] <;> omega + +/-- **An entry and its reversal net every account to zero.** -/ +theorem movement_with_reversal (a : Nat) (ls : List Line) : + movement a (ls ++ reversal ls) = 0 := by + rw [movement_append, movement_reversal]; omega + +theorem debits_reversal (ls : List Line) : debits (reversal ls) = credits ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + obtain ⟨a, s, m⟩ := l + cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih] + +theorem credits_reversal (ls : List Line) : credits (reversal ls) = debits ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + obtain ⟨a, s, m⟩ := l + cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih] + +/-- **A reversal is accepted exactly when the original is.** -/ +theorem accepted_reversal_iff (ls : List Line) : Accepted (reversal ls) ↔ Accepted ls := by + unfold Accepted + rw [debits_reversal, credits_reversal] + have hlen : (reversal ls).length = ls.length := List.length_map .. + have hpos : (∀ l ∈ reversal ls, 0 < l.amount) ↔ (∀ l ∈ ls, 0 < l.amount) := by + simp [reversal, Line.reverse] + rw [hlen, hpos] + constructor <;> rintro ⟨a, b, c⟩ <;> exact ⟨a, b, c.symm⟩ + +end Bookspec diff --git a/lean/Bookspec/Laws.lean b/lean/Bookspec/Laws.lean new file mode 100644 index 0000000..9669a64 --- /dev/null +++ b/lean/Bookspec/Laws.lean @@ -0,0 +1,62 @@ +import Bookspec.Ledger + +/-! +# bookspec's five laws + +The five laws of the first edition (`bookspec/spec/00-model.md`, "The five +laws"), each stated once, by name, as a theorem about *every* reachable +state of the books, ported from `verify/lean` (P13 step 4). Money is `Int`, +an exact count of the smallest unit; any finite set of exact decimals +scales to integers without loss, and every law is a law of addition. + +1. Debits equal credits (BS-entry-1). +2. Assets = Liabilities + Equity + (Revenue - Expenses) (BS-statement-2). +3. The trial balance balances (BS-statement-1). +4. Net income articulates to equity: a close credits equity with exactly + revenue less expenses (BS-period-1). +5. The cash-flow sections sum to the change in cash (BS-statement-3). +-/ + +namespace Bookspec + +/-- Law 1. In every reachable state the posted lines' debits equal their +credits (`net` is debits less credits). -/ +theorem law_debits_equal_credits {L : Ledger} (r : Reachable L) : + net (allLines L.posted) = 0 := + r.books_net_zero + +/-- Law 2. The accounting equation, in every reachable state. -/ +theorem law_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) := + r.accounting_equation + +/-- Law 3. The trial balance balances, in every reachable state. -/ +theorem law_trial_balance {L : Ledger} (r : Reachable L) : + tbDebits (allLines L.posted) (codes L.chart) + = tbCredits (allLines L.posted) (codes L.chart) := + r.trial_balance + +/-- Law 4. A close credits equity with exactly the period's net income. -/ +theorem law_net_income_articulates (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 := + close_credits_net_income L p ts hsum + +/-- Law 5. The three sections of the statement of cash flows sum to the +change in the cash accounts. -/ +theorem law_cash_flow_is_change_in_cash {L : Ledger} (r : Reachable L) (b c : Nat) + (hbc : b ≤ c) (F : List Line → Line → Flow) (C : List Line → List Int) + (hC : ∀ e, sum3 (C e) = 0) (cash : List Nat) (hd : Distinct cash) + (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) : + let es := (between b c L.posted).map Entry.lines + sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es + = sumOver (fun a => movement a (allLines (through c L.posted))) cash + - sumOver (fun a => movement a (allLines (through b L.posted))) cash := + r.cashflow_is_change_in_cash b c hbc F C hC cash hd hF + +end Bookspec diff --git a/lean/Bookspec/Ledger.lean b/lean/Bookspec/Ledger.lean new file mode 100644 index 0000000..d3ee8c7 --- /dev/null +++ b/lean/Bookspec/Ledger.lean @@ -0,0 +1,562 @@ +import Bookspec.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`; and, as one step +`record`, everything the books keep about how they are kept: settings, +conventions, decisions, open items and approvals (`apply_settings`, +`apply_convention`, `apply_decision`, `apply_open_item`, +`apply_approval`, and their retirements and resolutions), each a record +the step adds and nothing else; and an account's rename +(`rename_account`, `account.renamed`, rules.md B-31), since the model's +chart is codes and types and a name is no part of it. +-/ + +namespace Bookspec + +/-- 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, +and the record of how they are kept (settings, conventions, decisions, +open items, approvals), each record abstracted to a number. -/ +structure Ledger where + chart : Chart + posted : List Entry + drafts : List Entry + periods : List Period + records : List Nat + +/-- 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 } + /-- `apply_settings`, `apply_convention`, `apply_decision`, + `apply_open_item`, `apply_approval` and their retirements and + resolutions, and the 1099 records `set_vendor_1099`, + `set_vendor_w9_flag`, `add_instrument` and `set_entry_instrument`: a + record of how the books are kept, and nothing else. `rename_account` + too: a name is outside the chart the model keeps. -/ + | record (L : Ledger) (r : Nat) : Step L { L with records := r :: L.records } + +/-- 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 + | record r => exact ⟨h.distinct, h.accepted, h.known, h.draftsOpen⟩ + +/-- **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) := + Bookspec.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) := + Bookspec.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⟩ + | record => exact ⟨[], by simp⟩ + +/-- 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 + +/-! ## The statement of cash flows foots (rules.md B-14 rule 9) -/ + +/-- Some entries' cash, summed, is the movement of the cash accounts over +their lines, when the cash tag follows the account. -/ +theorem cashTotal_is_movement (F : List Line → Line → Flow) (cash : List Nat) + (hd : Distinct cash) (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) : + ∀ xs : List Entry, + cashTotal F (xs.map Entry.lines) = sumOver (fun a => movement a (allLines xs)) cash := by + intro xs + induction xs with + | nil => simpa [cashTotal, allLines] using (sumOver_zero cash).symm + | cons x xs ih => + simp only [List.map_cons, cashTotal, allLines, movement_append] + rw [sumOver_add, ← ih, cashOf, secNet_cash_is_movement (F x.lines) cash hd (hF x.lines)] + +/-- **The statement of cash flows foots**, in every reachable state: over +the posted entries dated after day `b` through day `c` (any selection of +them, `p`: the engine leaves out closing entries), operating + investing + +financing is the movement of the cash accounts over the same entries, for +any tagging whose cash tag follows the account, and whatever a member or +lender handled for each entry (`C`, rule 11) as long as it nets to zero +(`constructive_nets`). Every posted entry is accepted (`Reachable.inv`), +so each nets to zero. -/ +theorem Reachable.cashflow_foots {L : Ledger} (r : Reachable L) (b c : Nat) (p : Entry → Bool) + (F : List Line → Line → Flow) (C : List Line → List Int) (hC : ∀ e, sum3 (C e) = 0) + (cash : List Nat) (hd : Distinct cash) + (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) : + let xs := (between b c L.posted).filter p + sectionTotal F C 0 (xs.map Entry.lines) + sectionTotal F C 1 (xs.map Entry.lines) + + sectionTotal F C 2 (xs.map Entry.lines) + = sumOver (fun a => movement a (allLines xs)) cash := by + intro xs + rw [cashflow_sections_sum_to_cash_change, cashTotal_is_movement F cash hd hF] + · intro e he + obtain ⟨x, hx, rfl⟩ := List.mem_map.1 he + have hb := (List.mem_filter.1 hx).1 + exact (r.inv.accepted x (List.mem_filter.1 hb).1).net_zero + · exact fun e _ => hC e + +/-- **The sections are the change in the cash accounts' balances**: with +every entry between `b` and `c` counted, the three sections sum to the +cash accounts' movement through `c` less their movement through `b` +(their ending balance less their beginning balance). -/ +theorem Reachable.cashflow_is_change_in_cash {L : Ledger} (r : Reachable L) (b c : Nat) + (hbc : b ≤ c) (F : List Line → Line → Flow) (C : List Line → List Int) + (hC : ∀ e, sum3 (C e) = 0) (cash : List Nat) (hd : Distinct cash) + (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) : + let es := (between b c L.posted).map Entry.lines + sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es + = sumOver (fun a => movement a (allLines (through c L.posted))) cash + - sumOver (fun a => movement a (allLines (through b L.posted))) cash := by + intro es + have h := r.cashflow_foots b c (fun _ => true) F C hC cash hd hF + have hall : (between b c L.posted).filter (fun _ => true) = between b c L.posted := + List.filter_eq_self.2 (fun _ _ => rfl) + simp only [hall] at h + rw [h] + have hs : ∀ a, movement a (allLines (through c L.posted)) + = movement a (allLines (through b L.posted)) + movement a (allLines (between b c L.posted)) := + fun a => movement_split a b c hbc L.posted + rw [sumOver_congr _ _ cash (fun a _ => hs a), sumOver_add] + omega + +/-- **A reversal and its original in one period drop out together**: for +an entry and its reversal (lines flipped, tagged as the original's, and +what was handled for it mirrored, `constructive_neg`), the sum of their +flows in each section is zero. -/ +theorem cashflow_reversal_nets (F : List Line → Line → Flow) (C : List Line → List Int) + (e : List Line) (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l) + (hC : C (reversal e) = (C e).map (fun x => -x)) (k : Nat) : + sectionTotal F C k [e, reversal e] = 0 := by + simp only [sectionTotal, stmt_flows_reversal F C e hF hC, getD_neg] + omega + +/-! ## How the books are kept changes no figure -/ + +/-- **A record changes nothing the books hold**: a settings change, a +convention, a decision, an open item or an approval leaves the chart, every +posted entry, every draft and every period exactly as they were. (The +`record` step touches only `records` by definition: this pins the model. +The engine's side is checked in Rust by `settings_replay_is_pure`. +Settings that change how the same entries are presented, such as the +fiscal year, are outside the model.) -/ +theorem Step.record_changes_no_figure (L : Ledger) (r : Nat) : + let L' : Ledger := { L with records := r :: L.records } + L'.chart = L.chart ∧ L'.posted = L.posted ∧ L'.drafts = L.drafts ∧ L'.periods = L.periods := + ⟨rfl, rfl, rfl, rfl⟩ + +/-- **Any number of records changes no figure**, and they keep the +invariant: a reachable state plus records is reachable, with the same +books. -/ +theorem Reachable.records {L : Ledger} (h : Reachable L) (rs : List Nat) : + Reachable { L with records := rs ++ L.records } := by + induction rs with + | nil => simpa using h + | cons r rs ih => exact Reachable.step ih (Step.record _ r) + +end Bookspec diff --git a/lean/Bookspec/Statements.lean b/lean/Bookspec/Statements.lean new file mode 100644 index 0000000..011e4a3 --- /dev/null +++ b/lean/Bookspec/Statements.lean @@ -0,0 +1,683 @@ +import Bookspec.Entry + +/-! +# Balances and statements + +Mirrors `kernel::normal_balance`, `kernel::columns`, +`Ledger::account_balance`, and `reports::trial_balance`; and the statement +of cash flows (`kernel::take`, `kernel::apply_cash`, `kernel::entry_flows`, +`kernel::constructive`, `cashflow::cash_flow`'s footing and reconciliation +checks). +-/ + +namespace Bookspec + +/-- A chart of accounts: each account's code and type. -/ +abbrev Chart := List (Nat × AccountType) + +/-- The chart's codes. -/ +def codes (c : Chart) : List Nat := c.map Prod.fst + +@[simp] theorem codes_nil : codes [] = [] := rfl +@[simp] theorem codes_cons (a : Nat) (t : AccountType) (c : Chart) : + codes ((a, t) :: c) = a :: codes c := rfl + +/-- An account's balance on its normal side (`kernel::normal_balance`). -/ +def balance (t : AccountType) (m : Int) : Int := signed t.normal m + +/-- **A normal-side line raises a balance by its amount; an opposite-side +line lowers it.** -/ +theorem balance_after_line (t : AccountType) (m : Int) (s : Side) (a : Int) : + balance t (m + signed s a) = balance t m + (if s = t.normal then a else -a) := by + cases t <;> cases s <;> simp [balance, AccountType.normal, signed] <;> omega + +/-- The total balance of every account of type `t`. -/ +def typeTotal (t : AccountType) (ls : List Line) : Chart → Int + | [] => 0 + | (a, t') :: rest => (if t' = t then balance t' (movement a ls) else 0) + typeTotal t ls rest + +/-- The accounting equation's two sides differ by the net movement of the +chart's accounts. -/ +theorem equation_gap (ls : List Line) (c : Chart) : + typeTotal .asset ls c + typeTotal .expense ls c + - typeTotal .liability ls c - typeTotal .equity ls c - typeTotal .revenue ls c + = sumOver (fun a => movement a ls) (codes c) := by + induction c with + | nil => rfl + | cons x c ih => + obtain ⟨a, t⟩ := x + cases t <;> simp [typeTotal, balance, AccountType.normal, signed] <;> omega + +/-- **The accounting equation.** For lines that net to zero, over a chart +with distinct codes covering every line's account: +Assets = Liabilities + Equity + (Revenue - Expenses). -/ +theorem accounting_equation (ls : List Line) (c : Chart) (hd : Distinct (codes c)) + (hcov : ∀ l ∈ ls, l.account ∈ codes c) (hnet : net ls = 0) : + typeTotal .asset ls c + = typeTotal .liability ls c + typeTotal .equity ls c + + (typeTotal .revenue ls c - typeTotal .expense ls c) := by + have := equation_gap ls c + rw [sum_movements _ hd ls hcov, hnet] at this + omega + +/-! ## Trial balance -/ + +/-- The debit column for a movement (`kernel::columns`). -/ +def colDebit (m : Int) : Int := if 0 < m then m else 0 +/-- The credit column for a movement (`kernel::columns`). -/ +def colCredit (m : Int) : Int := if 0 < m then 0 else -m + +theorem columns_spec (m : Int) : + 0 ≤ colDebit m ∧ 0 ≤ colCredit m ∧ (colDebit m = 0 ∨ colCredit m = 0) + ∧ colDebit m - colCredit m = m := by + unfold colDebit colCredit; split <;> omega + +/-- The trial balance's debit column total. -/ +def tbDebits (ls : List Line) (as : List Nat) : Int := sumOver (fun a => colDebit (movement a ls)) as +/-- The trial balance's credit column total. -/ +def tbCredits (ls : List Line) (as : List Nat) : Int := + sumOver (fun a => colCredit (movement a ls)) as + +theorem tb_gap (ls : List Line) (as : List Nat) : + tbDebits ls as - tbCredits ls as = sumOver (fun a => movement a ls) as := by + induction as with + | nil => rfl + | cons a as ih => + simp only [tbDebits, tbCredits, sumOver_cons] at ih ⊢ + have := (columns_spec (movement a ls)).2.2.2 + omega + +/-- **The trial balance balances** for lines that net to zero. -/ +theorem trial_balance_balances (ls : List Line) (as : List Nat) (hd : Distinct as) + (hcov : ∀ l ∈ ls, l.account ∈ as) (hnet : net ls = 0) : + tbDebits ls as = tbCredits ls as := by + have := tb_gap ls as + rw [sum_movements as hd ls hcov, hnet] at this + omega + +/-- And conversely: a balanced trial balance means the lines net to zero. +The trial balance is a complete check of the books' arithmetic. -/ +theorem trial_balance_iff (ls : List Line) (as : List Nat) (hd : Distinct as) + (hcov : ∀ l ∈ ls, l.account ∈ as) : + tbDebits ls as = tbCredits ls as ↔ net ls = 0 := by + have := tb_gap ls as + rw [sum_movements as hd ls hcov] at this + omega + +/-! ## The statement of cash flows (rules.md B-14) + +Mirrors `kernel::Flow`, `kernel::take`, `kernel::apply_cash` and +`kernel::entry_flows`, and the identities `cashflow::cash_flow` checks at +runtime: the sections sum to the cash accounts' change, a reversal's flows +are its original's negated, and net income reconciles to operating cash. + +Lines are tagged per entry (`F : List Line → Line → Flow`), as the engine +tags them: a revenue or expense line is operating in one entry and +investing in another (rule 4), and a reversal is tagged by its chain's +root. The theorems hold for every such tagging; their hypotheses say what +the engine guarantees (the cash tag follows the account; revenue and +expense lines are operating or investing; a reversal's lines take its +original's tags). A line the engine splits between two sections (the bill +split, rule 12) is two lines here; a split keeps the entry's net. -/ + +/-- Where a line falls on the statement of cash flows (`kernel::Flow`). -/ +inductive Flow where + | cash + | operating + | investing + | financing + deriving DecidableEq, Repr + +/-- The net movement of the lines `f` tags `k`. -/ +def secNet (f : Line → Flow) (k : Flow) : List Line → Int + | [] => 0 + | l :: ls => (if f l = k then l.signed else 0) + secNet f k ls + +@[simp] theorem secNet_nil (f : Line → Flow) (k : Flow) : secNet f k [] = 0 := rfl +@[simp] theorem secNet_cons (f : Line → Flow) (k : Flow) (l : Line) (ls : List Line) : + secNet f k (l :: ls) = (if f l = k then l.signed else 0) + secNet f k ls := rfl + +/-- **Every line is in exactly one place**: an entry's net is its cash plus +its three sections' movements. -/ +theorem net_splits_by_flow (f : Line → Flow) (ls : List Line) : + net ls = secNet f .cash ls + secNet f .operating ls + secNet f .investing ls + + secNet f .financing ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [net_cons, secNet_cons, ih] + cases f l <;> simp <;> omega + +/-- The cash one section takes from what is left (`kernel::take`): only a +section moving against the cash, never more than its own movement. -/ +def take (rem n : Int) : Int := + if 0 < rem ∧ n < 0 then min rem (-n) else if rem < 0 ∧ 0 < n then max rem (-n) else 0 + +/-- `kernel::apply_cash`: the cash applied to each movement in order, and +what is left. -/ +def applyCash : Int → List Int → List Int × Int + | rem, [] => ([], rem) + | rem, n :: ns => (take rem n :: (applyCash (rem - take rem n) ns).1, + (applyCash (rem - take rem n) ns).2) + +/-- A sum of integers. -/ +def isum : List Int → Int + | [] => 0 + | x :: xs => x + isum xs + +@[simp] theorem isum_nil : isum [] = 0 := rfl +@[simp] theorem isum_cons (x : Int) (xs : List Int) : isum (x :: xs) = x + isum xs := rfl + +theorem isum_append (xs ys : List Int) : isum (xs ++ ys) = isum xs + isum ys := by + induction xs with + | nil => simp + | cons x xs ih => simp only [List.cons_append, isum_cons, ih]; omega + +theorem isum_neg (xs : List Int) : isum (xs.map (fun x => -x)) = -isum xs := by + induction xs with + | nil => rfl + | cons x xs ih => simp only [List.map_cons, isum_cons, ih]; omega + +/-- Applying cash invents and loses nothing: the parts and what is left +sum to the cash. -/ +theorem applyCash_conserves (rem : Int) (ns : List Int) : + isum (applyCash rem ns).1 + (applyCash rem ns).2 = rem := by + induction ns generalizing rem with + | nil => simp [applyCash] + | cons n ns ih => + simp only [applyCash, isum_cons] + have := ih (rem - take rem n) + omega + +theorem applyCash_length (rem : Int) (ns : List Int) : + (applyCash rem ns).1.length = ns.length := by + induction ns generalizing rem with + | nil => rfl + | cons n ns ih => simp [applyCash, ih] + +theorem take_zero (n : Int) : take 0 n = 0 := by + simp [take] + +/-- With no cash, nothing is applied and nothing is left. -/ +theorem applyCash_zero (ns : List Int) : (applyCash 0 ns).2 = 0 := by + induction ns with + | nil => rfl + | cons n ns ih => simp [applyCash, take_zero, ih] + +/-- Cash in is used up when the movements against it cover it. -/ +theorem applyCash_exhausts_pos (rem : Int) (ns : List Int) (h0 : 0 ≤ rem) + (h : rem + isum ns ≤ 0) : (applyCash rem ns).2 = 0 := by + induction ns generalizing rem with + | nil => simp [applyCash] at h ⊢; omega + | cons n ns ih => + simp only [applyCash] + simp only [isum_cons] at h + by_cases hr : rem = 0 + · subst hr; simp [take_zero, applyCash_zero] + · by_cases hn : n < 0 + · by_cases hle : -n ≤ rem + · have ht : take rem n = -n := by + simp only [take]; rw [ite_eq_left (by omega)]; omega + rw [ht]; exact ih _ (by omega) (by omega) + · have ht : take rem n = rem := by + simp only [take]; rw [ite_eq_left (by omega)]; omega + rw [ht, Int.sub_self]; exact applyCash_zero ns + · have ht : take rem n = 0 := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)] + rw [ht, Int.sub_zero]; exact ih _ h0 (by omega) + +/-- Cash out is used up when the movements against it cover it. -/ +theorem applyCash_exhausts_neg (rem : Int) (ns : List Int) (h0 : rem ≤ 0) + (h : 0 ≤ rem + isum ns) : (applyCash rem ns).2 = 0 := by + induction ns generalizing rem with + | nil => simp [applyCash] at h ⊢; omega + | cons n ns ih => + simp only [applyCash] + simp only [isum_cons] at h + by_cases hr : rem = 0 + · subst hr; simp [take_zero, applyCash_zero] + · by_cases hn : 0 < n + · by_cases hle : rem ≤ -n + · have ht : take rem n = -n := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega + rw [ht]; exact ih _ (by omega) (by omega) + · have ht : take rem n = rem := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega + rw [ht, Int.sub_self]; exact applyCash_zero ns + · have ht : take rem n = 0 := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)] + rw [ht, Int.sub_zero]; exact ih _ h0 (by omega) + +/-- **Balanced, the cash is used up**: when the cash and the movements sum +to zero, nothing is left over. -/ +theorem applyCash_exhausts (rem : Int) (ns : List Int) (h : rem + isum ns = 0) : + (applyCash rem ns).2 = 0 := by + rcases Int.le_total 0 rem with h0 | h0 + · exact applyCash_exhausts_pos rem ns h0 (by omega) + · exact applyCash_exhausts_neg rem ns h0 (by omega) + +theorem take_neg (r n : Int) : take (-r) (-n) = -take r n := by + simp only [take] + by_cases h1 : 0 < r ∧ n < 0 + · rw [ite_eq_right (by omega), ite_eq_left (by omega), ite_eq_left h1]; omega + · by_cases h2 : r < 0 ∧ 0 < n + · rw [ite_eq_left (by omega), ite_eq_right h1, ite_eq_left h2]; omega + · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right h1, ite_eq_right h2]; omega + +/-- Applying minus the cash to minus the movements gives minus the parts: +what lets a reversal mirror its original. -/ +theorem applyCash_neg (rem : Int) (ns : List Int) : + applyCash (-rem) (ns.map (fun x => -x)) + = ((applyCash rem ns).1.map (fun x => -x), -(applyCash rem ns).2) := by + induction ns generalizing rem with + | nil => rfl + | cons n ns ih => + simp only [List.map_cons, applyCash, take_neg] + have : -rem - -take rem n = -(rem - take rem n) := by omega + rw [this, ih] + +/-- An entry's cash: the net of the lines tagged cash. -/ +def cashOf (F : List Line → Line → Flow) (e : List Line) : Int := secNet (F e) .cash e + +/-- An entry's section movements, `[operating, investing, financing]`. -/ +def moves (F : List Line → Line → Flow) (e : List Line) : List Int := + [secNet (F e) .operating e, secNet (F e) .investing e, secNet (F e) .financing e] + +/-- An entry's cash flows per section (`kernel::entry_flows`). -/ +def flows (F : List Line → Line → Flow) (e : List Line) : List Int := + (applyCash (cashOf F e) (moves F e)).1 + +/-- **An entry's cash flows sum to its cash** (`entry_flows_sum`): for a +balanced entry, the sections' cash is exactly the cash that moved. -/ +theorem entry_flows_sum (F : List Line → Line → Flow) (e : List Line) (h : net e = 0) : + isum (flows F e) = cashOf F e := by + have hb := net_splits_by_flow (F e) e + have hx : (applyCash (cashOf F e) (moves F e)).2 = 0 := by + apply applyCash_exhausts + simp only [moves, cashOf, isum_cons, isum_nil] + omega + have := applyCash_conserves (cashOf F e) (moves F e) + simp only [flows] + omega + +theorem flows_length (F : List Line → Line → Flow) (e : List Line) : (flows F e).length = 3 := by + simp [flows, applyCash_length, moves] + +theorem secNet_reversal (f g : Line → Flow) (k : Flow) (ls : List Line) + (h : ∀ l ∈ ls, g l.reverse = f l) : secNet g k (reversal ls) = -secNet f k ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + simp only [secNet_cons, h l (by simp), Line.reverse_signed, + ih (fun m hm => h m (by simp [hm]))] + split <;> omega + +/-- **A reversal's flows are its original's, negated** (`flows_reversal`), +when its lines take its original's tags: what lets an entry and its +reversal drop out of the statement together (rules.md B-14 rule 6). -/ +theorem flows_reversal (F : List Line → Line → Flow) (e : List Line) + (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l) : + flows F (reversal e) = (flows F e).map (fun x => -x) := by + simp only [flows, cashOf, moves] + rw [secNet_reversal (F e) (F (reversal e)) .cash e hF, + secNet_reversal (F e) (F (reversal e)) .operating e hF, + secNet_reversal (F e) (F (reversal e)) .investing e hF, + secNet_reversal (F e) (F (reversal e)) .financing e hF] + have := applyCash_neg (secNet (F e) .cash e) + [secNet (F e) .operating e, secNet (F e) .investing e, secNet (F e) .financing e] + simp only [List.map_cons, List.map_nil] at this + rw [this] + +theorem isum_three (xs : List Int) (h : xs.length = 3) : + isum xs = xs.getD 0 0 + xs.getD 1 0 + xs.getD 2 0 := by + match xs, h with + | [a, b, c], _ => simp; omega + +/-! ### What a member or lender pays or receives for the company (rule 11) + +`kernel::constructive` (D-42): what is left unsettled of an entry's +kinds that can pay or receive for the company (`s`, a financing liability +or a member's capital) settles what is left of the kinds they pay or +receive for (`u`), as if through the cash accounts. The engine sums the +parts by section into an entry's constructive triple; the entry theorems +below take any triple that nets to zero (and, for reversals, mirrors), +which `constructive_nets` and `constructive_neg` give the kernel's. -/ + +/-- The credits among some movements, `Σ max(-m, 0)`: what cash in can +settle. -/ +def creditTotal : List Int → Int + | [] => 0 + | m :: ms => max (-m) 0 + creditTotal ms + +/-- The debits among some movements, `Σ max(m, 0)`: what cash out can +settle. -/ +def debitTotal : List Int → Int + | [] => 0 + | m :: ms => max m 0 + debitTotal ms + +theorem creditTotal_nonneg (ms : List Int) : 0 ≤ creditTotal ms := by + induction ms with + | nil => simp [creditTotal] + | cons m ms ih => simp only [creditTotal]; omega + +theorem debitTotal_nonneg (ms : List Int) : 0 ≤ debitTotal ms := by + induction ms with + | nil => simp [debitTotal] + | cons m ms ih => simp only [debitTotal]; omega + +theorem creditTotal_neg (ms : List Int) : + creditTotal (ms.map (fun x => -x)) = debitTotal ms := by + induction ms with + | nil => rfl + | cons m ms ih => simp only [List.map_cons, creditTotal, debitTotal, ih]; omega + +theorem debitTotal_neg (ms : List Int) : + debitTotal (ms.map (fun x => -x)) = creditTotal ms := by + induction ms with + | nil => rfl + | cons m ms ih => + simp only [List.map_cons, creditTotal, debitTotal, ih] + +/-- Cash in is used up when the credits cover it (whatever the debits). -/ +theorem applyCash_exhausts_in (rem : Int) (ns : List Int) (h0 : 0 ≤ rem) + (h : rem ≤ creditTotal ns) : (applyCash rem ns).2 = 0 := by + induction ns generalizing rem with + | nil => simp [applyCash, creditTotal] at h ⊢; omega + | cons n ns ih => + simp only [applyCash] + simp only [creditTotal] at h + by_cases hr : rem = 0 + · subst hr; simp [take_zero, applyCash_zero] + · by_cases hn : n < 0 + · by_cases hle : -n ≤ rem + · have ht : take rem n = -n := by + simp only [take]; rw [ite_eq_left (by omega)]; omega + rw [ht]; exact ih _ (by omega) (by omega) + · have ht : take rem n = rem := by + simp only [take]; rw [ite_eq_left (by omega)]; omega + rw [ht, Int.sub_self]; exact applyCash_zero ns + · have ht : take rem n = 0 := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)] + rw [ht, Int.sub_zero]; exact ih _ h0 (by omega) + +/-- Cash out is used up when the debits cover it (whatever the credits). -/ +theorem applyCash_exhausts_out (rem : Int) (ns : List Int) (h0 : rem ≤ 0) + (h : -rem ≤ debitTotal ns) : (applyCash rem ns).2 = 0 := by + induction ns generalizing rem with + | nil => simp [applyCash, debitTotal] at h ⊢; omega + | cons n ns ih => + simp only [applyCash] + simp only [debitTotal] at h + by_cases hr : rem = 0 + · subst hr; simp [take_zero, applyCash_zero] + · by_cases hn : 0 < n + · by_cases hle : rem ≤ -n + · have ht : take rem n = -n := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega + rw [ht]; exact ih _ (by omega) (by omega) + · have ht : take rem n = rem := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega + rw [ht, Int.sub_self]; exact applyCash_zero ns + · have ht : take rem n = 0 := by + simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)] + rw [ht, Int.sub_zero]; exact ih _ h0 (by omega) + +/-- Which way the money went (`kernel::OnBehalf`). -/ +inductive OnBehalf where + | paid + | received + deriving DecidableEq, Repr + +/-- The other way: what a reversal does. -/ +def OnBehalf.mirror : OnBehalf → OnBehalf + | .paid => .received + | .received => .paid + +/-- The cash the sources take, + in (`kernel::constructive`): paid, the +smaller of the sources' credits and the uses' debits; received, minus the +smaller of the sources' debits and the uses' credits. -/ +def onBehalfCash : OnBehalf → List Int → List Int → Int + | .paid, s, u => min (creditTotal s) (debitTotal u) + | .received, s, u => -min (debitTotal s) (creditTotal u) + +/-- `kernel::constructive`: the sources' parts and the uses' parts. -/ +def constructive (w : OnBehalf) (s u : List Int) : List Int × List Int := + ((applyCash (onBehalfCash w s u) s).1, (applyCash (-onBehalfCash w s u) u).1) + +/-- **What a member or lender handled for the company nets to zero** +(`constructive_nets`; Kani `constructive_nets_to_zero`): the sources take +exactly what the uses give, so an entry's flows still sum to its cash. -/ +theorem constructive_nets (w : OnBehalf) (s u : List Int) : + isum (constructive w s u).1 + isum (constructive w s u).2 = 0 := by + have hs := applyCash_conserves (onBehalfCash w s u) s + have hu := applyCash_conserves (-onBehalfCash w s u) u + have cs := creditTotal_nonneg s + have ds := debitTotal_nonneg s + have cu := creditTotal_nonneg u + have du := debitTotal_nonneg u + have ⟨xs, xu⟩ : (applyCash (onBehalfCash w s u) s).2 = 0 ∧ + (applyCash (-onBehalfCash w s u) u).2 = 0 := by + cases w with + | paid => + simp only [onBehalfCash] + exact ⟨applyCash_exhausts_in _ _ (by omega) (by omega), + applyCash_exhausts_out _ _ (by omega) (by omega)⟩ + | received => + simp only [onBehalfCash] + exact ⟨applyCash_exhausts_out _ _ (by omega) (by omega), + applyCash_exhausts_in _ _ (by omega) (by omega)⟩ + simp only [constructive] + omega + +theorem onBehalfCash_mirror (w : OnBehalf) (s u : List Int) : + onBehalfCash w.mirror (s.map (fun x => -x)) (u.map (fun x => -x)) + = -onBehalfCash w s u := by + cases w <;> simp only [OnBehalf.mirror, onBehalfCash, creditTotal_neg, debitTotal_neg] <;> omega + +/-- **The other way, minus the sources and uses give minus the parts** +(`constructive_neg`; Kani `constructive_mirrors`): a payment made for the +company and its reversal drop out together. -/ +theorem constructive_neg (w : OnBehalf) (s u : List Int) : + constructive w.mirror (s.map (fun x => -x)) (u.map (fun x => -x)) + = ((constructive w s u).1.map (fun x => -x), (constructive w s u).2.map (fun x => -x)) := by + simp only [constructive, onBehalfCash_mirror] + rw [applyCash_neg (onBehalfCash w s u) s, applyCash_neg (-onBehalfCash w s u) u] + +/-- Three sections' figures, summed. -/ +def sum3 (xs : List Int) : Int := xs.getD 0 0 + xs.getD 1 0 + xs.getD 2 0 + +@[simp] theorem sum3_cons (a b c : Int) : sum3 [a, b, c] = a + b + c := by + simp [sum3] + +/-- **The kernel's parts, by section, net to zero**: split the uses into +operating ones then investing ones (`kernel::constructive` takes them in +that order), and the triple (operating, investing, financing = the +sources) the engine adds to an entry's flows sums to zero. -/ +theorem constructive_sections_net (w : OnBehalf) (s uo ui : List Int) : + sum3 [isum ((constructive w s (uo ++ ui)).2.take uo.length), + isum ((constructive w s (uo ++ ui)).2.drop uo.length), + isum (constructive w s (uo ++ ui)).1] = 0 := by + have h := constructive_nets w s (uo ++ ui) + have hs := isum_append ((constructive w s (uo ++ ui)).2.take uo.length) + ((constructive w s (uo ++ ui)).2.drop uo.length) + rw [List.take_append_drop] at hs + rw [sum3_cons] + omega + +/-- Passes add: two triples that net to zero add to one that does. -/ +theorem sum3_add (xs ys : List Int) (hx : sum3 xs = 0) (hy : sum3 ys = 0) : + sum3 [xs.getD 0 0 + ys.getD 0 0, xs.getD 1 0 + ys.getD 1 0, xs.getD 2 0 + ys.getD 2 0] = 0 := by + rw [sum3_cons] + simp only [sum3] at hx hy + omega + +/-- Two triples, added section by section. -/ +def add3 (xs ys : List Int) : List Int := + [xs.getD 0 0 + ys.getD 0 0, xs.getD 1 0 + ys.getD 1 0, xs.getD 2 0 + ys.getD 2 0] + +/-- An entry's flows on the statement: its cash flows, plus `C e`, what a +member or lender paid or received for it, by section (rule 11). -/ +def stmtFlows (F : List Line → Line → Flow) (C : List Line → List Int) (e : List Line) : + List Int := + add3 (flows F e) (C e) + +/-- **An entry's statement flows sum to its cash** when what was handled +for it nets to zero: rule 11 moves no cash (`stmt_flows_sum`). -/ +theorem stmt_flows_sum (F : List Line → Line → Flow) (C : List Line → List Int) + (e : List Line) (h : net e = 0) (hC : sum3 (C e) = 0) : + sum3 (stmtFlows F C e) = cashOf F e := by + have he := entry_flows_sum F e h + rw [isum_three _ (flows_length F e)] at he + simp only [stmtFlows, add3, sum3_cons] + simp only [sum3] at hC + omega + +theorem getD_neg (xs : List Int) (k : Nat) : + (xs.map (fun x => -x)).getD k 0 = -xs.getD k 0 := by + induction xs generalizing k with + | nil => simp + | cons x xs ih => cases k with + | zero => simp + | succ k => simp only [List.map_cons, List.getD_cons_succ, ih] + +/-- **A reversal's statement flows are its original's, negated**, when its +lines take the original's tags and what was handled for it mirrors +(`constructive_neg`). -/ +theorem stmt_flows_reversal (F : List Line → Line → Flow) (C : List Line → List Int) + (e : List Line) (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l) + (hC : C (reversal e) = (C e).map (fun x => -x)) : + stmtFlows F C (reversal e) = (stmtFlows F C e).map (fun x => -x) := by + simp only [stmtFlows, add3, flows_reversal F e hF, hC, getD_neg, List.map_cons, + List.map_nil, List.cons.injEq, and_true] + refine ⟨?_, ?_, ?_⟩ <;> omega + +/-- A section's total over some entries: the sum of each entry's cash in +it (`k` = 0 operating, 1 investing, 2 financing), what a member or lender +handled for it included. -/ +def sectionTotal (F : List Line → Line → Flow) (C : List Line → List Int) (k : Nat) : + List (List Line) → Int + | [] => 0 + | e :: es => (stmtFlows F C e).getD k 0 + sectionTotal F C k es + +/-- The entries' cash, summed. -/ +def cashTotal (F : List Line → Line → Flow) : List (List Line) → Int + | [] => 0 + | e :: es => cashOf F e + cashTotal F es + +/-- **The sections sum to the change in cash** (plan P3): over any balanced +entries, operating + investing + financing is the entries' cash, exactly, +whatever a member or lender handled for them as long as it nets to zero +within each entry (rule 11, `constructive_nets`). The statement's footing +(rules.md B-14 rule 9) can't fail on posted entries. -/ +theorem cashflow_sections_sum_to_cash_change (F : List Line → Line → Flow) + (C : List Line → List Int) (es : List (List Line)) (h : ∀ e ∈ es, net e = 0) + (hC : ∀ e ∈ es, sum3 (C e) = 0) : + sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es = cashTotal F es := by + induction es with + | nil => rfl + | cons e es ih => + simp only [sectionTotal, cashTotal] + have he := stmt_flows_sum F C e (h e (by simp)) (hC e (by simp)) + simp only [sum3] at he + have := ih (fun x hx => h x (by simp [hx])) (fun x hx => hC x (by simp [hx])) + omega + +/-- When the cash tag follows the account (a line is cash exactly when +its account is a cash account), an entry's cash is the movement of the +cash accounts. -/ +theorem secNet_cash_is_movement (f : Line → Flow) (cash : List Nat) (hd : Distinct cash) + (hf : ∀ l, f l = .cash ↔ l.account ∈ cash) (ls : List Line) : + secNet f .cash ls = sumOver (fun a => movement a ls) cash := by + induction ls with + | nil => simpa using (sumOver_zero cash).symm + | cons l ls ih => + simp only [secNet_cons, movement_cons] + rw [sumOver_add, ← ih] + by_cases hc : l.account ∈ cash + · rw [ite_eq_left ((hf l).2 hc), sumOver_indicator l.account l.signed cash hd hc] + · rw [ite_eq_right (fun e => hc ((hf l).1 e)), sumOver_indicator_absent l.account l.signed cash hc] + +/-! ### Net income reconciled to operating cash (rules.md B-14 rule 8) -/ + +/-- Net movement of the lines on revenue and expense accounts (`pl`) +tagged `k` (`sel = true`), or on balance-sheet accounts (`sel = false`). -/ +def plNet (pl : Nat → Bool) (sel : Bool) (f : Line → Flow) (k : Flow) : List Line → Int + | [] => 0 + | l :: ls => (if pl l.account = sel ∧ f l = k then l.signed else 0) + plNet pl sel f k ls + +/-- Net movement of every revenue and expense line. -/ +def plAll (pl : Nat → Bool) : List Line → Int + | [] => 0 + | l :: ls => (if pl l.account = true then l.signed else 0) + plAll pl ls + +/-- Net income: revenue less expenses, `-(net of the P&L lines)`. -/ +def netIncome (pl : Nat → Bool) (e : List Line) : Int := -plAll pl e + +/-- G: the P&L lines rule 4 puts in investing (gains and losses). -/ +def gainLoss (pl : Nat → Bool) (F : List Line → Line → Flow) (e : List Line) : Int := + plNet pl true (F e) .investing e + +/-- W: minus the movement of the operating balance-sheet lines. -/ +def balanceChange (pl : Nat → Bool) (F : List Line → Line → Flow) (e : List Line) : Int := + -plNet pl false (F e) .operating e + +/-- X: what no cash, real or handled for the company, settled of the +operating movement. -/ +def noncashOp (F : List Line → Line → Flow) (C : List Line → List Int) (e : List Line) : Int := + secNet (F e) .operating e + (stmtFlows F C e).getD 0 0 + +theorem secNet_split (pl : Nat → Bool) (f : Line → Flow) (k : Flow) (ls : List Line) : + secNet f k ls = plNet pl true f k ls + plNet pl false f k ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [secNet_cons, plNet, ih] + cases pl l.account <;> by_cases h : f l = k <;> simp [h] <;> omega + +theorem plAll_split (pl : Nat → Bool) (f : Line → Flow) (ls : List Line) + (h : ∀ l ∈ ls, pl l.account = true → f l = .operating ∨ f l = .investing) : + plAll pl ls = plNet pl true f .operating ls + plNet pl true f .investing ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [plAll, plNet, ih (fun m hm => h m (by simp [hm]))] + cases hp : pl l.account + · simp + · rcases h l (by simp) hp with hk | hk <;> simp [hk] <;> omega + +/-- **Net income reconciles to operating cash**, entry by entry: +operating cash = NI + G + X + W, when revenue and expense lines are only +ever operating or investing (rules.md B-14 rule 8; ASC 230-10-45-28 to +45-30), whatever a member or lender handled for it (rule 11). -/ +theorem operating_reconciliation_ties (pl : Nat → Bool) (F : List Line → Line → Flow) + (C : List Line → List Int) (e : List Line) + (h : ∀ l ∈ e, pl l.account = true → F e l = .operating ∨ F e l = .investing) : + (stmtFlows F C e).getD 0 0 + = netIncome pl e + gainLoss pl F e + noncashOp F C e + balanceChange pl F e := by + have hs := secNet_split pl (F e) .operating e + have hp := plAll_split pl (F e) e h + simp only [netIncome, gainLoss, noncashOp, balanceChange] + omega + +/-- The operating section's total over some entries. -/ +def opTotal (pl : Nat → Bool) (F : List Line → Line → Flow) (C : List Line → List Int) : + List (List Line) → Int + | [] => 0 + | e :: es => netIncome pl e + gainLoss pl F e + noncashOp F C e + balanceChange pl F e + + opTotal pl F C es + +/-- **The reconciliation schedule ties to the operating section** over any +entries: the section's total is NI + G + X + W summed. -/ +theorem operating_reconciliation_ties_all (pl : Nat → Bool) (F : List Line → Line → Flow) + (C : List Line → List Int) (es : List (List Line)) + (h : ∀ e ∈ es, ∀ l ∈ e, pl l.account = true → F e l = .operating ∨ F e l = .investing) : + sectionTotal F C 0 es = opTotal pl F C es := by + induction es with + | nil => rfl + | cons e es ih => + simp only [sectionTotal, opTotal] + rw [operating_reconciliation_ties pl F C e (h e (by simp)), + ih (fun x hx => h x (by simp [hx]))] + +end Bookspec diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json new file mode 100644 index 0000000..16bbf3f --- /dev/null +++ b/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "bookspec", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/lakefile.toml b/lean/lakefile.toml new file mode 100644 index 0000000..a16dbc4 --- /dev/null +++ b/lean/lakefile.toml @@ -0,0 +1,5 @@ +name = "bookspec" +defaultTargets = ["Bookspec"] + +[[lean_lib]] +name = "Bookspec" diff --git a/lean/lean-toolchain b/lean/lean-toolchain new file mode 100644 index 0000000..ba8ebf2 --- /dev/null +++ b/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1