more primrec examples?

Stream: new members

[Jia Ming]

Hello, I'm exploring the computability folder right now and I absolutely LOVE it. Would mathlib welcome additional theorems like primrec nat.fact or primrec_pred nat.prime? The first one is a short proof that makes use of prec1 (not used anywhere else) and I don't know how the 2nd one will turn out yet. I could look and see where other typical textbook examples could fit in to mathlib nicely.

namespace nat
namespace primrec
-- proof that taking factorials is primitive recursive
theorem fact : primrec fact :=
(prec1 1 (mul'.comp (pair right (succ.comp left)))).of_eq $
  λ n, by simp; induction n; simp [*, mul_comm]

end primrec
end nat

Also, I noticed some omissions like primrec.nat_pow despite mathlib having nat.primrec.pow, while add, sub and mul are all synced, which to me looks like missing API.. Should I make a PR including these additions (if they are welcome)?

[Mario Carneiro]

Sure! The theorems that are in there are mostly those that I needed to build up to higher level theorems, but of course there are many functions in mathlib and most of the computable functions are primrec.

[Jia Ming]

Yay! awesome