Merge branch 'is_closed_gset' into 'master'

Formulate `is_closed_expr` in terms of `gset`s.

See merge request iris/iris!707

CHANGELOG.md

@@ -39,6 +39,11 @@ lemma.
   assumptions to remain compatible, and code that instantiates the BI interface
   needs to provide instances for the new classes.
 
+**Changes in `heap_lang`:**
+
+* The `is_closed_expr` predicate is formulated in terms of a
+  set of binders (as opposed to a list of binders).
+
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.

iris_heap_lang/metatheory.v

-From stdpp Require Import gmap.
+From stdpp Require Import gmap stringmap.
 From iris.heap_lang Require Export lang.
 From iris.prelude Require Import options.
 
 (* This file contains some metatheory about the heap_lang language,
   which is not needed for verifying programs. *)
 
-(* Closed expressions and values. *)
-Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
+(* Adding a binder to a set of identifiers. *)
+Local Definition set_binder_insert (x : binder) (X : stringset) : stringset :=
+  match x with
+  | BAnon => X
+  | BNamed f => {[f]} ∪ X
+  end.
+
+(* Check if expression [e] is closed w.r.t. the set [X] of variable names,
+   and that all the values in [e] are closed *)
+Fixpoint is_closed_expr (X : stringset) (e : expr) : bool :=
   match e with
   | Val v => is_closed_val v
   | Var x => bool_decide (x ∈ X)
-  | Rec f x e => is_closed_expr (f :b: x :b: X) e
+  | Rec f x e => is_closed_expr (set_binder_insert f (set_binder_insert x X)) e
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
      is_closed_expr X e
   | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | Xchg e1 e2 | FAA e1 e2 =>
@@ -22,19 +30,55 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
 with is_closed_val (v : val) : bool :=
   match v with
   | LitV _ => true
-  | RecV f x e => is_closed_expr (f :b: x :b: []) e
+  | RecV f x e => is_closed_expr (set_binder_insert f (set_binder_insert x ∅)) e
   | PairV v1 v2 => is_closed_val v1 && is_closed_val v2
   | InjLV v | InjRV v => is_closed_val v
   end.
 
