(An attempt of) improving the notation

- Notation for types
- Notation for pack and unit
- Better (?) levels for the relational judgement

theories/F_mu_ref_conc/lang.v

@@ -16,7 +16,7 @@ Module lang.
   Instance binop_dec_eq : EqDecision binop.
   Proof. solve_decision. Defined.
 
-  Inductive literal := Unit | Nat (n : nat) | Bool (b : bool) | Loc (l : loc).
+  Inductive literal := LitUnit | Nat (n : nat) | Bool (b : bool) | Loc (l : loc).
 
   Inductive expr :=
   | Var (x : string)
@@ -116,7 +116,7 @@ Module lang.
     | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b))
     | _,_,_ => None
     end.
-  Instance val_inh : Inhabited val := populate (LitV Unit).
+  Instance val_inh : Inhabited val := populate (LitV LitUnit).
 
   Fixpoint of_val (v : val) : expr :=
     match v with
@@ -171,10 +171,10 @@ Module lang.
   Proof.
     refine (inj_countable' (λ l, match l with
     | Nat n => inl (inl n) | Bool b => inl (inr b)
-    | Unit => inr (inl ()) | Loc l => inr (inr l)
+    | LitUnit => inr (inl ()) | Loc l => inr (inr l)
     end) (λ l, match l with
     | inl (inl n) => Nat n | inl (inr b) => Bool b
-    | inr (inl ()) => Unit | inr (inr l) => Loc l
+    | inr (inl ()) => LitUnit | inr (inr l) => Loc l
     end) _); by intros [].
   Qed.
 
@@ -240,7 +240,7 @@ Module lang.
            | GenNode 18 [e] => TApp (go e)
            | GenNode 19 [e] => Pack (go e)
            | GenNode 20 [e1; e2] => Unpack (go e1) (go e2)
-           | _ => Lit Unit (* dummy *)
+           | _ => Lit LitUnit (* dummy *)
            end).
     refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
   Qed.
@@ -393,7 +393,7 @@ Module lang.
       head_step (Unpack (Pack e1) e2) σ e' σ []
   (* Concurrency *)
   | ForkS e σ:
-      head_step (Fork e) σ (Lit Unit) σ [e]
+      head_step (Fork e) σ (Lit LitUnit) σ [e]
   (* Reference Types *)
   | AllocS e v σ l :
      to_val e = Some v → σ !! l = None →
@@ -403,7 +403,7 @@ Module lang.
      head_step (Load (Lit (Loc l))) σ (of_val v) σ []
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Lit (Loc l)) e) σ (Lit Unit) (<[l:=v]>σ) []
+     head_step (Store (Lit (Loc l)) e) σ (Lit LitUnit) (<[l:=v]>σ) []
   (* Compare and swap *)
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →

theories/F_mu_ref_conc/notation.v

@@ -12,7 +12,9 @@ Coercion of_val : val >-> expr.
 Coercion Nat : nat >-> literal.
 Coercion Bool : bool >-> literal.
 Coercion Loc : loc >-> literal.
-Notation "()" := lang.Unit : val_scope.
+Notation "()" := lang.LitUnit : val_scope.
+Notation "'Unit'" := (LitV LitUnit) : val_scope.
+Notation "'Unit'" := (Lit LitUnit) : expr_scope.
 
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
@@ -43,7 +45,10 @@ Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
 Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
 Notation "'ref' e" := (Alloc e%E)
   (at level 30, right associativity) : expr_scope.
