Push back admits in interp lemmas

Also, we now pull bounds out of the initial expression, rather than the
final expression, because it makes the proofs easier.  (It means we only
have to run bounds analysis with one var type, not talk about its
relatedness with multiple var types.)

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m52.60s | Total                                                                | 17m53.17s || -0m00.57s | -0.05%
--------------------------------------------------------------------------------------------------------------------
5m55.17s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.71s  || -0m00.53s | -0.15%
4m33.38s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.93s  || -0m00.55s | -0.20%
1m36.04s  | Experiments/NewPipeline/Toplevel2                                    | 1m35.94s  || +0m00.09s | +0.10%
0m38.56s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m38.44s  || +0m00.12s | +0.31%
0m38.50s  | p521_32.c                                                            | 0m38.63s  || -0m00.13s | -0.33%
0m37.71s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.22s  || +0m00.49s | +1.31%
0m35.06s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.71s  || +0m00.35s | +1.00%
0m31.97s  | p521_64.c                                                            | 0m32.06s  || -0m00.09s | -0.28%
0m23.81s  | p384_32.c                                                            | 0m23.59s  || +0m00.21s | +0.93%
0m20.73s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.94s  || -0m00.21s | -1.00%
0m18.80s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.85s  || -0m00.05s | -0.26%
0m13.79s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m14.00s  || -0m00.21s | -1.50%
0m12.56s  | Experiments/NewPipeline/CStringification                             | 0m12.59s  || -0m00.02s | -0.23%
0m10.52s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.49s  || +0m00.02s | +0.28%
0m08.64s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.49s  || +0m00.15s | +1.76%
0m08.45s  | p384_64.c                                                            | 0m08.51s  || -0m00.06s | -0.70%
0m05.48s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.50s  || -0m00.01s | -0.36%
0m05.36s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.55s  || -0m00.18s | -3.42%
0m04.06s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.10s  || -0m00.04s | -0.97%
0m03.92s  | secp256k1_32.c                                                       | 0m03.78s  || +0m00.14s | +3.70%
0m03.84s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.81s  || +0m00.02s | +0.78%
0m03.76s  | p256_32.c                                                            | 0m03.87s  || -0m00.11s | -2.84%
0m03.29s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.25s  || +0m00.04s | +1.23%
0m03.09s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m03.11s  || -0m00.02s | -0.64%
0m02.22s  | p224_32.c                                                            | 0m02.24s  || -0m00.02s | -0.89%
0m02.03s  | curve25519_32.c                                                      | 0m02.05s  || -0m00.02s | -0.97%
0m01.54s  | p224_64.c                                                            | 0m01.54s  || +0m00.00s | +0.00%
0m01.53s  | p256_64.c                                                            | 0m01.55s  || -0m00.02s | -1.29%
0m01.52s  | secp256k1_64.c                                                       | 0m01.51s  || +0m00.01s | +0.66%
0m01.38s  | curve25519_64.c                                                      | 0m01.39s  || -0m00.01s | -0.71%
0m01.31s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.22s  || +0m00.09s | +7.37%
0m01.27s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.27s  || +0m00.00s | +0.00%
0m01.26s  | Experiments/NewPipeline/CLI                                          | 0m01.25s  || +0m00.01s | +0.80%
0m01.04s  | Experiments/NewPipeline/CompilersTestCases                           | 0m00.97s  || +0m00.07s | +7.21%
0m01.02s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.12s  || -0m00.10s | -8.92%

2 files changed, 116 insertions, 47 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 4d9673eb1..10590c02b 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -1058,18 +1058,6 @@ Module Compilers.
     : Expr t
     := partial.EtaExpandWithListInfoFromBound (GeneralizeVar.GeneralizeVar (e _)) bound.
 
-  Definition CheckPartialEvaluateWithBounds
-             {A}
-             (relax_zrange : zrange -> option zrange)
-             {t} (E : Expr t)
-             (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
-             (b_out : ZRange.type.base.option.interp (type.final_codomain t))
-    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + A)
-    := let b_computed := partial.Extract E b_in in
-       if ZRange.type.base.option.is_tighter_than b_computed b_out
-       then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E)
-       else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)).
-
   Definition CheckedPartialEvaluateWithBounds
              (relax_zrange : zrange -> option zrange)
              {t} (E : Expr t)
