Stream: Coq users

Topic: ✔ Function with dependently-typed result type (PnP exercise)

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 22 2022 at 09:32):

Pierre Rousselin has marked this topic as resolved.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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