控訴期間の末日や所得税の額は、条文を読めば計算の手順が決まります。 それでも、年末年始に当たる末日の繰り下げや、税率の区分の境目のように、手で計算すると間違えやすい所があります。 プログラムに書いた場合も、その計算が条文どおりかを確かめるには手間がかかります。

lean-ritsuryo は、日本の法令が定める期間と税額の計算を Lean 4 で書いたライブラリと CLI です。 ライブラリの関数には、条文どおりに計算することの証明を付けています。 CLI もこの関数を呼んで計算します。

扱う計算は民法の期間計算、祝日の判定、控訴期間などの期限、所得税、相続税、消費税、延滞税、利子税、加算税の税額と、国税の端数処理です。 以下の出力はどれも v0.5.0 の ritsuryo で実行した結果です。

使ってみる

CLI の引数は AWS CLI と同じ文法で書きます。 どのコマンドも計算の結果 (Result)、途中の値 (Steps)、根拠の条文 (Basis)、計算の前提にした条文の読み方 (Assumptions) を JSON で出力します。

控訴期間

2026-12-15 に判決の送達を受けたときの控訴期間です。 2 週間の末日は 2026-12-29 ですが、この日は年末年始に当たるので、民事訴訟法 第95条第3項により末日は 2027-01-04 に繰り下がります。

$ ritsuryo deadline compute-appeal-deadline --served-date 2026-12-15 \
    --query '{Result: Result, RolledOver: Steps.RolledOverDays[].Date}'
{
    "Result": {
        "Deadline": "2027-01-04",
        "Period": "控訴期間",
        "Invariable": true
    },
    "RolledOver": [
        "2026-12-29",
        "2026-12-30",
        "2026-12-31",
        "2027-01-01",
        "2027-01-02",
        "2027-01-03"
    ]
}

RolledOver には、繰り下げのときに飛ばした日が並びます。 祝日の判定には内閣府の祝日 CSV を使い、その取得元と SHA-256 を出力の Data に書きます。

所得税

2026 年分で課税総所得金額が 7,000,000 円のとき、所得税は 974,000 円になります。 これは国税庁の速算表で求めた額 (7,000,000 × 23% − 636,000) と同じです。

$ ritsuryo income-tax compute-tax --tax-year 2026 --taxable-income 7000000 --query Result
{
    "IncomeTax": 974000,
    "ReconstructionTax": 20454,
    "DefenseTax": 0,
    "Total": 994454,
    "Payable": 994400
}

2027 年分からは、復興特別所得税が 1.1%、防衛特別所得税が 1% になります。 --tax-year 2027 を渡すと、 ReconstructionTax が 10714、 DefenseTax が 9740 になります。

条文を写して書く

lean-ritsuryo では、まず計算を条文の構造どおりの定義として書いています。 以下ではこの定義を仕様と呼びます。 Lean の定義は実行できるので、仕様をそのまま計算に使えることがあります。 仕様を実行に使えるかどうかで、書き方は次の 3 通りに分かれました。

仕様をそのまま実行するとき

民事訴訟法 第95条第3項は、期間の末日が日曜日、土曜日、祝日法の休日、1 月 2 日、1 月 3 日、12 月 29 日から 31 日までの日に当たるとき、期間はその翌日に満了すると定めます。 これらの日を判定する仕様は、条文の列挙をそのまま並べた関数です。

def isHolidaySpec (national : Date → Bool) (d : Date) : Bool :=
  HolidayClass.holds national d .sunday || HolidayClass.holds national d .saturday ||
    HolidayClass.holds national d .nationalHoliday || HolidayClass.holds national d .newYear ||
    HolidayClass.holds national d .yearEnd

この関数は十分に速いので、繰り下げの計算はこの仕様をそのまま呼んでいます。 この場合は、ほかに定義を書く必要がありません。

仕様の実行が遅く、速い実装を書くとき

