Skip to content

Commit 63690d5

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: div/mod completeness of the block partition — closes the Layer-2 residual (#42)
## Summary Layer 3 (second, deeper invariant): proves **`sumNat (blockCounts n k) = n` for all n and all k>0** — every item is covered exactly once. This discharges the exact `div`/`mod` arithmetic residual the Layer-2 `Partition` tiling proof explicitly left open, via the Euclidean division theorem plus a self-contained count of remainder slots. New module `Chapeliser.ABI.Invariants` (imports the Layer-2 `Partition` model; uses `divNatNZ`/`modNatNZ` because Prelude `div`/`mod` don't reduce at the type level). Sound+complete `Dec`, corollaries tying back to `PartitionComplete`, positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings (6 modules). Adversarial: false variants (`=9`, `=11`) rejected. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 338c268 commit 63690d5

2 files changed

Lines changed: 297 additions & 0 deletions

File tree

‎src/interface/abi/Chapeliser/ABI/Invariants.idr‎

Lines changed: 294 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,294 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Layer-3 invariant for Chapeliser's block partition: DIV/MOD COMPLETENESS.
5+
|||
6+
||| `Partition.idr` (Layer 2) proves the partition is a gapless, non-overlapping
7+
||| *tiling* for all `n`, `k`, and reduces full completeness to one residual
8+
||| arithmetic identity it explicitly leaves open:
9+
|||
10+
||| sumNat (perItemCounts n k) = n -- "the only div/mod obligation"
11+
|||
12+
||| This module discharges exactly that residual — the deeper, genuinely
13+
||| different theorem. Where the Layer-2 proof was *structural* (contiguity needs
14+
||| no reasoning about how `div`/`mod` evaluate), THIS proof is *arithmetic*: it
15+
||| pins down the values produced by integer division of `n` by `k` and shows
16+
||| the per-locale counts sum to exactly `n` — every one of the `n` items is
17+
||| covered exactly once. It rests on the Euclidean division theorem
18+
||| `n = (n mod k) + (n div k) * k` (contrib `Data.Nat.Division`) plus a
19+
||| self-contained count of how many locale indices receive the +1 remainder
20+
||| slot.
21+
|||
22+
||| Division note (Idris2 0.7.0): the Prelude `div`/`mod` on `Nat` go through the
23+
||| `Integral` interface to `divNat`/`modNat`, which are `export partial` and so
24+
||| do NOT reduce at the type level (idiom: "Nat div/mod do not reduce for
25+
||| symbolic operands"). The reducing, `public export` primitives are
26+
||| `divNatNZ`/`modNatNZ`, and `contrib`'s `DivisionTheorem` is stated over those.
27+
||| We therefore phrase the block counts with `divNatNZ`/`modNatNZ` — the SAME
28+
||| values the block partition uses (Prelude `div`/`mod` on a positive `Nat`
29+
||| literally call them), just written in the form that both reduces and matches
30+
||| the division theorem. `blockCounts n (S k')` is thus `perItemCounts n (S k')`
31+
||| with the division spelled in its reducing primitive.
32+
|||
33+
||| Combined with Layer 2 this yields, for ALL n and k>0, a partition that is
34+
||| complete (`sliceSum = n`) AND a perfect tiling — a fully proven even
35+
||| distribution with no items lost or duplicated.
36+
37+
module Chapeliser.ABI.Invariants
38+
39+
import Chapeliser.ABI.Types
40+
import Chapeliser.ABI.Partition
41+
import Data.Vect
42+
import Data.Nat
43+
import Data.Nat.Division
44+
import Decidable.Equality
45+
46+
%default total
47+
48+
--------------------------------------------------------------------------------
49+
-- The block partition's per-locale counts, in reducing (NZ) form
50+
--------------------------------------------------------------------------------
51+
52+
||| The block partition's per-locale counts for `n` items over `S k'` locales,
53+
||| using the `public export` division primitives so the type checker can reduce
54+
||| through them. This is exactly `perItemCounts n (S k')` from `Partition.idr`
55+
||| (which calls Prelude `div`/`mod` = `divNatNZ`/`modNatNZ` on the positive
56+
||| divisor `S k'`), reusing Partition's own `countsFrom`.
57+
public export
58+
blockCounts : (n, k' : Nat) -> Vect (S k') Nat
59+
blockCounts n k' =
60+
countsFrom 0 (divNatNZ n (S k') SIsNonZero) (modNatNZ n (S k') SIsNonZero) (S k')
61+
62+
--------------------------------------------------------------------------------
63+
-- Tiny boolean comparison facts (the `<` inside countsFrom)
64+
--------------------------------------------------------------------------------
65+
66+
||| Nothing is below zero.
67+
ltZeroFalse : (idx : Nat) -> (idx < 0) = False
68+
ltZeroFalse Z = Refl
69+
ltZeroFalse (S _) = Refl
70+
71+
||| `S a < S b` decides identically to `a < b` (the comparison steps S/S down).
72+
ltSuccSucc : (a, b : Nat) -> (S a < S b) = (a < b)
73+
ltSuccSucc _ _ = Refl
74+
75+
--------------------------------------------------------------------------------
76+
-- Counting the remainder ("+1") slots
77+
--------------------------------------------------------------------------------
78+
79+
||| `numBelow idx rem cnt` counts how many of the `cnt` consecutive locale
80+
||| indices `idx, idx+1, ..., idx+cnt-1` are strictly below `rem` — i.e. how many
81+
||| of those locales receive the extra remainder item. It mirrors EXACTLY the
82+
||| `if localeIdx < remainder then 1 else 0` decision inside `countsFrom`, using
83+
||| the same Prelude boolean `<`, so the sum lemma below reduces structurally.
84+
public export
85+
numBelow : (idx, rem, cnt : Nat) -> Nat
86+
numBelow _ _ Z = Z
87+
numBelow idx rem (S c) = (if idx < rem then 1 else 0) + numBelow (S idx) rem c
88+
89+
||| (a + b) + (c + d) = (a + c) + (b + d) — the only shuffle the sum law needs.
90+
rearrange : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
91+
rearrange a b c d =
92+
rewrite plusAssociative (a + b) c d in
93+
rewrite sym (plusAssociative a b c) in
94+
rewrite plusCommutative b c in
95+
rewrite plusAssociative a c b in
96+
rewrite sym (plusAssociative (a + c) b d) in
97+
Refl
98+
99+
||| Structural sum law: a `countsFrom` block contributes `base` per locale plus
100+
||| one extra for each locale index below `rem`. No div/mod facts used here — it
101+
||| is pure bookkeeping over the `if` in `countsFrom`.
102+
sumCountsFrom : (idx, base, rem, cnt : Nat) ->
103+
sumNat (countsFrom idx base rem cnt) = base * cnt + numBelow idx rem cnt
104+
sumCountsFrom idx base rem Z =
105+
rewrite multZeroRightZero base in Refl
106+
sumCountsFrom idx base rem (S c) =
107+
rewrite sumCountsFrom (S idx) base rem c in
108+
rewrite multRightSuccPlus base c in
109+
rearrange base (if idx < rem then 1 else 0) (base * c) (numBelow (S idx) rem c)
110+
111+
--------------------------------------------------------------------------------
112+
-- Evaluating the remainder count exactly
113+
--------------------------------------------------------------------------------
114+
115+
||| If the threshold is zero, no index is below it: the window contributes no
116+
||| extra items regardless of where it starts or how long it is.
117+
numBelowRemZero : (idx, cnt : Nat) -> numBelow idx 0 cnt = 0
118+
numBelowRemZero idx Z = Refl
119+
numBelowRemZero idx (S c) =
120+
rewrite ltZeroFalse idx in
121+
numBelowRemZero (S idx) c
122+
123+
||| Shifting both the index and the threshold up by one leaves the count
124+
||| unchanged: `S idx < S rem` holds exactly when `idx < rem`.
125+
numBelowShift : (idx, rem, cnt : Nat) ->
126+
numBelow (S idx) (S rem) cnt = numBelow idx rem cnt
127+
numBelowShift idx rem Z = Refl
128+
numBelowShift idx rem (S c) =
129+
-- head: (if S idx < S rem ..) = (if idx < rem ..) by ltSuccSucc;
130+
-- tail: numBelow (S (S idx)) (S rem) c = numBelow (S idx) rem c by IH.
131+
-- Combine the two equalities additively with cong2 (+).
132+
cong2 (+)
133+
(cong (\b => if b then (the Nat 1) else 0) (ltSuccSucc idx rem))
134+
(numBelowShift (S idx) rem c)
135+
136+
||| EXACT remainder count over the full locale range `[0, cnt)`: when the
137+
||| remainder `rem` does not exceed the number of locales `cnt`, exactly `rem`
138+
||| locales (indices 0 .. rem-1) receive the extra item. This is the heart of
139+
||| the arithmetic argument and is where `rem <= cnt` (i.e. `n mod k < k`) is
140+
||| consumed.
141+
numBelowFull : (rem, cnt : Nat) -> LTE rem cnt -> numBelow 0 rem cnt = rem
142+
numBelowFull Z cnt _ = numBelowRemZero 0 cnt
143+
numBelowFull (S r) (S c) (LTESucc le) =
144+
-- idx 0 < S r is True (0 < S r reduces to True), so head = 1; the tail is
145+
-- numBelow 1 (S r) c = numBelow 0 r c (numBelowShift), then IH gives r.
146+
rewrite numBelowShift 0 r c in
147+
cong S (numBelowFull r c le)
148+
149+
--------------------------------------------------------------------------------
150+
-- The remainder is below the locale count (n mod k < k)
151+
--------------------------------------------------------------------------------
152+
153+
||| `n mod (S k')` (in reducing NZ form) is strictly less than `S k'`, hence
154+
||| `<= S k'`. Strict bound from contrib's `boundModNatNZ`, then weakened.
155+
modLEk : (n, k' : Nat) -> LTE (modNatNZ n (S k') SIsNonZero) (S k')
156+
modLEk n k' = lteSuccLeft (boundModNatNZ n (S k') SIsNonZero)
157+
158+
--------------------------------------------------------------------------------
159+
-- MAIN LAYER-3 THEOREM
160+
--------------------------------------------------------------------------------
161+
162+
||| DIV/MOD COMPLETENESS, the residual left open by `Partition.idr`:
163+
||| for every item count `n` and every POSITIVE locale count `S k'`, the block
164+
||| partition's per-locale counts sum to exactly `n`. No item is dropped or
165+
||| double-assigned. Quantified over ALL n, k'.
166+
|||
167+
||| Proof: the counts sum to `base * k + (remainder count)` (`sumCountsFrom`);
168+
||| the remainder count is exactly `n mod k` because `n mod k <= k`
169+
||| (`numBelowFull` + `modLEk`); and `base * k + n mod k = n div k * k + n mod k
170+
||| = n` by the Euclidean division theorem.
171+
export
172+
blockCountsComplete : (n, k' : Nat) -> sumNat (blockCounts n k') = n
173+
blockCountsComplete n k' =
174+
let base : Nat
175+
base = divNatNZ n (S k') SIsNonZero
176+
rem : Nat
177+
rem = modNatNZ n (S k') SIsNonZero
178+
-- 1. structural sum law
179+
step1 : sumNat (blockCounts n k') = base * (S k') + numBelow 0 rem (S k')
180+
step1 = sumCountsFrom 0 base rem (S k')
181+
-- 2. the remainder count collapses to rem, using n mod k <= k
182+
step2 : numBelow 0 rem (S k') = rem
183+
step2 = numBelowFull rem (S k') (modLEk n k')
184+
-- 3. Euclidean division theorem: n = rem + base * (S k')
185+
divThm : n = rem + base * (S k')
186+
divThm = DivisionTheorem n (S k') SIsNonZero SIsNonZero
187+
in rewrite step1 in
188+
rewrite step2 in
189+
-- goal: base * (S k') + rem = n
190+
rewrite plusCommutative (base * (S k')) rem in
191+
-- goal: rem + base * (S k') = n
192+
sym divThm
193+
194+
||| Corollary in the Layer-2 vocabulary: the block partition's `sliceSum` equals
195+
||| `n` for all n and k>0. `blockPartitionComplete` (Layer 2) reduced sliceSum to
196+
||| `sumNat (perItemCounts n k)`; `blockCounts n k'` is that very count vector in
197+
||| reducing form, so this closes the completeness loop for the real strategy.
198+
export
199+
blockSlicesSumIsN : (n, k' : Nat) ->
200+
sliceSum (contiguousFrom 0 (blockCounts n k')) = n
201+
blockSlicesSumIsN n k' =
202+
rewrite contiguousComplete 0 (blockCounts n k') in
203+
blockCountsComplete n k'
204+
205+
||| The full `PartitionComplete` proof OBJECT for the block partition, packaged
206+
||| as a `Partition` (the Layer-2 invariant type `sliceSum p.slices = n`), now
207+
||| DISCHARGED for the real block strategy at any n and k>0 — previously only
208+
||| provable for hand-written fixed vectors in `Proofs.idr`.
209+
export
210+
blockPartitionIsComplete : (n, k' : Nat) ->
211+
PartitionComplete
212+
(MkPartition {n} {k = S k'} (contiguousFrom 0 (blockCounts n k')))
213+
blockPartitionIsComplete n k' = IsComplete (blockSlicesSumIsN n k')
214+
215+
--------------------------------------------------------------------------------
216+
-- Sound + complete decision for "these counts cover exactly n"
217+
--------------------------------------------------------------------------------
218+
219+
||| A natural decision: do a candidate count vector's slices sum to exactly the
220+
||| declared item total? Decidable because `sumNat` is a concrete Nat and `Nat`
221+
||| has `DecEq`. Sound (Yes carries the equality) and complete (No carries a
222+
||| refutation), via `decEq`.
223+
export
224+
decCoversExactly : (target : Nat) -> (counts : Vect k Nat) ->
225+
Dec (sumNat counts = target)
226+
decCoversExactly target counts = decEq (sumNat counts) target
227+
228+
||| Reduce a `Dec` to whether it is the `No` branch — a concrete projector that
229+
||| evaluates, used by the negative-control below (the `No contra` term itself
230+
||| does not reduce cheaply, but its tag does).
231+
public export
232+
decidedNo : Dec p -> Bool
233+
decidedNo (Yes _) = False
234+
decidedNo (No _) = True
235+
236+
--------------------------------------------------------------------------------
237+
-- POSITIVE controls: concrete inhabited instances
238+
--------------------------------------------------------------------------------
239+
240+
||| Positive witness: 10 items over 3 locales. base = 3, rem = 1, so counts are
241+
||| [4,3,3] summing to 10. Machine-checked by `Refl` (the NZ primitives reduce on
242+
||| concrete literals) AND re-derived by the general theorem below.
243+
export
244+
covers10over3 : sumNat (blockCounts 10 2) = 10
245+
covers10over3 = Refl
246+
247+
||| The same fact via the general Layer-3 theorem, confirming the abstract proof
248+
||| specialises to the concrete reduct.
249+
export
250+
covers10over3_general : sumNat (blockCounts 10 2) = 10
251+
covers10over3_general = blockCountsComplete 10 2
252+
253+
||| A second concrete instance where division is exact (rem = 0): 12 over 4 gives
254+
||| [3,3,3,3] summing to 12. Exercises the `rem = 0` branch of the counting.
255+
export
256+
covers12over4 : sumNat (blockCounts 12 3) = 12
257+
covers12over4 = Refl
258+
259+
||| A positive Dec witness: the decision says Yes for the [4,3,3] cover of 10.
260+
||| `decCoversExactly` returns `Yes` here, and we project its proof.
261+
export
262+
dec10over3Yes : decCoversExactly 10 (blockCounts 10 2) = Yes Refl
263+
dec10over3Yes = Refl
264+
265+
--------------------------------------------------------------------------------
266+
-- NEGATIVE / non-vacuity controls
267+
--------------------------------------------------------------------------------
268+
269+
||| Non-vacuity 1: the theorem is NOT trivially true for the wrong target. The
270+
||| block cover of 10 does not sum to 9. We derive it from the real total (10):
271+
||| if it were also 9 then 10 = 9, absurd. (A bare `Refl : ... = 9` would itself
272+
||| be a type error, which is the point.)
273+
export
274+
notCovers10as9 : Not (sumNat (blockCounts 10 2) = 9)
275+
notCovers10as9 prf =
276+
-- blockCountsComplete 10 2 : sumNat (blockCounts 10 2) = 10
277+
uninhabited (trans (sym (blockCountsComplete 10 2)) prf)
278+
279+
||| Non-vacuity 2: the decision procedure genuinely says No when the target is
280+
||| wrong (9 vs the true 10). If `decCoversExactly` always said Yes the theorem
281+
||| would be vacuous; this `Refl` (the No tag reduces concretely) rules it out.
282+
||| Paired with `notCovers10as9`, this is the sound+complete negative side of the
283+
||| decision (Yes side witnessed by `dec10over3Yes`).
284+
export
285+
dec10over3as9No : decidedNo (decCoversExactly 9 (blockCounts 10 2)) = True
286+
dec10over3as9No = Refl
287+
288+
||| Non-vacuity 3 (numBelow is real, not a constant): with threshold 0 nobody
289+
||| gets the extra slot, but with a positive threshold somebody does — these are
290+
||| DIFFERENT, so the remainder count truly depends on `rem`. A `Refl` here would
291+
||| be ill-typed (0 vs 2), so the negation is the honest statement.
292+
export
293+
remainderCountMatters : Not (numBelow 0 0 5 = numBelow 0 2 5)
294+
remainderCountMatters prf = uninhabited prf

‎src/interface/abi/chapeliser-abi.ipkg‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,11 @@ package chapeliser-abi
55

66
sourcedir = "."
77

8+
depends = contrib
9+
810
modules = Chapeliser.ABI.Types
911
, Chapeliser.ABI.Layout
1012
, Chapeliser.ABI.Foreign
1113
, Chapeliser.ABI.Proofs
1214
, Chapeliser.ABI.Partition
15+
, Chapeliser.ABI.Invariants

0 commit comments

Comments
 (0)