Commit b0eb3ed9 authored by Ralf Jung's avatar Ralf Jung
Browse files

formatting and nits

parent 6db3649f
......@@ -53,7 +53,7 @@ Proof.
- exact: persistently_idemp_2.
- (* emp ⊢ <pers> emp (ADMISSIBLE) *)
trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
+ apply forall_intro=>[[]].
+ apply forall_intro=>-[].
+ etrans; first exact: persistently_forall_2.
apply persistently_mono. exact: pure_intro.
- (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
......
......@@ -862,8 +862,7 @@ Lemma persistently_and P Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
Lemma persistently_or P Q : <pers> (P Q) <pers> P <pers> Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
Lemma persistently_impl P Q :
<pers> (P Q) <pers> P <pers> Q.
Lemma persistently_impl P Q : <pers> (P Q) <pers> P <pers> Q.
Proof.
apply impl_intro_l; rewrite -persistently_and.
apply persistently_mono, impl_elim with P; auto.
......
......@@ -107,7 +107,7 @@ Section bi_mixin.
The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
other laws. *)
bi_mixin_persistently_and_2 (P Q : PROP) :
((<pers> P) (<pers> Q)) <pers> (P Q);
(<pers> P) (<pers> Q) <pers> (P Q);
bi_mixin_persistently_exist_1 {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a);
......
......@@ -26,7 +26,8 @@ Section core.
by iApply "HPQ".
Qed.
Global Instance coreP_persistent `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
Global Instance coreP_persistent
`{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
Persistent (coreP P).
Proof.
rewrite /coreP /Persistent. iIntros "HC" (Q).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment