Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.coin-change

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/coin_change.clj1 definitions, 4 theorems

AHoF Coin Change (dynamic programming): the minimum number of coins that sum to a target amount, from unlimited coins of given denominations -- the canonical unbounded-knapsack-style min-DP. Each cell for amount a is the minimum over denominations c of 1 + dp(a - c); comparing the running best against a new candidate is: cell current-best candidate = if candidate <= current-best then candidate else current-best (keep the smaller coin count), over exact-rational counts. Proved native and axiom-free: the DP cell as the decidable rational min (via logic/if-data); a worked cell taking the cheaper candidate; a worked cell keeping the current best; and the certificates that the cell value is at most BOTH the candidate and the current best (native nnrat/at-most) -- it is their minimum. The denomination sweep and unreachable-amount handling are executable; what is proved is the min-DP cell choice. Requires audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.coin-change` prints this classification.

coin-change/cell :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

coin-change/takes-cheaper-candidate :
  → coin-change/cell 5 3 = 3

coin-change/keeps-current-best :
  → coin-change/cell 4 7 = 4

coin-change/at-most-candidate :
  → 3 ≤ 3

coin-change/at-most-current :
  → 3 ≤ 5