From 01eb6f6abf50021f939fc3535a2b98bab945b3e8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 19 Feb 2016 13:38:14 +0100
Subject: [PATCH] =?UTF-8?q?Tweak=20notations=20for=20Hoare=20triples=20{{?=
 =?UTF-8?q?=20P=20}}=20e=20@=20E=20{{=20=CE=A6=20}}?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Put level of the triple at 20, so we can write things like
  ▷ {{ P }} e @ E {{ Φ }} without parentheses.
* Use high levels for P, e and Φ.
* Allow @ E to be omitted in case E = ⊤.
---
 barrier/barrier.v             |  8 ++++----
 heap_lang/tests.v             |  2 +-
 program_logic/adequacy.v      |  6 +++---
 program_logic/hoare.v         | 14 +++++++++++---
 program_logic/hoare_lifting.v |  6 ++++--
 5 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index bf8cf050d..9e7464364 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -260,10 +260,10 @@ Section spec.
   Lemma barrier_spec (heapN N : namespace) :
     heapN ⊥ N →
     ∃ (recv send : loc -> iProp -n> iProp),
-      (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() @ ⊤ {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧
-      (∀ l P, {{ send l P ★ P }} signal (LocV l) @ ⊤ {{ λ _, True }}) ∧
-      (∀ l P, {{ recv l P }} wait (LocV l) @ ⊤ {{ λ _, P }}) ∧
-      (∀ l P Q, {{ recv l (P ★ Q) }} Skip @ ⊤ {{ λ _, recv l P ★ recv l Q }}) ∧
+      (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧
+      (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧
+      (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧
+      (∀ l P Q, {{ recv l (P ★ Q) }} Skip {{ λ _, recv l P ★ recv l Q }}) ∧
       (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)).
   Proof.
     intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)).
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index afc88d836..973c42488 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -86,7 +86,7 @@ Section ClosedProofs.
   Instance: authG heap_lang Σ heapRA.
   Proof. split; try apply _. by exists 1%nat. Qed.
 
-  Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e @ ⊤ {{ λ v, v = '2 }}.
+  Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
   Proof.
     apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 60bc36609..6ddf73e2f 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -53,7 +53,7 @@ Proof.
     by rewrite -Permutation_middle /= big_op_app.
 Qed.
 Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
-  {{ P }} e1 @ ⊤ {{ Φ }} →
+  {{ P }} e1 {{ Φ }} →
   nsteps step k ([e1],σ1) (t2,σ2) →
   1 < n → wsat (k + n) ⊤ σ1 r1 →
   P (k + n) r1 →
@@ -66,8 +66,8 @@ Proof.
   eapply uPred.const_intro; eauto.
 Qed.
 Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
-  ✓m →
-  {{ ownP σ1 ★ ownG m }} e1 @ ⊤ {{ Φ }} →
+  ✓ m →
+  {{ ownP σ1 ★ ownG m }} e1 {{ Φ }} →
   rtc step ([e1],σ1) (t2,σ2) →
   ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
 Proof.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 8924ef906..116c9da53 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,13 +1,21 @@
 From program_logic Require Export weakestpre viewshifts.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
-    (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → wp E e Φ))%I.
+  (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → wp E e Φ))%I.
 Instance: Params (@ht) 3.
 
 Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
+Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e Φ)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
 Notation "{{ P } } e @ E {{ Φ } }" := (True ⊑ ht E P e Φ)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e {{ Φ } }" := (True ⊑ ht ⊤ P e Φ)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
 Section hoare.
 Context {Λ : language} {Σ : iFunctor}.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 08245964c..cda141782 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -4,10 +4,12 @@ Import uPred.
 
 Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
   (default True%I ef (λ e, ht E P e Φ))
-  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : uPred_scope.
+  (at level 20, P, ef, Φ at level 200,
+   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : uPred_scope.
 Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
   (True ⊑ default True ef (λ e, ht E P e Φ))
-  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
+  (at level 20, P, ef, Φ at level 200,
+   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
 
 Section lifting.
 Context {Λ : language} {Σ : iFunctor}.
-- 
GitLab