Add a couple more identifiers to support eager rec

This will allow us to write rewrite rules that eagerly evaluate
recursion principles on the RHS.

After     | File Name                                                   | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------------------
35m52.89s | Total                                                       | 35m21.19s || +0m31.69s | +1.49%
-----------------------------------------------------------------------------------------------------------
1m03.44s  | GENERATEDIdentifiersWithoutTypesProofs.vo                   | 0m52.51s  || +0m10.92s | +20.81%
0m42.76s  | UnderLetsProofs.vo                                          | 0m37.59s  || +0m05.16s | +13.75%
1m50.02s  | RewriterRulesInterpGood.vo                                  | 1m46.65s  || +0m03.37s | +3.15%
3m14.40s  | p384_32.c                                                   | 3m16.54s  || -0m02.13s | -1.08%
1m53.47s  | RewriterRulesGood.vo                                        | 1m56.16s  || -0m02.68s | -2.31%
0m34.80s  | AbstractInterpretationZRangeProofs.vo                       | 0m32.33s  || +0m02.46s | +7.63%
0m22.80s  | ExtractionOCaml/word_by_word_montgomery                     | 0m20.53s  || +0m02.26s | +11.05%
2m55.61s  | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m53.77s  || +0m01.84s | +1.05%
2m37.56s  | Fancy/Compiler.vo                                           | 2m39.51s  || -0m01.94s | -1.22%
1m47.71s  | Fancy/Barrett256.vo                                         | 1m46.42s  || +0m01.29s | +1.21%
0m59.28s  | ExtractionHaskell/word_by_word_montgomery                   | 0m57.33s  || +0m01.95s | +3.40%
0m42.71s  | LanguageInversion.vo                                        | 0m40.75s  || +0m01.96s | +4.80%
0m40.95s  | ExtractionHaskell/unsaturated_solinas                       | 0m39.76s  || +0m01.19s | +2.99%
0m32.88s  | AbstractInterpretationProofs.vo                             | 0m31.38s  || +0m01.50s | +4.78%
0m28.98s  | PushButtonSynthesis/MontgomeryReductionReificationCache.vo  | 0m27.08s  || +0m01.90s | +7.01%
0m17.39s  | PushButtonSynthesis/BarrettReductionReificationCache.vo     | 0m18.95s  || -0m01.55s | -8.23%
0m12.51s  | GENERATEDIdentifiersWithoutTypes.vo                         | 0m11.11s  || +0m01.40s | +12.60%
0m12.30s  | ExtractionOCaml/word_by_word_montgomery.ml                  | 0m13.84s  || -0m01.53s | -11.12%
0m07.16s  | ExtractionHaskell/unsaturated_solinas.hs                    | 0m05.67s  || +0m01.49s | +26.27%
0m05.84s  | ExtractionHaskell/saturated_solinas.hs                      | 0m04.84s  || +0m01.00s | +20.66%
2m01.25s  | RewriterWf2.vo                                              | 2m01.06s  || +0m00.18s | +0.15%
1m22.67s  | Rewriter.vo                                                 | 1m22.48s  || +0m00.18s | +0.23%
0m54.42s  | AbstractInterpretationWf.vo                                 | 0m55.26s  || -0m00.83s | -1.52%
0m53.40s  | RewriterInterpProofs1.vo                                    | 0m52.85s  || +0m00.54s | +1.04%
0m46.26s  | p521_32.c                                                   | 0m46.58s  || -0m00.32s | -0.68%
0m44.94s  | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo   | 0m45.20s  || -0m00.26s | -0.57%
0m40.17s  | p521_64.c                                                   | 0m39.49s  || +0m00.67s | +1.72%
0m37.93s  | Fancy/Montgomery256.vo                                      | 0m37.31s  || +0m00.61s | +1.66%
0m36.59s  | PushButtonSynthesis/UnsaturatedSolinas.vo                   | 0m36.22s  || +0m00.37s | +1.02%
0m30.06s  | ExtractionHaskell/saturated_solinas                         | 0m29.33s  || +0m00.73s | +2.48%
0m29.61s  | LanguageWf.vo                                               | 0m29.48s  || +0m00.12s | +0.44%
0m26.76s  | PushButtonSynthesis/WordByWordMontgomery.vo                 | 0m26.77s  || -0m00.00s | -0.03%
0m26.23s  | SlowPrimeSynthesisExamples.vo                               | 0m26.36s  || -0m00.12s | -0.49%
0m25.30s  | RewriterWf1.vo                                              | 0m25.47s  || -0m00.16s | -0.66%
0m20.01s  | p448_solinas_64.c                                           | 0m19.97s  || +0m00.04s | +0.20%
0m19.56s  | p256_32.c                                                   | 0m20.04s  || -0m00.48s | -2.39%
0m19.28s  | secp256k1_32.c                                              | 0m18.86s  || +0m00.42s | +2.22%
0m16.08s  | CStringification.vo                                         | 0m15.70s  || +0m00.37s | +2.42%
0m16.04s  | p434_64.c                                                   | 0m15.20s  || +0m00.83s | +5.52%
0m13.39s  | ExtractionOCaml/unsaturated_solinas                         | 0m13.13s  || +0m00.25s | +1.98%
0m09.57s  | p224_32.c                                                   | 0m08.95s  || +0m00.62s | +6.92%
0m09.27s  | ExtractionOCaml/saturated_solinas                           | 0m10.22s  || -0m00.95s | -9.29%
0m08.70s  | p384_64.c                                                   | 0m07.93s  || +0m00.76s | +9.70%
0m08.43s  | ExtractionOCaml/unsaturated_solinas.ml                      | 0m09.07s  || -0m00.64s | -7.05%
0m07.44s  | ExtractionHaskell/word_by_word_montgomery.hs                | 0m08.35s  || -0m00.90s | -10.89%
0m06.97s  | ExtractionOCaml/saturated_solinas.ml                        | 0m07.28s  || -0m00.31s | -4.25%
0m06.81s  | BoundsPipeline.vo                                           | 0m06.78s  || +0m00.02s | +0.44%
0m06.72s  | PushButtonSynthesis/SaturatedSolinasReificationCache.vo     | 0m06.85s  || -0m00.12s | -1.89%
0m05.77s  | Fancy/Prod.vo                                               | 0m06.07s  || -0m00.30s | -4.94%
0m04.06s  | MiscCompilerPassesProofs.vo                                 | 0m03.84s  || +0m00.21s | +5.72%
0m03.71s  | PushButtonSynthesis/Primitives.vo                           | 0m03.34s  || +0m00.37s | +11.07%
0m03.34s  | PushButtonSynthesis/SmallExamples.vo                        | 0m03.26s  || +0m00.08s | +2.45%
0m03.16s  | PushButtonSynthesis/SaturatedSolinas.vo                     | 0m03.22s  || -0m00.06s | -1.86%
0m03.15s  | PushButtonSynthesis/BarrettReduction.vo                     | 0m03.29s  || -0m00.14s | -4.25%
0m02.84s  | PushButtonSynthesis/MontgomeryReduction.vo                  | 0m02.90s  || -0m00.06s | -2.06%
0m02.79s  | curve25519_32.c                                             | 0m02.92s  || -0m00.12s | -4.45%
0m02.12s  | curve25519_64.c                                             | 0m02.13s  || -0m00.00s | -0.46%
0m01.70s  | secp256k1_64.c                                              | 0m01.55s  || +0m00.14s | +9.67%
0m01.64s  | p256_64.c                                                   | 0m01.23s  || +0m00.40s | +33.33%
0m01.57s  | p224_64.c                                                   | 0m01.68s  || -0m00.10s | -6.54%
0m01.36s  | Language.vo                                                 | 0m01.33s  || +0m00.03s | +2.25%
0m01.33s  | CLI.vo                                                      | 0m01.32s  || +0m00.01s | +0.75%
0m01.26s  | AbstractInterpretation.vo                                   | 0m01.25s  || +0m00.01s | +0.80%
0m01.13s  | RewriterProofs.vo                                           | 0m01.18s  || -0m00.05s | -4.23%
0m01.13s  | StandaloneOCamlMain.vo                                      | 0m01.04s  || +0m00.08s | +8.65%
0m01.10s  | CompilersTestCases.vo                                       | 0m01.16s  || -0m00.05s | -5.17%
0m01.04s  | StandaloneHaskellMain.vo                                    | 0m01.18s  || -0m00.13s | -11.86%
0m00.76s  | MiscCompilerPasses.vo                                       | 0m00.74s  || +0m00.02s | +2.70%
0m00.60s  | PushButtonSynthesis/LegacySynthesisTactics.vo               | 0m00.66s  || -0m00.06s | -9.09%
0m00.46s  | UnderLets.vo                                                | 0m00.48s  || -0m00.01s | -4.16%
0m00.44s  | PushButtonSynthesis/ReificationCache.vo                     | 0m00.52s  || -0m00.08s | -15.38%

7 files changed, 232 insertions, 2 deletions

diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 63a7df1ed..808128025 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -509,6 +509,7 @@ Module Compilers.
                    | None => ZRange.type.base.option.None
                    end
              | ident.nat_rect _
+             | ident.eager_nat_rect _
                => fun O_case S_case n
                  => match n with
                    | Some n
@@ -519,6 +520,7 @@ Module Compilers.
                          n
                    | None => ZRange.type.base.option.None
                    end
+             | ident.eager_nat_rect_arrow _ _
              | ident.nat_rect_arrow _ _
                => fun O_case S_case n v
                  => match n with
@@ -531,6 +533,7 @@ Module Compilers.
                          v
                    | None => ZRange.type.base.option.None
                    end
+             | ident.eager_list_rect _ _
              | ident.list_rect _ _
                => fun N C ls
                  => match ls with
@@ -542,6 +545,18 @@ Module Compilers.
                          ls
                    | None => ZRange.type.base.option.None
                    end
+             | ident.eager_list_rect_arrow _ _ _
+               => fun N C ls v
+                 => match ls with
+                   | Some ls
+                     => list_rect
+                         _
+                         N
+                         (fun x xs rec => C x (Some xs) rec)
+                         ls
+                         v
+                   | None => ZRange.type.base.option.None
+                   end
              | ident.list_case _ _
                => fun N C ls
                  => match ls with
diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v
index a1e2f180e..85eef1cae 100644
--- a/src/AbstractInterpretationWf.v
+++ b/src/AbstractInterpretationWf.v
@@ -699,6 +699,7 @@ Module Compilers.
                        | solve [ eauto ]
                        | apply NatUtil.nat_rect_Proper_nondep
                        | apply ListUtil.list_rect_Proper
+                       | apply ListUtil.list_rect_arrow_Proper
                        | apply ListUtil.list_case_Proper
                        | apply ListUtil.pointwise_map
                        | apply ListUtil.fold_right_Proper
diff --git a/src/AbstractInterpretationZRangeProofs.v b/src/AbstractInterpretationZRangeProofs.v
index 81483714f..2ca2ea140 100644
--- a/src/AbstractInterpretationZRangeProofs.v
+++ b/src/AbstractInterpretationZRangeProofs.v
@@ -354,6 +354,16 @@ Module Compilers.
                                  | specialize (IH ls');
                                    generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
                                 intros
+                           | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls ?x) (list_rect ?P' ?N' ?C' ?ls' ?y) = true ]
+                             => is_var ls; is_var ls'; is_var x; is_var y;
+                                revert dependent y; try revert dependent x;
+                                let IH := fresh "IH" in
+                                revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *;
+                                [
+                                | exfalso; discriminate | exfalso; discriminate
+                                | specialize (IH ls');
+                                  generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
+                                intros
                            | [ H : forall a b, ?R a b = true -> ?R' (?f a) (?g b) = true |- ?R' (?f _) (?g _) = true ] => apply H; clear H
                            | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> ?R'' (?f a c) (?g b d) = true |- ?R'' (?f _ _) (?g _ _) = true ]
                              => apply H; clear H
@@ -362,6 +372,9 @@ Module Compilers.
                            | [ H : context[ZRange.type.base.option.is_bounded_by (?f (Some _) (Some _)) (?g _ _) = true]
                                |- ZRange.type.base.option.is_bounded_by (?f (Some _) (Some _)) (?g _ _) = true ]
                              => apply H
+                           | [ H : (forall a b, ?R0 a b = true -> forall c d, ?R1 c d = true -> forall e f, (forall g h, ?R3 g h = true -> ?R4 (e g) (f h) = true) -> forall i j, ?R5 i j = true -> ?R6 (?F _ _ _ _) (?G _ _ _ _) = true)
+                               |- ?R6 (?F _ _ _ _) (?G _ _ _ _) = true ]
+                             => apply H; clear H
                            end ].
 
           Local Lemma mul_by_halves_bounds x y n :
diff --git a/src/CStringification.v b/src/CStringification.v
index 9ae80d140..3560a5f82 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -241,12 +241,20 @@ Module Compilers.
              | ident.bool_rect T => fun '(t, (f, ((b, br), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 200) ("if " ++ b 200%nat ++ " then " ++ maybe_wrap_cast with_casts t 200%nat ++ " else " ++ maybe_wrap_cast with_casts f 200%nat), ZRange.type.base.option.None)
              | ident.nat_rect P
                => fun args => (show_application with_casts (fun _ => "nat_rect") args, ZRange.type.base.option.None)
+             | ident.eager_nat_rect P
+               => fun args => (show_application with_casts (fun _ => "eager_nat_rect") args, ZRange.type.base.option.None)
+             | ident.eager_nat_rect_arrow P Q
+               => fun args => (show_application with_casts (fun _ => "eager_nat_rect(→)") args, ZRange.type.base.option.None)
              | ident.nat_rect_arrow P Q
                => fun args => (show_application with_casts (fun _ => "nat_rect(→)") args, ZRange.type.base.option.None)
              | ident.option_rect A P
                => fun args => (show_application with_casts (fun _ => "option_rect") args, ZRange.type.base.option.None)
              | ident.list_rect A P
                => fun args => (show_application with_casts (fun _ => "list_rect") args, ZRange.type.base.option.None)
