feat: partial_fixpoint: partial functions with equations

[nomeata]

This PR adds the ability to define possibly non-terminating functions and still be able to reason about them equationally, as long as they are tail-recursive or monadic.

This is still WIP. In particular, syntax and naming is not finalized yet, and currently inconsistent and all-over the place.

Typical uses of this feature are

def ack : (n m : Nat) → Option Nat
  | 0,   y   => some (y+1)
  | x+1, 0   => ack x 1
  | x+1, y+1 => do ack x (← ack (x+1) y)
partial_fixpiont

def whileSome (f : α → Option α) (x : α) : α :=
  match f x with
  | none => x
  | some x' => whileSome f x'
partial_fixpiont

def computeLfp {α : Type u} [DecidableEq α] (f : α → α) (x : α) : α :=
  let next := f x
  if x ≠ next then
    computeLfp f next
  else
    x
partial_fixpiont

noncomputable def geom : Distr Nat := do
  let head ← coin
  if head then
    return 0
  else
    let n ← geom
    return (n + 1)
partial_fixpiont

This PR contains

• The necessary fragment of domain theory, up to (a variant of) Knaster–Tarski theorem
• A tactic to solve monotonicity goals compositionally (a bit like mathlib’s fun_prop)
• An attribute to extend that tactic
• A “derecursifyer” that uses that machinery to define recursive function, including support for dependent functions and mutual recursion.
• Fixed-point induction principles (technical, tediuos to use)
• For Option-valued functions: Partial correctness induction theorems that hide all the domain theory

This is heavily inspired by Isabelle’s partial_function command.