Stream: Coq users

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

view this post on Zulip Pierre Rousselin (Aug 21 2022 at 15:04):

I'm (partially) reading Programs and Proofs by Ilya Sergey. Last exercise in chapter 2 (FunProg.v) is the following.

Exercise [Functions with dependently-typed result type]

Write a function that has a dependent result type and whose result is
[true] for natural numbers of the form [4n + 1], [false] for numbers
of the form [4n + 3] and [n] for numbers of the from [2n].

Hint: Again, you might need to define a number of auxiliary
 (possibly, higher-order) functions to complete this exercise.

Failing at finding the solution, I read the solution in the git repository which is as follows:

Fixpoint dep_type (n : nat) : Set := match n with
  | 0 => nat
  | 1 => bool
  | n'.+2 => dep_type n'

Fixpoint dep_value_aux (n: nat): dep_type n -> dep_type n :=
  match n return dep_type n -> dep_type n with
  | 0 => fun x => x.+1
  | 1 => fun x => ~~x
  | n'.+2 => dep_value_aux n'

Fixpoint dep_value (n: nat): dep_type n :=
  match n  with
  | 0 => 0
  | 1 => true
  | n'.+2 => dep_value_aux n' (dep_value n')

Coq refuses the definition of dep_value_aux with the following message:

In environment
dep_value_aux : forall n : nat, dep_type n -> dep_type n
n : nat
n0 : nat
n' : nat
The term "n'" has type "nat" while it is expected to have type "dep_type ?n".

I guess that it used to work with coq 8.11.2 but does not with 8.15.2 which is the version I use.

view this post on Zulip Li-yao (Aug 21 2022 at 16:01):

There's some implicit argument option somewhere that needs to be disabled for this definition to work.

view this post on Zulip Kenji Maillard (Aug 21 2022 at 16:06):

Or you could probably replace | n'.+2 => dep_value_aux n' by | n'.+2 => @dep_value_aux n'

view this post on Zulip Paolo Giarrusso (Aug 21 2022 at 17:09):

Ah, so the behavior of Set Implicit Argument etc changed (assuming the settings were the same in both versions? if it did change, I guess it wouldn't be a regression...

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: Oct 04 2023 at 19:01 UTC