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, 0 insertions, 104 deletions

diff --git a/src/Reflection/ApplicationLemmas.v b/src/Reflection/ApplicationLemmas.v
deleted file mode 100644
index e8105c2f0..000000000
--- a/src/Reflection/ApplicationLemmas.v
+++ /dev/null
@@ -1,104 +0,0 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Application.
-
-Section language.
-  Context {base_type : Type}
-          {interp_base_type : base_type -> Type}
-          {op : flat_type base_type -> flat_type base_type -> Type}
-          {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}.
-
-  Lemma interp_apply' {n t}
-        (x : @expr base_type op _ t)
-        (args : binders_for' n t interp_base_type)
-    : interp interp_op (Apply' n x args) = ApplyInterped' n (interp interp_op x) args.
-  Proof.
-    generalize dependent t; induction n as [|n IHn]; intros.
-    { destruct x; reflexivity. }
-    { destruct x as [|?? x]; simpl; [ reflexivity | ].
-      apply IHn. }
-  Qed.
-
-  Lemma interp_apply {n t}
-        (x : @expr base_type op _ t)
-        (args : binders_for n t interp_base_type)
-    : interp interp_op (Apply n x args) = ApplyInterped (interp interp_op x) args.
-  Proof.
-    destruct n; [ reflexivity | ].
-    apply interp_apply'.
-  Qed.
-
-  Lemma fst_interp_all_binders_for_of' {A B}
-        (args : interp_all_binders_for' (Arrow A B) interp_base_type)
-    : fst_binder (interp_all_binders_for_of' args) = fst args.
-  Proof.
-    destruct B; reflexivity.
-  Qed.
-
-  Lemma snd_interp_all_binders_for_of' {A B}
-        (args : interp_all_binders_for' (Arrow A B) interp_base_type)
-    : snd_binder (interp_all_binders_for_of' args) = interp_all_binders_for_of' (snd args).
-  Proof.
-    destruct B.
-    { destruct args as [? []]; reflexivity. }
-    { destruct args; reflexivity. }
-  Qed.
-
-  Lemma fst_interp_all_binders_for_to' {A B}
-        (args : interp_all_binders_for (Arrow A B) interp_base_type)
-    : fst (interp_all_binders_for_to' args) = fst_binder args.
-  Proof.
-    destruct B; reflexivity.
-  Qed.
-
-  Lemma snd_interp_all_binders_for_to' {A B}
-        (args : interp_all_binders_for (Arrow A B) interp_base_type)
-    : snd (interp_all_binders_for_to' args) = interp_all_binders_for_to' (snd_binder args).
-  Proof.
-    destruct B; reflexivity.
-  Qed.
-
-  Lemma interp_all_binders_for_to'_of' {t} (args : interp_all_binders_for' t interp_base_type)
-    : interp_all_binders_for_to' (interp_all_binders_for_of' args) = args.
-  Proof.
-    induction t; destruct args; [ reflexivity | ].
-    apply injective_projections;
-      [ rewrite fst_interp_all_binders_for_to', fst_interp_all_binders_for_of'; reflexivity
-      | rewrite snd_interp_all_binders_for_to', snd_interp_all_binders_for_of', IHt; reflexivity ].
-  Qed.
-
-  Lemma interp_all_binders_for_of'_to' {t} (args : interp_all_binders_for t interp_base_type)
-    : interp_all_binders_for_of' (interp_all_binders_for_to' args) = args.
-  Proof.
-    induction t as [|A B IHt].
-    { destruct args; reflexivity. }
-    { destruct B; [ reflexivity | ].
-      destruct args; simpl; rewrite IHt; reflexivity. }
-  Qed.
-
-  Lemma interp_apply_all' {t}
-        (x : @expr base_type op _ t)
-        (args : interp_all_binders_for' t interp_base_type)
-    : interp interp_op (ApplyAll x (interp_all_binders_for_of' args)) = ApplyInterpedAll' (interp interp_op x) args.
-  Proof.
-    induction x as [|?? x IHx]; [ reflexivity | ].
-    simpl; rewrite <- IHx; destruct args.
-    rewrite snd_interp_all_binders_for_of', fst_interp_all_binders_for_of'; reflexivity.
-  Qed.
-
-  Lemma interp_apply_all {t}
-        (x : @expr base_type op _ t)
-        (args : interp_all_binders_for t interp_base_type)
-    : interp interp_op (ApplyAll x args) = ApplyInterpedAll (interp interp_op x) args.
-  Proof.
-    unfold ApplyInterpedAll.
-    rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity.
-  Qed.
-
-  Lemma interp_apply_all_to' {t}
-         (x : @expr base_type op _ t)
-         (args : interp_all_binders_for t interp_base_type)
-    : interp interp_op (ApplyAll x args) = ApplyInterpedAll' (interp interp_op x) (interp_all_binders_for_to' args).
-   Proof.
-    rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity.
-   Qed.
-End language.