Switch to fully uncurried form for reflection

This will eventually make a number of proofs easier.

Unfortunately, the correctness lemmas for AddCoordinates and LadderStep
no longer work (because of different arities), and there's a proof in
Experiments/Ed25519 that I've admitted.

The correctness lemmas will be easy to re-add when we have a more
general version that handle arbitrary type shapes.

1 files changed, 10 insertions, 10 deletions

diff --git a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
index c0c390d0b..bf8795d45 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
@@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
 Local Opaque Interp.
@@ -18,8 +17,8 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW)
-                                    (LiftOption.to' (Some args)))
+                  (Interp (@BoundedWordW.interp_op) ropW
+                          (LiftOption.to' (Some args)))
           with
           | Some _ => True
           | None => False
@@ -33,18 +32,19 @@ Lemma ExprBinOp_correct_and_bounded
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
           let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x')))
+                  (Interp (@ZBounds.interp_op) ropW (LiftOption.to' (Some x')))
           with
           | Some bounds => binop_bounds_good bounds = true
           | None => False
           end)
   : binop_correct_and_bounded ropW op.
 Proof.
-  intros x y Hx Hy.
-  pose x as x'; pose y as y'.
-  hnf in x, y; destruct_head' prod.
-  specialize (H0 (x', y') (conj Hx Hy)).
-  specialize (H1 (x', y') (conj Hx Hy)).
-  let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in
+  intros xy HxHy.
+  pose xy as xy'.
+  compute in xy; destruct_head' prod.
+  specialize (H0 xy' HxHy).
+  specialize (H1 xy' HxHy).
+  destruct HxHy as [Hx Hy].
+  let args := constr:(binop_args_to_bounded xy' Hx Hy) in
   t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
 Qed.