Tactic for solving typeability

- Change the types in the examples slightly
- Use notations in the examples
- Modify some tactics to make the proofs more smooth

F_mu_ref_conc/examples/counter.v

@@ -14,17 +14,18 @@ Definition CG_increment : val := λ: "x" "l" <>,
 
 Definition counter_read : val := λ: "x" <>, !"x".
 
-Definition CG_counter : expr :=
-  let: "l" := newlock in
+Definition CG_counter : val := λ: <>,
+  let: "l" := newlock #() in
   let: "x" := ref (#n 0) in
   (CG_increment "x" "l", counter_read "x").
 
 Definition FG_increment : val := λ: "v", rec: "inc" <> :=
-  Let "c" (!"v") (If (CAS "v" "c" (BinOp Add (#n 1) "c"))
-                     (Unit)
-                     ("inc" #())).
+  let: "c" := !"v" in
+  if: CAS "v" "c" (BinOp Add (#n 1) "c")
+  then #()
+  else "inc" #().
 
-Definition FG_counter : expr := 
+Definition FG_counter : val := λ: <>,
   let: "x" := Alloc (#n 0) in
   (FG_increment "x", counter_read "x").
 
@@ -34,10 +35,7 @@ Section CG_Counter.
   (* Coarse-grained increment *)  
   Lemma CG_increment_type Γ :
     typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
-  Proof.
-    unfold CG_increment. unlock.
-    eauto 25 with typeable.
-  Qed.
+  Proof. solve_typed. Qed.
 
   Hint Resolve CG_increment_type : typeable.
 
@@ -64,29 +62,20 @@ Section CG_Counter.
  
   Lemma counter_read_type Γ :
     typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
-  Proof.
-    unfold counter_read. unlock.
-    eauto 10 with typeable.
-  Qed.
+  Proof. solve_typed. Qed.
 
   Hint Resolve counter_read_type : typeable.
 
   Lemma CG_counter_type Γ :
-    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
-  Proof.
-    unfold CG_counter.
-    eauto 15 with typeable.
-  Qed.
+    typed Γ CG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
+  Proof. solve_typed. Qed.
 
   Hint Resolve CG_counter_type : typeable.
 
   (* Fine-grained increment *)
   Lemma FG_increment_type Γ :
     typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
-  Proof.
-    unfold FG_increment. unlock.
-    eauto 20 with typeable.
-  Qed.
+  Proof. solve_typed. Qed.
 
   Hint Resolve FG_increment_type : typeable.
 
@@ -120,11 +109,8 @@ Section CG_Counter.
   Qed.
 
   Lemma FG_counter_type Γ :
-    typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
-  Proof.
-    unfold FG_counter.
-    eauto 15 with typeable.
-  Qed.
+    typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
+  Proof. solve_typed. Qed.
 
   Hint Resolve FG_counter_type : typeable.
 
@@ -133,7 +119,6 @@ Section CG_Counter.
   Definition counter_inv l cnt cnt' : iProp Σ :=
     (∃ n, l ↦ₛ (#♭v false) ∗ cnt ↦ᵢ (#nv n) ∗ cnt' ↦ₛ (#nv n))%I.
 
-
   Lemma bin_log_counter_read_r Γ E1 E2 K x n t τ
     (Hspec : nclose specN ⊆ E1) :
     x ↦ₛ (#nv n)
@@ -273,17 +258,19 @@ Section CG_Counter.
   Qed.
 
   Lemma FG_CG_counter_refinement :
-    ∅ ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
+    ∅ ⊨ FG_counter ≤log≤ CG_counter :
+          TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
   Proof.
     unfold FG_counter, CG_counter.
-    rel_bind_r newlock.
+    iApply bin_log_related_arrow; try by (unlock; eauto).
+    iAlways. iIntros (? [? ?]) "/= [% %]"; simplify_eq/=.
+    unlock. rel_rec_l. rel_rec_r.
+    rel_bind_r (newlock #())%E.
     iApply (bin_log_related_newlock_r); auto; simpl.
     iIntros (l) "Hl".
     rel_rec_r.
     rel_alloc_r as cnt' "Hcnt'".
-    rel_bind_l (Alloc _).
-    iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
-    iIntros (cnt) "Hcnt".
+    rel_alloc_l as cnt "Hcnt". simpl.
 
     rel_rec_l.
     rel_rec_r.
@@ -312,7 +299,7 @@ End CG_Counter.
 
 Theorem counter_ctx_refinement :
   ∅ ⊨ FG_counter ≤ctx≤ CG_counter :
-         TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
+         TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
 Proof.
   eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
   apply FG_CG_counter_refinement.

F_mu_ref_conc/examples/lateearlychoice.v

@@ -51,7 +51,7 @@ Section Refinement.
     unfold rand. unlock. simpl.
     rel_rec_l.
     rel_bind_l (Alloc _).
-    iApply bin_log_related_alloc_l'; first eauto. iIntros (y) "Hy". simpl.
+    iApply bin_log_related_alloc_l'; first eauto. iNext. iIntros (y) "Hy". simpl.
     rel_rec_l.
     iMod (inv_alloc choiceN _ (∃ b, y ↦ᵢ (#♭v b))%I with "[Hy]") as "#Hinv".
     { iNext. eauto. }
@@ -89,7 +89,7 @@ Section Refinement.
     rel_fork_r as j "Hj".
     rel_rec_r.
     destruct b.
-    - iApply fupd_logrel'. tp_store j. iModIntro.
+    - tp_store j.
       by rel_load_r.
     - by rel_load_r.
   Qed.

F_mu_ref_conc/examples/lock.v

@@ -3,51 +3,40 @@ From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics.
 From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary relational_properties notation.
 From iris.base_logic Require Import namespaces.
 
-(** [newlock = alloc false] *)
-Definition newlock : expr := Alloc (#♭ false).
-(** [acquire = λ x. if cas(x, false, true) then #() else acquire(x) ] *)
-Definition acquire : val :=
-  RecV "acquire" "x"
-       (If (CAS "x" (#♭ false) (#♭ true))
-           (Unit)
-           (App "acquire" "x")).
-
-(** [release = λ x. x <- false] *)
-Definition release : val := LamV "x" (Store "x" (#♭ false)).
-(** [with_lock e l = λ x. (acquire l) ;; e x ;; (release l)] *)
+Definition newlock : val := λ: <>, ref (#♭ false).
+Definition acquire : val := rec: "acquire" "x" :=
+  if: CAS "x" (#♭ false) (#♭ true)
+  then #()
+  else "acquire" "x".
+
+Definition release : val := λ: "x", "x" <- #♭ false.
 Definition with_lock : val := λ: "e" "l" "x",
   acquire "l";;
-  Let "v" ("e" "x")
-    (release "l";; "v").
-
-Instance newlock_closed: Closed ∅ newlock.
-Proof. rewrite /newlock. solve_closed. Qed.
+  let: "v" := "e" "x" in
+  release "l";; "v".
 
 Definition LockType := Tref TBool.
 
 Hint Unfold LockType : typeable.
 
-Lemma newlock_type Γ : typed Γ newlock LockType.
-Proof. eauto with typeable. Qed.
+Lemma newlock_type Γ : typed Γ newlock (TArrow TUnit LockType).
+Proof. solve_typed. Qed.
+
+Hint Resolve newlock_type : typeable.
 
 Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
-Proof. unfold acquire. eauto 10 with typeable. Qed.
+Proof. solve_typed. Qed.
 
-Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
-Proof. unfold release. eauto with typeable. Qed.
+Hint Resolve acquire_type : typeable.
 
-Opaque acquire.
-Opaque release.
+Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
+Proof. solve_typed. Qed.
 
-Hint Resolve newlock_type : typeable.
 Hint Resolve release_type : typeable.
-Hint Resolve acquire_type : typeable.
 
 Lemma with_lock_type Γ τ τ' :
   typed Γ with_lock (TArrow (TArrow τ τ') (TArrow LockType (TArrow τ τ'))).
-Proof.
-  unfold with_lock. unlock. eauto 25 with typeable.
-Qed.
+Proof. solve_typed. Qed.
 
 Hint Resolve with_lock_type : typeable.
 
@@ -57,10 +46,12 @@ Section proof.
 
   Lemma steps_newlock ρ j K
     (Hcl : nclose specN ⊆ E1) :
-    spec_ctx ρ -∗ j ⤇ fill K newlock
+    spec_ctx ρ -∗ j ⤇ fill K (newlock #())%E
     ={E1}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros "#Hspec Hj".
+    unfold newlock. unlock.
+    tp_rec j. simpl.
     tp_alloc j as l "Hl". tp_normalise j.
     by iExists _; iFrame.
   Qed.
@@ -68,10 +59,11 @@ Section proof.
   Lemma bin_log_related_newlock_r Γ K t τ 
     (Hcl : nclose specN ⊆ E1) :
     (∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Loc l) : τ)%I
-    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K newlock : τ.
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (newlock #())%E: τ.
   Proof.
     iIntros "Hlog".
-    unfold newlock.
+    unfold newlock. unlock.
+    rel_rec_r.
     rel_alloc_r as l "Hl".
     iApply ("Hlog" with "Hl").
   Qed.
@@ -85,7 +77,7 @@ Section proof.
     ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v true).
   Proof.
     iIntros "#Hspec Hl Hj". 
-    unfold acquire.
+    unfold acquire. unlock.
     tp_rec j.
     tp_cas_suc j. 
     tp_if_true j.
@@ -99,6 +91,7 @@ Section proof.
     -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
+    unfold acquire. unlock.
     rel_rec_r.
     rel_cas_suc_r. simpl.
     rel_if_r.
@@ -113,7 +106,7 @@ Section proof.
     spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App release (Loc l))
     ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v false).
   Proof.
-    iIntros "#Hspec Hl Hj". unfold release.
+    iIntros "#Hspec Hl Hj". unfold release. unlock.
     tp_rec j.
     tp_store j. tp_normalise j.
     by iFrame.
@@ -126,7 +119,7 @@ Section proof.
     -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
-    unfold release.
+    unfold release. unlock.
     rel_rec_r.
     rel_store_r.
     by iApply "Hlog".
@@ -144,7 +137,7 @@ Section proof.
     ={E1}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros (Hev Hpf ?) "#Hspec HP Hl Hj".
-    unfold with_lock. unlock. (* TODO :( *)
+    unfold with_lock. unlock.
     tp_rec j.
     tp_rec j.
     tp_rec j; eauto using to_of_val.

F_mu_ref_conc/examples/par.v

@@ -21,10 +21,7 @@ Lemma par_type Γ τ1 τ2 :
   typed Γ par
         (TArrow (TArrow TUnit τ1) (TArrow (TArrow TUnit τ2)
             (TProd τ1 τ2))).
-Proof.    
-  unfold par. unlock.
-  eauto 40 with typeable.
-Qed.
+Proof. solve_typed. Qed.
 
 Hint Resolve par_type : typeable.
 
@@ -43,4 +40,5 @@ Section compatibility.
     iApply (bin_log_related_app with "[] He1").
     iApply binary_fundamental_masked; eauto with typeable.
   Qed.
+
 End compatibility.

F_mu_ref_conc/fundamental_binary.v

@@ -319,7 +319,7 @@ Section masked.
     Closed (dom _ Γ) e →
     Closed (dom _ Γ) e' →
     (↑ specN ⊆ E) →
-    □ ({E,E;(Autosubst_Classes.subst (ren (+1)) <$> Γ)} ⊨ e ≤log≤ e' : τ) -∗
+    □ ({E,E;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ e ≤log≤ e' : τ) -∗
     {E,E;Γ} ⊨ TLam e ≤log≤ TLam e' : TForall τ.
   Proof.
     rewrite bin_log_related_eq.
@@ -515,8 +515,8 @@ Section masked.
     iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
     iModIntro.
     iApply (wp_store with "Hv1"); auto using to_of_val. 
-    iNext. iIntros "Hw2". 
-    tp_store j; eauto; tp_normalise j.
+    iNext. iIntros "Hw2".
+    tp_store j.
     iMod ("Hclose" with "[Hw2 Hv2]").
     { iNext; iExists (_, _); simpl; iFrame. iFrame "IH2". }
     iExists UnitV; iFrame; auto.

F_mu_ref_conc/rel_tactics.v

@@ -304,7 +304,7 @@ Lemma tac_rel_alloc_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P e' v' K'
   envs_lookup nam_cl Δ1 = None →
   nam_cl ≠ nam →
   Δ2 = envs_snoc (envs_snoc Δ1 false nam (▷ P)%I) false nam_cl (▷ P ={E1 ∖ ↑N,E1}=∗ True)%I →
-  (Δ2 ⊢ |={E2}=> ∀ l,
+  (Δ2 ⊢ |={E2}=> ▷ ∀ l,
      (l ↦ᵢ v' -∗ bin_log_related E2 E1 Γ (fill K' (Loc l)) t τ)) →
   (Δ1 ⊢ bin_log_related E1 E1 Γ e t τ).
 Proof.
@@ -347,25 +347,27 @@ Tactic Notation "rel_alloc_l" "under" constr(N) "as" constr(nam) constr(nam_cl)
 
 Lemma tac_rel_alloc_l_simp `{logrelG Σ} Δ1 Δ2 E1 e' v' K' Γ e t τ :
   e = fill K' (Alloc e') →
+  IntoLaterNEnvs 1 Δ1 Δ2 →
   to_val e' = Some v' →
-  (Δ1 ⊢ ∀ l,
+  (Δ2 ⊢ ∀ l,
      (l ↦ᵢ v' -∗ bin_log_related E1 E1 Γ (fill K' (Loc l)) t τ)) →
   (Δ1 ⊢ bin_log_related E1 E1 Γ e t τ).
 Proof.
   intros ???.
   subst e.
-  rewrite -(bin_log_related_alloc_l' Γ E1). 2: eassumption.
-  done.
+  rewrite into_laterN_env_sound /=.
+  rewrite -(bin_log_related_alloc_l' Γ E1); eauto.
+  apply uPred.later_mono.
 Qed.
 
 Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
   iStartProof;
   eapply (tac_rel_alloc_l_simp);
     [tac_bind_helper (* e = fill K' .. *)
+    |apply _ (* IntoLaterNEnvs _ _ _ *)
     |solve_to_val (* to_val e' = Some v *)
     |iIntros (l) H (* new goal *)].
 
-
 Lemma tac_rel_load_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l K' Γ e t τ :
   nclose N ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, inv N P) →
@@ -436,8 +438,8 @@ Tactic Notation "rel_load_l" :=
   iStartProof;
   eapply (tac_rel_alloc_l_simp);
     [tac_bind_helper (* e = fill K' .. *)
-    |apply _  (* IntoLaterNenvs 1 Δ1 Δ2 *)
-    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?" 
+    |apply _  (* IntoLaterNenvs _ Δ1 Δ2 *)
+    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
     | (* new goal *)].
 
 Lemma tac_rel_store_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e' v' K' Γ e t τ :

F_mu_ref_conc/relational_properties.v

@@ -409,8 +409,8 @@ Section properties.
 
   Lemma bin_log_related_alloc_l Γ E1 E2 K e v t τ
     (Heval : to_val e = Some v) :
-    (|={E1,E2}=> ∀ (l : loc), l ↦ᵢ v -∗
-           {E2,E1;Γ} ⊨ fill K (Loc l) ≤log≤ t : τ)%I
+    (|={E1,E2}=> ▷ (∀ (l : loc), l ↦ᵢ v -∗
+           {E2,E1;Γ} ⊨ fill K (Loc l) ≤log≤ t : τ))%I
     -∗ {E1,E1;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
@@ -421,7 +421,7 @@ Section properties.
 
   Lemma bin_log_related_alloc_l' Γ E K e v t τ
     (Heval : to_val e = Some v) :
-    (∀ (l : loc), l ↦ᵢ v -∗ {E,E;Γ} ⊨ fill K (Loc l) ≤log≤ t : τ)%I
+    ▷ (∀ (l : loc), l ↦ᵢ v -∗ {E,E;Γ} ⊨ fill K (Loc l) ≤log≤ t : τ)%I
     -∗ {E,E;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".

F_mu_ref_conc/typing.v

@@ -119,6 +119,16 @@ Hint Constructors EqType : typeable.
 Hint Extern 10 (<[_:=_]>_ !! _ = Some _) => eapply lookup_insert : typeable.
 Hint Extern 20 (<[_:=_]>_ !! _ = Some _) => rewrite lookup_insert_ne; last done : typeable.
 
+Lemma locked_val_typed Γ (v : val) (τ : type) :
+  Γ ⊢ₜ of_val v : τ →
+  Γ ⊢ₜ of_val (locked v) : τ.
+Proof. by unlock. Qed.
+
+Tactic Notation "solve_typed" int_or_var(n) :=
+  try apply locked_val_typed; eauto n with typeable.
+
+Tactic Notation "solve_typed" := solve_typed 50.
+
 (** Environment substitution and closedness *)
 Definition env_subst := subst_p.