Split off lemmas about [InlineConst]

1 files changed, 41 insertions, 1 deletions

diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index 2d4ad5e0f..eb3e617e5 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -1,5 +1,6 @@
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Reflection.WfProofs.
+Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
 
 Local Open Scope ctype_scope.
 Section language.
@@ -26,4 +27,43 @@ Section language.
              | _ => rewrite <- surjective_pairing
              end.
   Qed.
+
+  Lemma interpf_SmartConst {t t'} v x x'
+        (Hin : List.In
+                 (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
+                         t (x, x'))
+                 (flatten_binding_list (t := t') base_type_code (SmartConst v) v))
+    : interpf interp_op x = x'.
+  Proof.
+    clear -Hin.
+    induction t'; simpl in *.
+    { intuition (inversion_sigma; inversion_prod; subst; eauto). }
+    { apply List.in_app_iff in Hin.
+      intuition (inversion_sigma; inversion_prod; subst; eauto). }
+  Qed.
+
+  Lemma interpf_SmartVarVar {t t'} v x x'
+        (Hin : List.In
+                 (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
+                         t (x, x'))
+                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v) v))
+    : interpf interp_op x = x'.
+  Proof.
+    clear -Hin.
+    induction t'; simpl in *.
+    { intuition (inversion_sigma; inversion_prod; subst; eauto). }
+    { apply List.in_app_iff in Hin.
+      intuition (inversion_sigma; inversion_prod; subst; eauto). }
+  Qed.
+
+  Lemma interpf_SmartVarVar_eq {t t'} v v' x x'
+        (Heq : v = v')
+        (Hin : List.In
+                 (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
+                         t (x, x'))
+                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v))
+    : interpf interp_op x = x'.
+  Proof.
+    eapply interpf_SmartVarVar; subst; eassumption.
+  Qed.
 End language.