Lean4

22. Coin change

MediumProgramAcademy Pass20 points

You have unlimited coins of each value in coins. Write coinChange coins amount: some k when k is the smallest number of coins that add up to amount, and none when no combination does.

Always taking the largest coin that fits does not work: with coins [1, 3, 4], 6 is 3 + 3, not 4 + 1 + 1.

Examples

  1. InputcoinChange [1, 2, 5] 11Outputsome 3
  2. InputcoinChange [2] 3Outputnone
  3. InputcoinChange [1] 0Outputsome 0

Submitting also runs 6 hidden tests.

Constraints

  • Coin values are positive.
  • Hidden tests use amounts up to 6,249, where plain recursion runs out of time.
dynamic programmingarraysperformance

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Learn the ideas

Similar problems

Solution.lean
Loading…
Loading editor…
3#guard (coinChange [1, 2, 5] 11) = (some 3)
4#guard (coinChange [2] 3) = (none)
5#guard (coinChange [1] 0) = (some 0)
examples

Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.

ReadyLn 1, Col 1Lean 4
Draft saved in this browser