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: Sep 23 2023 at 15:01 UTC