Skip to content
GitLab
Commit 6c0eb97a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix Absolute instances.

parent cb0d0dc9
Pipeline #6599 passed with stages
in 3 minutes and 43 seconds
Hide whitespace changes
Inline Side-by-side
theories/bi/monpred.v
View file @ 6c0eb97a
......@@ -635,7 +635,7 @@ Global Instance plainly_absolute P : Absolute (bi_plainly P).
Proof. apply emb_absolute. Qed.
Global Instance absolutely_absolute P : Absolute (∀ᵢ P).
Proof. apply emb_absolute. Qed.
Global Instance monPred_relatively_absolute P : Absolute (∃ᵢ P).
Global Instance relatively_absolute P : Absolute (∃ᵢ P).
Proof. apply emb_absolute. Qed.
Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q).
......@@ -653,7 +653,7 @@ Global Instance forall_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
@Absolute I PROP (∀ x, Φ x)%I.
Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
Global Instance exists_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
@Absolute I PROP (∀ x, Φ x)%I.
@Absolute I PROP (∃ x, Φ x)%I.
Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∗ 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