Pull out uniform fixpoint arguments

[antalsz]

Coq has an easier time doing termination proofs when we pull out fixpoint arguments that don't change. For instance, in GHC's compiler/utils/Util.hs, we find the function

-- Reformatted
all2 :: (a -> b -> Bool) -> [a] -> [b] -> Bool
all2 _ []     []     = True
all2 p (x:xs) (y:ys) = p x y && all2 p xs ys
all2 _ _      _      = False

We translate this, in ghc/Util.v, to

(* Reformatted *)
Definition all2 {a} {b} : (a -> b -> bool) -> list a -> list b -> bool :=
  fix all2 arg_0__ arg_1__ arg_2__ :=
    match arg_0__, arg_1__, arg_2__ with
    | _, nil,       nil       => true
    | p, cons x xs, cons y ys => andb (p x y) (all2 p xs ys)
    | _, _,         _         => false
    end.

Here, arg_0__ is p, and is the function to apply to the list elements pairwise. If this function is or contains a nested recursive call at a call site of and2, this will break! But if we instead produced

Definition all2_better_1 {a} {b} (p : a -> b -> bool) -> list a -> list b -> bool :=
  fix all2 arg_1__ arg_2__ :=
    match arg_1__, arg_2__ with
    | nil,       nil       => true
    | cons x xs, cons y ys => andb (p x y) (all2 xs ys)
    | _,         _         => false
    end.

or

Definition all2_better_2 {a} {b} (a -> b -> bool) -> list a -> list b -> bool :=
  fun p =>
  fix all2 arg_1__ arg_2__ :=
    match arg_1__, arg_2__ with
    | nil,       nil       => true
    | cons x xs, cons y ys => andb (p x y) (all2 xs ys)
    | _,         _         => false
    end.

or even

Definition all2_better_3 {a} {b} (a -> b -> bool) -> list a -> list b -> bool :=
  fun p arg_0__ arg_1__ =>
  let fix all2 arg_2__ arg_3__ :=
        match arg_2__, arg_3__ with
        | nil,       nil       => true
        | cons x xs, cons y ys => andb (p x y) (all2 xs ys)
        | _,         _         => false
        end
  in all2 p arg_0__ arg_1__.

Coq can β-reduce the outer function, inline the definition of p with the nested recursive call into the fix, and potentially see that the result is terminating.

It would be incredible to do this automatically, but even some sort of uniform fix arguments edit would be great.

[antalsz]

We have the following edit in CoreUtils/edits:

in CoreUtils.eqExpr rewrite forall p, Util.all2 p a1 a2 = NestedRecursionHelpers.all2Map p id id a1 a2

We wouldn't need this at all if Util.all2 were defined one of those better ways.

[sweirich]

Util.mapAndUnzip is another example that would benefit with this edit. Right now, we manually redefine the function in module-edits/Util/edits