Commit 56321b0f authored by Robbert Krebbers's avatar Robbert Krebbers

Remove `⌜φ⌝ ⊢ □ ⌜φ⌝` as a primitive rule, it can be derived.

parent 381e8509
......@@ -483,7 +483,12 @@ Lemma always_idemp P : □ □ P ⊣⊢ □ P.
Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
Lemma always_pure φ : ⌜φ⌝ ⌜φ⌝.
Proof. apply (anti_symm _); auto using always_pure_2. Qed.
Proof.
apply (anti_symm _); auto.
apply pure_elim'=> Hφ.
trans ( x : False, True : uPred M)%I; [by apply forall_intro|].
rewrite always_forall_2. auto using always_mono, pure_intro.
Qed.
Lemma always_forall {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof.
apply (anti_symm _); auto using always_forall_2.
......
......@@ -430,8 +430,6 @@ Qed.
Lemma always_idemp_2 P : P P.
Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
Lemma always_pure_2 φ : ⌜φ⌝ ⌜φ⌝.
Proof. by unseal. Qed.
Lemma always_forall_2 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof. by unseal. Qed.
Lemma always_exist_1 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
......
Markdown is supported
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