Add value_of_rawexpr_interp_related

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 6527e7a47..a1244dd74 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -2049,6 +2049,23 @@ Module Compilers.
                               | apply reify_interp_related ].
           Qed.
 
+          Lemma value_of_rawexpr_interp_related {e v}
+            : rawexpr_interp_related e v -> value_interp_related (value_of_rawexpr e) v.
+          Proof using Type.
+            destruct e; cbn [rawexpr_interp_related value_of_rawexpr]; break_innermost_match.
+            all: repeat first [ progress intros
+                              | exfalso; assumption
+                              | progress inversion_sigma
+                              | progress subst
+                              | progress cbn [eq_rect expr.interp type_of_rawexpr] in *
+                              | progress destruct_head'_ex
+                              | progress destruct_head'_and
+                              | assumption
+                              | apply reflect_interp_related
+                              | progress cbn [expr_interp_related]
+                              | solve [ eauto ] ].
+          Qed.
+
           Fixpoint pattern_default_interp' {K t} (p : pattern t) evm {struct p} : (var (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' var t p evm K
             := match p in pattern.pattern t return (var (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' var t p evm K with
                | pattern.Wildcard t => fun k v => k v