From 436d274de182ca3cf82a6bd7de3e8ed3d8230ef7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Jan 2020 22:48:51 +0100
Subject: [PATCH] Some generic results on binders that were in Iris.

---
 theories/binders.v | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/theories/binders.v b/theories/binders.v
index da5dea02..ba5aca17 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -8,7 +8,7 @@ a coercion.
 This library is used in various Iris developments, like heap-lang, LambdaRust,
 Iron, Fairis. *)
 From stdpp Require Export strings.
-From stdpp Require Import sets countable finite.
+From stdpp Require Import sets countable finite fin_maps.
 
 Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
@@ -68,3 +68,31 @@ Proof.
   induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
     first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
 Qed.
+
+Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
+  match b with BAnon => m | BNamed s => delete s m end.
+Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
+  match b with BAnon => m | BNamed s => <[s:=x]> m end.
+Instance: Params (@binder_insert) 4 := {}.
+
+Section binder_delete_insert.
+  Context `{FinMap string M}.
+
+  Global Instance binder_insert_proper `{Equiv A} b :
+    Proper ((≡) ==> (≡) ==> (≡@{M A})) (binder_insert b).
+  Proof. destruct b; solve_proper. Qed.
+
+  Lemma lookup_binder_delete_None {A} (m : M A) b s :
+    binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
+  Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
+  Lemma binder_insert_fmap {A B} (f : A → B) (x : A) b (m : M A) :
+    f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
+  Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
+
+  Lemma binder_delete_insert {A} b s x (m : M A) :
+    b ≠ BNamed s → binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
+  Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
+  Lemma binder_delete_delete {A} b s (m : M A) :
+    binder_delete b (delete s m) = delete s (binder_delete b m).
+  Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
+End binder_delete_insert.
-- 
GitLab