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
Print nat_rec say?
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.
@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
nat_rec just to check we are talking about the same one. I am also assuming you imported
From HoTT Require Import HoTT.?
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
Thank you @Paolo Giarrusso ! Once again, I had some bad namespace issue :expressionless:
Last updated: Feb 09 2023 at 00:03 UTC