Pierre Rousselin (Aug 22 2022 at 09:32): Pierre Rousselin (Aug 22 2022 at 09:32):My bad... I am very sorry but actually, the file with the exercises has Set Implicit Arguments while the one with the solutions has not. I should have checked. I didn't think an implicit argument was the cause of this problem, now I will be more careful with this.
Notification Bot (Aug 22 2022 at 09:32):Pierre Rousselin has marked this topic as resolved.
Malcolm Sharpe (Aug 23 2022 at 15:43):Thanks for posting, as I found this quite a useful exercise for myself as I learn dependent types. Though it's not quite related to your question, I find the solution surprisingly over-complicated. It seems much easier to do it this way:
Require Import Nat.
Definition is_even (n : nat) : bool := n mod 2 =? 0.
Definition solution (n : nat) : if is_even n then nat else bool :=
if is_even n as e return (if e then nat else bool)
then n / 2
else is_even (n / 2).
Example solution_test_true : solution 9 = true. Proof. reflexivity. Qed.
Example solution_test_false : solution 7 = false. Proof. reflexivity. Qed.
Example solution_test_nat : solution 10 = 5. Proof. reflexivity. Qed.
Is there is some subtle reason to use the approach in the model solution?
Paolo Giarrusso (Aug 24 2022 at 02:21):I'd say not for this exercise; I think the pattern in the model solution can come up in practice and be worth learning, but isn't needed for this exercise indeed.
Paolo Giarrusso (Aug 24 2022 at 02:24):(and no I don't have a good example in mind; interpreters for intrinsically typed syntax move in that direction, and type-directed transformers can move much further. In all those cases, I'd probably reach for Coq-Equations first).
Last updated: Feb 04 2023 at 21:02 UTC