diff options
Diffstat (limited to 'src/Compilers/Z/CommonSubexpressionEliminationInterp.v')
| -rw-r--r-- | src/Compilers/Z/CommonSubexpressionEliminationInterp.v | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v deleted file mode 100644 index 7e7f7910a..000000000 --- a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v +++ /dev/null @@ -1,23 +0,0 @@ -(** * Common Subexpression Elimination for PHOAS Syntax *) -Require Import Coq.Lists.List. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.CommonSubexpressionEliminationInterp. -Require Import Crypto.Compilers.Z.CommonSubexpressionElimination. - -Lemma InterpCSE_gen inline_symbolic_expr_in_lookup t (e : Expr t) prefix - (Hwf : Wf e) - : forall x, Interp (@CSE_gen inline_symbolic_expr_in_lookup t e prefix) x = Interp e x. -Proof. - apply InterpCSE; - auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb, denote_symbolic_op. -Qed. - -Lemma InterpCSE inline_symbolic_expr_in_lookup t (e : Expr t) (Hwf : Wf e) - : forall x, Interp (@CSE inline_symbolic_expr_in_lookup t e) x = Interp e x. -Proof. - apply InterpCSE_gen; auto. -Qed. - -Hint Rewrite @InterpCSE using solve_wf_side_condition : reflective_interp. |