12. Verified maximum
Write maximum : List Nat → Nat and prove maximum_spec : MaxSpec maximum. There are no tests: the specification is the judge.
MaxSpec f asks for two things. The result is at least every element, and for a nonempty list it is one of the elements. The second half matters: without it, returning the sum of the list would also be “at least every element”.
What the judge checks
maximum_spec : MaxSpec maximumThe definitions these names refer to are the read-only lines above the editor. Write any helper lemmas you need before the final theorem.
Constraints
maximum []may be anything, but 0 is the natural choice.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.
\to in the editor, or click: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.