-
+Notation "'pack' v" := (PackV v)
+  (at level 30, right associativity) : val_scope.
+Notation "'pack' e" := (Pack e%E)
+  (at level 30, right associativity) : expr_scope.
 Notation "e1 × e2" := (BinOp Mul e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
 Notation "e1 + e2" := (BinOp Add e1%E e2%E)

theories/F_mu_ref_conc/tactics.v

@@ -196,7 +196,7 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ᵢ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ᵢ v')) Δ' = Some Δ'' →
-  envs_entails Δ'' (Φ (LitV Unit)) →
+  envs_entails Δ'' (Φ (LitV LitUnit)) →
   envs_entails Δ (WP Store (Lit (Loc l)) e @ E {{ Φ }}).
 Proof.
   intros. eapply wand_apply; first by eapply wp_store.

theories/F_mu_ref_conc/typing.v

@@ -39,6 +39,29 @@ Inductive EqType : type → Prop :=
   | EqTProd τ τ' : EqType τ → EqType τ' → EqType (TProd τ τ')
   | EqSum τ τ' : EqType τ → EqType τ' → EqType (TSum τ τ').
 
+Delimit Scope FType_scope with F.
+Bind Scope FType_scope with type.
+Notation "'Unit'" := TUnit : FType_scope.
+Notation "'Bool'" := TBool : FType_scope.
+(* TODO: this clash with the module `Nat` *)
+(* Notation "'Nat'" := TNat : FType_scope. *)
+Infix "×" := TProd : FType_scope.
+Notation "(×)" := TProd (only parsing) : FType_scope.
+Infix "+" := TSum : FType_scope.
+Notation "(+)" := TSum (only parsing) : FType_scope.
+Infix "→" := TArrow : FType_scope.
+Notation "(→)" := TArrow (only parsing) : FType_scope.
+Notation "μ: τ" :=
+  (TRec τ%F)
+  (at level 100, τ at level 200) : FType_scope.
+Notation "∀: τ" :=
+  (TForall τ%F)
+  (at level 100, τ at level 200) : FType_scope.
+Notation "∃: τ" :=
+  (TExists τ%F)
+  (at level 100, τ at level 200) : FType_scope.
+Notation "'ref' τ" := (Tref τ%F) (at level 30, right associativity): FType_scope.
+
 (** Typing judgements *)
 Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 
@@ -103,15 +126,15 @@ Hint Constructors typed : typeable.
 Lemma TCAS' Γ e1 e2 e3 τ :
   Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
   EqType τ → 
-  Γ ⊢ₜ CAS e1 e2 e3 : TBool.
+  Γ ⊢ₜ CAS e1 e2 e3 : Bool.
 Proof. eauto using TCAS. Qed.
 
 Hint Resolve TCAS' : typeable.
 Remove Hints TCAS : typeable.
 
 Lemma TUNFOLD' Γ e τ τ' :
-  Γ ⊢ₜ e : TRec τ →
-  τ' = τ.[TRec τ/] →
+  Γ ⊢ₜ e : (μ: τ)%F →
+  τ' = τ.[(μ: τ)%F/] →
   Γ ⊢ₜ Unfold e : τ'.
 Proof. intros. subst τ'. by econstructor. Qed.
 
@@ -203,4 +226,4 @@ Proof.
 Qed.
 
 (* Type synonyms *)
-Notation MAYBE τ := (TSum TUnit τ) (only parsing).
+Notation MAYBE τ := (Unit + τ)%F (only parsing).

theories/examples/lock.v

@@ -183,7 +183,7 @@ Section lock_rules_r.
   Lemma steps_acquire ρ j K l
     (Hcl : nclose specN ⊆ E1) :
     spec_ctx ρ -∗ l ↦ₛ #false -∗ j ⤇ fill K (acquire #l)
-    ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ #true.
+    ={E1}=∗ j ⤇ fill K Unit ∗ l ↦ₛ #true.
   Proof.
     iIntros "#Hspec Hl Hj". 
     unfold acquire. unlock.
@@ -196,7 +196,7 @@ Section lock_rules_r.
   Lemma bin_log_related_acquire_r Γ K l t τ
     (Hcl : nclose specN ⊆ E1) :
     l ↦ₛ #false -∗
-    (l ↦ₛ #true -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ) -∗
+    (l ↦ₛ #true -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
     {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (acquire #l) : τ.
   Proof.
     iIntros "Hl Hlog".
@@ -259,7 +259,7 @@ Section lock_rules_r.
   Lemma bin_log_related_release_r Γ K l t τ (b : bool)
     (Hcl : nclose specN ⊆ E1) :
     l ↦ₛ #b -∗
-    (l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ) -∗
+    (l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
     {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (release #l) : τ.
   Proof.
     iIntros "Hl Hlog".

theories/examples/stack/module_refinement.v

@@ -46,7 +46,7 @@ Section Mod_refinement.
       { rewrite /prestack_owns big_sepM_empty fmap_empty.
         iFrame "Hemp". }
       iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
-      iAssert (preStackLink γ τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
+      iAssert (preStackLink γ τi (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK".
       { rewrite preStackLink_unfold.
         iExists _, _. iSplitR; simpl; trivial.
         iFrame "Histk". iLeft. iSplit; trivial. }

theories/examples/stack/refinement.v

@@ -342,7 +342,7 @@ Section Full_refinement.
     { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
       iFrame "Hemp". }
     iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
-    iAssert (StackLink τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
+    iAssert (StackLink τi (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
     { rewrite StackLink_unfold.
       iExists _, _. iSplitR; simpl; trivial.
       iFrame "Histk". iLeft. iSplit; trivial. }

theories/examples/ticket_lock.v

@@ -22,28 +22,26 @@ Definition acquire : val :=
 Definition release : val :=
   λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
 
-Definition LockType := TProd (Tref TNat) (Tref TNat).
+Definition LockType : type := ref TNat × ref TNat.
 
 Hint Unfold LockType : typeable.
 
-Lemma newlock_type Γ : typed Γ newlock (TArrow TUnit LockType).
+Lemma newlock_type Γ : typed Γ newlock (Unit → LockType).
 Proof. solve_typed. Qed.
 
 Hint Resolve newlock_type : typeable.
 
-Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
+Lemma acquire_type Γ : typed Γ acquire (LockType → TUnit).
 Proof. unlock acquire wait_loop. solve_typed. Qed.
 
 Hint Resolve acquire_type : typeable.
 
-Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
+Lemma release_type Γ : typed Γ release (LockType → TUnit).
 Proof. solve_typed. Qed.
 
 Hint Resolve release_type : typeable.
 
-Definition lockτ := TExists (TProd (TProd (TArrow TUnit (TVar 0))
-                                          (TArrow (TVar 0) TUnit))
-                                          (TArrow (TVar 0) TUnit)).
+Definition lockτ : type := ∃: (Unit → TVar 0) × (TVar 0 → Unit) × (TVar 0 → Unit).
 Lemma ticket_lock_typed Γ : typed Γ (Pack (newlock, acquire, release)) lockτ.
 Proof.
   apply TPack with LockType.

theories/examples/various.v

@@ -16,7 +16,7 @@ Section refinement.
       (λ: "f", "f" #();; !"x")
     ≤log≤
       (λ: "f", "f" #();; #1)
-    : TArrow (TArrow TUnit TUnit) TNat.
+    : ((Unit → Unit) → TNat).
   Proof.
   iIntros (Δ).
   rel_alloc_l as x "Hx".
@@ -68,7 +68,7 @@ Section refinement.
     ≤log≤
       (let: "x" := ref #1 in
        λ: "f", "f" #();; !"x")
-    : TArrow (TArrow TUnit TUnit) TNat.
+    : ((Unit → Unit) → TNat).
   Proof.
     iIntros (Δ).
     rel_alloc_l as x "Hx".

theories/logrel/fundamental_binary.v

@@ -56,17 +56,17 @@ Section masked.
     iApply wp_value. eauto.
   Qed.
 
-  Lemma bin_log_related_unit Δ Γ : {E;Δ;Γ} ⊨ #() ≤log≤ #() : TUnit.
+  Lemma bin_log_related_unit Δ Γ : {E;Δ;Γ} ⊨ #() ≤log≤ #() : Unit.
   Proof.
     value_case.
   Qed.
 
-  Lemma bin_log_related_nat Δ Γ (n : nat) : {E;Δ;Γ} ⊨ # n ≤log≤ # n : TNat.
+  Lemma bin_log_related_nat Δ Γ (n : nat) : {E;Δ;Γ} ⊨ #n ≤log≤ #n : TNat.
   Proof.
     value_case.
   Qed.
 
-  Lemma bin_log_related_bool Δ Γ (b : bool) : {E;Δ;Γ} ⊨ # b ≤log≤ # b : TBool.
+  Lemma bin_log_related_bool Δ Γ (b : bool) : {E;Δ;Γ} ⊨ #b ≤log≤ #b : Bool.
   Proof.
     value_case.
   Qed.

theories/logrel/logrel_binary.v

@@ -35,22 +35,39 @@ End bin_log_def.
 Notation "⟦ Γ ⟧*" := (interp_env Γ).
 
 Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related E1 E2 Δ Γ e%E e'%E τ)
+  (bin_log_related E1 E2 Δ Γ e%E e'%E (τ)%F)
   (at level 74, E1 at level 50, E2 at next level,
-   Δ at next level, Γ at next level, e, e', τ at next level,
+   Δ at next level, Γ at next level, e, e' at next level,
+   τ at level 98,
    format "'[hv' '{' E1 ',' E2 ';'  Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
 Notation "'{' E ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related E E Δ Γ e%E e'%E τ)
-  (at level 74, E at level 50, Δ at next level, Γ at next level, e, e', τ at next level,
+  (bin_log_related E E Δ Γ e%E e'%E (τ)%F)
+  (at level 74, E at level 50, Δ at next level, Γ at next level, e, e' at next level,
+   τ at level 98,
    format "'[hv' '{' E ';'  Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
 Notation "'{' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related ⊤ ⊤ Δ Γ e%E e'%E τ)
-  (at level 74, Δ at level 50, Γ at next level, e, e', τ at next level,
+  (bin_log_related ⊤ ⊤ Δ Γ e%E e'%E (τ)%F)
+  (at level 74, Δ at level 50, Γ at next level, e, e' at next level,
+   τ at level 98,
    format "'[hv' '{' Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
 Notation "Γ ⊨ e '≤log≤' e' : τ" :=
-  (∀ Δ, bin_log_related ⊤ ⊤ Δ Γ e%E e'%E τ)%I
-  (at level 74, e, e', τ at next level,
+  (∀ Δ, bin_log_related ⊤ ⊤ Δ Γ e%E e'%E (τ)%F)%I
+  (at level 74, e, e' at next level,
+   τ at level 98,
    format "'[hv' Γ  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
+(* TODO: 
+If I set the level for τ at 98 then the 
+following wouldn't pass:
+
+Lemma refinement1 `{logrelG Σ} Γ :
+    Γ ⊨ #() ≤log≤ #() : (Unit → Unit) → TNat.
+
+If the level is 99 then the following is not parsed.
+
+
+   Lemma refinement1 `{logrelG Σ} Γ :
+    Γ ⊨ #() ≤log≤ #() : (Unit → Unit) → TNat -∗ True.
+*)
 
 (** [interp_env] properties *)
 Section interp_env_facts.

theories/logrel/proofmode/tactics_rel.v

@@ -92,6 +92,8 @@ Tactic Notation "rel_vals" :=
   iStartProof;
   iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | simpl ].
 
+Tactic Notation "rel_finish" := by (rel_vals; simpl; eauto).
+
 Tactic Notation "rel_apply_l" open_constr(lem) :=
   (iPoseProofCore lem as false true (fun H =>
     rel_reshape_cont_l ltac:(fun K e =>
@@ -226,7 +228,7 @@ Tactic Notation "rel_pack_r" := rel_unpack_r.
 Lemma tac_rel_fork_l `{logrelG Σ} ℶ Δ E1 E2 e' K eres Γ e t τ :
   e = fill K (Fork e') →
   Closed ∅ e' →
-  eres = fill K (Lit Unit) →
+  eres = fill K Unit →
   envs_entails ℶ (|={E1,E2}=> ▷ WP e' {{ _ , True%I }} ∗ bin_log_related E2 E1 Δ Γ eres t τ) →
   envs_entails ℶ (bin_log_related E1 E1 Δ Γ e t τ).
 Proof.
@@ -247,7 +249,7 @@ Lemma tac_rel_fork_r `{logrelG Σ} ℶ Δ E1 E2 e' K Γ e t eres τ :
   nclose specN ⊆ E1 →
   e = fill K (Fork e') →
   Closed ∅ e' →
-  eres = fill K (Lit Unit) →
+  eres = fill K Unit →
   envs_entails ℶ (∀ i, i ⤇ e' -∗ bin_log_related E1 E2 Δ Γ t eres τ) →
   envs_entails ℶ (bin_log_related E1 E2 Δ Γ t e τ).
 Proof.
@@ -381,7 +383,7 @@ Lemma tac_rel_store_l_simp `{logrelG Σ} ℶ1 ℶ2 ℶ3 i1 E1 Δ Γ K (l : loc)
   IntoLaterNEnvs 1 ℶ1 ℶ2 →
   envs_lookup i1 ℶ2 = Some (false, l ↦ᵢ v)%I →
   envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) ℶ2 = Some ℶ3 →
-  eres = fill K (Lit Unit) →
+  eres = fill K Unit →
   envs_entails ℶ3 (bin_log_related E1 E1 Δ Γ eres t τ) →
   envs_entails ℶ1 (bin_log_related E1 E1 Δ Γ e t τ).
 Proof.
@@ -412,7 +414,7 @@ Lemma tac_rel_store_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) t' v' e
   to_val t' = Some v' →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
   envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) ℶ1 = Some ℶ2 →
-  tres = fill K (Lit Unit) →
+  tres = fill K Unit →
   envs_entails ℶ2 (bin_log_related E1 E2 Δ Γ e tres τ) →
   envs_entails ℶ1 (bin_log_related E1 E2 Δ Γ e t τ).
 Proof.

theories/logrel/proofmode/tactics_threadpool.v

@@ -77,7 +77,7 @@ Lemma tac_tp_store `{logrelG Σ} j Δ1 Δ2 Δ3 E1 ρ i1 i2 i3 p K' e l e' v' v Q
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I →
   to_val e' = Some v →
   envs_simple_replace i3 false
-     (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (Lit Unit))) i3 (l ↦ₛ v)) Δ2 = Some Δ3 →
+     (Esnoc (Esnoc Enil i2 (j ⤇ fill K' Unit)) i3 (l ↦ₛ v)) Δ2 = Some Δ3 →
   (envs_entails Δ3 Q) →
   (envs_entails Δ1 Q).
 Proof.
@@ -335,7 +335,7 @@ Lemma tac_tp_fork `{logrelG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' Q :
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
   e = fill K' (Fork e') →
   envs_simple_replace i2 false 
-    (Esnoc Enil i2 (j ⤇ fill K' (Lit Unit))) Δ1 = Some Δ2 →
+    (Esnoc Enil i2 (j ⤇ fill K' Unit)) Δ1 = Some Δ2 →
   envs_entails Δ2 (∀ (j' : nat), j' ⤇ e' -∗ |={E1,E2}=> Q)%I →
   envs_entails Δ1 (|={E1,E2}=> Q).
 Proof.