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, 3 insertions, 12 deletions

diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v
index 50d05d032..b3b83698e 100644
--- a/src/Reflection/InterpWf.v
+++ b/src/Reflection/InterpWf.v
@@ -69,19 +69,10 @@ Section language.
 
     Lemma interp_wf
              {t} {e1 e2 : expr t}
-             {G}
-             (HG : forall t x x',
-                 List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) G
-                 -> x = x')
-             (Rwf : wf G e1 e2)
-    : interp_type_gen_rel_pointwise (fun _ => eq) (interp e1) (interp e2).
+             (Rwf : wf e1 e2)
+    : forall x, interp e1 x = interp e2 x.
     Proof.
-      induction Rwf; simpl; repeat intro; simpl in *; subst; eauto.
-      match goal with
-      | [ H : _ |- _ ]
-        => apply H; intros; progress destruct_head' or; [ | solve [ eauto ] ]
-      end.
-      inversion_sigma; inversion_prod; repeat subst; simpl; auto.
+      destruct Rwf; simpl; eauto.
     Qed.
   End wf.
 End language.