1 files changed, 40 insertions, 0 deletions
diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v
new file mode 100644
index 000000000..b44811b06
--- /dev/null
+++ b/src/Compilers/Named/WfInterp.v
@@ -0,0 +1,40 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Section language.
+  Context {base_type_code Name interp_base_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}
+          {Context : @Context base_type_code Name interp_base_type}.
+
+  Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t}
+        (Hwf : prop_of_option (wff ctx e))
+    : @interpf base_type_code interp_base_type op Name Context interp_op ctx t e <> None.
+  Proof using Type.
+    revert dependent ctx; induction e;
+      repeat first [ progress intros
+                   | progress simpl in *
+                   | progress unfold option_map, LetIn.Let_In in *
+                   | congruence
+                   | progress specialize_by_assumption
+                   | progress destruct_head' and
+                   | progress break_innermost_match_step
+                   | progress break_match_hyps
+                   | progress autorewrite with push_prop_of_option in *
+                   | progress specialize_by auto
+                   | solve [ intuition eauto ] ].
+  Qed.
+
+  Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t}
+        (Hwf : wf ctx e)
+        v
+    : @interp base_type_code interp_base_type op Name Context interp_op ctx t e v <> None.
+  Proof using Type.
+    destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto.
+  Qed.
+End language.