Commit 01eb6f6a by Robbert Krebbers

### Tweak notations for Hoare triples {{ P }} e @ E {{ Φ }}

```* 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 = ⊤.```
parent 397250e0
 ... @@ -260,10 +260,10 @@ Section spec. ... @@ -260,10 +260,10 @@ Section spec. Lemma barrier_spec (heapN N : namespace) : Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → heapN ⊥ N → ∃ (recv send : loc -> iProp -n> iProp), ∃ (recv send : loc -> iProp -n> iProp), (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() @ ⊤ {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧ (∀ 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, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) @ ⊤ {{ λ _, P }}) ∧ (∀ 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, {{ recv l (P ★ Q) }} Skip {{ λ _, recv l P ★ recv l Q }}) ∧ (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)). (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)). Proof. Proof. intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)). intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)). ... ...
 ... @@ -86,7 +86,7 @@ Section ClosedProofs. ... @@ -86,7 +86,7 @@ Section ClosedProofs. Instance: authG heap_lang Σ heapRA. Instance: authG heap_lang Σ heapRA. Proof. split; try apply _. by exists 1%nat. Qed. 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. Proof. apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot. apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot. apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l. apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l. ... ...
 ... @@ -53,7 +53,7 @@ Proof. ... @@ -53,7 +53,7 @@ Proof. by rewrite -Permutation_middle /= big_op_app. by rewrite -Permutation_middle /= big_op_app. Qed. Qed. Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 : Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 : {{ P }} e1 @ ⊤ {{ Φ }} → {{ P }} e1 {{ Φ }} → nsteps step k ([e1],σ1) (t2,σ2) → nsteps step k ([e1],σ1) (t2,σ2) → 1 < n → wsat (k + n) ⊤ σ1 r1 → 1 < n → wsat (k + n) ⊤ σ1 r1 → P (k + n) r1 → P (k + n) r1 → ... @@ -66,8 +66,8 @@ Proof. ... @@ -66,8 +66,8 @@ Proof. eapply uPred.const_intro; eauto. eapply uPred.const_intro; eauto. Qed. Qed. Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 : Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 : ✓m → ✓ m → {{ ownP σ1 ★ ownG m }} e1 @ ⊤ {{ Φ }} → {{ ownP σ1 ★ ownG m }} e1 {{ Φ }} → rtc step ([e1],σ1) (t2,σ2) → rtc step ([e1],σ1) (t2,σ2) → ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2). ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2). Proof. Proof. ... ...
 From program_logic Require Export weakestpre viewshifts. From program_logic Require Export weakestpre viewshifts. Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ) 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. Instance: Params (@ht) 3. Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ) 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 Φ) 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. Section hoare. Context {Λ : language} {Σ : iFunctor}. Context {Λ : language} {Σ : iFunctor}. ... ...
 ... @@ -4,10 +4,12 @@ Import uPred. ... @@ -4,10 +4,12 @@ Import uPred. Local Notation "{{ P } } ef ?@ E {{ Φ } }" := Local Notation "{{ P } } ef ?@ E {{ Φ } }" := (default True%I ef (λ e, ht E P 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 {{ Φ } }" := Local Notation "{{ P } } ef ?@ E {{ Φ } }" := (True ⊑ default True ef (λ e, ht E P 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. Section lifting. Context {Λ : language} {Σ : iFunctor}. Context {Λ : language} {Σ : iFunctor}. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!