Add Z instantiations of InlineConst

6 files changed, 35 insertions, 2 deletions

diff --git a/_CoqProject b/_CoqProject
index 8375be807..30f5a6b33 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -200,6 +200,9 @@ src/Reflection/Z/BinaryNotationConstants.v
 src/Reflection/Z/CNotations.v
 src/Reflection/Z/FoldTypes.v
 src/Reflection/Z/HexNotationConstants.v
+src/Reflection/Z/Inline.v
+src/Reflection/Z/InlineInterp.v
+src/Reflection/Z/InlineWf.v
 src/Reflection/Z/Interpretations128.v
 src/Reflection/Z/Interpretations64.v
 src/Reflection/Z/InterpretationsGen.v
diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v
index 946e84316..74abeef10 100644
--- a/src/Reflection/Inline.v
+++ b/src/Reflection/Inline.v
@@ -1,7 +1,6 @@
 (** * Inline: Remove some [Let] expressions *)
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Util.Tactics.
 
 Local Open Scope ctype_scope.
 Section language.
diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
index caf1931fb..7bee4a70c 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Reflection/InlineInterp.v
@@ -5,7 +5,9 @@ Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.InlineWf.
 Require Import Crypto.Reflection.InterpProofs.
 Require Import Crypto.Reflection.Inline.
-Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SpecializeBy.
 
 
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/Z/Inline.v b/src/Reflection/Z/Inline.v
new file mode 100644
index 000000000..989286232
--- /dev/null
+++ b/src/Reflection/Z/Inline.v
@@ -0,0 +1,7 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Reflection.Z.Syntax.Util.
+
+Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t
+  := @InlineConst base_type op (is_const) t e.
diff --git a/src/Reflection/Z/InlineInterp.v b/src/Reflection/Z/InlineInterp.v
new file mode 100644
index 000000000..132b79f73
--- /dev/null
+++ b/src/Reflection/Z/InlineInterp.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.InlineInterp.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Reflection.Z.Inline.
+
+Definition InterpInlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x
+  := @InterpInlineConst _ _ _ _ _ t e Hwf.
+
+Hint Rewrite @InterpInlineConst using solve [ eassumption | eauto with wf ] : reflective_interp.
diff --git a/src/Reflection/Z/InlineWf.v b/src/Reflection/Z/InlineWf.v
new file mode 100644
index 000000000..5d5eb0617
--- /dev/null
+++ b/src/Reflection/Z/InlineWf.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.InlineWf.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Reflection.Z.Inline.
+
+Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : Wf (InlineConst e)
+  := @Wf_InlineConst _ _ _ t e Hwf.
+
+Hint Resolve Wf_InlineConst : wf.