Commit 314d8a2e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge remote-tracking branch 'origin/master' into gen_proofmode

parents 7c00020b db735a45
Pipeline #7014 passed with stage
in 34 minutes and 5 seconds
......@@ -1092,8 +1092,6 @@ Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
FromModal P Q FromModal P Q.
Proof. by rewrite /FromModal=> ->. Qed.
(* ElimModal *)
(* AsValid *)
Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
......@@ -1550,14 +1548,14 @@ Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
Global Instance frame_later p R R' P Q Q' :
NoBackTrack (MaybeIntoLaterN 1 R' R)
NoBackTrack (MaybeIntoLaterN true 1 R' R)
Frame p R P Q MakeLaterN 1 Q Q' Frame p R' ( P) Q'.
Proof.
rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
by rewrite later_affinely_persistently_if_2 later_sep.
Qed.
Global Instance frame_laterN p n R R' P Q Q' :
NoBackTrack (MaybeIntoLaterN n R' R)
NoBackTrack (MaybeIntoLaterN true n R' R)
Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'.
Proof.
rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
......@@ -1587,116 +1585,121 @@ Proof.
Qed.
(* IntoLater *)
Global Instance into_laterN_0 P : IntoLaterN 0 P P.
Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.
Global Instance into_laterN_later n n' m' P Q lQ :
Global Instance into_laterN_later only_head n n' m' P Q lQ :
NatCancel n 1 n' m'
(** If canceling has failed (i.e. [1 = m']), we should make progress deeper
into [P], as such, we continue with the [IntoLaterN] class, which is required
to make progress. If canceling has succeeded, we do not need to make further
progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
into [P], as such, we continue with [MaybeIntoLaterN]. *)
TCIf (TCEq 1 m') (IntoLaterN n' P Q) (MaybeIntoLaterN n' P Q)
TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q)
MakeLaterN m' Q lQ
IntoLaterN n ( P) lQ | 2.
IntoLaterN only_head n ( P) lQ | 2.
Proof.
rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
move=> Hn [_ ->|->] <-;
by rewrite -later_laterN -laterN_plus -Hn Nat.add_comm.
Qed.
Global Instance into_laterN_laterN n m n' m' P Q lQ :
Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
NatCancel n m n' m'
TCIf (TCEq m m') (IntoLaterN n' P Q) (MaybeIntoLaterN n' P Q)
TCIf (TCEq m m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q)
MakeLaterN m' Q lQ
IntoLaterN n (^m P) lQ | 1.
IntoLaterN only_head n (^m P) lQ | 1.
Proof.
rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
Qed.
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
IntoLaterN n P1 Q1 MaybeIntoLaterN n P2 Q2
IntoLaterN n (P1 P2) (Q1 Q2) | 10.
IntoLaterN false n P1 Q1 MaybeIntoLaterN false n P2 Q2
IntoLaterN false n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_and. Qed.
Global Instance into_laterN_and_r n P P2 Q2 :
IntoLaterN n P2 Q2 IntoLaterN n (P P2) (P Q2) | 11.
IntoLaterN false n P2 Q2 IntoLaterN false n (P P2) (P Q2) | 11.
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Qed.
Global Instance into_laterN_forall {A} n (Φ Ψ : A PROP) :
( x, IntoLaterN false n (Φ x) (Ψ x))
IntoLaterN false n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
Global Instance into_laterN_exist {A} n (Φ Ψ : A PROP) :
( x, IntoLaterN false n (Φ x) (Ψ x))
IntoLaterN false n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
IntoLaterN n P1 Q1 MaybeIntoLaterN n P2 Q2
IntoLaterN n (P1 P2) (Q1 Q2) | 10.
IntoLaterN false n P1 Q1 MaybeIntoLaterN false n P2 Q2
IntoLaterN false n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_or. Qed.
Global Instance into_laterN_or_r n P P2 Q2 :
IntoLaterN n P2 Q2
IntoLaterN n (P P2) (P Q2) | 11.
IntoLaterN false n P2 Q2
IntoLaterN false n (P P2) (P Q2) | 11.
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
Qed.
Global Instance into_laterN_forall {A} n (Φ Ψ : A PROP) :
( x, IntoLaterN n (Φ x) (Ψ x)) IntoLaterN n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
Global Instance into_laterN_exist {A} n (Φ Ψ : A PROP) :
( x, IntoLaterN n (Φ x) (Ψ x))
IntoLaterN n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
Global Instance into_later_affinely n P Q :
MaybeIntoLaterN n P Q MaybeIntoLaterN n (bi_affinely P) (bi_affinely Q).
MaybeIntoLaterN false n P Q
MaybeIntoLaterN false n (bi_affinely P) (bi_affinely Q).
Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
Global Instance into_later_absorbingly n P Q :
MaybeIntoLaterN n P Q MaybeIntoLaterN n (bi_absorbingly P) (bi_absorbingly Q).
MaybeIntoLaterN false n P Q
MaybeIntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
Global Instance into_later_plainly n P Q :
MaybeIntoLaterN n P Q MaybeIntoLaterN n (bi_plainly P) (bi_plainly Q).
MaybeIntoLaterN false n P Q
MaybeIntoLaterN false n (bi_plainly P) (bi_plainly Q).
Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
Global Instance into_later_persistently n P Q :
MaybeIntoLaterN n P Q MaybeIntoLaterN n (bi_persistently P) (bi_persistently Q).
MaybeIntoLaterN false n P Q
MaybeIntoLaterN false n (bi_persistently P) (bi_persistently Q).
Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
MaybeIntoLaterN n P Q MaybeIntoLaterN n P Q.
MaybeIntoLaterN false n P Q MaybeIntoLaterN false n P Q.
Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
IntoLaterN n P1 Q1 MaybeIntoLaterN n P2 Q2
IntoLaterN n (P1 P2) (Q1 Q2) | 10.
IntoLaterN false n P1 Q1 MaybeIntoLaterN false n P2 Q2
IntoLaterN false n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
Global Instance into_laterN_sep_r n P P2 Q2 :
IntoLaterN n P2 Q2
IntoLaterN n (P P2) (P Q2) | 11.
IntoLaterN false n P2 Q2
IntoLaterN false n (P P2) (P Q2) | 11.
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
Qed.
Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat A PROP) (l: list A) :
( x k, IntoLaterN n (Φ k x) (Ψ k x))
IntoLaterN n ([ list] k x l, Φ k x) ([ list] k x l, Ψ k x).
( x k, IntoLaterN false n (Φ k x) (Ψ k x))
IntoLaterN false n ([ list] k x l, Φ k x) ([ list] k x l, Ψ k x).
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opL_commute. by apply big_sepL_mono.
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
(Φ Ψ : K A PROP) (m : gmap K A) :
( x k, IntoLaterN n (Φ k x) (Ψ k x))
IntoLaterN n ([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
( x k, IntoLaterN false n (Φ k x) (Ψ k x))
IntoLaterN false n ([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opM_commute. by apply big_sepM_mono.
Qed.
Global Instance into_laterN_big_sepS n `{Countable A}
(Φ Ψ : A PROP) (X : gset A) :
( x, IntoLaterN n (Φ x) (Ψ x))
IntoLaterN n ([ set] x X, Φ x) ([ set] x X, Ψ x).
( x, IntoLaterN false n (Φ x) (Ψ x))
IntoLaterN false n ([ set] x X, Φ x) ([ set] x X, Ψ x).
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opS_commute. by apply big_sepS_mono.
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
(Φ Ψ : A PROP) (X : gmultiset A) :
( x, IntoLaterN n (Φ x) (Ψ x))
IntoLaterN n ([ mset] x X, Φ x) ([ mset] x X, Ψ x).
( x, IntoLaterN false n (Φ x) (Ψ x))
IntoLaterN false n ([ mset] x X, Φ x) ([ mset] x X, Ψ x).
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opMS_commute. by apply big_sepMS_mono.
......
......@@ -239,6 +239,7 @@ Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
hypothesis).
- Instantiate the premise of the wand or implication.
*)
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
into_wand : ?p R ?q P - Q.
Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
......@@ -416,26 +417,36 @@ IntoLaterN n P P' MaybeIntoLaterN n Q Q'
-------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
>>
The Boolean [only_head] indicates whether laters should only be stripped in
head position or also below other logical connectives. For [iNext] it should
strip laters below other logical connectives, but this should not happen while
framing, e.g. the following should succeed:
<<
Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Qed.
>>
*)
Class MaybeIntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
maybe_into_laterN : P ^n Q.
Arguments MaybeIntoLaterN {_} _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode MaybeIntoLaterN + - - - : typeclass_instances.
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
into_laterN :> MaybeIntoLaterN n P Q.
Arguments IntoLaterN {_} _%nat_scope _%I _%I.
Hint Mode IntoLaterN + - ! - : typeclass_instances.
Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
into_laterN :> MaybeIntoLaterN only_head n P Q.
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Instance maybe_into_laterN_default {PROP : sbi} n (P : PROP) :
MaybeIntoLaterN n P P | 1000.
Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
MaybeIntoLaterN only_head n P P | 1000.
Proof. apply laterN_intro. Qed.
(* In the case both parameters are evars and n=0, we have to stop the
search and unify both evars immediately instead of looping using
other instances. *)
Instance maybe_into_laterN_default_0 {PROP : sbi} (P : PROP) :
MaybeIntoLaterN 0 P P | 0.
Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.
Class FromLaterN {PROP : sbi} (n : nat) (P Q : PROP) := from_laterN : ^n Q P.
......
......@@ -1206,16 +1206,16 @@ Qed.
(** * Later *)
Class MaybeIntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
into_laterN_env : env_Forall2 (MaybeIntoLaterN n) Γ1 Γ2.
into_laterN_env : env_Forall2 (MaybeIntoLaterN false n) Γ1 Γ2.
Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
into_later_persistent: MaybeIntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
into_later_persistent: MaybeIntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
into_later_spatial: MaybeIntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance into_laterN_env_nil n : MaybeIntoLaterNEnv n Enil Enil.
Proof. constructor. Qed.
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
MaybeIntoLaterNEnv n Γ1 Γ2 MaybeIntoLaterN n P Q
MaybeIntoLaterNEnv n Γ1 Γ2 MaybeIntoLaterN false n P Q
MaybeIntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.
......
......@@ -433,7 +433,8 @@ Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
MaybeIntoLaterN n P Q MakeMonPredAt i Q 𝓠 MaybeIntoLaterN n (P i) 𝓠.
MaybeIntoLaterN false n P Q MakeMonPredAt i Q 𝓠
MaybeIntoLaterN false n (P i) 𝓠.
Proof.
rewrite /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
by rewrite monPred_at_later.
......
......@@ -356,4 +356,10 @@ Proof.
iEval (rewrite (Nat.add_comm x y) // H).
done.
Qed.
Lemma test_iFrame_later_1 P Q : P Q - (P Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
Lemma test_iFrame_later_2 P Q : P Q - ( P Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
End tests.
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