Commit 92745fe3 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Updated through viewshifts.v

parent 69915de0
......@@ -1808,6 +1808,10 @@ Global Instance const_relevant φ : RelevantP (⧆■ φ : uPred M)%I.
Proof. by rewrite /RelevantP relevant_const. Qed.
Global Instance relevant_relevant P : RelevantP ( P).
Proof. by intros; apply relevant_intro'. Qed.
Global Instance relevant_affine' P : RelevantP P RelevantP ( P).
Proof. by intros; rewrite /RelevantP; rewrite relevant_affine;
rewrite {1}(relevantP P).
Qed.
Global Instance and_relevant P Q :
RelevantP P RelevantP Q RelevantP (P Q).
Proof. by intros; rewrite /RelevantP relevant_and; apply and_mono. Qed.
......@@ -1870,6 +1874,8 @@ Qed.
(* Affine *)
Global Instance affine_affine' P : AffineP ( P).
Proof. rewrite /AffineP ?affine_equiv; auto. Qed.
Global Instance affine_relevant' P : AffineP P AffineP ( P).
Proof. intros. rewrite /AffineP. rewrite -relevant_affine. auto. Qed.
Global Instance emp_affine : AffineP (Emp)%I.
Proof. by intros; rewrite /AffineP affine_equiv; auto. Qed.
Global Instance and_affine P Q :
......
......@@ -6,7 +6,7 @@ Import uPred.
Definition own `{inG Λ Σ (gmapR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownG (to_globalF γ a).
Definition ownl `{inG Λ Σ (gmapR gname A)} (γ : gname) (a : A) : ilPropG Λ Σ :=
Definition ownl `{inG Λ Σ (gmapR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownGl (to_globalF γ a).
Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
......@@ -15,7 +15,7 @@ Typeclasses Opaque to_globalF own ownl.
Definition owne `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownG (to_globalFe a).
Definition ownle `{inG Λ Σ A} (a : A) : ilPropG Λ Σ :=
Definition ownle `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownGl (to_globalFe a).
Instance: Params (@to_globalFe) 4.
Instance: Params (@own) 4.
......@@ -65,28 +65,34 @@ Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_prope
Lemma own_op γ a1 a2 : own γ (a1 a2) ⊣⊢ (own γ a1 own γ a2).
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (own γ).
Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
Lemma own_valid γ a : own γ a a.
Proof.
move=>a b [c ->]. rewrite own_op. unfold own, ownG.
apply sep_elim_l.
Qed.
Lemma own_valid γ a : own γ a ⧆✓ a.
Proof.
rewrite /own ownG_valid /to_globalF.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
apply affine_mono.
trans ( cmra_transport inG_prf {[γ := a]} : iPropG Λ Σ)%I; last destruct inG_prf; auto.
by rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
Qed.
Lemma own_valid_r γ a : own γ a (own γ a a).
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ( a own γ a).
Lemma own_valid_r γ a : own γ a (own γ a a).
Proof. apply: uPred.relevant_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ( a own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
(*
Global Instance own_timeless γ a : Timeless a TimelessP (own γ a).
Proof. rewrite /own; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent a PersistentP (own γ a).
*)
Global Instance own_core_persistent γ a : Persistent a RelevantP (own γ a).
Proof. rewrite /own; apply _. Qed.
(* TODO: This also holds if we just have a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a E (G : gset gname) :
a True (|={E}=> γ, (γ G) own γ a).
a Emp (|={E}=> γ, (γ G) own γ a).
Proof.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( γ, γ G m = to_globalF γ a) ownG m)%I).
......@@ -101,7 +107,7 @@ Proof.
- apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv // left_id.
Qed.
Lemma own_alloc a E : a True (|={E}=> γ, own γ a).
Lemma own_alloc a E : a Emp (|={E}=> γ, own γ a).
Proof.
intros Ha. rewrite (own_alloc_strong a E ) //; [].
apply pvs_mono, exist_mono=>?. eauto with I.
......@@ -125,7 +131,7 @@ Proof.
by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
Qed.
Lemma own_empty `{Empty A, !CMRAUnit A} γ E : True (|={E}=> own γ ).
Lemma own_empty `{Empty A, !CMRAUnit A} γ E : Emp (|={E}=> own γ ).
Proof.
rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty inG_id
......@@ -153,20 +159,28 @@ Global Instance owne_proper : Proper ((≡) ==> (⊣⊢)) (owne) := ne_proper _.
Lemma owne_op a1 a2 : owne (a1 a2) ⊣⊢ (owne a1 owne a2).
Proof. by rewrite /owne -ownG_op to_globalFe_op. Qed.
Global Instance owne_mono : Proper (flip () ==> ()) (owne).
Proof. move=>a b [c H]. rewrite H owne_op. eauto with I. Qed.
Lemma owne_valid a : owne a a.
Proof. move=>a b [c ->]. rewrite /owne //= /to_globalFe.
eapply ownG_mono. simpl.
rewrite cmra_transport_op -iprod_op_singleton.
eexists; eauto.
Qed.
Lemma owne_valid a : owne a ⧆✓ a.
Proof.
rewrite /owne ownG_valid /to_globalFe.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
apply affine_mono.
trans ( cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma owne_valid_r a : owne a (owne a a).
Proof. apply: uPred.always_entails_r. apply owne_valid. Qed.
Lemma owne_valid_l a : owne a ( a owne a).
Lemma owne_valid_r a : owne a (owne a a).
Proof. apply: uPred.relevant_entails_r. apply owne_valid. Qed.
Lemma owne_valid_l a : owne a ( a owne a).
Proof. by rewrite comm -owne_valid_r. Qed.
(*
Global Instance owne_timeless a : Timeless a TimelessP (owne a).
Proof. rewrite /owne; apply _. Qed.
Global Instance owne_core_persistent a : Persistent a PersistentP (owne a).
*)
Global Instance owne_core_persistent a : Persistent a RelevantP (owne a).
Proof. rewrite /owne; apply _. Qed.
(* TODO: This also holds if we just have a at the current step-idx, as Iris
......@@ -191,7 +205,7 @@ Proof.
Qed.
Lemma owne_empty `{Empty A, !CMRAUnit A} E :
True (|={E}=> owne ).
Emp (|={E}=> owne ).
Proof.
rewrite ownG_empty /owne. apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty inG_id
......
......@@ -22,7 +22,6 @@ Definition gname := positive.
Definition globalF (Σ : gFunctors) : iFunctor :=
IFunctor (iprodRF (projT2 Σ)).
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation ilPropG Λ Σ := (ilProp Λ (globalF Σ)).
Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
inG_id : gid Σ;
......
......@@ -27,27 +27,27 @@ Qed.
Lemma always_inv N P : inv N P ⊣⊢ inv N P.
Proof. by rewrite relevant_relevant'. Qed.
(*
Lemma inv_alloc N E P : nclose N E ⧆▷ P |={E}=> inv N P.
Proof.
intros. rewrite -(pvs_mask_weaken N) //.
by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
eapply pvs_mono, exist_mono. intros i. unfold ownI. rewrite ?affine_equiv.
apply and_intro; eauto with I.
Qed.
*)
(** Invariants can be opened around any frame-shifting assertion. *)
From iris.proofmode Require Import coq_tactics.
Existing Instance coq_tactics.envs_dom.
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
fsaV nclose N E
(inv N P ( P - fsa (E nclose N) (λ a, ⧆▷ P Ψ a))) fsa E Ψ.
(inv N P ( P - fsa (E nclose N) (λ a, ⧆▷ P Ψ a))) fsa E Ψ.
Proof.
iIntros {??} "[#Hinv HΨ]"; rewrite /inv; iDestruct "Hinv" as {i} "[% Hi]".
iApply (fsa_open_close E (E {[encode i]})); auto; first by set_solver.
iPvs (pvs_openI' _ _ with "Hi") as "HP"; [set_solver..|iPvsIntro].
iApply (fsa_mask_weaken _ (E N)); first set_solver.
iApply fsa_wand_r; iSplitL; [iApply "HΨ"|iIntros {v} "[HP HΨ]"].
- iClear "Hi"; auto.
- iClear "Hi"; auto; rewrite affine_elim. auto.
- iPvs (pvs_closeI' _ _ P with "[HP]"); try set_solver.
* iSplit; [iClear "HP" | iClear "Hi"]; auto.
rewrite affine_elim. auto.
......
......@@ -4,19 +4,19 @@ From iris.proofmode Require Import pviewshifts invariants.
Import uPred.
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
( (P |={E1,E2}=> Q))%I.
( (P - |={E1,E2}=> Q))%I.
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (True (P ={E1,E2}=> Q)%I)
Notation "P ={ E1 , E2 }=> Q" := (Emp (P ={E1,E2}=> Q)%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : uPred_scope.
Notation "P ={ E }=> Q" := (True (P ={E}=> Q)%I)
Notation "P ={ E }=> Q" := (Emp (P ={E}=> Q)%I)
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=> Q") : C_scope.
......@@ -38,8 +38,10 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q R : iProp Λ Σ.
Implicit Types N : namespace.
From iris.proofmode Require Import coq_tactics.
Existing Instance coq_tactics.envs_dom.
Lemma vs_alt E1 E2 P Q : P (|={E1,E2}=> Q) P ={E1,E2}=> Q.
Proof. iIntros {Hvs} "! ?". by iApply Hvs. Qed.
Proof. iIntros {Hvs}. iIntros "_ ! ?". by iApply Hvs. Qed.
Global Instance vs_ne E1 E2 n :
Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
......@@ -57,49 +59,53 @@ Global Instance vs_mono' E1 E2 :
Proof. solve_proper. Qed.
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
Proof. iIntros "! []". Qed.
Proof. iIntros "_ ! []"; auto. Qed.
Lemma vs_timeless E P : TimelessP P P ={E}=> P.
Proof. iIntros {?} "! HP". by iApply pvs_timeless. Qed.
Proof. iIntros {?} "_ ! HP". by iApply pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
E2 E1 E3 ((P ={E1,E2}=> Q) (Q ={E2,E3}=> R)) (P ={E1,E3}=> R).
E2 E1 E3 ((P ={E1,E2}=> Q) (Q ={E2,E3}=> R)) (P ={E1,E3}=> R).
Proof.
iIntros {?} "#[HvsP HvsQ] ! HP".
iPvs ("HvsP" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!").
iPvs ("HvsP" with "! HP") as "HQ"; first done.
iApply ("HvsQ" with "!"). auto.
Qed.
Lemma vs_transitive' E P Q R : ((P ={E}=> Q) (Q ={E}=> R)) (P ={E}=> R).
Lemma vs_transitive' E P Q R : ((P ={E}=> Q) (Q ={E}=> R)) (P ={E}=> R).
Proof. apply vs_transitive; set_solver. Qed.
Lemma vs_reflexive E P : P ={E}=> P.
Proof. by iIntros "! HP". Qed.
Proof. iIntros "_ ! HP". iApply pvs_intro; auto. Qed.
Lemma vs_impl E P Q : (P Q) (P ={E}=> Q).
Proof. iIntros "#HPQ ! HP". by iApply "HPQ". Qed.
Lemma vs_wand E P Q : (P - Q) (P ={E}=> Q).
Proof. iIntros "#HPQ ! HP". iApply pvs_intro. iApply ("HPQ" with "!"); auto. Qed.
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) (R P ={E1,E2}=> R Q).
Proof. iIntros "#Hvs ! [$ HP]". by iApply "Hvs". Qed.
Proof. iIntros "#Hvs ! [$ HP]". by iApply ("Hvs" with "!"). Qed.
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) (P R ={E1,E2}=> Q R).
Proof. iIntros "#Hvs ! [HP $]". by iApply "Hvs". Qed.
Proof. iIntros "#Hvs ! [HP $]". by iApply ("Hvs" with "!"). Qed.
Lemma vs_mask_frame E1 E2 Ef P Q :
Ef E1 E2 (P ={E1,E2}=> Q) (P ={E1 Ef,E2 Ef}=> Q).
Proof.
iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply ("Hvs" with "!").
Qed.
Lemma vs_mask_frame' E Ef P Q : Ef E (P ={E}=> Q) (P ={E Ef}=> Q).
Proof. intros; apply vs_mask_frame; set_solver. Qed.
Lemma vs_inv N E P Q R :
nclose N E (inv N R ( R P ={E nclose N}=> R Q)) (P ={E}=> Q).
nclose N E (inv N R ( R P ={E nclose N}=> R Q)) (P ={E}=> Q).
Proof.
iIntros {?} "#[? Hvs] ! HP". iInv N as "HR".
iApply ("Hvs" with "!"). by iSplitL "HR".
iIntros {?} "#[Hinv Hvs] ! HP". iInv "Hinv" as "HR".
iApply ("Hvs" with "!").
unfold inv, ownI.
iClear "Hinv".
iSplitL "HR"; auto.
Qed.
Lemma vs_alloc N P : P ={N}=> inv N P.
Proof. iIntros "! HP". by iApply inv_alloc. Qed.
Lemma vs_alloc N P : P ={N}=> inv N P.
Proof. iIntros "_ ! HP". by iApply inv_alloc. Qed.
End vs.
Section vs_ghost.
......@@ -114,6 +120,6 @@ Proof. by intros; apply vs_alt, own_updateP. Qed.
Lemma vs_update E γ a a' : a ~~> a' own γ a ={E}=> own γ a'.
Proof. by intros; apply vs_alt, own_update. Qed.
Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ : True ={E}=> own γ .
Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ : Emp ={E}=> own γ .
Proof. by intros; eapply vs_alt, own_empty. Qed.
End vs_ghost.
......@@ -172,6 +172,7 @@ Proof.
destruct Hwf; constructor;
naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
envs_lookup i Δ = Some (p,P) Δ (P envs_delete i p Δ).
Proof.
......@@ -195,6 +196,28 @@ Proof.
rewrite (env_lookup_perm (env_relevant Δ) i P) //=; last apply env_relevant_lookup_true; auto.
rewrite env_relevant_delete_true //=.
Qed.
Lemma envs_lookup_relevant_sound' Δ i p P `{RelevantP _ P}:
envs_lookup i Δ = Some (p,P) Δ ( P Δ).
Proof.
destruct p; first apply envs_lookup_relevant_sound.
intros. rewrite {1}of_envs_def.
rewrite -(relevant_relevant' (uPred_const (envs_wf Δ))).
rewrite relevant_sep_dup'_1.
rewrite -assoc. rewrite {2}relevant_elim -of_envs_def.
rewrite {1}envs_lookup_sound //= (of_envs_def Δ).
rewrite relevant_elim.
ecancel [_]%I.
rewrite -{1}(relevant_relevant' P).
rewrite {1}(relevant_sep_dup'_1 P).
ecancel [ P]%I.
to_front [_]%I.
rewrite sep_elim_r. rewrite env_relevant_delete_false.
ecancel [Π★ (map uPred_relevant (env_relevant _))]%I.
rewrite (env_lookup_perm (env_spatial Δ) i P) //=; last apply env_spatial_lookup_false; auto.
rewrite env_spatial_delete_false //=.
rewrite relevant_elim.
auto.
Qed.
Lemma envs_lookup_split Δ i p P :
envs_lookup i Δ = Some (p,P)
......@@ -550,10 +573,23 @@ Global Instance to_relevantP_always_trans P Q :
Proof. rewrite /ToRelevantP=> ->. by rewrite relevant_relevant'. Qed.
Global Instance to_relevantP_always P : ToRelevantP ( P) P | 1.
Proof. done. Qed.
Global Instance to_relevantP_always_affine P : ToRelevantP (⧆□ P) P | 1.
Proof. rewrite /ToRelevantP. rewrite affine_elim. auto. Qed.
Global Instance to_relevantP_relevant P :
RelevantP P ToRelevantP P P | 100.
Proof. done. Qed.
Class ToRelevantP_Intro (P Q : uPred M) := to_relevantP_intro : P Q.
Arguments to_relevantP_intro : clear implicits.
Global Instance to_relevantP_intro_always_trans P Q :
ToRelevantP_Intro P Q ToRelevantP_Intro ( P) ( Q) | 0.
Proof. rewrite /ToRelevantP_Intro=> ->. by rewrite relevant_relevant'. Qed.
Global Instance to_relevantP_intro_always P : ToRelevantP_Intro ( P) ( P) | 1.
Proof. rewrite /ToRelevantP_Intro. rewrite relevant_relevant'. done. Qed.
Global Instance to_relevantP_intro_relevant P :
RelevantP P ToRelevantP_Intro P P | 100.
Proof. done. Qed.
Lemma tac_relevant Δ Δ' i p P P' Q :
envs_lookup i Δ = Some (p, P)%I ToRelevantP P P'
envs_replace i p true (Esnoc Enil i P') Δ = Some Δ'
......@@ -574,12 +610,12 @@ Proof.
by rewrite ?right_id relevant_wand_impl_1 relevant_elim HQ.
Qed.
Lemma tac_impl_intro_relevant Δ Δ' i P P' Q :
ToRelevantP P P'
ToRelevantP_Intro P P'
envs_app true (Esnoc Enil i P') Δ = Some Δ'
Δ' Q Δ (P Q).
Proof.
intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
by rewrite right_id {1}(to_relevantP P) relevant_and_sep_l_1 wand_elim_r.
by rewrite right_id {1}(to_relevantP_intro P) relevant_and_sep_l_1 wand_elim_r.
Qed.
Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ (φ Δ Q) Δ (P Q).
Proof.
......@@ -594,7 +630,7 @@ Proof.
rewrite right_id. by apply wand_mono.
Qed.
Lemma tac_wand_intro_relevant Δ Δ' i P P' Q :
ToRelevantP P P'
ToRelevantP_Intro P P'
envs_app true (Esnoc Enil i P') Δ = Some Δ'
Δ' Q Δ (P - Q).
Proof.
......@@ -761,7 +797,8 @@ Proof.
rewrite wand_Emp //=.
Qed.
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
(* TODO: we want a version that actually deletes relevant *)
Lemma tac_pose_proof_hyp_spare Δ Δ' Δ'' i p j P Q :
envs_lookup_delete i Δ = Some (p, P, Δ')
envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ''
Δ'' Q Δ Q.
......@@ -773,6 +810,18 @@ Proof.
by rewrite right_id wand_elim_r.
Qed.
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
envs_lookup_delete i Δ = Some (p, P, Δ')
envs_app p (Esnoc Enil j P) Δ' = Some Δ''
Δ'' Q Δ Q.
Proof.
intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
- rewrite envs_lookup_sound // envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
- rewrite envs_lookup_sound // envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
Qed.
Lemma tac_apply Δ Δ' i p R P1 P2 :
envs_lookup_delete i Δ = Some (p, R, Δ')%I ToWand R P1 P2
Δ' P1 Δ P2.
......@@ -904,6 +953,9 @@ Proof. simpl=>->. by rewrite -relevant_sep' (relevant_relevant' Q1) (relevant_re
Global Instance sep_destruct_sep P Q : SepDestruct false (P Q) P Q.
Proof. by apply sep_destruct_spatial. Qed.
Global Instance sep_destruct_sep' P Q :
RelevantP P RelevantP Q SepDestruct true (P Q) P Q.
Proof. intros; by apply sep_destruct_relevant. Qed.
Global Instance sep_destruct_ownM (a b : M) :
SepDestruct false (uPred_ownM (a b)) (uPred_ownM a) (uPred_ownM b).
Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.
......@@ -999,19 +1051,18 @@ Global Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
Frame R ( x, Φ x) (Some ( x, if mΨ x is Some Q then Q else Emp))%I.
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
(*
Lemma tac_frame Δ Δ' i p R P mQ :
envs_lookup_delete i Δ = Some (p, R, Δ')%I Frame R P mQ
(if mQ is Some Q then (if p then Δ else Δ') Q else True)
(if mQ is Some Q then Δ' Q else Δ' Emp)
Δ P.
Proof.
intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
- rewrite envs_lookup_relevant_sound // relevant_elim.
rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
- rewrite envs_lookup_sound //; simpl.
rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I;
rewrite relevant_elim; auto.
- rewrite envs_lookup_sound //; simpl.
rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
Qed.
*)
(** * Disjunction *)
Class OrSplit (P Q1 Q2 : uPred M) := or_split : (Q1 Q2) P.
......
......@@ -8,40 +8,74 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.
Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i j p P Q Φ :
FSASplit Q E fsa fsaV Φ
fsaV nclose N E envs_lookup j Δ = Some (p, inv N P)
envs_app false (Esnoc Enil i ( P)) Δ = Some Δ'
Δ' fsa (E nclose N) (λ a, ⧆▷ P Φ a) Δ Q.
Proof.
intros ????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
rewrite envs_lookup_relevant_sound'; eauto.
rewrite relevant_elim. eapply sep_mono. auto.
rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.
(*
Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
FSASplit Q E fsa fsaV Φ
fsaV nclose N E of_envs Δ inv N P
envs_app false (Esnoc Enil i ( P)) Δ = Some Δ'
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Proof.
intros ????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
rewrite // -always_and_sep_l. apply and_intro; first done.
rewrite // -relevant_and_sep_l_1. apply and_intro; first done.
rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.
*)
(*
Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i j p P Q Φ :
FSASplit Q E fsa fsaV Φ
fsaV nclose N E envs_lookup j Δ = Some (p, inv N P) TimelessP P
envs_app false (Esnoc Enil i P) Δ = Some Δ'
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Proof.
intros ?????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
rewrite // -relevant_and_sep_l_1. apply and_intro, wand_intro_l; first done.
trans (|={E N}=> P Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
apply (fsa_strip_pvs _).
rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
apply: fsa_mono=> v.
apply sep_mono; auto. apply affine_mono. apply later_intro.
Qed.
*)
(*
Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
FSASplit Q E fsa fsaV Φ
fsaV nclose N E of_envs Δ inv N P TimelessP P
envs_app false (Esnoc Enil i P) Δ = Some Δ'
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Proof.
intros ?????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
rewrite // -relevant_and_sep_l_1. apply and_intro, wand_intro_l; first done.
trans (|={E N}=> P Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
apply (fsa_strip_pvs _).
rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
apply: fsa_mono=> v. by rewrite -later_intro.
apply: fsa_mono=> v.
apply sep_mono; auto. apply affine_mono. apply later_intro.
Qed.
*)
End invariants.
Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
eapply tac_inv_fsa with _ _ _ _ N H _ _;
eapply tac_inv_fsa with _ _ _ _ _ H N _ _ _;
[let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P
|try fast_done (* atomic *)
|done || eauto with ndisj (* [eauto with ndisj] is slow *)
|iAssumption || fail "iInv: invariant" N "not found"
|env_cbv; reflexivity
| env_cbv; reflexivity || fail "iInv: invariant not found"
| env_cbv; reflexivity || fail "iOpenInv: invariant not found"
|simpl (* get rid of FSAs *)].
Tactic Notation "iInv" constr(N) "as" constr(pat) :=
......@@ -59,6 +93,7 @@ Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
constr(pat) :=
let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2 x3 x4} pat.
(*
Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
......@@ -66,12 +101,13 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
apply _ || fail "iInv: cannot viewshift in goal" P
|try fast_done (* atomic *)
|done || eauto with ndisj (* [eauto with ndisj] is slow *)
|iAssumption || fail "iOpenInv: invariant" N "not found"
| env_cbv; reflexivity || fail "iOpenInv: invariant" N "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iInv:" P "not timeless"
|env_cbv; reflexivity
|simpl (* get rid of FSAs *)].
Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as pat.
Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1) "}"
......@@ -87,3 +123,4 @@ Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2 x3 x4} pat.
*)
......@@ -5,6 +5,7 @@ Inductive spec_pat :=
| SRelevant : spec_pat
| SPure : spec_pat
| SAlways : spec_pat
| SAffine : spec_pat
| SName : string spec_pat
| SForall : spec_pat.
......@@ -17,6 +18,7 @@ Inductive token :=
| TPersistent : token
| TPure : token
| TAlways : token
| TAffine : token
| TForall : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
......@@ -31,6 +33,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
| String "@" s => tokenize_go s (TAffine :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""