English
If f : α → β and g : α → ℕ × β → β are primitive recursive in the right way, then the recursion on natural numbers with base case f a and step given by g a (n, IH) is Primrec₂ in a.
Русский
Если f : α → β и g : α → ℕ × β → β заданы примитивно рекурсивно, то рекурсия по натуральному числу с базовым случаем f a и шагом g a (n, IH) является Primrec₂ по a.
LaTeX
$$$ Primrec f \rightarrow Primrec_2 g \rightarrow Primrec_2 (\\lambda a (n : \mathbb{N}). n.rec (motive := (\\lambda _ => β)) (f a) (\\lambda n IH. g a (n, IH)))$$$
Lean4
theorem nat_rec {f : α → β} {g : α → ℕ × β → β} (hf : Primrec f) (hg : Primrec₂ g) :
Primrec₂ fun a (n : ℕ) => n.rec (motive := fun _ => β) (f a) fun n IH => g a (n, IH) :=
Primrec₂.nat_iff.2 <|
((Nat.Primrec.casesOn' .zero <|
(Nat.Primrec.prec hf <|
.comp hg <|
Nat.Primrec.left.pair <|
(Nat.Primrec.left.comp .right).pair <|
Nat.Primrec.pred.comp <| Nat.Primrec.right.comp .right).comp <|
Nat.Primrec.right.pair <| Nat.Primrec.right.comp Nat.Primrec.left).comp <|
Nat.Primrec.id.pair <| (Primcodable.prim α).comp Nat.Primrec.left).of_eq
fun n =>
by
simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat, Option.bind_some, Option.map_map,
Option.map_some]
rcases @decode α _ n.unpair.1 with - | a; · rfl
simp only [Nat.pred_eq_sub_one, encode_some, Nat.succ_eq_add_one, encodek, Option.map_some, Option.bind_some,
Option.map_map]
induction n.unpair.2 <;> simp [*, encodek]
