From 446bc64428ce0c7bce4b82b53d93546a0e60f114 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 18 Jan 2020 14:24:22 -0500 Subject: [PATCH] More `subst_map` lemmas. --- theories/heap_lang/metatheory.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v index 20bccf498..532eff0f2 100644 --- a/theories/heap_lang/metatheory.v +++ b/theories/heap_lang/metatheory.v @@ -187,6 +187,10 @@ 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_empty b v e : + subst_map (binder_insert b v ∅) e = subst' b v e. +Proof. by rewrite subst_map_binder_insert binder_delete_empty subst_map_empty. 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)). @@ -196,6 +200,12 @@ Proof. - by rewrite delete_idemp subst_subst delete_insert_delete. - by rewrite delete_insert_ne // subst_map_insert subst_subst_ne. Qed. +Lemma subst_map_binder_insert_2_empty b1 v1 b2 v2 e : + subst_map (binder_insert b1 v1 (binder_insert b2 v2 ∅)) e = + subst' b2 v2 (subst' b1 v1 e). +Proof. + by rewrite subst_map_binder_insert_2 !binder_delete_empty subst_map_empty. +Qed. (* subst_map on closed expressions *) Lemma subst_map_is_closed X e vs : -- GitLab