Support for translating fixed-points to eliminations (cf. Issue #18)

[nateyazdani]

Quick aside: I know that I'm submitting this on a Friday evening, so I want to emphasize that code review can easily wait until next week :-)

The translation approach is mostly as described in Issue #18:

1. Reorder the fixed-point's parameters to align with the appropriate eliminator, which follows the standard order from the inductive definition.
2. Partially evaluate the functional (fixed-point body) on each hypothetical constructor to derive the minor premises (a.k.a., case branches), while also exposing structurally recursive calls. Partial evaluation is done with beta-iota normalization.
3. Replace each recursive call with a reference to the appropriate recurrence binding (e.g., an inductive hypothesis).
4. Wrap the resulting term to accept arguments in the same order as the original fixed-point and reorder them for the elimination expression.

Support for whole-module translation will come in a subsequent PR.

The translated function will not necessary satisfy definitional equality with the original (fixed-point) form but has equivalent computational behavior (more precisely, bisimulative). This "definitional difference" can lead to an ill-typed translation when a proof term contains an expansion of another constant; List.In_nth demonstrates such a situation, unlike List.nth_In (for comparison). Whole-module translation will solve such problems, via compositionality analogous to ornamental lifting.

As one would expect, this translation only supports "primitive" structural recursion, in which each recursive call is on a direct descendent of the current structural guard value (i.e., no fancy transformation for n-induction). (Implicitly, that also leaves mutual recursion unsupported.) The benefit of this restriction is that the translated term corresponds extremely closely to its original form.

The new helper functions for fixed-point support also led to substantial simplification of the translation for bare (non-recursive) match expressions.

Tests were added to plugin/coq/Desugar.v and linked into plugin/test.sh.

I'm going to read through the current resubmission draft this weekend, to check for any mismatch between the paper's description of this translation and its present implementation.

[tlringer]

I think the best thing would be to go over this PR together when we meet.

[nateyazdani]

Alright, I think that I've covered all the needed revisions:

• Tests now compare translated term against an expected form (generated with current translation).
• That overly technical comment is now clarified.
• abstract_subterm now lives in the Abstraction module.
• Context management for eliminate_fixpoint now lives in init_fixpoint.
• factor_assums is now named abstract_assums, consistent with the meaning of "abstraction" in abstract_subterm. Perhaps this function should also move to the Abstraction module?
• Test case exposing an unrelated bug removed, with issue #24 filed for the bug.