1 files changed, 29 insertions, 0 deletions
diff --git a/src/Compilers/Z/CommonSubexpressionEliminationWf.v b/src/Compilers/Z/CommonSubexpressionEliminationWf.v
new file mode 100644
index 000000000..4f46f9454
--- /dev/null
+++ b/src/Compilers/Z/CommonSubexpressionEliminationWf.v
@@ -0,0 +1,29 @@
+(** * Common Subexpression Elimination for PHOAS Syntax *)
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.CommonSubexpressionEliminationWf.
+Require Import Crypto.Compilers.Z.CommonSubexpressionElimination.
+
+Lemma Wf_CSE_gen t (e : Expr _ _ t)
+      prefix
+      (Hlen : forall var1 var2, length (prefix var1) = length (prefix var2))
+      (Hprefix : forall var1 var2 n t1 t2 e1 e2,
+          List.nth_error (prefix var1) n = Some (existT _ t1 e1)
+          -> List.nth_error (prefix var2) n = Some (existT _ t2 e2)
+          -> exists pf : t1 = t2, wff nil (eq_rect _ (@exprf _ _ _) e1 _ pf) e2)
+      (Hwf : Wf e)
+  : Wf (@CSE_gen t e prefix).
+Proof.
+  apply Wf_CSE; auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb.
+Qed.
+
+Lemma Wf_CSE t (e : Expr _ _ t)
+      (Hwf : Wf e)
+  : Wf (@CSE t e).
+Proof.
+  apply Wf_CSE_gen; simpl; auto.
+  { destruct n; simpl; try congruence. }
+Qed.
+
+Hint Resolve Wf_CSE : wf.