get rid of substitution in Case (use lambdas); introduce Match as derived form...

get rid of substitution in Case (use lambdas); introduce Match as derived form that involves binders

heap_lang/derived.v

@@ -9,6 +9,7 @@ Notation LamV x e := (RecV BAnom x e).
 Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
 Notation SeqCtx e2 := (LetCtx BAnom e2).
 Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
 
 Section derived.
 Context {Σ : rFunctor}.
@@ -34,6 +35,20 @@ Proof. intros ?. by rewrite -wp_let. Qed.
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ || Skip @ E {{ Φ }}.
 Proof. rewrite -wp_seq // -wp_value //. Qed.
 
+Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
+  to_val e0 = Some v0 →
+  ▷ || subst' e1 x1 v0 @ E {{ Φ }} ⊑ || Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_case_inl // -[X in _ ⊑ X]later_intro. by apply wp_let.
+Qed.
+
+Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
+  to_val e0 = Some v0 →
+  ▷ || subst' e2 x2 v0 @ E {{ Φ }} ⊑ || Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -wp_case_inr // -[X in _ ⊑ X]later_intro. by apply wp_let.
+Qed.
+
 Lemma wp_le E (n1 n2 : Z) P Φ :
   (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
   (n2 < n1 → P ⊑ ▷ Φ (LitV (LitBool false))) →

heap_lang/lang.v

@@ -36,7 +36,7 @@ Inductive expr :=
   (* Sums *)
   | InjL (e : expr)
   | InjR (e : expr)
-  | Case (e0 : expr) (x1 : binder) (e1 : expr) (x2 : binder) (e2 : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr)
   (* Concurrency *)
   | Fork (e : expr)
   (* Heap *)
@@ -107,7 +107,7 @@ Inductive ectx_item :=
   | SndCtx
   | InjLCtx
   | InjRCtx
-  | CaseCtx (x1 : binder) (e1 : expr) (x2 : binder) (e2 : expr)
+  | CaseCtx (e1 : expr) (e2 : expr)
   | AllocCtx
   | LoadCtx
   | StoreLCtx (e2 : expr)
@@ -132,7 +132,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | SndCtx => Snd e
   | InjLCtx => InjL e
   | InjRCtx => InjR e
-  | CaseCtx x1 e1 x2 e2 => Case e x1 e1 x2 e2
+  | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
   | StoreLCtx e2 => Store e e2
@@ -160,10 +160,8 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
   | Snd e => Snd (subst e x v)
   | InjL e => InjL (subst e x v)
   | InjR e => InjR (subst e x v)
-  | Case e0 x1 e1 x2 e2 =>
-     Case (subst e0 x v)
-       x1 (if decide (BNamed x ≠ x1) then subst e1 x v else e1)
-       x2 (if decide (BNamed x ≠ x2) then subst e2 x v else e2)
+  | Case e0 e1 e2 =>
+     Case (subst e0 x v) (subst e1 x v) (subst e2 x v)
   | Fork e => Fork (subst e x v)
   | Loc l => Loc l
   | Alloc e => Alloc (subst e x v)
@@ -213,12 +211,12 @@ Inductive head_step : expr → state → expr → state → option expr → Prop
   | SndS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      head_step (Snd (Pair e1 e2)) σ e2 σ None
-  | CaseLS e0 v0 x1 e1 x2 e2 σ :
+  | CaseLS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjL e0) x1 e1 x2 e2) σ (subst' e1 x1 v0) σ None
-  | CaseRS e0 v0 x1 e1 x2 e2 σ :
+     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
+  | CaseRS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjR e0) x1 e1 x2 e2) σ (subst' e2 x2 v0) σ None
+     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
   | ForkS e σ:
      head_step (Fork e) σ (Lit LitUnit) σ (Some e)
   | AllocS e v σ l :

heap_lang/lifting.v

@@ -147,20 +147,20 @@ Proof.
     ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
-Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Φ :
+Lemma wp_case_inl E e0 v0 e1 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ || subst' e1 x1 v0 @ E {{ Φ }} ⊑ || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
+  ▷ || App e1 e0 @ E {{ Φ }} ⊑ || Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
-    (subst' e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
+  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
+    (App e1 e0) None) ?right_id //; intros; inv_step; eauto.
 Qed.
 
-Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Φ :
+Lemma wp_case_inr E e0 v0 e1 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ || subst' e2 x2 v0 @ E {{ Φ }} ⊑ || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
+  ▷ || App e2 e0 @ E {{ Φ }} ⊑ || Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
-    (subst' e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
+  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
+    (App e2 e0) None) ?right_id //; intros; inv_step; eauto.
 Qed.
 
 End lifting.

heap_lang/notation.v

@@ -28,7 +28,7 @@ Notation "<>" := BAnom : binder_scope.
    pretty printing. *)
 Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
 Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
-  (Case e0 x1 e1 x2 e2)
+  (Match e0 x1 e1 x2 e2)
   (e0, x1, e1, x2, e2 at level 200) : lang_scope.
 Notation "()" := LitUnit : lang_scope.
 Notation "# l" := (Lit l%Z%L) (at level 8, format "# l").

heap_lang/substitution.v

@@ -66,11 +66,6 @@ Instance subst_rec f y e x v er :
   SubstIf (BNamed x ≠ f ∧ BNamed x ≠ y) e x v er →
   Subst (Rec f y e) x v (Rec f y er).
 Proof. intros [??]; red; f_equal/=; case_decide; auto. Qed.
-Instance subst_case e0 x1 e1 x2 e2 x v e0r e1r e2r :
-  Subst e0 x v e0r →
-  SubstIf (BNamed x ≠ x1) e1 x v e1r → SubstIf (BNamed x ≠ x2) e2 x v e2r →
-  Subst (Case e0 x1 e1 x2 e2) x v (Case e0r x1 e1r x2 e2r).
-Proof. intros ? [??] [??]; red; f_equal/=; repeat case_decide; auto. Qed.
 
 Instance subst_app e1 e2 x v e1r e2r :
   Subst e1 x v e1r → Subst e2 x v e2r → Subst (App e1 e2) x v (App e1r e2r).
@@ -97,6 +92,10 @@ Instance subst_injL e x v er : Subst e x v er → Subst (InjL e) x v (InjL er).
 Proof. by intros; red; f_equal/=. Qed.
 Instance subst_injR e x v er : Subst e x v er → Subst (InjR e) x v (InjR er).
 Proof. by intros; red; f_equal/=. Qed.
+Instance subst_case e0 e1 e2 x v e0r e1r e2r :
+  Subst e0 x v e0r → Subst e1 x v e1r → Subst e2 x v e2r →
+  Subst (Case e0 e1 e2) x v (Case e0r e1r e2r).
+Proof. by intros; red; f_equal/=. Qed.
 Instance subst_fork e x v er : Subst e x v er → Subst (Fork e) x v (Fork er).
 Proof. by intros; red; f_equal/=. Qed.
 Instance subst_alloc e x v er : Subst e x v er → Subst (Alloc e) x v (Alloc er).
@@ -134,9 +133,7 @@ Fixpoint is_closed (X : stringset) (e : expr) : bool :=
   | Snd e => is_closed X e
   | InjL e => is_closed X e
   | InjR e => is_closed X e
-  | Case e0 x1 e1 x2 e2 =>
-     is_closed X e0 &&
-     is_closed (of_binder x1 ∪ X) e1 && is_closed (of_binder x2 ∪ X) e2
+  | Case e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2
   | Fork e => is_closed X e
   | Loc l => true
   | Alloc e => is_closed X e