仕様の計算が遅いときは、速く計算できる実装を別に書き、実装が仕様と一致することを証明します。 扱いは、一致がすべての入力で成り立つか、条件付きで成り立つかで分かれます。

実装がすべての入力で仕様と一致するとき

所得税法 第89条は、課税総所得金額を表の区分に分けてそれぞれに税率を掛け、合計した額を税額とします。 この条文を写した仕様が incomeTaxCentsSpec で、税率表の区分を 1 つずつたどって税額を積み上げます。 金額は百分の一円を 1 とする整数で表しています。

def table : List Bracket := [
  ⟨some 1950000, 5⟩, ⟨some 3300000, 10⟩, ⟨some 6950000, 20⟩, ⟨some 9000000, 23⟩,
  ⟨some 18000000, 33⟩, ⟨some 40000000, 40⟩, ⟨none, 45⟩]

def incomeTaxCentsSpec (x : Nat) : Nat :=
  progressiveCents table 0 x

国税庁の速算表 (税率 × 金額 − 控除額) を使えば、区分をたどらずに 1 本の式で同じ税額を出せます。

def quickCents (x : Nat) : Nat :=
  if x ≤ 1950000 then 5 * x
  else if x ≤ 3300000 then 10 * x - 9750000
  else if x ≤ 6950000 then 20 * x - 42750000
  else if x ≤ 9000000 then 23 * x - 63600000
  else if x ≤ 18000000 then 33 * x - 153600000
  else if x ≤ 40000000 then 40 * x - 279600000
  else 45 * x - 479600000

仕様と速算表の式がどの金額でも等しいことを証明し、その定理に @[csimp] を付けます。

@[csimp]
theorem incomeTaxCentsSpec_eq_quickCents : @incomeTaxCentsSpec = @quickCents := by
  funext x
  simp only [incomeTaxCentsSpec, table, progressiveCents, quickCents]
  repeat' split
  all_goals omega

@[csimp] の付いた等式があると、Lean のコンパイラは、左辺の関数を呼ぶ箇所を右辺の関数を呼ぶように書き換えます。 そのため、ライブラリの税額の関数はソースでは仕様の incomeTaxCentsSpec を呼んでいても、実行されるのは速算表の式です。 書き換えられたことは、コンパイラが出力する中間表現 (IR) で確かめられます。 次は incomeTaxCentsSpec x を返すだけの関数 probeIncome の IR です。

def probeIncome (x_1 : @& tobj) : tobj :=
  let x_2 : tobj := Ritsuryo.Tax.Income.quickCents x_1;

コンパイラは仕様を呼ぶ関数をコンパイルするときに書き換えるので、 @[csimp] の定理はその関数より前に書いておきます。 相続税の税率表も同じ形にしています。

実装が条件付きで仕様と一致するとき

民法 第143条は、週、月、年で定めた期間を暦に従って計算し、応当日の前日に満了すると定めます。 この条文を写した仕様は応当日を次のように求めます。

def correspondingDaySpec (start : Date) : Length → Option Date
  | .days n => some (start.addDaysNaive n)
  | .weeks n => some (weekCorrespondingSpec start n)
  | len =>
    let ym := lastMonthSpec start len
    if start.day ≤ ym.daysInMonth then some ⟨ym.year, ym.month, start.day⟩ else none

日の期間は addDaysNaive で翌日を n 回たどり、週の期間は weekCorrespondingSpec で翌日をたどりながら同じ曜日の日を探します。 月と年の期間も、 lastMonthSpec が 1 か月ずつ進めて最後の月を求めます。 どれも、計算の回数が期間の日数か月数に比例して増えます。

実装は日付を通算日 (ある基準日からの日数) に直して計算します。

def correspondingDays (start : Date) : Length → Option Int
  | .days n => some (start.toDays + n)
  | .weeks n => some (start.toDays + 7 * n)
  | len =>
    let ym := lastMonth start len
    if start.day ≤ ym.daysInMonth then some (toDays ⟨ym.year, ym.month, start.day⟩) else none

