It’s my pleasure to announce a new Rocq library for partial programs that was designed with Meven Lennon-Bertand and Kenji Maillard, and is now available on opam.
opam install rocq-partial
It lets you write and combine partial fixed points as follows:
Definition ack : nat → nat → partial nat :=
#pfix ack (m : nat) (n : nat),
match m, n with
| 0, _ => ret (S n)
| S m', 0 => ack m' 1
| S m', S n' => k ← ack m n' ;; ack m' k
end.
Definition ack_sum : nat → partial nat :=
#pfix ack_sum n,
if n =? 0 then ret 0
else
k ← lift (ack n n) ;;
l ← ack_sum (n - 1) ;;
ret (k + l).
It’s quite in the early stages, so there’s probably a lot missing compared to what one can find in the wild in Agda or Lean. It’s mostly driven from use cases, so if you have some that do not fit what is provided don’t hesitate to open issues or pull requests.