Commit 8ca83760 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

More instances for monPred.

parent 66a41586
...@@ -739,8 +739,8 @@ Qed. ...@@ -739,8 +739,8 @@ Qed.
Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') := Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') :=
make_embed : P Q. make_embed : P Q.
Arguments MakeMorphism {_ _ _} _%I _%I. Arguments MakeMorphism {_ _ _} _%I _%I.
Global Instance make_embed_true `{BiEmbedding PROP PROP'} : Global Instance make_embed_pure `{BiEmbedding PROP PROP'} φ :
MakeMorphism True True. MakeMorphism ⌜φ⌝ ⌜φ⌝.
Proof. by rewrite /MakeMorphism bi_embed_pure. Qed. Proof. by rewrite /MakeMorphism bi_embed_pure. Qed.
Global Instance make_embed_emp `{BiEmbedding PROP PROP'} : Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
MakeMorphism emp emp. MakeMorphism emp emp.
......
...@@ -6,147 +6,218 @@ Section bi. ...@@ -6,147 +6,218 @@ Section bi.
Context {I : bi_index} {PROP : bi}. Context {I : bi_index} {PROP : bi}.
Local Notation monPred := (monPred I PROP). Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred. Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : PROP.
Implicit Types φ : Prop. Implicit Types φ : Prop.
Implicit Types i j : I. Implicit Types i j : I.
Global Instance as_valid_monPred_car φ P : Class MakeMonPredCar i P 𝓟 :=
AsValid φ P AsValid φ ( i, P i). make_monPred_car : P i 𝓟.
Arguments MakeMonPredCar _ _%I _%I.
Global Instance make_monPred_car_pure φ i : MakeMonPredCar i ⌜φ⌝ ⌜φ⌝.
Proof. rewrite /MakeMonPredCar. by unseal. Qed.
Global Instance make_monPred_car_emp i : MakeMonPredCar i emp emp.
Proof. rewrite /MakeMonPredCar. by unseal. Qed.
Global Instance make_monPred_car_embed i : MakeMonPredCar i P P.
Proof. rewrite /MakeMonPredCar. by unseal. Qed.
Global Instance make_monPred_car_in i j : MakeMonPredCar j (monPred_in i) i j.
Proof. rewrite /MakeMonPredCar. by unseal. Qed.
Global Instance make_monPred_car_default i P : MakeMonPredCar i P (P i) | 100.
Proof. by rewrite /MakeMonPredCar. Qed.
Global Instance as_valid_monPred_car φ P (Φ : I PROP) :
AsValid φ P ( i, MakeMonPredCar i P (Φ i)) AsValid φ ( i, Φ i).
Proof. Proof.
rewrite /AsValid /bi_valid=> ->; unseal; split. rewrite /MakeMonPredCar /AsValid /bi_valid=> -> EQ. setoid_rewrite <-EQ.
unseal; split.
- move=>[/= /bi.forall_intro //]. - move=>[/= /bi.forall_intro //].
- move=>H. split=>i. rewrite /= H bi.forall_elim //. - move=>H. split=>i. rewrite /= H bi.forall_elim //.
Qed. Qed.
Global Instance into_pure_monPred_car P φ i : IntoPure P φ IntoPure (P i) φ. Global Instance into_pure_monPred_car P φ i :
Proof. rewrite /IntoPure=> ->. by unseal. Qed. IntoPure P φ IntoPure (P i) φ.
Global Instance from_pure_monPred_car P φ i : FromPure P φ FromPure (P i) φ. Proof. rewrite /IntoPure=>->. by unseal. Qed.
Proof. rewrite /FromPure=> <-. by unseal. Qed. Global Instance from_pure_monPred_car P φ i :
FromPure P φ FromPure (P i) φ.
Proof. rewrite /FromPure=><-. by unseal. Qed.
Global Instance into_pure_monPred_in i j :
@IntoPure PROP (monPred_in i j) (i j).
Proof. rewrite /IntoPure. by unseal. Qed.
Global Instance from_pure_monPred_in i j :
@FromPure PROP (monPred_in i j) (i j).
Proof. rewrite /FromPure. by unseal. Qed.
Global Instance into_internal_eq_monPred_car {A : ofeT} (x y : A) P i : Global Instance into_internal_eq_monPred_car {A : ofeT} (x y : A) P i :
IntoInternalEq P x y IntoInternalEq (P i) x y. IntoInternalEq P x y IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEq=> ->. by unseal. Qed. Proof. rewrite /IntoInternalEq=> ->. by unseal. Qed.
Global Instance into_persistent_monPred_car p P Q i: Global Instance into_persistent_monPred_car p P Q 𝓠 i :
IntoPersistent p P Q IntoPersistent p (P i) (Q i) | 0. IntoPersistent p P Q MakeMonPredCar i Q 𝓠 IntoPersistent p (P i) 𝓠 | 0.
Proof. Proof.
rewrite /IntoPersistent /bi_persistently_if. unseal=>-[/(_ i)]. rewrite /IntoPersistent /MakeMonPredCar /bi_persistently_if.
by destruct p. unseal=>-[/(_ i) ?] <-. by destruct p.
Qed. Qed.
Global Instance from_always_monPred_car a pe P Q i :
FromAlways a pe false P Q FromAlways a pe false (P i) (Q i) | 0. Global Instance from_always_monPred_car a pe P Q 𝓠 i :
FromAlways a pe false P Q MakeMonPredCar i Q 𝓠
FromAlways a pe false (P i) 𝓠 | 0.
Proof. Proof.
rewrite /FromAlways /bi_persistently_if /bi_affinely_if=><-. rewrite /FromAlways /MakeMonPredCar /bi_persistently_if /bi_affinely_if=><-.
by destruct a, pe; try unseal. by destruct a, pe=><-; try unseal.
Qed. Qed.
Global Instance into_wand_monPred_car p q R P Q i : Global Instance into_wand_monPred_car p q R P 𝓟 Q 𝓠 i :
IntoWand p q R P Q IntoWand p q (R i) (P i) (Q i). IntoWand p q R P Q MakeMonPredCar i P 𝓟 MakeMonPredCar i Q 𝓠
IntoWand p q (R i) 𝓟 𝓠.
Proof. Proof.
rewrite /IntoWand /bi_affinely_if /bi_persistently_if=>/bi.wand_elim_l' <-. rewrite /IntoWand /MakeMonPredCar /bi_affinely_if /bi_persistently_if.
apply bi.wand_intro_r. by destruct p, q; unseal. destruct p, q=> /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r;
revert H; unseal; done.
Qed.
Global Instance from_forall_monPred_car_wand P Q (Φ Ψ : I PROP) i :
( j, MakeMonPredCar j P (Φ j)) ( j, MakeMonPredCar j Q (Ψ j))
FromForall ((P - Q) i)%I (λ j, i j Φ j - Ψ j)%I.
Proof.
rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2.
setoid_rewrite H1. setoid_rewrite H2. done.
Qed.
Global Instance into_forall_monPred_car_wand P Q (Φ Ψ : I PROP) i :
( j, MakeMonPredCar j P (Φ j)) ( j, MakeMonPredCar j Q (Ψ j))
IntoForall ((P - Q) i) (λ j, i j Φ j - Ψ j)%I.
Proof.
rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2.
setoid_rewrite H1. setoid_rewrite H2. done.
Qed.
Global Instance from_forall_monPred_car_impl P Q (Φ Ψ : I PROP) i :
( j, MakeMonPredCar j P (Φ j)) ( j, MakeMonPredCar j Q (Ψ j))
FromForall ((P Q) i)%I (λ j, i j Φ j Ψ j)%I.
Proof.
rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2.
setoid_rewrite H1. setoid_rewrite H2. done.
Qed.
Global Instance into_forall_monPred_car_impl P Q (Φ Ψ : I PROP) i :
( j, MakeMonPredCar j P (Φ j)) ( j, MakeMonPredCar j Q (Ψ j))
IntoForall ((P Q) i) (λ j, i j Φ j Ψ j)%I.
Proof.
rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2.
setoid_rewrite H1. setoid_rewrite H2. done.
Qed. Qed.
Global Instance from_forall_monPred_car_wand P Q i :
FromForall ((P - Q) i)%I (λ j, i j P j - Q j)%I.
Proof. rewrite /FromForall. by unseal. Qed.
Global Instance into_forall_monPred_car_wand P Q i :
IntoForall ((P - Q) i) (λ j, i j P j - Q j)%I.
Proof. rewrite /IntoForall. by unseal. Qed.
Global Instance from_forall_monPred_car_impl P Q i :
FromForall ((P Q) i)%I (λ j, i j P j Q j)%I.
Proof. rewrite /FromForall. by unseal. Qed.
Global Instance into_forall_monPred_car_impl P Q i :
IntoForall ((P Q) i) (λ j, i j P j Q j)%I.
Proof. rewrite /IntoForall. by unseal. Qed.
Global Instance from_and_monPred_car P Q1 Q2 i: Global Instance from_and_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
FromAnd P Q1 Q2 FromAnd (P i) (Q1 i) (Q2 i). FromAnd P Q1 Q2 MakeMonPredCar i Q1 𝓠1 MakeMonPredCar i Q2 𝓠2
Proof. rewrite /FromAnd=> <-. by unseal. Qed. FromAnd (P i) 𝓠1 𝓠2.
Global Instance into_and_monPred_car p P Q1 Q2 i: Proof. rewrite /FromAnd /MakeMonPredCar /MakeMonPredCar=> <- <- <-. by unseal. Qed.
IntoAnd p P Q1 Q2 IntoAnd p (P i) (Q1 i) (Q2 i). Global Instance into_and_monPred_car p P Q1 𝓠1 Q2 𝓠2 i :
IntoAnd p P Q1 Q2 MakeMonPredCar i Q1 𝓠1 MakeMonPredCar i Q2 𝓠2
IntoAnd p (P i) 𝓠1 𝓠2.
Proof. Proof.
rewrite /IntoAnd /bi_affinely_if /bi_persistently_if=>-[/(_ i)]. rewrite /IntoAnd /MakeMonPredCar /bi_affinely_if /bi_persistently_if.
by destruct p; unseal. destruct p=>-[/(_ i) H] <- <-; revert H; unseal; done.
Qed. Qed.
Global Instance from_sep_monPred_car P Q1 Q2 i: Global Instance from_sep_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
FromSep P Q1 Q2 FromSep (P i) (Q1 i) (Q2 i). FromSep P Q1 Q2 MakeMonPredCar i Q1 𝓠1 MakeMonPredCar i Q2 𝓠2
Proof. rewrite /FromSep=> <-. by unseal. Qed. FromSep (P i) 𝓠1 𝓠2.
Global Instance into_sep_monPred_car P Q1 Q2 i: Proof. rewrite /FromSep /MakeMonPredCar=> <- <- <-. by unseal. Qed.
IntoSep P Q1 Q2 IntoSep (P i) (Q1 i) (Q2 i). Global Instance into_sep_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
Proof. rewrite /IntoSep=> ->. by unseal. Qed. IntoSep P Q1 Q2 MakeMonPredCar i Q1 𝓠1 MakeMonPredCar i Q2 𝓠2
IntoSep (P i) 𝓠1 𝓠2.
Global Instance from_or_monPred_car P Q1 Q2 i: Proof. rewrite /IntoSep /MakeMonPredCar=> -> <- <-. by unseal. Qed.
FromOr P Q1 Q2 FromOr (P i) (Q1 i) (Q2 i).
Proof. rewrite /FromOr=> <-. by unseal. Qed. Global Instance from_or_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
Global Instance into_or_monPred_car P Q1 Q2 i: FromOr P Q1 Q2 MakeMonPredCar i Q1 𝓠1 MakeMonPredCar i Q2 𝓠2
IntoOr P Q1 Q2 IntoOr (P i) (Q1 i) (Q2 i). FromOr (P i) 𝓠1 𝓠2.
Proof. rewrite /IntoOr=> ->. by unseal. Qed. Proof. rewrite /FromOr /MakeMonPredCar=> <- <- <-. by unseal. Qed.
Global Instance into_or_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
Global Instance from_exist_monPred_car {A} P (Φ : A monPred) i : IntoOr P Q1 Q2 MakeMonPredCar i Q1 𝓠1 MakeMonPredCar i Q2 𝓠2
FromExist P Φ FromExist (P i) (λ a, Φ a i). IntoOr (P i) 𝓠1 𝓠2.
Proof. rewrite /FromExist=><-. by unseal. Qed. Proof. rewrite /IntoOr /MakeMonPredCar=> -> <- <-. by unseal. Qed.
Global Instance into_exist_monPred_car {A} P (Φ : A monPred) i :
IntoExist P Φ IntoExist (P i) (λ a, Φ a i). Global Instance from_exist_monPred_car {A} P (Φ : A monPred) (Ψ : A PROP) i :
Proof. rewrite /IntoExist=>->. by unseal. Qed. FromExist P Φ ( a, MakeMonPredCar i (Φ a) (Ψ a)) FromExist (P i) Ψ.
Proof.
Global Instance from_forall_monPred_car {A} P (Φ : A monPred) i : rewrite /FromExist /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
FromForall P Φ FromForall (P i) (λ a, Φ a i). Qed.
Proof. rewrite /FromForall=><-. by unseal. Qed. Global Instance into_exist_monPred_car {A} P (Φ : A monPred) (Ψ : A PROP) i :
Global Instance into_forall_monPred_car {A} P (Φ : A monPred) i : IntoExist P Φ ( a, MakeMonPredCar i (Φ a) (Ψ a)) IntoExist (P i) Ψ.
IntoForall P Φ IntoForall (P i) (λ a, Φ a i). Proof.
Proof. rewrite /IntoForall=>->. by unseal. Qed. rewrite /IntoExist /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
Qed.
Class MakeMonPredCar i P (Q : PROP) :=
make_monPred_car : P i Q. Global Instance from_forall_monPred_car {A} P (Φ : A monPred) (Ψ : A PROP) i :
Arguments MakeMonPredCar _ _%I _%I. FromForall P Φ ( a, MakeMonPredCar i (Φ a) (Ψ a)) FromForall (P i) Ψ.
Global Instance make_monPred_car_true i : MakeMonPredCar i True True. Proof.
Proof. rewrite /MakeMonPredCar. by unseal. Qed. rewrite /FromForall /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
Global Instance make_monPred_car_emp i : MakeMonPredCar i emp emp. Qed.
Proof. rewrite /MakeMonPredCar. by unseal. Qed. Global Instance into_forall_monPred_car {A} P (Φ : A monPred) (Ψ : A PROP) i :
Global Instance make_monPred_car_default i P : MakeMonPredCar i P (P i). IntoForall P Φ ( a, MakeMonPredCar i (Φ a) (Ψ a)) IntoForall (P i) Ψ.
Proof. by rewrite /MakeMonPredCar. Qed. Proof.
rewrite /IntoForall /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
Qed.
Global Instance from_forall_monPred_car_all P (Φ : I PROP) i :
( i, MakeMonPredCar i P (Φ i)) FromForall (monPred_all P i) Φ.
Proof.
rewrite /FromForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
Qed.
Global Instance into_forall_monPred_car_all P (Φ : I PROP) i :
( i, MakeMonPredCar i P (Φ i)) IntoForall (monPred_all P i) Φ.
Proof.
rewrite /IntoForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
Qed.
(* FIXME : there are two good ways to frame under a call to (* FIXME : there are two good ways to frame under a call to
monPred_car. This may cause some backtracking in the typeclass monPred_car. This may cause some backtracking in the typeclass
search, and hence performance issues. *) search, and hence performance issues. *)
Global Instance frame_monPred_car i p P Q (Q' : PROP) R : Global Instance frame_monPred_car i p P Q 𝓠 R :
Frame p R P Q MakeMonPredCar i Q Q' Frame p (R i) (P i) Q'. Frame p R P Q MakeMonPredCar i Q 𝓠 Frame p (R i) (P i) 𝓠.
Proof. Proof.
rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-. rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
by destruct p; unseal. by destruct p; unseal.
Qed. Qed.
Global Instance frame_monPred_car_embed i p P Q (Q' R: PROP) : Global Instance frame_monPred_car_embed i p P Q 𝓠 𝓡 :
Frame p R P Q MakeMonPredCar i Q Q' Frame p R (P i) Q'. Frame p 𝓡 P Q MakeMonPredCar i Q 𝓠 Frame p 𝓡 (P i) 𝓠.
Proof. Proof.
rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-. rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
by destruct p; unseal. by destruct p; unseal.
Qed. Qed.
Global Instance from_modal_monPred_car i P Q : Global Instance from_modal_monPred_car i P Q 𝓠 :
FromModal P Q FromModal (P i) (Q i). FromModal P Q MakeMonPredCar i Q 𝓠 FromModal (P i) 𝓠.
Proof. by rewrite /FromModal=>->. Qed. Proof. by rewrite /FromModal /MakeMonPredCar=> <- <-. Qed.
End bi. End bi.
Hint Mode MakeMonPredCar + + - ! -.
Section sbi. Section sbi.
Context {I : bi_index} {PROP : sbi}. Context {I : bi_index} {PROP : sbi}.
Local Notation monPred := (monPred I PROP). Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred. Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : PROP.
Implicit Types φ : Prop. Implicit Types φ : Prop.
Implicit Types i j : I. Implicit Types i j : I.
Global Instance is_except_0_monPred_car i P : Global Instance is_except_0_monPred_car i P :
IsExcept0 P IsExcept0 (P i). IsExcept0 P IsExcept0 (P i).
Proof. rewrite /IsExcept0=>- [/(_ i)]. by unseal. Qed. Proof. rewrite /IsExcept0=>- [/(_ i)]. by unseal. Qed.
Global Instance into_except_0_monPred_car i P Q :
IntoExcept0 P Q IntoExcept0 (P i) (Q i). Global Instance into_except_0_monPred_car_fwd i P Q 𝓠 :
Proof. rewrite /IntoExcept0=> ->. by unseal. Qed. IntoExcept0 P Q MakeMonPredCar i Q 𝓠 IntoExcept0 (P i) 𝓠.
Global Instance into_later_monPred_car i n P Q : Proof. rewrite /IntoExcept0 /MakeMonPredCar=> -> <-. by unseal. Qed.
IntoLaterN n P Q IntoLaterN n (P i) (Q i). Global Instance into_except_0_monPred_car_bwd i P 𝓟 Q :
IntoExcept0 P Q MakeMonPredCar i P 𝓟 IntoExcept0 𝓟 (Q i).
Proof. rewrite /IntoExcept0 /MakeMonPredCar=> H <-. rewrite H. by unseal. Qed.
Global Instance into_later_monPred_car i n P Q 𝓠 :
IntoLaterN n P Q MakeMonPredCar i Q 𝓠 IntoLaterN n (P i) 𝓠.
Proof. Proof.
rewrite /IntoLaterN=> ->. induction n as [|? IH]=>//. rewrite /= -IH. by unseal. rewrite /IntoLaterN /MakeMonPredCar=> -> <-.
induction n as [|? IH]=>//. rewrite /= -IH. by unseal.
Qed. Qed.
Global Instance from_later_monPred_car i n P Q : Global Instance from_later_monPred_car i n P Q 𝓠 :
FromLaterN n P Q FromLaterN n (P i) (Q i). FromLaterN n P Q MakeMonPredCar i Q 𝓠 FromLaterN n (P i) 𝓠.
Proof. Proof.
rewrite /FromLaterN=> <-. induction n as [|? IH]=>//. rewrite /= IH. by unseal. rewrite /FromLaterN /MakeMonPredCar=> <- <-.
induction n as [|? IH]=>//. rewrite /= IH. by unseal.
Qed. Qed.
End sbi. End sbi.
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