Defining general recursive functions on their domains

Stream: general

[Trebor Huang]

Given an arbitrary general recursive function, how can we (1) define the domain on which it is total, and (2) define the function as a PFun? Here's my method which is in theory generally workable:

/-
To define a function

  f(0) = f(1) = 0
  f(n) = f(n/2) + 1  for n even
  f(n) = f(3*n+1) + 1 for n odd

But we don't know whether it is total yet. Can we
define f as a `PFun`? To do that, we need a
predicate for its domain.
-/

inductive Domain : Nat → Prop
| zero : Domain 0
| one : Domain 1
-- We can have cycles here, eg.
--  even : Domain n → Domain (2*n)
-- But this is slightly cleaner.
| even : Domain (n+1) → Domain (2*n+2)
| odd : Domain (6*n+10) → Domain (2*n+3)

/-
If we define `Domain` as a Type, then it is
known as the Bove–Capretta predicate, and we can
happily recurse along that, giving
  f (n : Nat) : Domain n → Nat
And if one day we manage to prove ∀ n, Domain n
then we can get the total function.
-/

inductive Prec : Nat → Nat → Prop
| even : Prec (n+1) (2*n+2)
| odd : Prec (6*n+10) (2*n+3)
| trans : Prec m n → Prec n p → Prec m p

def Prec' (u v : Subtype Domain) : Prop := Prec u.val v.val

/- Mostly just do the obvious thing, induction
on `Prec` is now available because we are proving
a `Prop` too. -/
theorem WfPrec' : WellFounded Prec' := sorry

Now we just do well-founded recursion, giving Subtype Domain -> Nat, which can then be converted to a PFun. Is there a neater way to do this? And can this be fully automated?

[Eric Wieser]

Can you write a sorry for your PFun question?

[Eric Wieser]

It's not clear to me what you're asking for

[Trebor Huang]

Use docs4#PFun.equivSubtype

[Trebor Huang]

After looking at the library I think the current fastest way is to write it as a fixpoint, then using PFun.fix