From 9054147a09bb78548d22cd067977cb3a19a465ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Apr 2019 10:40:10 +0200
Subject: [PATCH] Binders library that's used in many Iris developments.

---
 _CoqProject        |  1 +
 theories/binders.v | 49 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 theories/binders.v

diff --git a/_CoqProject b/_CoqProject
index dc2c81e2..123fc871 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,3 +44,4 @@ theories/infinite.v
 theories/nat_cancel.v
 theories/namespaces.v
 theories/telescopes.v
+theories/binders.v
diff --git a/theories/binders.v b/theories/binders.v
new file mode 100644
index 00000000..72c0f7e8
--- /dev/null
+++ b/theories/binders.v
@@ -0,0 +1,49 @@
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements a type [binder] with elements [BAnon] for the
+anonymous binder, and [BNamed] for named binders. This type is isomorphic to
+[option string], but we use a special type so that we can define [BNamed] as
+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.
+
+Inductive binder := BAnon | BNamed :> string → binder.
+Bind Scope binder_scope with binder.
+Delimit Scope binder_scope with binder.
+Notation "<>" := BAnon : binder_scope.
+
+Instance binder_dec_eq : EqDecision binder.
+Proof. solve_decision. Defined.
+Instance binder_inhabited : Inhabited binder := populate BAnon.
+Instance binder_countable : Countable binder.
+Proof.
+ refine (inj_countable'
+   (λ mx, match mx with BAnon => None | BNamed x => Some x end)
+   (λ mx, match mx with None => BAnon | Some x => BNamed x end) _); by intros [].
+Qed.
+
+(** The functions [cons_binder mx X] and [app_binder mxs X] are typically used
+to collect the free variables of an expression. Here [X] is the current list of
+free variables, and [mx], respectively [mxs], are the binders that are being
+added. *)
+Definition cons_binder (mx : binder) (X : list string) : list string :=
+  match mx with BAnon => X | BNamed x => x :: X end.
+Infix ":b:" := cons_binder (at level 60, right associativity).
+Fixpoint app_binder (mxs : list binder) (X : list string) : list string :=
+  match mxs with [] => X | b :: mxs => b :b: app_binder mxs X end.
+Infix "+b+" := app_binder (at level 60, right associativity).
+
+Instance set_unfold_cons_binder x mx X P :
+  SetUnfoldElemOf x X P → SetUnfoldElemOf x (mx :b: X) (BNamed x = mx ∨ P).
+Proof.
+  constructor. rewrite <-(set_unfold (x ∈ X) P).
+  destruct mx; simpl; rewrite ?elem_of_cons; naive_solver.
+Qed.
+Instance set_unfold_app_binder x mxl X P :
+  SetUnfoldElemOf x X P → SetUnfoldElemOf x (mxl +b+ X) (BNamed x ∈ mxl ∨ P).
+Proof.
+  constructor. rewrite <-(set_unfold (x ∈ X) P). induction mxl; set_solver.
+Qed.
-- 
GitLab