+             | ident.eager_list_rect A P
+               => fun args => (show_application with_casts (fun _ => "eager_list_rect") args, ZRange.type.base.option.None)
+             | ident.eager_list_rect_arrow A P Q
+               => fun args => (show_application with_casts (fun _ => "eager_list_rect(→)") args, ZRange.type.base.option.None)
              | ident.list_case A P
                => fun args => (show_application with_casts (fun _ => "list_case") args, ZRange.type.base.option.None)
              | ident.List_length T
@@ -381,8 +389,12 @@ Module Compilers.
                 | ident.prod_rect A B T => "prod_rect"
                 | ident.bool_rect T => "bool_rect"
                 | ident.nat_rect P => "nat_rect"
+                | ident.eager_nat_rect P => "eager_nat_rect"
                 | ident.nat_rect_arrow P Q => "nat_rect(→)"
+                | ident.eager_nat_rect_arrow P Q => "eager_nat_rect(→)"
                 | ident.list_rect A P => "list_rect"
+                | ident.eager_list_rect A P => "eager_list_rect"
+                | ident.eager_list_rect_arrow A P Q => "eager_list_rect(→)"
                 | ident.list_case A P => "list_case"
                 | ident.List_length T => "length"
                 | ident.List_seq => "seq"
@@ -1280,11 +1292,15 @@ Module Compilers.
                | ident.prod_rect _ _ _
                | ident.bool_rect _
                | ident.nat_rect _
+               | ident.eager_nat_rect _
                | ident.nat_rect_arrow _ _
+               | ident.eager_nat_rect_arrow _ _
                | ident.Some _
                | ident.None _
                | ident.option_rect _ _
                | ident.list_rect _ _
+               | ident.eager_list_rect _ _
+               | ident.eager_list_rect_arrow _ _ _
                | ident.list_case _ _
                | ident.List_length _
                | ident.List_seq
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index d8a8138a6..c250253e1 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -236,6 +236,34 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                           (Compilers.base.type.type_base base.type.nat) ->
                         (fun x : Compilers.base.type => type.base x) P ->
                         (fun x : Compilers.base.type => type.base x) Q)%ptype
