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, 8 insertions, 14 deletions

diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v
index 54240947a..52e816df5 100644
--- a/src/Reflection/EtaInterp.v
+++ b/src/Reflection/EtaInterp.v
@@ -1,6 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -42,11 +41,9 @@ Section language.
       Context (exprf_eta : forall {t} (e : exprf t), exprf t)
               (eq_interp_exprf_eta : forall t e, interpf (@interp_op) (@exprf_eta t e) = interpf (@interp_op) e).
       Lemma interp_expr_eta_gen {t e}
-        : interp_type_gen_rel_pointwise
-            (fun _ => eq)
-            (interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e))
-            (interp (@interp_op) e).
-      Proof. t. Admitted.
+        : forall x,
+          interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e) x = interp (@interp_op) e x.
+      Proof. t. Qed.
     End gen_type.
     (* Local *) Hint Rewrite @interp_expr_eta_gen.
 
@@ -55,10 +52,7 @@ Section language.
     Proof. induction e; t. Qed.
 
     Lemma InterpExprEtaGen {t e}
-      : interp_type_gen_rel_pointwise
-          (fun _ => eq)
-          (Interp (@interp_op) (ExprEtaGen eta (t:=t) e))
-          (Interp (@interp_op) e).
+      : forall x, Interp (@interp_op) (ExprEtaGen eta (t:=t) e) x = Interp (@interp_op) e x.
     Proof. apply interp_expr_eta_gen; intros; apply interpf_exprf_eta_gen. Qed.
   End gen_flat_type.
   (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen.
@@ -82,15 +76,15 @@ Section language.
   Proof. t. Qed.
   (* Local *) Hint Rewrite @interpf_exprf_eta'.
   Lemma interp_expr_eta {t e}
-    : interp_type_gen_rel_pointwise (fun _ => eq) (interp (@interp_op) (expr_eta (t:=t) e)) (interp (@interp_op) e).
+    : forall x, interp (@interp_op) (expr_eta (t:=t) e) x = interp (@interp_op) e x.
   Proof. t. Qed.
   Lemma interp_expr_eta' {t e}
-    : interp_type_gen_rel_pointwise (fun _ => eq) (interp (@interp_op) (expr_eta' (t:=t) e)) (interp (@interp_op) e).
+    : forall x, interp (@interp_op) (expr_eta' (t:=t) e) x = interp (@interp_op) e x.
   Proof. t. Qed.
   Lemma InterpExprEta {t e}
-    : interp_type_gen_rel_pointwise (fun _ => eq) (Interp (@interp_op) (ExprEta (t:=t) e)) (Interp (@interp_op) e).
+    : forall x, Interp (@interp_op) (ExprEta (t:=t) e) x = Interp (@interp_op) e x.
   Proof. apply interp_expr_eta. Qed.
   Lemma InterpExprEta' {t e}
-    : interp_type_gen_rel_pointwise (fun _ => eq) (Interp (@interp_op) (ExprEta' (t:=t) e)) (Interp (@interp_op) e).
+    : forall x, Interp (@interp_op) (ExprEta' (t:=t) e) x = Interp (@interp_op) e x.
   Proof. apply interp_expr_eta'. Qed.
 End language.