Add lemma about wff and interpf of Named

2 files changed, 42 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 6602f9b54..4a5583bba 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -162,6 +162,7 @@ src/Reflection/Named/RegisterAssign.v
 src/Reflection/Named/SmartMap.v
 src/Reflection/Named/Syntax.v
 src/Reflection/Named/Wf.v
+src/Reflection/Named/WfInterp.v
 src/Reflection/Z/BinaryNotationConstants.v
 src/Reflection/Z/BoundsInterpretations.v
 src/Reflection/Z/CNotations.v
diff --git a/src/Reflection/Named/WfInterp.v b/src/Reflection/Named/WfInterp.v
new file mode 100644
index 000000000..b8cfb7fbe
--- /dev/null
+++ b/src/Reflection/Named/WfInterp.v
@@ -0,0 +1,41 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.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}
+          {ContextOk : ContextOk Context}.
+
+  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.
+    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.
+    destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto.
+  Qed.
+End language.