Commit 84da47cb authored by Ralf Jung's avatar Ralf Jung

WIP: try to prove more rules for salways

parent d7d1317d
......@@ -296,12 +296,22 @@ Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
Proof. by intros ->. Qed.
Lemma internal_eq_sym {A : ofeT} (a b : A) : a b b a.
Proof. apply (internal_eq_rewrite a b (λ b, b a)%I); auto. solve_proper. Qed.
Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A uPred M) P
{HΨ : NonExpansive Ψ} : (P b a) (P Ψ a) P Ψ b.
Proof. intros HP. apply: internal_eq_rewrite. rewrite HP. exact: internal_eq_sym. Qed.
Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A uPred M) P
{HΨ : Contractive Ψ} : (P (a b)) (P Ψ a) P Ψ b.
Proof.
move: HΨ=> /contractiveI HΨ Heq ?.
apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
Qed.
Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A uPred M) P
{HΨ : Contractive Ψ} : (P (b a)) (P Ψ a) P Ψ b.
Proof.
intros HP. apply: internal_eq_rewrite_contractive.
rewrite HP. apply later_mono. exact: internal_eq_sym.
Qed.
Lemma pure_impl_forall φ P : (⌜φ⌝ P) ( _ : φ, P).
Proof.
......@@ -466,13 +476,29 @@ Proof.
by rewrite -(exist_intro a).
- apply exist_elim=> a; apply sep_mono; auto using exist_intro.
Qed.
Lemma sep_exist_r {A} (Φ: A uPred M) Q: ( a, Φ a) Q a, Φ a Q.
Lemma sep_exist_r {A} (Φ: A uPred M) Q : ( a, Φ a) Q a, Φ a Q.
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
Lemma sep_forall_l {A} P (Ψ : A uPred M) : P ( a, Ψ a) a, P Ψ a.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma sep_forall_r {A} (Φ : A uPred M) Q : ( a, Φ a) Q a, Φ a Q.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma and_forall_l {A} P (Ψ : A uPred M) : P ( a, Ψ a) a, P Ψ a.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma and_forall_r {A} (Φ : A uPred M) Q : ( a, Φ a) Q a, Φ a Q.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma exist_forall {A} (Ψ : A uPred M) :
( a, Ψ a) ( P : uPred M, ( a, Ψ a P) P).
Proof.
apply (anti_symm ()).
- apply exist_elim=>a. apply forall_intro=>P. apply impl_intro_r.
rewrite and_forall_l. rewrite (forall_elim a) impl_elim_r. done.
- rewrite (forall_elim ( a, Ψ a)%I). eapply impl_elim; first done.
apply forall_intro=>a. apply impl_intro_r. rewrite -[x in _ x](exist_intro a).
apply and_elim_r.
Qed.
(* Always derived *)
Hint Resolve always_mono always_elim.
Global Instance always_mono' : Proper (() ==> ()) (@uPred_always M).
......@@ -513,6 +539,9 @@ Proof.
rewrite -(internal_eq_refl a) always_pure; auto.
Qed.
Lemma always_intro_clearctx P Q : Q P Q.
Proof. intros <-. rewrite always_pure. apply True_intro. Qed.
Lemma always_and_sep P Q : (P Q) (P Q).
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
Lemma always_and_sep_l' P Q : P Q P Q.
......@@ -713,27 +742,117 @@ Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
(* Strong always. *)
Global Instance salways_ne : NonExpansive (@uPred_salways M).
Proof. solve_proper. Qed.
Global Instance salways_proper :
Proper (() ==> ()) (@uPred_salways M) := ne_proper _.
Lemma salways_mono P Q : (P Q) P Q.
Proof.
intros HPQ. rewrite /uPred_salways {2}(_ : True (P Q)); last first.
{ eapply (anti_symm ()); first exact: entails_impl. apply True_intro. }
eapply (internal_eq_rewrite _ _ (λ x, Q (x Q))%I); first solve_proper.
{ exact: internal_eq_sym. }
eapply (internal_eq_rewrite' _ _ (λ x, Q (x Q))%I); first solve_proper; first done.
apply equiv_internal_eq. eapply (anti_symm ()).
- apply impl_intro_l. rewrite left_id. done.
- eapply impl_elim; first done. apply True_intro.
Qed.
Global Instance salways_mono' : Proper (() ==> ()) (@uPred_salways M).
Proof. intros P Q; apply salways_mono. Qed.
Global Instance salways_flip_mono' :
Proper (flip () ==> flip ()) (@uPred_salways M).
Proof. intros P Q; apply salways_mono. Qed.
Lemma salways_elim P : P P.
Proof.
apply: (internal_eq_rewrite _ _ id).
- exact: internal_eq_sym.
- exact: True_intro.
Qed.
Lemma salways_intro P : P ( P)%I.
Lemma salways_intro_clearctx P Q : Q (P Q).
Proof.
intros HP. rewrite <-salways_mono; last done.
exact: internal_eq_refl.
exact: internal_eq_refl'.
Qed.
Lemma salways_idemp P : P P.
Proof.
rewrite /uPred_salways.
eapply (internal_eq_rewrite' _ _ (λ x, (x _) True)%I); first solve_proper; first done.
apply salways_intro_clearctx. apply internal_eq_refl.
Qed.
Lemma salways_intro P Q : ( P Q) P Q.
Proof. intros <-. apply salways_idemp. Qed.
Lemma salways_pure φ : ⌜φ⌝ ⌜φ⌝.
Proof.
apply (anti_symm ()).
- apply pure_elim'=>?. apply salways_intro_clearctx, pure_intro. done.
- by rewrite salways_elim.
Qed.
Lemma salways_always P : P P.
Proof.
apply (anti_symm ()).
- rewrite (salways_mono _ P); first done. apply always_elim.
- rewrite /uPred_salways.
eapply (internal_eq_rewrite' _ _ (λ x, x True)%I); first solve_proper; first done.
apply salways_intro_clearctx. rewrite always_pure. done.
Qed.
Lemma salways_forall {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof.
apply (anti_symm ()).
- apply forall_intro=>a. apply salways_mono. rewrite (forall_elim a) //.
- rewrite /uPred_salways. rewrite (internal_eq_forall Ψ (λ _, True)%I).
eapply (internal_eq_rewrite' _ _ (λ x, x True)%I); first solve_proper; first done.
apply salways_intro_clearctx. apply forall_intro=>_. done.
Qed.
Lemma salways_and P Q : (P Q) P Q.
Proof. rewrite !and_alt salways_forall. by apply forall_proper=> -[]. Qed.
Lemma salways_impl P Q : (P Q) P Q.
Proof.
apply impl_intro_l; rewrite -salways_and.
apply salways_mono, impl_elim with P; auto.
Qed.
(*
Lemma salways_impl' P Q: (■ P → ■ Q) ⊢ ■ (■ P → Q).
Proof.
rewrite /uPred_salways. unseal. split=>n x ? Himpl.
split=>n' x' ??. split; first done. intros _ n'' x'' ??? HP.
eapply Himpl with n'' x; try done. etrans; done. eapply cmra_validN_le; first done. omega.
Qed.
Lemma salways_or {A} (P Q : uPred M) : (■ (P ∨ Q)) ⊢ (■ P) ∨ (■ Q).
Proof. Abort.
Lemma salways_exist {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊣⊢ (∃ a, ■ Ψ a).
Proof.
apply (anti_symm (⊢)).
- rewrite exist_forall. rewrite (forall_elim (∃ a, ■ Ψ a)%I).
rewrite salways_impl [(■ ∃ a : A, ■ Ψ a)%I]salways_elim.
eapply impl_elim; first done.
rewrite salways_forall. apply forall_intro=>a.
rewrite salways_forall. apply forall_mono=>P.
rewrite salways_impl. apply impl_mono; last exact: salways_elim.
rewrite salways_forall. apply forall_mono=>a. rewrite salways_impl.
apply impl_intro_r. eapply impl_elim; first exact: and_elim_r.
apply forall_intro=>a. rewrite and_elim_r (forall_elim a). apply impl_mono.
rewrite /uPred_salways. etrans; last exact: (internal_eq_exist Ψ (λ _, True)%I).
rewrite -salways_always always_exist.
rewrite -[(■ _)%I](idemp (∧)%I) {1}salways_elim and_exist_r.
apply exist_elim=>a. rewrite -[x in _ ⊢ x](exist_intro a).
rewrite /uPred_salways. Abort.
Lemma salways_later P : ■ ▷ P ⊣⊢ ▷ ■ P.
Proof.
rewrite /uPred_salways. eapply (anti_symm (⊢)).
- rewrite -{1}later_True -later_equivI.
- eapply (internal_eq_rewrite_contractive' _ _ (λ x, ▷ x ≡ True)%I); first solve_contractive; first done.
apply equiv_internal_eq. apply later_True.
Abort.
*)
(* Own and valid derived *)
Lemma always_ownM (a : M) : Persistent a uPred_ownM a uPred_ownM a.
......
......@@ -379,6 +379,18 @@ Proof.
- by symmetry; apply Hab with x.
- by apply Ha.
Qed.
Lemma internal_eq_forall {A : Type} (Ψ1 Ψ2 : A uPred M) :
( x, Ψ1 x Ψ2 x) ( x, Ψ1 x) ( x, Ψ2 x).
Proof.
split=>n x ? Heq. rewrite uPred_internal_eq_eq. eapply forall_ne=>y.
move: Heq. unseal=>Heq. apply Heq.
Qed.
Lemma internal_eq_exist {A : Type} (Ψ1 Ψ2 : A uPred M) :
( x, Ψ1 x Ψ2 x) ( x, Ψ1 x) ( x, Ψ2 x).
Proof.
split=>n x ? Heq. rewrite uPred_internal_eq_eq. eapply exist_ne=>y.
move: Heq. unseal=>Heq. apply Heq.
Qed.
(* BI connectives *)
Lemma sep_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
......
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