...

Commits (3)
 ... ... @@ -540,18 +540,18 @@ Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed. Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R. Proof. iIntros "H". repeat iSplit. - iDestruct "H" as "[\$ _]". - iDestruct "H" as "[_ [\$ _]]". - iDestruct "H" as "[_ [_ #\$]]". - by iDestruct "H" as "[\$ _]". - by iDestruct "H" as "[_ [\$ _]]". - by iDestruct "H" as "[_ [_ #\$]]". Qed. Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} : P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R. Proof. iIntros "H". repeat iSplit. - iDestruct "H" as "[\$ _]". - iDestruct "H" as "[_ [\$ _]]". - iDestruct "H" as "[_ [_ #\$]]". - by iDestruct "H" as "[\$ _]". - by iDestruct "H" as "[_ [\$ _]]". - by iDestruct "H" as "[_ [_ #\$]]". Qed. Check "test_and_sep_affine_bi". ... ...
 ... ... @@ -212,7 +212,7 @@ Proof. iCombine "Hf" "HP" as "Hf". rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f). iApply (@big_sepM_impl with "Hf"). iIntros "!#" (γ b' ?) "[(Hγ' & #\$ & #\$) HΦ]". iIntros "!#" (γ b' ?) "[(Hγ' & #? & #?) HΦ]". iFrame "#". iInv N as (b) "[>Hγ _]". iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ \$]"; first by iFrame. iModIntro. iSplitL; last done. iNext; iExists true. iFrame. ... ...
 ... ... @@ -93,7 +93,18 @@ Qed. Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2). Proof. apply iff_reflect. by rewrite ident_beq_true. Qed. (** Copies of some [option] combinators for better reduction control. *) (** Copies of some [list] and [option] combinators for better reduction control. *) Definition pm_app {A} : list A → list A → list A := fix go l l' := match l with [] => l' | x :: l => x :: go l l' end. Definition pm_rev_append {A} : list A → list A → list A := fix go l l' := match l with [] => l' | x :: l => go l (x :: l') end. Definition pm_reverse {A} (l : list A) : list A := pm_rev_append l []. Definition pm_foldr {A B} (f : B → A → A) (a : A) : list B → A := fix go l := match l with [] => a | x :: l => f x (go l) end. Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B := match mx with Some x => f x | None => None end. Arguments pm_option_bind {_ _} _ !_ /. ... ...
 ... ... @@ -623,6 +623,125 @@ Proof. - setoid_rewrite <-(right_id emp%I _ (Pout _)). auto. Qed. (** * Covfefe *) Definition covfefe (p : bool) (P : PROP) (Q : PROP) (acts : list (envs_action PROP)) (Q' : PROP) := □?p P ∗ (([∗ list] act ∈ acts, envs_action_to_prop act) -∗ Q') ⊢ Q. Lemma covfefe_continue {A} (x : A) p P Q : covfefe p P Q [AContinue x p P] Q. Proof. by rewrite /covfefe /= right_id wand_elim_r. Qed. Lemma covfefe_name i p P Q : covfefe p P Q [ARename i p P] Q. Proof. by rewrite /covfefe /= right_id wand_elim_r. Qed. Lemma covfefe_fresh p P Q : covfefe p P Q [AFresh p P] Q. Proof. by rewrite /covfefe /= right_id wand_elim_r. Qed. Lemma covfefe_clear (p : bool) P Q : (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) → covfefe p P Q [] Q. Proof. intros. rewrite /covfefe /= left_id. destruct p; simpl; by rewrite sep_elim_r. Qed. Lemma covfefe_pure (p : bool) P Q φ : IntoPure P φ → (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) → covfefe p P Q [APure φ] Q. Proof. intros ? HPQ. rewrite /covfefe /= right_id. destruct p; simpl. - by rewrite (into_pure P) intuitionistically_affinely wand_elim_r. - destruct HPQ. + by rewrite -(affine_affinely P) (into_pure P) wand_elim_r. + rewrite (into_pure P) -{1}(persistent_absorbingly_affinely ⌜ _ ⌝)%I. by rewrite absorbingly_sep_l wand_elim_r. Qed. Lemma covfefe_frame p P Q Q' : Frame p P Q Q' → covfefe p P Q [] Q'. Proof. intros. by rewrite /covfefe /= left_id. Qed. Lemma covfefe_and_l (p : bool) P Q P1 P2 res Q' : (if p then IntoAnd p P P1 P2 : Type else TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2) (TCOr (Affine P2) (Absorbing Q)))) → covfefe p P1 Q res Q' → covfefe p P Q res Q'. Proof. rewrite /covfefe /IntoAnd /IntoSep=> HP HP1. destruct p; simpl in *. { by rewrite HP and_elim_l. } destruct HP as [HP|[HP [?|?]]]. - by rewrite HP and_elim_l. - by rewrite HP sep_elim_l. - by rewrite HP (comm _ P1) -assoc HP1 sep_elim_r. Qed. Lemma covfefe_and_r (p : bool) P Q P1 P2 res Q' : (if p then IntoAnd p P P1 P2 : Type else TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2) (TCOr (Affine P1) (Absorbing Q)))) → covfefe p P2 Q res Q' → covfefe p P Q res Q'. Proof. rewrite /covfefe /IntoAnd /IntoSep=> HP HP1. destruct p; simpl in *. { by rewrite HP and_elim_r. } destruct HP as [HP|[HP [?|?]]]. - by rewrite HP and_elim_r. - by rewrite HP sep_elim_r. - by rewrite HP -assoc HP1 sep_elim_r. Qed. Lemma covfefe_and (p : bool) P Q P1 P2 res1 res2 Q' Q'' : (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) → covfefe p P1 Q res1 Q' → covfefe p P2 Q' res2 Q'' → covfefe p P Q (pm_app res1 res2) Q''. Proof. rewrite (_ : pm_app = app) // /covfefe /IntoAnd /IntoSep /=. destruct p; simpl. - intros -> HP1 HP2. rewrite intuitionistically_and persistent_and_sep_1. rewrite -HP1 -assoc. apply sep_mono; first done. apply wand_intro_l. rewrite assoc -(comm _ (□ _))%I -assoc. by rewrite big_sepL_app -wand_curry wand_elim_r. - intros -> HP1 HP2. rewrite -HP1 -assoc. apply sep_mono; first done. apply wand_intro_l. rewrite assoc -(comm _ P2)%I -assoc. by rewrite big_sepL_app -wand_curry wand_elim_r. Qed. Lemma covfefe_intuitionistic p P Q P' res Q' : IntoPersistent p P P' → (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) → covfefe true P' Q res Q' → covfefe p P Q res Q'. Proof. rewrite /covfefe /IntoPersistent /=. destruct p; simpl. - rewrite /bi_intuitionistically. by intros -> _. - intros HP HPQ HP'. destruct HPQ. + by rewrite -(affine_affinely P) HP. + rewrite HP -absorbingly_intuitionistically_into_persistently. by rewrite absorbingly_sep_l HP'. Qed. Lemma covfefe_modal p P Q φ p' P' res Q' Q'' : ElimModal φ p p' P P' Q Q' → φ → covfefe p' P' Q' res Q'' → covfefe p P Q res Q''. Proof. rewrite /ElimModal /covfefe /= => HP Hφ HP'. rewrite -HP //. apply sep_mono; first done. by apply wand_intro_l. Qed. Lemma tac_covfefe Δ i p P Q Q' acts : envs_lookup i Δ = Some (p, P) → covfefe p P Q acts Q' → match envs_replace_actions i p acts Δ with | Some (Δ', φs, cs) => pm_foldr (λ P1 P2 : Prop, P1 → P2) (envs_entails Δ' Q') φs | None => False end → envs_entails Δ Q. Proof. rewrite envs_entails_eq /covfefe => ? <- HQ'. destruct (envs_replace_actions _ _ _ _) as [[[Δ' φs] cs]|] eqn:Hact; last done. rewrite envs_replace_actions_sound //. apply sep_mono, wand_mono=> //. rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> Hφs. move: HQ'. clear -Hφs. induction Hφs; simpl; auto. Qed. End bi_tactics. (** The following _private_ classes are used internally by [tac_modal_intro] / ... ...
 ... ... @@ -316,8 +316,11 @@ Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP := Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP := Envs Enil (env_spatial Δ) (env_counter Δ). Definition envs_set_counter {PROP} (c : positive) (Δ : envs PROP) : envs PROP := Envs (env_intuitionistic Δ) (env_spatial Δ) c. Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP := Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)). envs_set_counter (Pos_succ (env_counter Δ)) Δ. Fixpoint envs_split_go {PROP} (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) := ... ... @@ -341,9 +344,60 @@ Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP := in match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end. Inductive envs_action (PROP : bi) := | AFresh (p : bool) (P : PROP) | ARename (j : ident) (p : bool) (P : PROP) | AContinue {A} (x : A) (p : bool) (P : PROP) | APure (φ : Prop). Arguments AFresh {_} _ _. Arguments ARename {_} _ _ _. Arguments AContinue {_ _} _ _ _. Arguments APure {_} _. Definition envs_action_to_prop {PROP} (act : envs_action PROP) : PROP := match act with | AFresh p P | ARename _ p P | AContinue _ p P => □?p P | APure φ => ⌜ φ ⌝ end%I. Fixpoint envs_replace_actions_filter {PROP} (c : positive) (acts : list (envs_action PROP)) (Γp Γs : env PROP) (φs : list Prop) (cont : list (ident * sigT id)) : positive * env PROP * env PROP * list Prop * list (ident * sigT id) := match acts with | [] => (c,Γp,Γs,pm_reverse φs,pm_reverse cont) | act :: acts => match act with | AFresh q P => if q then envs_replace_actions_filter (Pos_succ c) acts (Esnoc Γp (IAnon c) P) Γs φs cont else envs_replace_actions_filter (Pos_succ c) acts Γp (Esnoc Γs (IAnon c) P) φs cont | ARename j q P => if q then envs_replace_actions_filter c acts (Esnoc Γp j P) Γs φs cont else envs_replace_actions_filter c acts Γp (Esnoc Γs j P) φs cont | AContinue x q P => if q then envs_replace_actions_filter (Pos_succ c) acts (Esnoc Γp (IAnon c) P) Γs φs ((IAnon c,existT _ x) :: cont) else envs_replace_actions_filter (Pos_succ c) acts Γp (Esnoc Γs (IAnon c) P) φs ((IAnon c,existT _ x) :: cont) | APure φ => envs_replace_actions_filter c acts Γp Γs (φ :: φs) cont end end. Definition envs_replace_actions {PROP} (i : ident) (p : bool) (acts : list (envs_action PROP)) (Δ : envs PROP) : option (envs PROP * list Prop * list (ident * sigT id)) := let '(c,Γp,Γs,φs,cont) := envs_replace_actions_filter (env_counter Δ) acts Enil Enil [] [] in Δ ← envs_simple_replace i p (if p then Γp else Γs) Δ; Δ ← envs_app (beq p false) (if p then Γs else Γp) Δ; Some (envs_set_counter c Δ, φs, cont). Section envs. Context {PROP : bi}. Implicit Types Γ : env PROP. Implicit Types Γ Γs Γp : env PROP. Implicit Types Δ : envs PROP. Implicit Types P Q : PROP. ... ... @@ -665,10 +719,12 @@ Proof. - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne. Qed. Lemma envs_incr_counter_equiv Δ : envs_Forall2 (⊣⊢) Δ (envs_incr_counter Δ). Lemma envs_set_counter_equiv c Δ : envs_Forall2 (⊣⊢) Δ (envs_set_counter c Δ). Proof. done. Qed. Lemma envs_incr_counter_sound Δ : of_envs (envs_incr_counter Δ) ⊣⊢ of_envs Δ. Lemma envs_set_counter_sound c Δ : of_envs (envs_set_counter c Δ) ⊣⊢ of_envs Δ. Proof. by f_equiv. Qed. Lemma envs_incr_counter_sound Δ : of_envs (envs_incr_counter Δ) ⊣⊢ of_envs Δ. Proof. apply envs_set_counter_sound. Qed. Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' : (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) → ... ... @@ -711,4 +767,41 @@ Proof. - by rewrite right_id. - rewrite /= IH (comm _ Q _) assoc. done. Qed. Lemma envs_replace_actions_filter_sound c acts Γp Γs φs cont c' Γp' Γs' φs' cont' : envs_replace_actions_filter c acts Γp Γs φs cont = (c', Γp', Γs', φs', cont') → ([∗ list] act ∈ acts, envs_action_to_prop act) ∗ ⌜ Forall id φs ⌝ ∗ □ [∧] Γp ∗ [∗] Γs ⊢ ⌜ Forall id φs' ⌝ ∗ □ [∧] Γp' ∗ [∗] Γs'. Proof. revert c Γp Γs φs cont c' Γp' Γs' φs' cont'. induction acts as [|act acts IH]; intros c Γp Γs φs cont c' Γp' Γs' φs' cont' Hact; simplify_eq/=. { by rewrite left_id (_ : pm_reverse = reverse) // Forall_reverse. } destruct act as [[] P|j [] P|A x [] P|φ] eqn:?; (etrans; [|by eapply IH]); rewrite /= ?intuitionistically_and ?and_sep_intuitionistically; try solve_sep_entails. rewrite Forall_cons /= pure_and affinely_and -sep_and. solve_sep_entails. Qed. Lemma envs_replace_actions_sound Δ Δ' i p acts P φs cs : envs_lookup i Δ = Some (p, P) → envs_replace_actions i p acts Δ = Some (Δ', φs, cs) → of_envs Δ ⊢ □?p P ∗ (([∗ list] act ∈ acts, envs_action_to_prop act) -∗ ⌜ Forall id φs ⌝ ∗ of_envs Δ'). Proof. rewrite /envs_replace_actions=> ? Hact. destruct (envs_replace_actions_filter _ _ _ _ _ _) as [[[[c Γp] Γs] φs'] cont] eqn:Hfilter. destruct (envs_simple_replace _ _ _ _) as [Δ1|] eqn:?; simplify_eq/=. destruct (envs_app _ _ _) as [Δ2|] eqn:?; simplify_eq/=. move: Hfilter=> /envs_replace_actions_filter_sound /=. rewrite Forall_nil. rewrite intuitionistically_True_emp affinely_True_emp affinely_emp !right_id. intros ->. rewrite envs_simple_replace_sound // envs_app_sound //. apply sep_mono; first done. apply wand_intro_l. rewrite -!assoc. apply sep_mono; first done. destruct p; simpl. - by rewrite wand_curry assoc wand_elim_r envs_set_counter_sound. - by rewrite !wand_elim_r envs_set_counter_sound. Qed. End envs.
 ... ... @@ -1217,6 +1217,96 @@ Tactic Notation "iModCore" constr(H) := |pm_prettify(* subgoal *)]. (** * Basic destruct tactic *) Ltac iSolveCovfefe pat := lazymatch pat with | IFresh => apply covfefe_fresh | IDrop => apply covfefe_clear; [pm_reduce; iSolveTC || let P := match goal with |- TCOr (Affine ?P) _ => P end in fail "iDestruct: cannot clear " P "; not affine and the goal not absorbing"] | IFrame => apply covfefe_frame; [iSolveTC || let R := match goal with |- Frame _ ?R _ _ => R end in fail "iDestruct: cannot frame" R] | IIdent ?i => apply (covfefe_name i) | IPureElim => eapply covfefe_pure; [iSolveTC || let P := match goal with |- IntoPure ?P _ => P end in fail "iDestruct:" P "not pure" |pm_reduce; iSolveTC || let P := match goal with |- TCOr (Affine ?P) _ => P end in fail "iDestruct:" P "not affine and the goal not absorbing"] | IList [[?pat; IDrop]] => eapply covfefe_and_l; [pm_reduce; iSolveTC || let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in fail "iDestruct: cannot destruct" P |iSolveCovfefe pat] | IList [[IDrop; ?pat]] => eapply covfefe_and_r; [pm_reduce; iSolveTC || let P := match goal with |- context [ IntoAnd _ ?P _ _ ] => P end in fail "iDestruct: cannot destruct" P |iSolveCovfefe pat] | IList [[?pat1; ?pat2]] => eapply covfefe_and; [pm_reduce; iSolveTC || let P := lazymatch goal with | |- IntoSep ?P _ _ => P | |- IntoAnd _ ?P _ _ => P end in fail "iDestruct: cannot destruct" P |iSolveCovfefe pat1 |iSolveCovfefe pat2] | IAlwaysElim ?pat => eapply covfefe_intuitionistic; [iSolveTC || let P := match goal with |- IntoPersistent _ ?P _ => P end in fail "iDestruct:" P "not persistent" |pm_reduce; iSolveTC || let P := match goal with |- TCOr (Affine ?P) _ => P end in fail "iDestruct:" P "not affine and the goal not absorbing" |iSolveCovfefe pat] | IModalElim ?pat => eapply covfefe_modal; [iSolveTC || let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in fail "iMod: cannot eliminate modality" P "in" Q |solve [iSolveSideCondition] || fail "iDestruct: `>`-pattern only supported with trivial side-conditions" |iSolveCovfefe pat] | _ => apply (covfefe_continue pat) end. Tactic Notation "iCovfefe" constr(H) "as" constr(pat) "with" tactic(tac) := let rec go_cont cs := lazymatch cs with | [] => idtac | (?i, existT intro_pat ?pat) :: ?cs => tac i pat; go_cont cs end in let pat := intro_pat.parse_one pat in notypeclasses refine (tac_covfefe _ H _ _ _ _ _ _ _ _); [pm_reflexivity || fail "iDestruct:" H "not found" |iSolveCovfefe pat |lazymatch goal with | |- context K [ envs_replace_actions ?i ?p ?acts ?Δ ] => lazymatch eval pm_eval in (envs_replace_actions i p acts Δ) with | None => fail "iDestruct: name clash" | Some (?Δ, ?φs, ?cs) => let res := context K [Some (Δ, φs, cs)] in convert_concl_no_check res; pm_reduce; repeat intro; go_cont cs end end]. Local Ltac iDestructHypGo Hz pat := lazymatch pat with | IFresh => ... ... @@ -1228,16 +1318,15 @@ Local Ltac iDestructHypGo Hz pat := | IFrame => iFrameHyp Hz | IIdent ?y => iRename Hz into y | IList [[]] => iExFalso; iExact Hz | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1 | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2 | IList [[?pat1; ?pat2]] => let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2 | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2] | IPureElim => iPure Hz as ? | IRewrite Right => iPure Hz as -> | IRewrite Left => iPure Hz as <- | IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat | IList [[_; IDrop]] => iCovfefe Hz as pat with iDestructHypGo | IList [[IDrop; _]] => iCovfefe Hz as pat with iDestructHypGo | IList [[_; _]] => iCovfefe Hz as pat with iDestructHypGo | IAlwaysElim _ => iCovfefe Hz as pat with iDestructHypGo | IModalElim _ => iCovfefe Hz as pat with iDestructHypGo | _ => fail "iDestruct:" pat "invalid" end. Local Ltac iDestructHypFindPat Hgo pat found pats := ... ...
 ... ... @@ -12,9 +12,11 @@ Declare Reduction pm_eval := cbv [ env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app envs_simple_replace envs_replace envs_split envs_clear_spatial envs_clear_intuitionistic envs_incr_counter envs_clear_spatial envs_clear_intuitionistic envs_set_counter envs_incr_counter envs_split_go envs_split env_to_prop (* PM option combinators *) envs_replace_actions_filter envs_replace_actions (* PM list and option combinators *) pm_app pm_rev_append pm_reverse pm_foldr pm_option_bind pm_from_option pm_option_fun ]. Ltac pm_eval t := ... ...