Auto-generate lifting-compatible eliminators for lifted inductive types (fixes #19)

[nateyazdani]

These commits resolve issue #19 by generating custom variants of eliminators (by default named <typename>_rect_sigT and <typename>_ind_sigT) for lifted inductive types. These are then declared as the liftings of the base type's corresponding eliminators. (Coq still generates the normal eliminators <typename>_rect and <typename>_ind, which the lifting algorithm just ignores.)

The generated eliminators follow the structure described and demonstrated in the comments of issue #19. To briefly summarize, the difference from a normal Coq eliminator is that every occurrence of a sigma-typed variable, even in the motive, is eta-expanded. This allows the core lifting algorithm to continue relying on its assumptions about eta-expansion in its own rewriting process.

For example, consider an eliminator of the following form:

Ind_rect (par_1 : Par_1) ... (par_n : Par_n)
         (P : forall (idx_1 : Idx_1) ... (idx_m : Idx_m),
                Ind par_1 ... par_n idx_1 ... idx_n -> Type)
         ...
         (case_i : forall (arg_1 : Arg_1) ... (arg_n : Arg_n),
           P ... <recursive_reference> ->
           P ... (constructor_i par_1 ... par_n arg_1 ... arg_n))
         ...
  : forall (idx_1 : Idx_1) ... (idx_n : Idx_n)
           (H : Ind par_1 ... par_n idx_1 ... idx_n),
      P par_1 ... par_n idx_1 ... idx_n H

When one of the index types (e.g., Idx_i) is a sigma type sigT ..., every use of a quantified index (idx_i : Idx_i) needs to be eta-expanded into existT (projT1 idx_i) (projT2 idx_i).

The crux of the challenge is that we want an eliminator variant that accepts a motive P in whose type every sigma-type index is eta-expanded.

The reason that this is so challenging is because it puts us right up against one of the main theoretical restrictions of CIC, which is the mandatory abstraction over indices in elimination/destruction forms. (This is closely related to the unprovability of UIP in plain CIC, though we're thankfully clear of the aspects that make UIP unprovable.)

If the ith index is the only one of a sigma type, then the motive type should have the following form:

forall (idx_1 : Idx_1) ... (idx_m : Idx_m),
  Ind par_1 ... par_n idx_1 ... (existT (projT1 idx_i) (projT2 idx_i)) ... idx_n -> Type

The implementation works by translating each eliminator term generated by Coq (e.g., <typename>_rect) into an expression, which is then type-checked by Coq and defined (e.g., as <typename>_rect_sigT ). Passing through a top-level expression allows us to leverage Coq's inference of universe instances+constraints and its automatic elaboration of nested pattern-matches; this allows to offload the complexity of constructing terms near the "edge" of Coq's expressivity.

Rather than go on and on about details that may or may not be helpful to the code review, I'll stop here after the high level summary, and elaborate on request to the level of detail desired.

[nateyazdani]

The testcases all pass. The benchmark results should be unaffected, but the script still doesn't fully work for me. (Similar problem to last time, with the error "head: illegal line count -- -1".)

Inspecting the intermediate log files (together/*/*.out) indicates that benchmark results are indeed unaffected by these changes. I've attached two examples, postorder/avl100.out and search/avl100.out, and I'm happy to post more if you'd like.

The generated eliminator is registered as a lifting by define_lifted_eliminator; I'll make an inline comment so that you can find it. And yes, we use the lifting cache for that purpose, since it's really a lifting registry rather than a "cache" per se.