54. Verified count of occurrences
Write count : Nat → List Nat → Nat and prove two things.
count_spec : CountSpec count describes counting one element at a time: nothing in [], one more for a matching head, and the same for a different head.
count_append: counting in xs ++ ys is counting in each part and adding. This one needs induction.
What the judge checks
count_spec : CountSpec count
count_append : ∀ (x : Nat) (xs ys : List Nat), count x (xs ++ ys) = count x xs + count x ysThe definitions these names refer to are the read-only lines above the editor. Write any helper lemmas you need before the final theorem.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem and one Medium problem a week are 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.