@@ -1078,11 +1066,12 @@ Module Compilers.
     : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + list { t : _ & ident t })
     := dlet_nd e := GeneralizeVar.ToFlat E in
        let E := GeneralizeVar.FromFlat e in
+       let b_computed := partial.Extract E b_in in
        match CheckCasts.GetUnsupportedCasts E with
        | nil => (let E := PartialEvaluateWithBounds E b_in in
-                 dlet_nd e := GeneralizeVar.ToFlat E in
-                 let E := GeneralizeVar.FromFlat e in
-                 CheckPartialEvaluateWithBounds relax_zrange E b_in b_out)
+                if ZRange.type.base.option.is_tighter_than b_computed b_out
+                then @inl (Expr t) _ (RelaxZRange.expr.Relax relax_zrange E)
+                else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)))
        | unsupported_casts => inr (inr unsupported_casts)
        end.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index a54b21dd8..341448363 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -72,21 +72,25 @@ Module Compilers.
               (bottom' : forall A, abstract_domain' A)
               (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v)
               (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
-              (interp_ident : forall t, ident t -> type.interp base_interp t)
-              (interp_ident_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (interp_ident t idc)).
+              (ident_interp_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (ident_interp t idc)).
       Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
       Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop
         := type.related_hetero (@abstraction_relation').
       Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')).
       Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')).
       Local Notation var := (type.interp base_interp).
-      Local Notation expr := (@expr.expr base_type ident var).
-      Local Notation UnderLets := (@UnderLets base_type ident var).
+      Local Notation expr := (@expr.expr base_type ident).
+      Local Notation UnderLets := (@UnderLets base_type ident).
       Local Notation value := (@value base_type ident var abstract_domain').
       Local Notation value_with_lets := (@value_with_lets base_type ident var abstract_domain').
       Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain').
-      Context (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> expr t -> UnderLets (expr t)).
+      Context (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> @expr var t -> @UnderLets var (@expr var t))
+              (interp_ident : forall t, ident t -> value_with_lets t)
+              (ident_extract : forall t, ident t -> abstract_domain t).
       Local Notation eta_expand_with_bound' := (@eta_expand_with_bound' base_type ident _ abstract_domain' annotate bottom').
+      Local Notation eval_with_bound' := (@partial.eval_with_bound' base_type ident _ abstract_domain' annotate bottom' interp_ident).
+      Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract).
+      Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract).
       (*
       Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom').
       Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom').
@@ -211,7 +215,7 @@ Module Compilers.
 
       Section extract.
         Context (ident_extract : forall t, ident t -> abstract_domain t)
-                {ident_extract_Proper : forall {t}, Proper (eq ==> abstract_domain_R) (ident_extract t)}.
+        {ident_extract_Proper : forall {t}, Proper (eq ==> abstract_domain_R) (ident_extract t)}.
 
         Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract).
         Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract).
@@ -233,6 +237,25 @@ Module Compilers.
         Qed.
       End extract.
  *)
