From d3674cace598d673d60f7ed0c18be4a6434d4b44 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Dec 2018 16:13:22 -0500 Subject: Add value_of_rawexpr_interp_related --- src/Experiments/NewPipeline/RewriterWf1.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Experiments') 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 -- cgit v1.2.3