Prove always_if_pure.

7293e063 · Robbert Krebbers · 648f146d · 7293e063
Commit 7293e063 authored Sep 28, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

algebra/upred.v algebra/upred.v +3 -0

No files found.
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1081,6 +1081,9 @@ Lemma always_if_elim p P : □?p P ⊢ P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
 Lemma always_elim_if p P : □ P ⊢ □?p P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
+
+Lemma always_if_pure p φ : □?p ■ φ ⊣⊢ ■ φ.
+Proof. destruct p; simpl; auto using always_pure. Qed.
 Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
 Proof. destruct p; simpl; auto using always_and. Qed.
 Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.