Convert fixed-point expressions to eliminator applications

[nateyazdani]

This would be an extension of match desugaring.

Problem and suggested translation process

For simple cases where a match expression is nested immediately inside the function body (e.g., fix f (n : nat) : A := match n with S n' => e_S | O => e_O end), translating fixed-points will be more or less straightforward; we can simply substitute for each possible recursive call in each branch of the match expression (e.g., e_S[IHn'/(f n')]).

The translation will get a bit tricker if the fixed-point takes multiple parameters, as that will require pushing any lambda-bindings after the recursive parameter into the branches of the match expression (equivalently, into the cases of an eliminator application), but Coq's utility functions can handle most of the dirty work for that.

The biggest challenge is when the fixed-point's body does not contain an immediate match expression. When that happens, the fixed-point body could even contain multiple match expressions (e.g., fix f ... : A := if ... then match ... end else match ... end), and we will somehow need to extract a single branch for each constructor. The most robust approach would be to substitute each constructor form of the recursive parameter, partially evaluate (which will reduce every internal match expression on the recursive parameter), and then substitute recursive calls like before.

Example of the translation process

Input:

fix f (x:A) (n:nat) (y:B) {struct n} : C :=
  if Nat.eqb n 7 then
    match n with S n' => e_S | O => e_O end
  else
    match n with S n' => e_S' | O => e_O' end

Factor out/in non-recursive parameters

Pull out pre-recursion parameters:

fun (x:A) : nat -> B -> C =>
  fix f (n : nat) (y : B) {struct n} : C :=
    if Nat.eqb n 7 then
      match n with S n' => e_S[f/(f x)] | O => e_O[f/(f x)] end
    else
      match n with S n' => e_S'[f/(f x)] | O => e_O'[f/(f x)] end

Push in post-recursion parameters:

fun (x:A) : nat -> B -> C =>
  fix f (n:nat) : B -> C :=
    fun (y:B) : C =>
      if Nat.eqb n 7 then
        match n with S n' => e_S[f/(f x)] | O => e_O[f/(f x)] end
      else
        match n with S n' => e_S'[f/(f x)] | O => e_O'[f/(f x)] end

Save the fixed-point expression's type, nat -> B -> C, to use as the elimination motive P later on.

Extract elimination case for constructor S

Decompose bindings up to the recursive reference:

x:A, f:nat -> B -> C, n:nat |- fun (y:B) => if Nat.eqb n 7 then match n with ... end else match n with ... end

Abstract constructor parameters (with recurrence following each recursive field), substitute constructor form for n, and then partially evaluate:

x:A, f:nat -> B -> C, n':nat, IHn':B -> C |- fun (y:B) => if Nat.eqb (S n') 7 then match (S n') with ... end else match (S n') with ... end
-->*[iota]
x:A, f:nat -> B -> C, n':nat, IHn':B -> C |- fun (y:B) => if Nat.eqb (S n') 7 then e_S[f/(f x)] else e_S'[f/(f x)]

Substitute the relevant recurrence for each recursive call:

x:A, f:nat -> B -> C, n':nat, IHn':B -> C |- fun (y:B) => if Nat.eqb (S n') 7 then e_S[f/(f x)][IHn'/(f n')] else e_S'[f/(f x)][IHn'/(f n')]

At this point, I'd recommend using Vars.noccurn to assert that there truly are no references to f left in the term. Coq's fixed-point rules say that that should be the case, but an explicit check will help debug index/offset calculations.

Delete functional recursive reference (from fixed-point):

x:A, n':nat, IHn':B -> C |- fun (y:B) => if Nat.eqb (S n') 7 then e_S[f/(f x)][IHn'/(f n')] else e_S'[f/(f x)][IHn'/(f n')]

Recompose constructor+recurrence parameters:

x:A |- fun (n':nat) (IH:B -> C) (y:B) : C => if Nat.eqb (S n') 7 then e_S[f/(f x)][IH/(f n')] else e_S'[f/(f x)][IH/(f n')]

We now have the elimination case for the S constructor, case_S.

Extract elimination case for constructor O

Same process as for S.

Construct eliminator application

We have built two elimination cases:

x:A |- case_S : nat -> (B -> C) -> B -> C (* forall (n:nat) (P n), P (S n) *)
x:A |- case_O : B -> C (* P O *)

With those expressions and the earlier elimination motive, we build an application of the eliminator:

x:A |- nat_rect P case_S case_O : P
fun (x:A) : P => nat_rect P case_S case_O

And that's it. Coq's (and our) utility functions can handle the index shuffling, substitution, and de-/re-composition of binders, but it will still be tricky to get all the offsets and whatnot right.

[nateyazdani]

Resolved by PR #23.