Stream: new members
Topic: more primrec examples?
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
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 (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
Jia Ming (Dec 10 2020 at 12:22):
Last updated: May 15 2021 at 00:39 UTC