Solve more to_val side-conditions using vm_compute.

heap_lang/derived.v

@@ -17,36 +17,31 @@ Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
-Lemma wp_lam E x ef e v Φ :
-  to_val e = Some v →
-  Closed (x :b: []) ef →
+Lemma wp_lam E x ef e Φ :
+  is_Some (to_val e) → Closed (x :b: []) ef →
   ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
 Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
 
-Lemma wp_let E x e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed (x :b: []) e2 →
+Lemma wp_let E x e1 e2 Φ :
+  is_Some (to_val e1) → Closed (x :b: []) e2 →
   ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
 Proof. apply wp_lam. Qed.
 
-Lemma wp_seq E e1 e2 v Φ :
-  to_val e1 = Some v →
-  Closed [] e2 →
+Lemma wp_seq E e1 e2 Φ :
+  is_Some (to_val e1) → Closed [] e2 →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
 Proof. intros ??. by rewrite -wp_let. Qed.
 
 Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq // -wp_value //. Qed.
+Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
 
-Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
-  to_val e0 = Some v0 →
-  Closed (x1 :b: []) e1 →
+Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
+  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
   ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 
-Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
-  to_val e0 = Some v0 →
-  Closed (x2 :b: []) e2 →
+Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
+  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
   ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
 

heap_lang/lifting.v

@@ -81,13 +81,13 @@ Proof.
   rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
 Qed.
 
-Lemma wp_rec E f x erec e1 e2 v2 Φ :
+Lemma wp_rec E f x erec e1 e2 Φ :
   e1 = Rec f x erec →
-  to_val e2 = Some v2 →
+  is_Some (to_val e2) →
   Closed (f :b: x :b: []) erec →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
-  intros -> ??. rewrite -(wp_lift_pure_det_head_step (App _ _)
+  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
     intros; inv_head_step; eauto.
 Qed.
@@ -122,35 +122,35 @@ Proof.
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_fst E e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+Lemma wp_fst E e1 v1 e2 Φ :
+  to_val e1 = Some v1 → is_Some (to_val e2) →
   ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
+  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_snd E e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+Lemma wp_snd E e1 e2 v2 Φ :
+  is_Some (to_val e1) → to_val e2 = Some v2 →
   ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
+  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_case_inl E e0 v0 e1 e2 Φ :
-  to_val e0 = Some v0 →
+Lemma wp_case_inl E e0 e1 e2 Φ :
+  is_Some (to_val e0) →
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
+  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
     (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_case_inr E e0 v0 e1 e2 Φ :
-  to_val e0 = Some v0 →
+Lemma wp_case_inr E e0 e1 e2 Φ :
+  is_Some (to_val e0) →
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
+  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
     (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 End lifting.

heap_lang/tactics.v

@@ -129,6 +129,9 @@ Proof.
   - do 2 f_equal. apply proof_irrel.
   - exfalso. unfold Closed in *; eauto using is_closed_correct.
 Qed.
+Lemma to_val_is_Some e :
+  is_Some (to_val e) → is_Some (heap_lang.to_val (to_expr e)).
+Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
 
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
@@ -172,12 +175,16 @@ Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
 Ltac solve_to_val :=
   try match goal with
-  | |- language.to_val ?e = Some ?v => change (to_val e = Some v)
+  | |- context E [language.to_val ?e] =>
+     let X := context E [to_val e] in change X
   end;
   match goal with
   | |- to_val ?e = Some ?v =>
      let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
      apply W.to_val_Some; simpl; reflexivity
+  | |- is_Some (to_val ?e) =>
+     let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
+     apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
 
 (** Substitution *)

heap_lang/wp_tactics.v

@@ -13,6 +13,7 @@ Ltac wp_bind K :=
 Ltac wp_done :=
   match goal with
   | |- Closed _ _ => solve_closed
+  | |- is_Some (to_val _) => solve_to_val
   | |- to_val _ = Some _ => solve_to_val
   | |- language.to_val _ = Some _ => solve_to_val
   | |- Is_true (atomic _) => rewrite /= ?to_of_val; fast_done