diff options
-rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index ef0bdbbe2..2dd3decc4 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -385,6 +385,20 @@ Module Compilers. cbn [List.length List.combine fold_left] in *; try discriminate; inversion Hls'; eauto. } Qed. + + Lemma app_forall_vars_lam_forall_vars {p k f evm v} + : @pattern.type.app_forall_vars p k (pattern.type.lam_forall_vars f) evm = Some v + -> v = f _. + Proof using Type. + revert v; cbv [pattern.type.app_forall_vars pattern.type.lam_forall_vars]. + generalize (rev (PositiveSet.elements p)); clear p; intro ls. + generalize (PositiveMap.empty base.type). + induction ls as [|x xs IHxs]; cbn [list_rect fold_right]; [ congruence | ]. + intros t v H; eapply IHxs; clear IHxs. + rewrite <- H. + break_innermost_match; [ | now discriminate ]. + reflexivity. + Qed. End type. End pattern. |