## Stream: Coq users

### Topic: Does nat_rec from hott library compute?

#### Callan McGill (Feb 28 2022 at 04:14):

Hi, I am trying to write the ackermann function using only primitive recursion using the hott library but it doesn't seem to compute. I realize that use of univalence doesn't compute but I don't think that should change things here unless I am confused

``````Definition ack : nat -> nat -> nat.
Proof.
refine (nat_rec _ _ _).
(* ack 0 n = succ n *)
- exact succ.
- intros m ack_m.
Check nat_rec.
refine (nat_rec _ _ _).
(* ack (succ m) 0 = ack m 1 *)
* exact (ack_m 1%nat).
* intros ack_succ_m_0 ack_succ_m_n.
refine (ack_m _).
exact ack_succ_m_n.
Defined.

Compute ack (succ 0) 0.
``````

This gives back:

``````     = nat_rec (fun _ : nat => nat -> nat) (fun x : nat => (x.+1)%nat)
(fun (n : nat) (x : (fun _ : nat => nat -> nat) n) =>
nat_rec (fun _ : nat => nat) (x 1%nat)
(fun (n0 : nat) (x0 : (fun _ : nat => nat) n0) => x x0)) 1 0%nat
: nat
``````

#### Paolo Giarrusso (Feb 28 2022 at 07:05):

What does `Print nat_rec` say?

#### Paolo Giarrusso (Feb 28 2022 at 07:16):

I'd wonder if it's an axiom for some reason, or if it's marked Opaque (`About nat_rec` might be better to find that out). In the latter case, vm_compute will help.

#### Ali Caglayan (Feb 28 2022 at 09:43):

@Callan McGill I am unable to reproduce the issue on my end. Univalence will not change anything unless you actually start using it so that's not relevant here. Could you try using `Locate` on `nat_rec` just to check we are talking about the same one. I am also assuming you imported `From HoTT Require Import HoTT.`?

#### Ramkumar Ramachandra (Feb 28 2022 at 09:44):

Strange. I get

``````nat_rec
: forall P : nat -> Type0,
P 0%nat ->
(forall n : nat, P n -> P (n.+1)%nat) -> forall n : nat, P n
= 2%nat
: nat
``````

#### Callan McGill (Feb 28 2022 at 14:58):

Thank you @Paolo Giarrusso ! Once again, I had some bad namespace issue :expressionless:

Last updated: Jun 15 2024 at 08:01 UTC