blob: 93d422b2dbda2c0d471866ad20c1efa19161aa3b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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 inline_symbolic_expr_in_lookup 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 inline_symbolic_expr_in_lookup 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 inline_symbolic_expr_in_lookup t (e : Expr t)
(Hwf : Wf e)
: Wf (@CSE inline_symbolic_expr_in_lookup t e).
Proof.
apply Wf_CSE_gen; simpl; auto.
{ destruct n; simpl; try congruence. }
Qed.
Hint Resolve Wf_CSE : wf.
|
