From ff87776ba94c707786cb32990a41be1ad1bdc5f0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 18 Jan 2020 16:51:24 +0100 Subject: [PATCH] Add lemma `subst_map_binder_insert_2`. --- theories/heap_lang/metatheory.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v index a2874c21c..20bccf498 100644 --- a/theories/heap_lang/metatheory.v +++ b/theories/heap_lang/metatheory.v @@ -187,6 +187,15 @@ Lemma subst_map_binder_insert b v vs e : subst_map (binder_insert b v vs) e = subst' b v (subst_map (binder_delete b vs) e). Proof. destruct b; rewrite ?subst_map_insert //. Qed. +Lemma subst_map_binder_insert_2 b1 v1 b2 v2 vs e : + subst_map (binder_insert b1 v1 (binder_insert b2 v2 vs)) e = + subst' b2 v2 (subst' b1 v1 (subst_map (binder_delete b2 (binder_delete b1 vs)) e)). +Proof. + destruct b1 as [|s1], b2 as [|s2]=> /=; auto using subst_map_insert. + rewrite subst_map_insert. destruct (decide (s1 = s2)) as [->|]. + - by rewrite delete_idemp subst_subst delete_insert_delete. + - by rewrite delete_insert_ne // subst_map_insert subst_subst_ne. +Qed. (* subst_map on closed expressions *) Lemma subst_map_is_closed X e vs : -- GitLab