Skip to content
Snippets Groups Projects
Commit 7fd2a308 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung
Browse files

Use big op properly instead of `env_map`. Simplify some proofs.

parent f02ecca3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/bi/lib/atomic.v
+ 2
− 1
View file @ 7fd2a308
......@@ -464,7 +464,8 @@ Section proof_mode.
Proof.
intros ? HΓs ->. rewrite envs_entails_unseal of_envs_eq' /atomic_acc /=.
setoid_rewrite env_to_prop_sound =>HAU.
apply aupd_intro; [apply _..|]. done.
rewrite bi.persistent_and_sep_assoc. apply: aupd_intro.
by rewrite -bi.persistent_and_sep_assoc.
Qed.
End proof_mode.
......
iris/proofmode/coq_tactics.v
+ 2
− 2
View file @ 7fd2a308
......@@ -922,7 +922,7 @@ Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
transform_intuitionistic_env :
(∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
(∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
<affine> ([∧] env_map_pers Γin) ⊢ M (<affine> ([∧] env_map_pers Γout));
<affine> env_and_pers Γin ⊢ M (<affine> env_and_pers Γout);
transform_intuitionistic_env_wf : env_wf Γin → env_wf Γout;
transform_intuitionistic_env_dom i : Γin !! i = None → Γout !! i = None;
}.
......@@ -1147,7 +1147,7 @@ Lemma into_laterN_env_sound {PROP : bi} n (Δ1 Δ2 : envs PROP) :
MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
Proof.
intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq.
rewrite ![([∧] _ ∧ _)%I]persistent_and_affinely_sep_l.
rewrite ![(env_and_pers _ ∧ _)%I]persistent_and_affinely_sep_l.
rewrite !laterN_and !laterN_sep.
rewrite -{1}laterN_intro. apply and_mono, sep_mono.
- apply pure_mono; destruct 1; constructor; naive_solver.
......
iris/proofmode/environments.v
+ 28
− 83
View file @ 7fd2a308
......@@ -78,12 +78,6 @@ Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
| env_Forall2_snoc Γ1 Γ2 i x y :
env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).
Fixpoint env_map {A B} (f : A → B) (Γ : env A) : env B :=
match Γ with
| Enil => Enil
| Esnoc Γ j x => Esnoc (env_map f Γ) j (f x)
end.
Inductive env_subenv {A} : relation (env A) :=
| env_subenv_nil : env_subenv Enil Enil
| env_subenv_snoc Γ1 Γ2 i x :
......@@ -199,10 +193,6 @@ Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
Global Instance env_to_list_proper (P : relation A) :
Proper (env_Forall2 P ==> Forall2 P) env_to_list.
Proof. induction 1; constructor; auto. Qed.
Global Instance env_map_proper {B} (P : relation A) (Q : relation B) (f : A → B) :
Proper (P ==> Q) f →
Proper (env_Forall2 P ==> env_Forall2 Q) (env_map f).
Proof. intros Hf. induction 1; constructor; auto. Qed.
Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
......@@ -218,40 +208,6 @@ Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
Global Instance env_to_list_subenv_proper :
Proper (env_subenv ==> sublist) (@env_to_list A).
Proof. induction 1; simpl; constructor; auto. Qed.
Lemma env_map_lookup {B} (f : A → B) Γ i :
env_map f Γ !! i = f <$> Γ !! i.
Proof.
induction Γ; simpl; first done.
case_match; naive_solver.
Qed.
Lemma env_map_delete {B} (f : A → B) Γ i :
env_map f (env_delete i Γ) = env_delete i (env_map f Γ).
Proof.
induction Γ as [|? IH]; simpl; first done.
case_match; first naive_solver.
simpl. rewrite IH. done.
Qed.
Lemma env_map_app {B} (f : A → B) Γ1 Γ2 :
env_app (env_map f Γ1) (env_map f Γ2) = (env_map f) <$> env_app Γ1 Γ2.
Proof.
induction Γ1 as [|Γ1 IH i]; simpl; first done.
rewrite IH. clear IH.
destruct (env_app Γ1 Γ2) as [Γ'|]; simpl; last done.
rewrite env_map_lookup.
destruct (Γ' !! i) as [x|]; done.
Qed.
Lemma env_map_replace {B} (f : A → B) i Γi Γ :
env_replace i (env_map f Γi) (env_map f Γ) = (env_map f) <$> env_replace i Γi Γ.
Proof.
induction Γ as [|Γ IH j]; simpl; first done.
case_match.
{ rewrite env_map_app //. }
rewrite IH. clear IH.
rewrite env_map_lookup.
destruct (Γi !! _) as [x|]; simpl; first done.
destruct (env_replace i Γi Γ) as [Γ'|]; done.
Qed.
End env.
Record envs (PROP : bi) := Envs {
......@@ -265,14 +221,6 @@ Global Arguments env_intuitionistic {_} _.
Global Arguments env_spatial {_} _.
Global Arguments env_counter {_} _.
Notation env_map_pers Γ := (env_map bi_persistently Γ).
Global Instance env_persistently_persistent {PROP : bi} (Γ : env PROP) :
Persistent ([∧] env_map_pers Γ).
Proof. induction Γ; simpl; apply _. Qed.
Global Instance env_persistently_absorbing {PROP : bi} (Γ : env PROP) :
Absorbing ([∧] env_map_pers Γ).
Proof. induction Γ; simpl; apply _. Qed.
(** We now define the judgment [envs_entails Δ Q] for proof mode entailments.
This judgment expresses that [Q] can be proved under the proof mode environment
[Δ]. To improve performance and to encapsulate the internals of the proof mode
......@@ -300,8 +248,10 @@ Record envs_wf' {PROP : bi} (Γp Γs : env PROP) := {
Definition envs_wf {PROP : bi} (Δ : envs PROP) :=
envs_wf' (env_intuitionistic Δ) (env_spatial Δ).
Notation env_and_pers Γ := ([∧ list] P ∈ env_to_list Γ, <pers> P)%I.
Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP :=
(⌜envs_wf' Γp Γs⌝ ∧ [∧] (env_map_pers Γp) ∧ [∗] Γs)%I.
(⌜envs_wf' Γp Γs⌝ ∧ env_and_pers Γp ∧ [∗] Γs)%I.
Global Instance: Params (@of_envs') 1 := {}.
Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
of_envs' (env_intuitionistic Δ) (env_spatial Δ).
......@@ -438,16 +388,17 @@ Implicit Types P Q : PROP.
Lemma of_envs_eq Δ :
of_envs Δ =
(⌜envs_wf Δ⌝ ∧
[∧] (env_map_pers (env_intuitionistic Δ)) ∧
env_and_pers (env_intuitionistic Δ) ∧
[∗] env_spatial Δ)%I.
Proof. done. Qed.
(** An environment is a ∗ of something intuitionistic and the spatial environment.
TODO: Can we define it as such? *)
Lemma of_envs_eq' Δ :
of_envs Δ ⊣⊢
(⌜envs_wf Δ⌝ ∧ <affine> [∧] (env_map_pers (env_intuitionistic Δ))) ∗ [∗] env_spatial Δ.
⌜envs_wf Δ⌝ ∧ <affine> env_and_pers (env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
Proof.
rewrite of_envs_eq [([∧] _ ∧ _)%I]persistent_and_affinely_sep_l persistent_and_sep_assoc //.
rewrite of_envs_eq [(env_and_pers _ ∧ _)%I]persistent_and_affinely_sep_l.
rewrite persistent_and_sep_assoc //.
Qed.
Global Instance envs_Forall2_refl (R : relation PROP) :
......@@ -492,7 +443,8 @@ Proof.
intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply and_mono; simpl in *.
- apply pure_mono=> -[???]. constructor;
naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
- by repeat f_equiv.
- f_equiv; [|by repeat f_equiv].
induction Hp; simpl; repeat (done || f_equiv).
Qed.
Global Instance of_envs_proper' :
Proper (env_Forall2 (⊣⊢) ==> env_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs' PROP).
......@@ -546,20 +498,15 @@ Proof.
naive_solver eauto using env_delete_wf, env_delete_fresh).
rewrite -persistently_and_intuitionistically_sep_l assoc.
apply and_mono; last done. apply and_intro.
+ rewrite (env_lookup_perm (env_map_pers Γp)).
2:{ rewrite env_map_lookup. erewrite Heqo. done. }
simpl. rewrite and_elim_l. done.
+ rewrite (env_lookup_perm Γp) //= and_elim_l //.
+ destruct rp; last done.
rewrite (env_lookup_perm (env_map_pers Γp)).
2:{ rewrite env_map_lookup. erewrite Heqo. done. }
simpl. rewrite and_elim_r. rewrite env_map_delete //.
rewrite (env_lookup_perm Γp) //= and_elim_r //.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite pure_True ?left_id; last (destruct Hwf; constructor;
naive_solver eauto using env_delete_wf, env_delete_fresh).
rewrite (env_lookup_perm Γs) //=.
rewrite ![(P ∗ _)%I]comm.
rewrite persistent_and_sep_assoc.
done.
rewrite persistent_and_sep_assoc. done.
Qed.
Lemma envs_lookup_sound Δ i p P :
envs_lookup i Δ = Some (p,P) →
......@@ -576,11 +523,7 @@ Proof.
rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
- rewrite -persistently_and_intuitionistically_sep_l.
rewrite (env_lookup_perm (env_map_pers Γp)).
2:{ rewrite env_map_lookup. erewrite Heqo. done. }
rewrite !assoc. apply and_mono; last done. simpl.
rewrite -!assoc. apply and_mono; first done.
rewrite and_elim_r. rewrite env_map_delete. done.
rewrite (env_lookup_perm Γp) //= [(⌜_⌝ ∧ _)%I]and_elim_r !assoc //.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite (env_lookup_perm Γs) //=.
rewrite [(⌜_⌝ ∧ _)%I]and_elim_r.
......@@ -657,7 +600,7 @@ Qed.
Lemma envs_app_sound Δ Δ' p Γ :
envs_app p Γ Δ = Some Δ' →
of_envs Δ ⊢ (if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
of_envs Δ ⊢ (if p then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
destruct Δ as [Γp Γs], p; simplify_eq/=.
......@@ -668,8 +611,7 @@ Proof.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
naive_solver eauto using env_app_fresh.
+ apply and_intro.
* rewrite and_elim_l. rewrite (env_app_perm _ _ (env_map_pers Γp')).
2:{ erewrite env_map_app. erewrite Heqo. done. }
* rewrite and_elim_l. rewrite (env_app_perm _ _ Γp') //.
rewrite affinely_elim big_opL_app sep_and. done.
* rewrite and_elim_r. rewrite sep_elim_r. done.
- destruct (env_app Γ Γp) eqn:Happ,
......@@ -689,7 +631,8 @@ Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
envs_simple_replace i p Γ Δ = Some Δ' →
of_envs (envs_delete true i p Δ) ⊢ (if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
of_envs (envs_delete true i p Δ) ⊢
(if p then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
rewrite /envs_simple_replace /envs_delete !of_envs_eq=> ?.
apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
......@@ -699,12 +642,11 @@ Proof.
+ destruct Hwf; constructor; simpl; eauto using env_replace_wf.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
+ rewrite (env_replace_perm _ _ (env_map_pers Γp')).
2:{ erewrite env_map_replace. erewrite Heqo. done. }
+ rewrite (env_replace_perm _ _ Γp') //.
rewrite big_opL_app. apply and_intro; first apply and_intro.
* rewrite and_elim_l affinely_elim sep_elim_l. done.
* rewrite sep_elim_r and_elim_l. rewrite env_map_delete. done.
* rewrite and_elim_r sep_elim_r. done.
* rewrite sep_elim_r and_elim_l //.
* rewrite and_elim_r sep_elim_r //.
- destruct (env_app Γ Γp) eqn:Happ,
(env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
apply wand_intro_l, and_intro; [apply pure_intro|].
......@@ -724,12 +666,14 @@ Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Q
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
of_envs Δ ⊢ □?p P ∗ ((if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ').
of_envs Δ ⊢ □?p P ∗ ((if p then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
of_envs Δ ⊢ □?p P ∗ (((if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
of_envs Δ ⊢
□?p P ∗ (((if p then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ') ∧
(□?p P -∗ of_envs Δ)).
Proof.
intros. apply pure_elim with (envs_wf Δ).
{ rewrite of_envs_eq. apply and_elim_l. }
......@@ -748,7 +692,8 @@ Qed.
Lemma envs_replace_sound' Δ Δ' i p q Γ :
envs_replace i p q Γ Δ = Some Δ' →
of_envs (envs_delete true i p Δ) ⊢ (if q then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
of_envs (envs_delete true i p Δ) ⊢
(if q then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
- apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
......@@ -762,7 +707,7 @@ Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
Lemma envs_replace_sound Δ Δ' i p q P Γ :
envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
of_envs Δ ⊢ □?p P ∗ ((if q then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ').
of_envs Δ ⊢ □?p P ∗ ((if q then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
......@@ -864,7 +809,7 @@ Proof.
Qed.
Lemma env_to_prop_and_pers_sound Γ i P :
□ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> [∧] (env_map_pers (Esnoc Γ i P)).
□ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> env_and_pers (Esnoc Γ i P).
Proof.
revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
- by rewrite right_id.
......
iris/proofmode/modalities.v
+ 14
− 18
View file @ 7fd2a308
......@@ -159,29 +159,25 @@ Section modality1.
modality_spatial_action M = MIEnvId → P ⊢ M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_intuitionistic_forall_big_and C Γ :
Lemma modality_intuitionistic_forall_big_and C Ps :
modality_intuitionistic_action M = MIEnvForall C →
Forall C (env_to_list Γ) →
<affine> [∧] (env_map_pers Γ) ⊢ M (<affine> [∧] (env_map_pers Γ)).
Forall C Ps →
(<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
Proof.
induction Γ as [|Γ IH i P]; intros ? HΓ; simpl.
- rewrite affinely_True_emp. apply modality_emp.
- inversion HΓ; subst. clear HΓ.
rewrite affinely_and -modality_and_forall //. apply and_mono.
+ by eapply modality_intuitionistic_forall.
+ eauto.
induction 2 as [|P Ps ? _ IH]; simpl.
{ rewrite affinely_True_emp. apply modality_emp. }
rewrite affinely_and -modality_and_forall //. apply and_mono, IH.
by eapply modality_intuitionistic_forall.
Qed.
Lemma modality_intuitionistic_id_big_and Γ :
Lemma modality_intuitionistic_id_big_and Ps :
modality_intuitionistic_action M = MIEnvId →
<affine> [∧] (env_map_pers Γ) ⊢ M (<affine> [∧] (env_map_pers Γ)).
(<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
Proof.
intros. induction Γ as [|Γ IH i P]; simpl.
- rewrite affinely_True_emp. apply modality_emp.
- rewrite affinely_and {1}IH. clear IH.
rewrite persistent_and_affinely_sep_l_1.
rewrite {1}[(<affine> <pers> P)%I]modality_intuitionistic_id //.
rewrite affinely_elim modality_sep. f_equiv.
apply: sep_and.
intros. induction Ps as [|P Ps IH]; simpl.
{ rewrite affinely_True_emp. apply modality_emp. }
rewrite -affinely_and_r. rewrite {1}IH {IH}.
rewrite !persistently_and_intuitionistically_sep_l.
by rewrite {1}(modality_intuitionistic_id P) // modality_sep.
Qed.
Lemma modality_spatial_forall_big_sep C Ps :
modality_spatial_action M = MIEnvForall C →
......
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