binders.v 4.31 KB
Newer Older
1
2
3
4
5
6
7
8
(** 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.
9
From stdpp Require Import sets countable finite fin_maps.
10
11
12
13
14
15
16
17
18
19
20
21

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'
Michael Sammler's avatar
Michael Sammler committed
22
23
   (λ b, match b with BAnon => None | BNamed s => Some s end)
   (λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
24
25
Qed.

Michael Sammler's avatar
Michael Sammler committed
26
27
28
(** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
to collect the free variables of an expression. Here [ss] is the current list of
free variables, and [b], respectively [bs], are the binders that are being
29
added. *)
Michael Sammler's avatar
Michael Sammler committed
30
31
Definition cons_binder (b : binder) (ss : list string) : list string :=
  match b with BAnon => ss | BNamed s => s :: ss end.
32
Infix ":b:" := cons_binder (at level 60, right associativity).
Michael Sammler's avatar
Michael Sammler committed
33
34
Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
  match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
35
36
Infix "+b+" := app_binder (at level 60, right associativity).

Michael Sammler's avatar
Michael Sammler committed
37
38
Instance set_unfold_cons_binder s b ss P :
  SetUnfoldElemOf s ss P  SetUnfoldElemOf s (b :b: ss) (BNamed s = b  P).
39
Proof.
Michael Sammler's avatar
Michael Sammler committed
40
41
  constructor. rewrite <-(set_unfold (s  ss) P).
  destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
42
Qed.
Michael Sammler's avatar
Michael Sammler committed
43
44
45
Instance set_unfold_app_binder s bs ss P Q :
  SetUnfoldElemOf (BNamed s) bs P  SetUnfoldElemOf s ss Q 
  SetUnfoldElemOf s (bs +b+ ss) (P  Q).
46
Proof.
Michael Sammler's avatar
Michael Sammler committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
  intros HinP HinQ.
  constructor. rewrite <-(set_unfold (s  ss) Q), <-(set_unfold (BNamed s  bs) P).
  clear HinP HinQ.
  induction bs; set_solver.
Qed.

Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
Proof. induction ss1; by f_equal/=. Qed.

Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.

Instance cons_binder_Permutation b : Proper (() ==> ()) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.

Instance app_binder_Permutation : Proper (() ==> () ==> ()) app_binder.
Proof.
  assert ( bs, Proper (() ==> ()) (app_binder bs)).
65
  { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
Michael Sammler's avatar
Michael Sammler committed
66
67
  induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
    first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
68
Qed.
69
70
71
72
73
74
75
76
77
78
79
80
81
82

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.

83
  Lemma binder_delete_empty {A} b : binder_delete b  =@{M A} .
84
  Proof. destruct b; simpl; eauto using delete_empty. Qed.
85

86
87
88
89
90
91
92
93
94
95
96
97
98
99
  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.