Zulip Chat Archive

Stream: new members

Topic: more primrec examples?

view this post on Zulip Jia Ming (Dec 10 2020 at 08:29):

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)?

view this post on Zulip Mario Carneiro (Dec 10 2020 at 10:49):

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.

view this post on Zulip Jia Ming (Dec 10 2020 at 12:22):

Yay! awesome

Last updated: May 15 2021 at 00:39 UTC