+(* Parallel substitution *)
+Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
+  match e with
+  | Val _ => e
+  | Var y => if vs !! y is Some v then Val v else Var y
+  | Rec f y e => Rec f y (subst_map (binder_delete y (binder_delete f vs)) e)
+  | App e1 e2 => App (subst_map vs e1) (subst_map vs e2)
+  | UnOp op e => UnOp op (subst_map vs e)
+  | BinOp op e1 e2 => BinOp op (subst_map vs e1) (subst_map vs e2)
+  | If e0 e1 e2 => If (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
+  | Pair e1 e2 => Pair (subst_map vs e1) (subst_map vs e2)
+  | Fst e => Fst (subst_map vs e)
+  | Snd e => Snd (subst_map vs e)
+  | InjL e => InjL (subst_map vs e)
+  | InjR e => InjR (subst_map vs e)
+  | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
+  | Fork e => Fork (subst_map vs e)
+  | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
+  | Free e => Free (subst_map vs e)
+  | Load e => Load (subst_map vs e)
+  | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
+  | Xchg e1 e2 => Xchg (subst_map vs e1) (subst_map vs e2)
+  | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
+  | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
+  | NewProph => NewProph
+  | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
+  end.
+
+(* Properties *)
+Local Instance set_unfold_elem_of_insert_binder x y X Q :
+  SetUnfoldElemOf y X Q →
+  SetUnfoldElemOf y (set_binder_insert x X) (Q ∨ BNamed y = x).
+Proof. destruct 1; constructor; destruct x; set_solver. Qed.
+
 Lemma is_closed_weaken X Y e : is_closed_expr X e → X ⊆ Y → is_closed_expr Y e.
 Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
 
-Lemma is_closed_weaken_nil X e : is_closed_expr [] e → is_closed_expr X e.
-Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
+Lemma is_closed_weaken_empty X e : is_closed_expr ∅ e → is_closed_expr X e.
+Proof. intros. by apply is_closed_weaken with ∅, empty_subseteq. Qed.
 
-Lemma is_closed_subst X e x v :
-  is_closed_val v → is_closed_expr (x :: X) e → is_closed_expr X (subst x v e).
+Lemma is_closed_subst X e y v :
+  is_closed_val v →
+  is_closed_expr ({[y]} ∪ X) e →
+  is_closed_expr X (subst y v e).
 Proof.
   intros Hv. revert X.
   induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
@@ -43,24 +87,26 @@ Proof.
     end; eauto using is_closed_weaken with set_solver.
 Qed.
 Lemma is_closed_subst' X e x v :
-  is_closed_val v → is_closed_expr (x :b: X) e → is_closed_expr X (subst' x v e).
+  is_closed_val v →
+  is_closed_expr (set_binder_insert x X) e →
+  is_closed_expr X (subst' x v e).
 Proof. destruct x; eauto using is_closed_subst. Qed.
 
-(* Substitution *)
 Lemma subst_is_closed X e x es : is_closed_expr X e → x ∉ X → subst x es e = e.
 Proof.
-  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
-    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
+  revert X. induction e=> X /=;
+   rewrite ?bool_decide_spec ?andb_True=> ??;
+   repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
 Qed.
 
-Lemma subst_is_closed_nil e x v : is_closed_expr [] e → subst x v e = e.
-Proof. intros. apply subst_is_closed with []; set_solver. Qed.
+Lemma subst_is_closed_empty e x v : is_closed_expr ∅ e → subst x v e = e.
+Proof. intros. apply subst_is_closed with (∅:stringset); set_solver. Qed.
 
 Lemma subst_subst e x v v' :
   subst x v (subst x v' e) = subst x v' e.
 Proof.
   intros. induction e; simpl; try (f_equal; by auto);
-    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
+    simplify_option_eq; auto using subst_is_closed_empty with f_equal.
 Qed.
 Lemma subst_subst' e x v v' :
   subst' x v (subst' x v' e) = subst' x v' e.
@@ -70,7 +116,7 @@ Lemma subst_subst_ne e x y v v' :
   x ≠ y → subst x v (subst y v' e) = subst y v' (subst x v e).
 Proof.
   intros. induction e; simpl; try (f_equal; by auto);
-    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
+    simplify_option_eq; auto using eq_sym, subst_is_closed_empty with f_equal.
 Qed.
 Lemma subst_subst_ne' e x y v v' :
   x ≠ y → subst' x v (subst' y v' e) = subst' y v' (subst' x v e).
@@ -122,10 +168,10 @@ Qed.
 
 (* The stepping relation preserves closedness *)
 Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
-  is_closed_expr [] e1 →
+  is_closed_expr ∅ e1 →
   map_Forall (λ _ v, from_option is_closed_val true v) σ1.(heap) →
   head_step e1 σ1 obs e2 σ2 es →
-  is_closed_expr [] e2 ∧ Forall (is_closed_expr []) es ∧
+  is_closed_expr ∅ e2 ∧ Forall (is_closed_expr ∅) es ∧
   map_Forall (λ _ v, from_option is_closed_val true v) σ2.(heap).
 Proof.
   intros Cl1 Clσ1 STEP.
@@ -141,32 +187,6 @@ Proof.
   - case_match; try apply map_Forall_insert_2; by naive_solver.
 Qed.
 
-Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
-  match e with
-  | Val _ => e
-  | Var y => if vs !! y is Some v then Val v else Var y
-  | Rec f y e => Rec f y (subst_map (binder_delete y (binder_delete f vs)) e)
-  | App e1 e2 => App (subst_map vs e1) (subst_map vs e2)
-  | UnOp op e => UnOp op (subst_map vs e)
-  | BinOp op e1 e2 => BinOp op (subst_map vs e1) (subst_map vs e2)
-  | If e0 e1 e2 => If (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
-  | Pair e1 e2 => Pair (subst_map vs e1) (subst_map vs e2)
-  | Fst e => Fst (subst_map vs e)
-  | Snd e => Snd (subst_map vs e)
-  | InjL e => InjL (subst_map vs e)
-  | InjR e => InjR (subst_map vs e)
-  | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
-  | Fork e => Fork (subst_map vs e)
-  | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
-  | Free e => Free (subst_map vs e)
-  | Load e => Load (subst_map vs e)
-  | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
-  | Xchg e1 e2 => Xchg (subst_map vs e1) (subst_map vs e2)
-  | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
-  | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
-  | NewProph => NewProph
-  | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
-  end.
 
 Lemma subst_map_empty e : subst_map ∅ e = e.
 Proof.
@@ -216,7 +236,6 @@ Proof.
   by rewrite subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
 Qed.
 
-(* subst_map on closed expressions *)
 Lemma subst_map_is_closed X e vs :
   is_closed_expr X e →
   (∀ x, x ∈ X → vs !! x = None) →
@@ -224,11 +243,11 @@ Lemma subst_map_is_closed X e vs :
 Proof.
   revert X vs. assert (∀ x x1 x2 X (vs : gmap string val),
     (∀ x, x ∈ X → vs !! x = None) →
-    x ∈ x2 :b: x1 :b: X →
+    x ∈ set_binder_insert x2 (set_binder_insert x1 X) →
     binder_delete x1 (binder_delete x2 vs) !! x = None).
   { intros x x1 x2 X vs ??. rewrite !lookup_binder_delete_None. set_solver. }
   induction e=> X vs /= ? HX; repeat case_match; naive_solver eauto with f_equal.
 Qed.
 
-Lemma subst_map_is_closed_nil e vs : is_closed_expr [] e → subst_map vs e = e.
-Proof. intros. apply subst_map_is_closed with []; set_solver. Qed.
+Lemma subst_map_is_closed_empty e vs : is_closed_expr ∅ e → subst_map vs e = e.
+Proof. intros. apply subst_map_is_closed with (∅ : stringset); set_solver. Qed.