Commit 436d274d authored by Robbert Krebbers's avatar Robbert Krebbers

Some generic results on binders that were in Iris.

parent f4f0f216
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment