From 625b72507670750ba2545977ba49283c1431a8c3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 12 Dec 2018 13:51:36 -0500 Subject: Add projT1_app_with_unification_resultT --- src/Experiments/NewPipeline/RewriterWf1.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 5f999e82d..7e3b23011 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -1308,6 +1308,36 @@ Module Compilers. | progress cps_id'_with_option app_transport_with_unification_resultT'_cps_id ]. Qed. + Local Notation mk_new_evm0 evm ls + := (fold_right + (fun i k evm' + => k match PositiveMap.find i evm with + | Some v => PositiveMap.add i v evm' + | None => evm' + end) (fun evm' => evm') + (List.rev ls)) (only parsing). + + Local Notation mk_new_evm evm ps + := (mk_new_evm0 + evm + (PositiveSet.elements ps)) (only parsing). + + + Lemma projT1_app_with_unification_resultT {t p K f v res} + : @app_with_unification_resultT_cps var t p K f v _ (@Some _) = Some res + -> projT1 res = mk_new_evm (projT1 v) (pattern.collect_vars p) (PositiveMap.empty _). + Proof using Type. + cbv [app_with_unification_resultT_cps]. + repeat first [ progress inversion_option + | progress subst + | progress cbn [projT1] in * + | progress intros + | reflexivity + | progress cbv [Option.bind] in * + | progress cps_id'_with_option app_transport_with_unification_resultT'_cps_id + | break_match_hyps_step ltac:(fun _ => idtac) ]. + Qed. + Lemma reveal_rawexpr_cps_gen_id assume_known e T k : @reveal_rawexpr_cps_gen ident var assume_known e T k = k (reveal_rawexpr_gen assume_known e). Proof. -- cgit v1.2.3