Exercises
🚧 This section is very much work in progress.
To work on these problems, we recommend you first install the Rocq prover or use it inside your browser. The source of the following problems is available on GitHub.
Every exercise has a difficulty level, ranging from beginner to advanced.
For more advanced exercises, you can visit Hydras & Co which presents an exploration of some properties of Kirby and Paris' hydra battles, including the study of several representations of ordinal numbers and a part of the so-called Ketonen and Solovay machinery.
Tail of a List
Write a function last : forall {A:Type}, list A -> A -> A where last l d returns the last element of the list l, or the default value d if l is empty.
the last element of a list
> Eval compute in last [1 ; 2 ; 3 ] 0;;
= 3 : nat
> Eval compute in last [] 0.
= 0 : nat
Open Scope list_scope.
Fixpoint last {A} (l:list A) (d:A) : A :=
match l with
| [] => d
| [a] => a
| a :: l => last l d
end.