Add EtaInterp, EtaWf

1 files changed, 63 insertions, 0 deletions

diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v
new file mode 100644
index 000000000..95732ad3d
--- /dev/null
+++ b/src/Reflection/EtaInterp.v
@@ -0,0 +1,63 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Eta.
+Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Section language.
+  Context {base_type_code : Type}
+          {interp_base_type : base_type_code -> Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}.
+
+  Local Notation exprf := (@exprf base_type_code op interp_base_type).
+
+  Local Ltac t_step :=
+    match goal with
+    | _ => reflexivity
+    | _ => progress simpl in *
+    | _ => intro
+    | _ => progress break_match
+    | _ => progress destruct_head prod
+    | _ => progress cbv [LetIn.Let_In]
+    | [ H : _ |- _ ] => rewrite H
+    | _ => progress autorewrite with core
+    | [ H : forall A B x, ?f A B x = x, H' : context[?f _ _ _] |- _ ]
+      => rewrite H in H'
+    | _ => progress unfold interp_flat_type_eta, interp_flat_type_eta', exprf_eta, exprf_eta', expr_eta, expr_eta'
+    end.
+  Local Ltac t := repeat t_step.
+
+  Section gen_flat_type.
+    Context (eta : forall {A B}, A * B -> A * B)
+            (eq_eta : forall A B x, @eta A B x = x).
+    Lemma eq_interp_flat_type_eta_gen {var t T f} x
+      : @interp_flat_type_eta_gen base_type_code var eta t T f x = f x.
+    Proof. induction t; t. Qed.
+
+    (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen.
+
+    Lemma interpf_exprf_eta_gen {t e}
+      : interpf (@interp_op) (exprf_eta_gen eta (t:=t) e) = interpf (@interp_op) e.
+    Proof. induction e; t. Qed.
+  End gen_flat_type.
+  (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen.
+  (* Local *) Hint Rewrite @interpf_exprf_eta_gen.
+
+  Lemma eq_interp_flat_type_eta {var t T f} x
+    : @interp_flat_type_eta base_type_code var t T f x = f x.
+  Proof. t. Qed.
+  (* Local *) Hint Rewrite @eq_interp_flat_type_eta.
+  Lemma eq_interp_flat_type_eta' {var t T f} x
+    : @interp_flat_type_eta' base_type_code var t T f x = f x.
+  Proof. t. Qed.
+  (* Local *) Hint Rewrite @eq_interp_flat_type_eta'.
+  Lemma interpf_exprf_eta {t e}
+    : interpf (@interp_op) (exprf_eta (t:=t) e) = interpf (@interp_op) e.
+  Proof. t. Qed.
+  (* Local *) Hint Rewrite @interpf_exprf_eta.
+  Lemma interpf_exprf_eta' {t e}
+    : interpf (@interp_op) (exprf_eta' (t:=t) e) = interpf (@interp_op) e.
+  Proof. t. Qed.
+  (* Local *) Hint Rewrite @interpf_exprf_eta'.
+End language.