✔ Function with dependently-typed result type (PnP exercise) · Coq users

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'
  end.

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'
  end.

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

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.

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.

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'

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...

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):

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.

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).

Stream: Coq users

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

Pierre Rousselin (Aug 21 2022 at 15:04):