Commit 4ac0be9f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Proof mode instances for the plainness modality.

parent c6f4eac5
...@@ -19,6 +19,9 @@ Global Instance from_assumption_persistently_r P Q : ...@@ -19,6 +19,9 @@ Global Instance from_assumption_persistently_r P Q :
FromAssumption true P Q FromAssumption true P ( Q). FromAssumption true P Q FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed. Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed.
Global Instance from_assumption_plainly_l p P Q :
FromAssumption p P Q FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite plainly_elim. Qed.
Global Instance from_assumption_persistently_l p P Q : Global Instance from_assumption_persistently_l p P Q :
FromAssumption p P Q FromAssumption p ( P) Q. FromAssumption p P Q FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite persistently_elim. Qed. Proof. rewrite /FromAssumption=><-. by rewrite persistently_elim. Qed.
...@@ -48,6 +51,8 @@ Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) : ...@@ -48,6 +51,8 @@ Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
@IntoPure M ( a) ( a). @IntoPure M ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed. Proof. by rewrite /IntoPure discrete_valid. Qed.
Global Instance into_pure_plainly P φ : IntoPure P φ IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite plainly_pure. Qed.
Global Instance into_pure_persistently P φ : IntoPure P φ IntoPure ( P) φ. Global Instance into_pure_persistently P φ : IntoPure P φ IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed. Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed.
...@@ -95,6 +100,8 @@ Proof. ...@@ -95,6 +100,8 @@ Proof.
rewrite -cmra_valid_intro //. auto with I. rewrite -cmra_valid_intro //. auto with I.
Qed. Qed.
Global Instance from_pure_plainly P φ : FromPure P φ FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
Global Instance from_pure_persistently P φ : FromPure P φ FromPure ( P) φ. Global Instance from_pure_persistently P φ : FromPure P φ FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed. Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
Global Instance from_pure_later P φ : FromPure P φ FromPure ( P) φ. Global Instance from_pure_later P φ : FromPure P φ FromPure ( P) φ.
...@@ -254,6 +261,9 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 : ...@@ -254,6 +261,9 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
FromLaterN n P1 Q1 FromLaterN n P2 Q2 FromLaterN n (P1 P2) (Q1 Q2). FromLaterN n P1 Q1 FromLaterN n P2 Q2 FromLaterN n (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed. Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
Global Instance from_later_plainly n P Q :
FromLaterN n P Q FromLaterN n ( P) ( Q).
Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
Global Instance from_later_persistently n P Q : Global Instance from_later_persistently n P Q :
FromLaterN n P Q FromLaterN n ( P) ( Q). FromLaterN n P Q FromLaterN n ( P) ( Q).
Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed. Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
...@@ -306,6 +316,9 @@ Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed. ...@@ -306,6 +316,9 @@ Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
Global Instance into_wand_forall {A} p (Φ : A uPred M) P Q x : Global Instance into_wand_forall {A} p (Φ : A uPred M) P Q x :
IntoWand p (Φ x) P Q IntoWand p ( x, Φ x) P Q. IntoWand p (Φ x) P Q IntoWand p ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed. Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
Global Instance into_wand_plainly p R P Q :
IntoWand p R P Q IntoWand p ( R) P Q.
Proof. rewrite /IntoWand=> ->. by rewrite plainly_elim. Qed.
Global Instance into_wand_persistently p R P Q : Global Instance into_wand_persistently p R P Q :
IntoWand p R P Q IntoWand p ( R) P Q. IntoWand p R P Q IntoWand p ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed. Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
...@@ -343,6 +356,12 @@ Proof. intros. by rewrite /FromAnd and_sep_r. Qed. ...@@ -343,6 +356,12 @@ Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed. Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
Global Instance from_and_plainly p P Q1 Q2 :
FromAnd false P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2).
Proof.
intros. apply mk_from_and_and.
by rewrite plainly_and_sep_l' -plainly_sep -(from_and _ P).
Qed.
Global Instance from_and_persistently p P Q1 Q2 : Global Instance from_and_persistently p P Q1 Q2 :
FromAnd false P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2). FromAnd false P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2).
Proof. Proof.
...@@ -434,10 +453,14 @@ Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed. ...@@ -434,10 +453,14 @@ Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed. Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
Global Instance into_and_plainly p P Q1 Q2 :
IntoAnd true P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).
Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?plainly_and and_sep_r. Qed.
Global Instance into_and_persistently p P Q1 Q2 : Global Instance into_and_persistently p P Q1 Q2 :
IntoAnd true P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2). IntoAnd true P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).
Proof. Proof.
rewrite /IntoAnd=>->. destruct p; by rewrite ?persistently_and persistently_and_sep_r. rewrite /IntoAnd=>->.
destruct p; by rewrite ?persistently_and persistently_and_sep_r.
Qed. Qed.
Global Instance into_and_later p P Q1 Q2 : Global Instance into_and_later p P Q1 Q2 :
IntoAnd p P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2). IntoAnd p P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).
...@@ -619,6 +642,9 @@ Global Instance from_or_bupd P Q1 Q2 : ...@@ -619,6 +642,9 @@ Global Instance from_or_bupd P Q1 Q2 :
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed. Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance from_or_pure φ ψ : @FromOr M ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed. Proof. by rewrite /FromOr pure_or. Qed.
Global Instance from_or_plainly P Q1 Q2 :
FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
Global Instance from_or_persistently P Q1 Q2 : Global Instance from_or_persistently P Q1 Q2 :
FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2). FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed. Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
...@@ -637,6 +663,9 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q. ...@@ -637,6 +663,9 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
Proof. done. Qed. Proof. done. Qed.
Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed. Proof. by rewrite /IntoOr pure_or. Qed.
Global Instance into_or_plainly P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
Global Instance into_or_persistently P Q1 Q2 : Global Instance into_or_persistently P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr ( P) ( Q1) ( Q2). IntoOr P Q1 Q2 IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed. Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
...@@ -661,6 +690,9 @@ Qed. ...@@ -661,6 +690,9 @@ Qed.
Global Instance from_exist_pure {A} (φ : A Prop) : Global Instance from_exist_pure {A} (φ : A Prop) :
@FromExist M A x, φ x (λ a, ⌜φ a)%I. @FromExist M A x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed. Proof. by rewrite /FromExist pure_exist. Qed.
Global Instance from_exist_plainly {A} P (Φ : A uPred M) :
FromExist P Φ FromExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
Global Instance from_exist_persistently {A} P (Φ : A uPred M) : Global Instance from_exist_persistently {A} P (Φ : A uPred M) :
FromExist P Φ FromExist ( P) (λ a, (Φ a))%I. FromExist P Φ FromExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed. Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
...@@ -698,6 +730,9 @@ Proof. ...@@ -698,6 +730,9 @@ Proof.
apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ). apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed. Qed.
Global Instance into_exist_plainly {A} P (Φ : A uPred M) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Global Instance into_exist_persistently {A} P (Φ : A uPred M) : Global Instance into_exist_persistently {A} P (Φ : A uPred M) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I. IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed. Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
...@@ -714,6 +749,9 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed. ...@@ -714,6 +749,9 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
(* IntoForall *) (* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A uPred M) : IntoForall ( a, Φ a) Φ. Global Instance into_forall_forall {A} (Φ : A uPred M) : IntoForall ( a, Φ a) Φ.
Proof. done. Qed. Proof. done. Qed.
Global Instance into_forall_plainly {A} P (Φ : A uPred M) :
IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Global Instance into_forall_persistently {A} P (Φ : A uPred M) : Global Instance into_forall_persistently {A} P (Φ : A uPred M) :
IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I. IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed. Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
...@@ -768,6 +806,9 @@ Proof. ...@@ -768,6 +806,9 @@ Proof.
rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a). rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed. Qed.
Global Instance elim_modal_plainly P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal plainly_elim wand_elim_r. Qed.
Global Instance elim_modal_persistently P Q : ElimModal ( P) P Q Q. Global Instance elim_modal_persistently P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed. Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed.
......
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