+  | eager_nat_rect : forall P : Compilers.base.type,
+                     ident
+                       (((fun x : Compilers.base.type => type.base x)
+                           ()%etype ->
+                         (fun x : Compilers.base.type => type.base x) P) ->
+                        ((fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.nat) ->
+                         (fun x : Compilers.base.type => type.base x) P ->
+                         (fun x : Compilers.base.type => type.base x) P) ->
+                        (fun x : Compilers.base.type => type.base x)
+                          (Compilers.base.type.type_base base.type.nat) ->
+                        (fun x : Compilers.base.type => type.base x) P)%ptype
+  | eager_nat_rect_arrow : forall P Q : Compilers.base.type,
+                           ident
+                             (((fun x : Compilers.base.type => type.base x) P ->
+                               (fun x : Compilers.base.type => type.base x) Q) ->
+                              ((fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.type_base base.type.nat) ->
+                               ((fun x : Compilers.base.type => type.base x)
+                                  P ->
+                                (fun x : Compilers.base.type => type.base x)
+                                  Q) ->
+                               (fun x : Compilers.base.type => type.base x) P ->
+                               (fun x : Compilers.base.type => type.base x) Q) ->
+                              (fun x : Compilers.base.type => type.base x)
+                                (Compilers.base.type.type_base base.type.nat) ->
+                              (fun x : Compilers.base.type => type.base x) P ->
+                              (fun x : Compilers.base.type => type.base x) Q)%ptype
   | list_rect : forall A P : Compilers.base.type,
                 ident
                   (((fun x : Compilers.base.type => type.base x) ()%etype ->
@@ -248,6 +276,41 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                    (fun x : Compilers.base.type => type.base x)
                      (Compilers.base.type.list A) ->
                    (fun x : Compilers.base.type => type.base x) P)%ptype
+  | eager_list_rect : forall A P : Compilers.base.type,
+                      ident
+                        (((fun x : Compilers.base.type => type.base x)
+                            ()%etype ->
+                          (fun x : Compilers.base.type => type.base x) P) ->
+                         ((fun x : Compilers.base.type => type.base x) A ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.list A) ->
+                          (fun x : Compilers.base.type => type.base x) P ->
+                          (fun x : Compilers.base.type => type.base x) P) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.list A) ->
+                         (fun x : Compilers.base.type => type.base x) P)%ptype
+  | eager_list_rect_arrow : forall A P Q : Compilers.base.type,
+                            ident
+                              (((fun x : Compilers.base.type => type.base x)
+                                  P ->
+                                (fun x : Compilers.base.type => type.base x)
+                                  Q) ->
+                               ((fun x : Compilers.base.type => type.base x)
+                                  A ->
+                                (fun x : Compilers.base.type => type.base x)
+                                  (Compilers.base.type.list A) ->
+                                ((fun x : Compilers.base.type => type.base x)
+                                   P ->
+                                 (fun x : Compilers.base.type => type.base x)
+                                   Q) ->
+                                (fun x : Compilers.base.type => type.base x)
+                                  P ->
+                                (fun x : Compilers.base.type => type.base x)
+                                  Q) ->
+                               (fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.list A) ->
+                               (fun x : Compilers.base.type => type.base x) P ->
+                               (fun x : Compilers.base.type => type.base x) Q)%ptype
   | list_case : forall A P : Compilers.base.type,
                 ident
                   (((fun x : Compilers.base.type => type.base x) ()%etype ->
@@ -799,7 +862,11 @@ show_match_ident = r"""match # with
  | ident.bool_rect T =>
  | ident.nat_rect P =>
  | ident.nat_rect_arrow P Q =>
+ | ident.eager_nat_rect P =>
+ | ident.eager_nat_rect_arrow P Q =>
  | ident.list_rect A P =>
+ | ident.eager_list_rect A P =>
+ | ident.eager_list_rect_arrow A P Q =>
  | ident.list_case A P =>
  | ident.List_length T =>
  | ident.List_seq =>
@@ -876,7 +943,7 @@ remake = False
 if remake:
   assert(os.path.exists('/tmp/pr.out'))
   assert(os.path.exists('/tmp/sm.out'))
-  with open('/tmp/pr.out', 'r') as f: print_ident = re.sub(r'^For.*\n', '', f.read(), flags=re.MULTILINE)
+  with open('/tmp/pr.out', 'r') as f: print_ident = re.sub(r'^For [^ ]*: Argument.*', '', f.read(), flags=re.MULTILINE|re.DOTALL)
   with open('/tmp/sm.out', 'r') as f: show_match_ident = f.read()
 
 prefix = 'Compilers.'
@@ -1405,7 +1472,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
         | bool_rect
         | nat_rect
         | nat_rect_arrow
+        | eager_nat_rect
+        | eager_nat_rect_arrow
         | list_rect
+        | eager_list_rect
+        | eager_list_rect_arrow
         | list_case
         | List_length
         | List_seq
@@ -1495,7 +1566,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | bool_rect => Compilers.base.type
              | nat_rect => Compilers.base.type
              | nat_rect_arrow => Compilers.base.type * Compilers.base.type
+             | eager_nat_rect => Compilers.base.type
+             | eager_nat_rect_arrow => Compilers.base.type * Compilers.base.type
              | list_rect => Compilers.base.type * Compilers.base.type
+             | eager_list_rect => Compilers.base.type * Compilers.base.type
+             | eager_list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type
              | list_case => Compilers.base.type * Compilers.base.type
              | List_length => Compilers.base.type
              | List_seq => unit
@@ -1586,7 +1661,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | bool_rect => false
              | nat_rect => false
              | nat_rect_arrow => false
+             | eager_nat_rect => false
+             | eager_nat_rect_arrow => false
              | list_rect => false
+             | eager_list_rect => false
+             | eager_list_rect_arrow => false
              | list_case => false
              | List_length => false
              | List_seq => true
@@ -1677,7 +1756,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | bool_rect, Compilers.ident.bool_rect T => Datatypes.Some T
              | nat_rect, Compilers.ident.nat_rect P => Datatypes.Some P
              | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Datatypes.Some (P, Q)
+             | eager_nat_rect, Compilers.ident.eager_nat_rect P => Datatypes.Some P
+             | eager_nat_rect_arrow, Compilers.ident.eager_nat_rect_arrow P Q => Datatypes.Some (P, Q)
              | list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P)
+             | eager_list_rect, Compilers.ident.eager_list_rect A P => Datatypes.Some (A, P)
+             | eager_list_rect_arrow, Compilers.ident.eager_list_rect_arrow A P Q => Datatypes.Some (A, P, Q)
              | list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P)
              | List_length, Compilers.ident.List_length T => Datatypes.Some T
              | List_seq, Compilers.ident.List_seq => Datatypes.Some tt
@@ -1764,7 +1847,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | bool_rect, _
              | nat_rect, _
              | nat_rect_arrow, _
+             | eager_nat_rect, _
+             | eager_nat_rect_arrow, _
              | list_rect, _
+             | eager_list_rect, _
+             | eager_list_rect_arrow, _
              | list_case, _
              | List_length, _
              | List_seq, _
@@ -1856,7 +1943,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | bool_rect => fun T => ((type.base ()%etype -> type.base T) -> (type.base ()%etype -> type.base T) -> type.base (Compilers.base.type.type_base base.type.bool) -> type.base T)%ptype
              | nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype
              | nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
+             | eager_nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype
+             | eager_nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
              | list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
+             | eager_list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
+             | eager_list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype
              | list_case => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
              | List_length => fun T => (type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
              | List_seq => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list (Compilers.base.type.type_base base.type.nat)))%ptype
@@ -1947,7 +2038,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | bool_rect => fun T => @Compilers.ident.bool_rect T
              | nat_rect => fun P => @Compilers.ident.nat_rect P
              | nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of nat_rect_arrow arg') with (P, Q) => @Compilers.ident.nat_rect_arrow P Q end
+             | eager_nat_rect => fun P => @Compilers.ident.eager_nat_rect P
+             | eager_nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_nat_rect_arrow arg') with (P, Q) => @Compilers.ident.eager_nat_rect_arrow P Q end
              | list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_rect arg') with (A, P) => @Compilers.ident.list_rect A P end
+             | eager_list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_list_rect arg') with (A, P) => @Compilers.ident.eager_list_rect A P end
+             | eager_list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of eager_list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.eager_list_rect_arrow A P Q end
              | list_case => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_case arg') with (A, P) => @Compilers.ident.list_case A P end
              | List_length => fun T => @Compilers.ident.List_length T
              | List_seq => fun _ => @Compilers.ident.List_seq
@@ -2045,7 +2140,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.bool_rect T => f _ (@Compilers.ident.bool_rect T)
            | Compilers.ident.nat_rect P => f _ (@Compilers.ident.nat_rect P)
            | Compilers.ident.nat_rect_arrow P Q => f _ (@Compilers.ident.nat_rect_arrow P Q)
+           | Compilers.ident.eager_nat_rect P => f _ (@Compilers.ident.eager_nat_rect P)
+           | Compilers.ident.eager_nat_rect_arrow P Q => f _ (@Compilers.ident.eager_nat_rect_arrow P Q)
            | Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P)
+           | Compilers.ident.eager_list_rect A P => f _ (@Compilers.ident.eager_list_rect A P)
+           | Compilers.ident.eager_list_rect_arrow A P Q => f _ (@Compilers.ident.eager_list_rect_arrow A P Q)
            | Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P)
            | Compilers.ident.List_length T => f _ (@Compilers.ident.List_length T)
            | Compilers.ident.List_seq => f _ Compilers.ident.List_seq
@@ -2135,7 +2234,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
       | bool_rect {T : base.type} : ident ((type.base ()%pbtype -> type.base T) -> (type.base ()%pbtype -> type.base T) -> type.base (base.type.type_base base.type.bool) -> type.base T)%ptype
       | nat_rect {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)%ptype
       | nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
+      | eager_nat_rect {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)%ptype
+      | eager_nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
       | list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
+      | eager_list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
+      | eager_list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype
       | list_case {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
       | List_length {T : base.type} : ident (type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat))%ptype
       | List_seq : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list (base.type.type_base base.type.nat)))%ptype
@@ -2225,7 +2328,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @bool_rect T => Raw.ident.bool_rect
            | @nat_rect P => Raw.ident.nat_rect
            | @nat_rect_arrow P Q => Raw.ident.nat_rect_arrow
+           | @eager_nat_rect P => Raw.ident.eager_nat_rect
+           | @eager_nat_rect_arrow P Q => Raw.ident.eager_nat_rect_arrow
            | @list_rect A P => Raw.ident.list_rect
+           | @eager_list_rect A P => Raw.ident.eager_list_rect
+           | @eager_list_rect_arrow A P Q => Raw.ident.eager_list_rect_arrow
            | @list_case A P => Raw.ident.list_case
            | @List_length T => Raw.ident.List_length
            | @List_seq => Raw.ident.List_seq
@@ -2316,7 +2423,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @bool_rect T => []
            | @nat_rect P => []
            | @nat_rect_arrow P Q => []
+           | @eager_nat_rect P => []
+           | @eager_nat_rect_arrow P Q => []
            | @list_rect A P => []
+           | @eager_list_rect A P => []
+           | @eager_list_rect_arrow A P Q => []
            | @list_case A P => []
            | @List_length T => []
            | @List_seq => []
@@ -2407,7 +2518,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @bool_rect T => fun _ => @Compilers.ident.bool_rect _
            | @nat_rect P => fun _ => @Compilers.ident.nat_rect _
            | @nat_rect_arrow P Q => fun _ => @Compilers.ident.nat_rect_arrow _ _
+           | @eager_nat_rect P => fun _ => @Compilers.ident.eager_nat_rect _
+           | @eager_nat_rect_arrow P Q => fun _ => @Compilers.ident.eager_nat_rect_arrow _ _
            | @list_rect A P => fun _ => @Compilers.ident.list_rect _ _
+           | @eager_list_rect A P => fun _ => @Compilers.ident.eager_list_rect _ _
+           | @eager_list_rect_arrow A P Q => fun _ => @Compilers.ident.eager_list_rect_arrow _ _ _
            | @list_case A P => fun _ => @Compilers.ident.list_case _ _
            | @List_length T => fun _ => @Compilers.ident.List_length _
            | @List_seq => fun _ => @Compilers.ident.List_seq
@@ -2502,7 +2617,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @bool_rect T, Compilers.ident.bool_rect T' => Datatypes.Some tt
            | @nat_rect P, Compilers.ident.nat_rect P' => Datatypes.Some tt
            | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Datatypes.Some tt
+           | @eager_nat_rect P, Compilers.ident.eager_nat_rect P' => Datatypes.Some tt
+           | @eager_nat_rect_arrow P Q, Compilers.ident.eager_nat_rect_arrow P' Q' => Datatypes.Some tt
            | @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt
+           | @eager_list_rect A P, Compilers.ident.eager_list_rect A' P' => Datatypes.Some tt
+           | @eager_list_rect_arrow A P Q, Compilers.ident.eager_list_rect_arrow A' P' Q' => Datatypes.Some tt
            | @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt
            | @List_length T, Compilers.ident.List_length T' => Datatypes.Some tt
            | @List_seq, Compilers.ident.List_seq => Datatypes.Some tt
@@ -2589,7 +2708,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @bool_rect _, _
            | @nat_rect _, _
            | @nat_rect_arrow _ _, _
+           | @eager_nat_rect _, _
+           | @eager_nat_rect_arrow _ _, _
            | @list_rect _ _, _
+           | @eager_list_rect _ _, _
+           | @eager_list_rect_arrow _ _ _, _
            | @list_case _ _, _
            | @List_length _, _
            | @List_seq, _
@@ -2681,7 +2804,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.bool_rect T => @bool_rect (base.relax T)
            | Compilers.ident.nat_rect P => @nat_rect (base.relax P)
            | Compilers.ident.nat_rect_arrow P Q => @nat_rect_arrow (base.relax P) (base.relax Q)
+           | Compilers.ident.eager_nat_rect P => @eager_nat_rect (base.relax P)
+           | Compilers.ident.eager_nat_rect_arrow P Q => @eager_nat_rect_arrow (base.relax P) (base.relax Q)
            | Compilers.ident.list_rect A P => @list_rect (base.relax A) (base.relax P)
+           | Compilers.ident.eager_list_rect A P => @eager_list_rect (base.relax A) (base.relax P)
+           | Compilers.ident.eager_list_rect_arrow A P Q => @eager_list_rect_arrow (base.relax A) (base.relax P) (base.relax Q)
            | Compilers.ident.list_case A P => @list_case (base.relax A) (base.relax P)
            | Compilers.ident.List_length T => @List_length (base.relax T)
            | Compilers.ident.List_seq => @List_seq
@@ -2772,7 +2899,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.bool_rect T => tt
            | Compilers.ident.nat_rect P => tt
            | Compilers.ident.nat_rect_arrow P Q => tt
+           | Compilers.ident.eager_nat_rect P => tt
+           | Compilers.ident.eager_nat_rect_arrow P Q => tt
            | Compilers.ident.list_rect A P => tt
+           | Compilers.ident.eager_list_rect A P => tt
+           | Compilers.ident.eager_list_rect_arrow A P Q => tt
            | Compilers.ident.list_case A P => tt
            | Compilers.ident.List_length T => tt
            | Compilers.ident.List_seq => tt
diff --git a/src/Language.v b/src/Language.v
index 52c340d18..695073248 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -877,7 +877,11 @@ Module Compilers.
         | bool_rect {T:base.type} : ident ((unit -> T) -> (unit -> T) -> bool -> T)
         | nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P)
         | nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q)
+        | eager_nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P)
+        | eager_nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q)
         | list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
+        | eager_list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
+        | eager_list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q)
         | list_case {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P) -> list A -> P)
         | List_length {T} : ident (list T -> nat)
         | List_seq : ident (nat -> nat -> list nat)
@@ -1057,8 +1061,16 @@ Module Compilers.
                => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
              | nat_rect_arrow P Q
                => fun O_case S_case => Datatypes.nat_rect _ O_case S_case
+             | eager_nat_rect P
+               => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
+             | eager_nat_rect_arrow P Q
+               => fun O_case S_case => Datatypes.nat_rect _ O_case S_case
              | list_rect A P
                => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
+             | eager_list_rect A P
+               => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
+             | eager_list_rect_arrow A P Q
+               => fun N_case C_case => Datatypes.list_rect _ N_case C_case
              | list_case A P
                => fun N_case C_case => ListUtil.list_case _ (N_case tt) C_case
              | List_length T => @List.length _
@@ -1149,6 +1161,7 @@ Module Compilers.
     Notation LiteralNat := (@Literal base.type.nat).
     Notation LiteralZRange := (@Literal base.type.zrange).
     Definition literal {T} (v : T) := v.
+    Definition eagerly {T} (v : T) := v.
 
     (** TODO: MOVE ME? *)
     Module Thunked.
@@ -1291,6 +1304,25 @@ Module Compilers.
         | @Thunked.nat_rect ?T
           => let rT := base.reify T in
              then_tac (@ident.nat_rect rT)
+        | eagerly (@Datatypes.nat_rect) ?T0 ?P0
+          => lazymatch (eval cbv beta in T0) with
+             | fun _ => _ -> _ => else_tac ()
+             | fun _ => ?T => reify_rec (eagerly (@Thunked.nat_rect) T (fun _ : Datatypes.unit => P0))
+             | T0 => else_tac ()
+             | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T' P0)
+             end
+        | eagerly (@Datatypes.nat_rect) ?T0
+          => lazymatch (eval cbv beta in T0) with
+             | (fun _ => ?P -> ?Q)
+               => let rP := base.reify P in
+                  let rQ := base.reify Q in
+                  then_tac (@ident.eager_nat_rect_arrow rP rQ)
+             | T0 => else_tac ()
+             | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T')
+            end
+        | eagerly (@Thunked.nat_rect) ?T
+          => let rT := base.reify T in
+             then_tac (@ident.eager_nat_rect rT)
         | @Datatypes.list_rect ?A ?T0 ?Pnil
           => lazymatch (eval cbv beta in T0) with
             | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil))
@@ -1301,6 +1333,27 @@ Module Compilers.
           => let rA := base.reify A in
              let rT := base.reify T in
              then_tac (@ident.list_rect rA rT)
+        | eagerly (@Datatypes.list_rect) ?A ?T0 ?Pnil
+          => lazymatch (eval cbv beta in T0) with
+             | fun _ => _ -> _ => else_tac ()
+             | fun _ => ?T => reify_rec (eagerly (@Thunked.list_rect) A T (fun _ : Datatypes.unit => Pnil))
+             | T0 => else_tac ()
+             | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T' Pnil)
+             end
+        | eagerly (@Datatypes.list_rect) ?A ?T0
+          => lazymatch (eval cbv beta in T0) with
+             | (fun _ => ?P -> ?Q)
+               => let rA := base.reify A in
+                  let rP := base.reify P in
+                  let rQ := base.reify Q in
+                  then_tac (@ident.eager_list_rect_arrow rA rP rQ)
+             | T0 => else_tac ()
+             | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T')
+             end
+        | eagerly (@Thunked.list_rect) ?A ?T
+          => let rA := base.reify A in
+             let rT := base.reify T in
+             then_tac (@ident.eager_list_rect rA rT)
         | @ListUtil.list_case ?A ?T0 ?Pnil
           => lazymatch (eval cbv beta in T0) with
             | fun _ => ?T => reify_rec (@Thunked.list_case A T (fun _ : Datatypes.unit => Pnil))
@@ -1398,6 +1451,7 @@ Module Compilers.
           => let rA := base.reify A in
              then_tac (@ident.None rA)
         | ZRange.Build_zrange => then_tac ident.Build_zrange
+        | eagerly (?f ?x) => reify_rec (eagerly f x)
         | fancy.interp ?idc
           => let ridc := (eval cbv [to_fancy] in (to_fancy idc)) in
              then_tac ridc
diff --git a/src/LanguageWf.v b/src/LanguageWf.v
index 1119e1977..d1083e43d 100644
--- a/src/LanguageWf.v
+++ b/src/LanguageWf.v
@@ -221,7 +221,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
       destruct idc; cbn [type.eqv ident.gen_interp type.interp base.interp base.base_interp];
         try solve [ typeclasses eauto
                   | cbv [respectful]; repeat intro; subst; destruct_head_hnf bool; destruct_head_hnf prod; destruct_head_hnf option; destruct_head_hnf zrange; eauto
-                  | cbv [respectful]; repeat intro; (apply nat_rect_Proper_nondep || apply list_rect_Proper || apply list_case_Proper); repeat intro; eauto ].
+                  | cbv [respectful]; repeat intro; (apply nat_rect_Proper_nondep || apply list_rect_Proper || apply list_case_Proper || apply list_rect_arrow_Proper); repeat intro; eauto ].
     Qed.
 
     Global Instance eqv_Reflexive_Proper {t} (idc : ident t) : Proper type.eqv (ident.interp idc) | 1.