Library iris.program_logic.binders

From iris.prelude Require Export strings gmap.
From iris.program_logic Require Import ectxi_language.

Inductive binder := BAnon | BNamed : string → binder.
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.

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).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Proof. solve_decision. Defined.

Instance set_unfold_cons_binder x mx X P :
  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
Proof.
  constructor. rewrite -(set_unfold (x ∈ X) P).
  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.