Get rid of of_val_unlock.

theories/lang/tactics.v

@@ -185,7 +185,8 @@ Ltac solve_to_val :=
   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; unfold W.to_expr; unlock; reflexivity
+     apply W.to_val_Some; simpl; unfold W.to_expr;
+     ((unlock; exact eq_refl) || (idtac; exact eq_refl))
   | |- 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

theories/typing/base.v

@@ -14,13 +14,8 @@ Ltac solve_typing :=
   (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
   (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
 
-Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
-Proof. by unlock. Qed.
-
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
-Hint Resolve
-     of_val_unlock
-     submseteq_cons submseteq_inserts_l submseteq_inserts_r
+Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
   : lrust_typing.
 
 Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>

theories/typing/function.v

@@ -397,10 +397,9 @@ Section typing.
   Qed.
 
   Lemma type_rec {A} E L fb (argsb : list binder) ef e n
-        (fp : A → fn_params n) T `{!CopyC T, !SendC T} :
-    ef = (funrec: fb argsb := e)%E →
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+    IntoVal ef (funrec: fb argsb := e) →
     n = length argsb →
-    Closed (fb :b: "return" :b: argsb +b+ []) e →
     □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
           typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
                      [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
@@ -410,8 +409,7 @@ Section typing.
                      (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn fp).
   Proof.
-    iIntros (-> -> Hc) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
-    { unfold IntoVal. simpl. rewrite ->(decide_left Hc). done. }
+    iIntros (<-%of_to_val ->) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
     iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
@@ -422,10 +420,9 @@ Section typing.
   Qed.
 
   Lemma type_fn {A} E L (argsb : list binder) ef e n
-        (fp : A → fn_params n) T `{!CopyC T, !SendC T} :
-    ef = (funrec: <> argsb := e)%E →
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+    IntoVal ef (funrec: <> argsb := e) →
     n = length argsb →
-    Closed ("return" :b: argsb +b+ []) e →
     □ (∀ x ϝ k (args : vec val (length argsb)),
         typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
                    [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
@@ -434,7 +431,7 @@ Section typing.
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn fp).
   Proof.
-    iIntros (???) "#He". iApply type_rec; try done. iIntros "!# *".
+    iIntros (??) "#He". iApply type_rec; try done. iIntros "!# *".
     iApply typed_body_mono; last iApply "He"; try done.
     eapply contains_tctx_incl. by constructor.
   Qed.

theories/typing/lib/panic.v

@@ -18,7 +18,7 @@ Section panic.
 
   Lemma panic_type : typed_val panic (fn(∅) → emp).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "!# *".
+    intros E L. iApply type_fn; [done|]. iIntros "!# *".
     inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
     by iApply wp_value.
   Qed.