日と週の期間は通算日に n か 7 * n を足すだけです。 月と年の期間も、 lastMonth が月の通し番号に n を足して最後の月を求めます。

ライブラリの期間の計算 compute はこの実装を使い、その結果が仕様と一致することを定理 PER-1 で証明しています。

theorem per1_compute_eq_spec (event : Date) (h : event.Valid) (startAtMidnight : Bool)
    (len : Length) :
    (compute event startAtMidnight len).start = Civil.startDateSpec event startAtMidnight ∧
      (compute event startAtMidnight len).corresponding =
        Civil.correspondingDaySpec (Civil.startDateSpec event startAtMidnight) len ∧
      (compute event startAtMidnight len).expiry = Civil.expirySpec event startAtMidnight len

仮定の h : event.Valid は、出来事の日 event が実在する日付であることを表します。 PER-1 が一致を保証するのはこの仮定が成り立つときだけで、 @[csimp] はこのような仮定の付いた等式には使えません。 そのため、ライブラリの関数からは実装を直接呼んでいます。 @[csimp] を使うには、実在する日付だけを表す型を作り、関数の引数をその型にする必要があります。

仕様が手順ではなく結果の条件を定めるとき

民法 第142条などの繰り下げの規定は、末日が休日なら「その翌日」に満了すると書いています。 翌日も休日のときについては書いていないので、lean-ritsuryo は休日でない最初の日まで繰り下げると読んでいます。 この読み方が定めているのは、計算の手順ではなく、結果が満たすべき条件です。 仕様が実行できる関数ではないので、繰り下げの実装を 1 つ書きました。 実装は通算日を 1 日ずつ進め、休日でない日が見つかったところで止まります。

def rolloverDays (isHoliday : Int → Bool) : Nat → Int → Option Int
  | 0, _ => none
  | fuel + 1, z => if isHoliday z then rolloverDays isHoliday fuel (z + 1) else some z

fuel は調べる日数の上限で、上限までに休日でない日がなければ none を返します。 定理 ROL-1 は、この実装の結果が次の 2 つの条件を満たすことを証明しています。

• 繰り下げた日は、もとの日以後で休日でない
• もとの日から繰り下げた日の前日までは、すべて休日である

lean-ritsuryo の定理の多くはこの形で、1 つの関数が満たす性質を述べています。 たとえば次のような性質です。

• 期間の末日は起算点についても長さについても単調である
• 所得税は課税所得が増えると減らず、課税所得から所得税を引いた額も減らない
• 消費税の端数処理を品目ごとにしたときと合計でしたときの差は、品目の数から 1 を引いた円以下である
• 民法 第900条の法定相続分の合計は 1 になる

定理には TAX-1 のような ID を付けていて、ID は全部で 35 個あります。 祝日は内閣府の CSV に載っているすべての年について、祝日法 第2条と第3条から導いた日が CSV と一致することを Lean のカーネルで確かめています。 春分の日と秋分の日だけは、CSV から日付を取っています。 定理はすべて lake build のときに Lean が検査し、どの証明も sorry 、 admit 、 native_decide を使っていません。

Lean で防げる誤り

テストは、選んだ入力について結果を確かめます。 定理はすべての入力について述べていて、Lean は lake build のたびにその証明を検査します。 そのため、次のような誤りは選んだ入力に現れなくてもビルドの時点でエラーになります。

税率表の写し間違い

速算表の控除額を 1 つ写し間違え、695 万円超 900 万円以下の区分の 636,000 円を 636,500 円にしてみました。

else if x ≤ 9000000 then 23 * x - 63650000

すると、仕様と速算表の式が等しいという証明が通らず、Lean がエラーを出します。

$ lake env lean typo.lean
typo.lean:16:12: error: omega could not prove the goal:

