Commit b3891ed5 authored by Robbert Krebbers's avatar Robbert Krebbers

Group iff properties in uPred.

parent 20c86477
Pipeline #2661 passed with stage
in 8 minutes and 58 seconds
......@@ -563,11 +563,6 @@ Proof.
Qed.
(* Derived logical stuff *)
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
Proper (() ==> () ==> ()) (@uPred_iff M) := ne_proper_2 _.
Lemma False_elim P : False P.
Proof. by apply (pure_elim False). Qed.
Lemma True_intro P : P True.
......@@ -606,16 +601,6 @@ Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
Lemma entails_impl P Q : (P Q) True P Q.
Proof. auto using impl_intro_l. Qed.
Lemma iff_refl Q P : Q P P.
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
Lemma iff_equiv P Q : (True P Q) (P Q).
Proof.
intros HPQ; apply (anti_symm ());
apply impl_entails; rewrite HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : (P Q) True P Q.
Proof. intros ->; apply iff_refl. Qed.
Lemma and_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
Proof. auto. Qed.
Lemma and_mono_l P P' Q : (P Q) P P' Q P'.
......@@ -783,10 +768,6 @@ Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
Proof. by intros ->. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : a b b a.
Proof. apply (eq_rewrite a b (λ b, b a)%I); auto. solve_proper. Qed.
Lemma eq_iff P Q : P Q P Q.
Proof.
apply (eq_rewrite P Q (λ Q, P Q))%I; first solve_proper; auto using iff_refl.
Qed.
Lemma pure_alt φ : φ _ : φ, True.
Proof.
......@@ -805,6 +786,25 @@ Proof.
apply or_elim. by rewrite -(exist_intro true). by rewrite -(exist_intro false).
Qed.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
Proper (() ==> () ==> ()) (@uPred_iff M) := ne_proper_2 _.
Lemma iff_refl Q P : Q P P.
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
Lemma iff_equiv P Q : (True P Q) (P Q).
Proof.
intros HPQ; apply (anti_symm ());
apply impl_entails; rewrite HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : (P Q) True P Q.
Proof. intros ->; apply iff_refl. Qed.
Lemma eq_iff P Q : P Q P Q.
Proof.
apply (eq_rewrite P Q (λ Q, P Q))%I; first solve_proper; auto using iff_refl.
Qed.
(* BI connectives *)
Lemma sep_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
Proof.
......
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