+      Lemma interp_eval_with_bound'
+            {t} (e_st e1 e2 : expr t)
+            (Hwf : expr.wf3 nil e_st e1 e2)
+            (st : type.for_each_lhs_of_arrow abstract_domain t)
+        : (forall arg1 arg2
+                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                  (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
+              type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1
+              = type.app_curried (expr.interp ident_interp e2) arg2)
+          /\ (forall arg1
+                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
+                 abstraction_relation'
+                   _
+                   (extract_gen e_st st)
+                   (type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1)).
+      Proof using Type.
+        cbv [extract_gen extract'].
+        cbv [eval_with_bound'].
+      Admitted.
 
       Lemma interp_eta_expand_with_bound'
             {t} (e1 e2 : expr t)
@@ -247,6 +270,7 @@ Module Compilers.
       Admitted.
 
 
+
   (*
       Definition eval_with_bound' {t} (e : @expr value_with_lets t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)
@@ -276,6 +300,7 @@ Module Compilers.
                 (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
                 (is_annotation : forall t, ident t -> bool).
         Context (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop).
+        Context (cast_outside_of_range : zrange -> Z -> Z).
         Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation').
         (*Context {annotate_ident_Proper : forall t, Proper (abstract_domain'_R t ==> eq) (annotate_ident t)}
                 {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}
@@ -284,7 +309,26 @@ Module Compilers.
                 (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2))
                 (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2).
          *)
+        Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
         Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+        Local Notation extract := (@ident.extract abstract_domain' abstract_interp_ident).
+
+        Lemma interp_eval_with_bound
+              {t} (e_st e1 e2 : expr t)
+              (Hwf : expr.wf3 nil e_st e1 e2)
+              (st : type.for_each_lhs_of_arrow abstract_domain t)
+          : (forall arg1 arg2
+                    (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                    (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
+                type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1
+                = type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e2) arg2)
+            /\ (forall arg1
+                       (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
+                   abstraction_relation'
+                     _
+                     (extract e_st st)
+                     (type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1)).
+        Proof using Type. cbv [extract eval_with_bound]; apply interp_eval_with_bound'; assumption. Qed.
 
         Lemma interp_eta_expand_with_bound
               {t} (e1 e2 : expr t)
@@ -297,17 +341,10 @@ Module Compilers.
         Proof. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto. Qed.
 
 (*
-        Definition eval_with_bound {t} (e : @expr value_with_lets t)
-                   (st : type.for_each_lhs_of_arrow abstract_domain t)
-          : @expr var t
-          := @eval_with_bound' base.type ident var abstract_domain' annotate bottom' (@interp_ident) t e st.
-
         Definition eval {t} (e : @expr value_with_lets t) : @expr var t
           := @eval' base.type ident var abstract_domain' annotate bottom' (@interp_ident) t e.
 
 
-        Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-          := @extract_gen base.type ident abstract_domain' abstract_interp_ident t e bound.
 *)
         (*
         Section extract.
@@ -403,23 +440,39 @@ Module Compilers.
           = partial.Extract e b_in.
       Proof. apply Extract_FromFlat_ToFlat'; assumption. Qed.
 
-      (*Lemma interp_eval
-            Definition eval {var} {t} (e : @expr _ t) : expr t
+      (*    Definition eval {var} {t} (e : @expr _ t) : expr t
         := (@partial.ident.eval)
              var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation t e.
-      Definition eval_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
-        := (@partial.ident.eval_with_bound)
-             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation t e bound.
       Definition Eval {t} (e : Expr t) : Expr t
         := fun var => eval (e _).
-      Definition EvalWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
-        := fun var => eval_with_bound (e _) bound.
-      Definition extract {t} (e : expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-        := @partial.ident.extract abstract_domain' abstract_interp_ident t e bound.
       Definition Extract {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
         := @partial.ident.extract abstract_domain' abstract_interp_ident t (e _) bound.
        *)
 
+
+      Lemma interp_eval_with_bound
+            cast_outside_of_range
+            {t} (e_st e1 e2 : expr t)
+            (Hwf : expr.wf3 nil e_st e1 e2)
+            (st : type.for_each_lhs_of_arrow abstract_domain t)
+        : (forall arg1 arg2
+                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                  (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
+              type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1
+              = type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e2) arg2)
+          /\ (forall arg1
+                  (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
+                 abstraction_relation'
+                   (extract e_st st)
+                   (type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1)).
+      Proof using Type.
+        cbv [eval_with_bound]; split;
+          [ intros arg1 arg2 Harg12 Harg1
+          | intros arg1 Harg1 ].
+        all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ].
+        all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation'); eauto.
+      Qed.
+
       Lemma interp_eta_expand_with_bound
             {t} (e1 e2 : expr t)
             (Hwf : expr.wf nil e1 e2)
@@ -435,6 +488,23 @@ Module Compilers.
         { apply ZRange.type.option.is_bounded_by_impl_related_hetero. }
       Qed.
 
+      Lemma Interp_EvalWithBound
+            cast_outside_of_range
+            {t} (e : Expr t)
+            (Hwf : expr.Wf3 e)
+            (st : type.for_each_lhs_of_arrow abstract_domain t)
+        : (forall arg1 arg2
+                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                  (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
+              type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (EvalWithBound e st)) arg1
+              = type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) e) arg2)
+          /\ (forall arg1
+                     (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
+                 abstraction_relation'
+                   (Extract e st)
+                   (type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (EvalWithBound e st)) arg1)).
+      Proof using Type. cbv [Extract EvalWithBound]; apply interp_eval_with_bound, Hwf. Qed.
+
       Lemma Interp_EtaExpandWithBound
             {t} (E : Expr t)
             (Hwf : Wf E)
@@ -606,9 +676,6 @@ Module Compilers.
   End RelaxZRange.
   Hint Resolve RelaxZRange.expr.Wf_Relax : wf.
 
-  Axiom admit_pf : False.
-  Local Notation admit := (match admit_pf with end).
-
   Lemma Interp_PartialEvaluateWithBounds
         cast_outside_of_range
         {t} (E : Expr t)
@@ -621,21 +688,33 @@ Module Compilers.
       = type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) E) arg2.
   Proof.
     cbv [PartialEvaluateWithBounds].
-  Admitted.
+    intros arg1 arg2 Harg12 Harg1.
+    assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1)
+      by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]).
+    assert (arg2_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg2)
+      by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]).
+    rewrite <- (@GeneralizeVar.Interp_gen1_GeneralizeVar _ _ _ _ _ E) by auto with wf.
+    eapply Interp_EvalWithBound; eauto with wf.
+  Qed.
 
   Lemma Interp_PartialEvaluateWithBounds_bounded
         cast_outside_of_range
         {t} (E : Expr t)
         (Hwf : Wf E)
         (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+        {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R _ _ (fun _ => eq))) b_in}
     : forall arg1
         (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       ZRange.type.base.option.is_bounded_by
-        (partial.Extract (PartialEvaluateWithBounds E b_in) b_in)
+        (partial.Extract E b_in)
         (type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1)
       = true.
   Proof.
-  Admitted.
+    cbv [PartialEvaluateWithBounds].
+    intros arg1 Harg1.
+    rewrite <- Extract_FromFlat_ToFlat by auto with wf.
+    eapply Interp_EvalWithBound; eauto with wf.
+  Qed.
 
   Lemma Interp_PartialEvaluateWithListInfoFromBounds
         {t} (E : Expr t)
@@ -674,7 +753,7 @@ Module Compilers.
                                            = type.app_curried (Interp E) arg2)
       /\ Wf rv.
   Proof.
-    cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *;
+    cbv [CheckedPartialEvaluateWithBounds Let_In] in *;
       break_innermost_match_hyps; inversion_sum; subst.
     let H := lazymatch goal with H : _ = nil |- _ => H end in
     pose proof (@Interp_WithoutUnsupportedCasts _ _ H ltac:(solve [ auto with wf ])) as H'; clear H;
@@ -690,13 +769,14 @@ Module Compilers.
         by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]).
       split.
       all: repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances
+                        | rewrite <- Extract_FromFlat_ToFlat by auto; apply Interp_PartialEvaluateWithBounds_bounded; auto
                         | rewrite Extract_FromFlat_ToFlat by auto with wf
-                        | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]
-                        | apply Interp_PartialEvaluateWithBounds_bounded; auto
+                        | progress intros
                         | progress cbv [ident.interp]
                         | rewrite RelaxZRange.expr.Interp_Relax; eauto
-                        | erewrite !Interp_PartialEvaluateWithBounds
+                        | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]
                         | solve [ eauto with wf ]
+                        | erewrite !Interp_PartialEvaluateWithBounds
                         | apply type.app_curried_Proper
                         | apply expr.Wf_Interp_Proper_gen
                         | progress intros ]. }