証明は金額を税率表の 7 つの区分で場合分けし、区分ごとに 2 つの式が等しいことを omega (整数の 1 次式の等式と不等式を判定する Lean の手続き) で示します。 証明できずに残ったのは、695 万円超 900 万円以下の区分だけでした。 この区分では条文どおりの積み上げが 23 * x - 63600000 になり、書き間違えた 23 * x - 63650000 とはどの金額でも 500 円ずれるので、等式が成り立ちません。

700 万円を例に使うテストでもこの誤りは見つかりますが、4,000 万円を超える区分の誤りは、その金額を例に入れないテストでは見つかりません。 証明は、7 つの区分のどれに誤りがあっても、その区分でエラーになります。

一方、区分の境目の x ≤ 6950000 を x < 6950000 に変えても、証明は通りました。 ちょうど 6,950,000 円のときは、20% の区分の式でも 23% の区分の式でも税額が 962,500 円になり、どの金額でも税額が変わらないからです。

繰り下げを 1 日で止める誤り

「その翌日」を文字どおり 1 日だけ繰り下げる関数にすると、翌日も休日のとき、その休日が期間の末日になってしまいます。 次のコードでは、2026-12-29 を 1 日だけ繰り下げた 2026-12-30 も民事訴訟法 第95条第3項の休日に当たることを、Lean のカーネルで確かめています。

def court : Date → Bool := RolloverRule.civilProcedure95.isHoliday Holiday.isHoliday

def rolloverOnce (H : Date → Bool) (d : Date) : Date :=
  if H d then Date.ofDays (d.toDays + 1) else d

example : court (rolloverOnce court ⟨2026, 12, 29⟩) = true := by decide +kernel

この関数は ROL-1 の 1 つ目の条件を満たさないので、ROL-1 は証明できません。 休日なら必ず 2 日進めるような繰り下げすぎる関数も、2 つ目の条件を満たさないので証明できません。

月末をまたぐ期間

2025-01-31 から始まる期間では、1 か月は 2025-02-28 に満了し、続く 1 か月は 2025-03-31 に満了します。 一方、2 か月の期間は 2025-03-30 に満了します。 1 か月の計算を 2 回くり返して 2 か月の期間を求める実装は、この例で 1 日ずれるので、PER-1 を証明できません。

防げない誤り

Lean が確かめるのは、実装が仕様と一致することと、実装が定理に書いた性質を満たすことです。 仕様そのものが条文を読み違えていれば、実装も読み違えたとおりに計算し、証明も通ります。

この誤りを減らすため、仕様は条文の構造どおりに書き、条文と並べて読み比べられるようにしています。 条文の読み方は docs/interpretation.md に書き、国税庁のタックスアンサーに載っている計算例とも照らしています。

実行時間とバイナリの大きさ

リリースの ritsuryo は 3.4 MB の実行ファイル 1 つで (x86_64-linux)、ほかに必要なのは C ライブラリだけです。 1 回の実行は約 6 ms で終わります。

Lean で書いたプログラムは、ライブラリの書き方によってはバイナリが 140 MB になります。 lean-ritsuryo は関数に根拠の条文を記録するために独自の属性を使っています。 この属性を定義するモジュールは Lean を import していて、通常の import で読み込むと Lean 全体がリンクされます。 lean-ritsuryo はこのモジュールを meta import で読み込み、属性をコンパイルのときだけ使うようにしています。

入手

GitHub のリリース に、x86_64-linux、aarch64-linux、aarch64-darwin のアーカイブがあります。

curl -sSfL https://github.com/conao3/lean-ritsuryo/releases/download/v0.5.0/ritsuryo-x86_64-linux.tar.gz | tar -xz
./ritsuryo --version
# ritsuryo 0.5.0

Nix を使う場合は nix run github:conao3/lean-ritsuryo -- help で実行できます。

ライセンスは Apache-2.0 で、リポジトリは https://github.com/conao3/lean-ritsuryo です。 条文の読み方の違いや計算の誤りに気づいたら、Issue で教えてください。