The goal of this project is to solve Project Euler problems in a fast, proven-correct, and readable manner, priotized in that order.
The general structure of a solution will be:
-- The problem stated as clearly as possible, abstracted to take some notion of
-- input. This will normally be a ℕ representing an upper limit.
problem′ : A → ℕ
-- The problem filled in with the example given in the problem statement. Note
-- that not all problems have appropriate examples.
example : ℕ
-- A proof that the example matches the expected value, as a sort of smoke test
-- of our problem description.
example-correct : example ≡ n
-- The problem with the specific input desired.
problem : ℕ
-- The fast solution, again abstracted over the input.
solution′ : A → ℕ
-- A proof that for all inputs, our solution matches the problem.
solution-correct : problem′ ≗ solution′
-- The solution instantiated at the particular input the problem statement
-- calls for.
solution : ℕ
-- Output the solution.
open import Data.Nat.Show
open import IO
import IO.Primitive as Prim
main : Prim.IO _
main = run (putStrLn (show solution))