diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v index 5a268321e429e059ff9fe7c2b2e988cdbb861e7a..e0115b86352f27b53286c0b16d8714111b77ec0b 100644 --- a/algebra/upred_big_op.v +++ b/algebra/upred_big_op.v @@ -4,7 +4,7 @@ Import uPred. (** We define the following big operators: -- The operators [ [★] Ps ] and [ [∧] Ps ] fold [★] and [∧] over the list [Ps]. +- The operator [ [★] Ps ] folds [★] over the list [Ps]. This operator is not a quantifier, so it binds strongly. - The operator [ [★ list] k ↦ x ∈ l, P ] asserts that [P] holds separately for each element [x] at position [x] in the list [l]. This operator is a @@ -18,10 +18,6 @@ Import uPred. (** * Big ops over lists *) (* These are the basic building blocks for other big ops *) -Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M := - match Ps with [] => True | P :: Ps => P ∧ uPred_big_and Ps end%I. -Instance: Params (@uPred_big_and) 1. -Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope. Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M := match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I. Instance: Params (@uPred_big_sep) 1. @@ -75,28 +71,13 @@ Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. (** ** Generic big ops over lists of upreds *) -Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M). -Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. - -Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M). -Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. - -Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M). -Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M). Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. -Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M). -Proof. - induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. - - by rewrite IH. - - by rewrite !assoc (comm _ P). - - etrans; eauto. -Qed. Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M). Proof. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. @@ -105,31 +86,17 @@ Proof. - etrans; eauto. Qed. -Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs. -Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed. Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. -Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs. -Proof. - intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l. -Qed. Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [★] Ps ⊢ [★] Qs. Proof. intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l. Qed. - -Lemma big_sep_and Ps : [★] Ps ⊢ [∧] Ps. -Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. - -Lemma big_and_elem_of Ps P : P ∈ Ps → [∧] Ps ⊢ P. -Proof. induction 1; simpl; auto with I. Qed. Lemma big_sep_elem_of Ps P : P ∈ Ps → [★] Ps ⊢ P. Proof. induction 1; simpl; auto with I. Qed. (** ** Persistence *) -Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP ([∧] Ps). -Proof. induction 1; apply _. Qed. Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([★] Ps). Proof. induction 1; apply _. Qed. @@ -157,8 +124,6 @@ Proof. Qed. (** ** Timelessness *) -Global Instance big_and_timeless Ps : TimelessL Ps → TimelessP ([∧] Ps). -Proof. induction 1; apply _. Qed. Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([★] Ps). Proof. induction 1; apply _. Qed. diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v index fd58f1aefd8d4af071b805ec246d01b0e92ad95c..5f1a0ca2d3730ad06b80d4cc9cb923274f2dd2b9 100644 --- a/proofmode/coq_tactics.v +++ b/proofmode/coq_tactics.v @@ -19,7 +19,7 @@ Record envs_wf {M} (Δ : envs M) := { }. Coercion of_envs {M} (Δ : envs M) : uPred M := - (■ envs_wf Δ ★ □ [∧] env_persistent Δ ★ [★] env_spatial Δ)%I. + (■ envs_wf Δ ★ □ [★] env_persistent Δ ★ [★] env_spatial Δ)%I. Instance: Params (@of_envs) 1. Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := { @@ -110,7 +110,7 @@ Implicit Types Δ : envs M. Implicit Types P Q : uPred M. Lemma of_envs_def Δ : - of_envs Δ = (■ envs_wf Δ ★ □ [∧] env_persistent Δ ★ [★] env_spatial Δ)%I. + of_envs Δ = (■ envs_wf Δ ★ □ [★] env_persistent Δ ★ [★] env_spatial Δ)%I. Proof. done. Qed. Lemma envs_lookup_delete_Some Δ Δ' i p P : @@ -127,13 +127,13 @@ Lemma envs_lookup_sound Δ i p P : Proof. rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep. - ecancel [□ [∧] _; □ P; [★] _]%I; apply pure_intro. + - rewrite (env_lookup_perm Γp) //= always_sep. + ecancel [□ [★] _; □ P; [★] Γs]%I; apply pure_intro. destruct Hwf; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh. - destruct (Γs !! i) eqn:?; simplify_eq/=. rewrite (env_lookup_perm Γs) //=. - ecancel [□ [∧] _; P; [★] _]%I; apply pure_intro. + ecancel [□ [★] _; P; [★] (env_delete _ _)]%I; apply pure_intro. destruct Hwf; constructor; naive_solver eauto using env_delete_wf, env_delete_fresh. Qed. @@ -151,7 +151,7 @@ Lemma envs_lookup_split Δ i p P : Proof. rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=. - - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep. + - rewrite (env_lookup_perm Γp) //= always_sep. rewrite pure_equiv // left_id. cancel [□ P]%I. apply wand_intro_l. solve_sep_entails. - destruct (Γs !! i) eqn:?; simplify_eq/=. @@ -188,7 +188,7 @@ Proof. - apply sep_intro_True_l; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using Esnoc_wf. intros j; case_decide; naive_solver. - + by rewrite always_and_sep always_sep assoc. + + by rewrite always_sep assoc. - apply sep_intro_True_l; [apply pure_intro|]. + destruct Hwf; constructor; simpl; eauto using Esnoc_wf. intros j; case_decide; naive_solver. @@ -206,8 +206,7 @@ Proof. intros j. apply (env_app_disjoint _ _ _ j) in Happ. naive_solver eauto using env_app_fresh. + rewrite (env_app_perm _ _ Γp') //. - rewrite big_and_app always_and_sep always_sep (big_sep_and Γ). - solve_sep_entails. + rewrite big_sep_app always_sep. solve_sep_entails. - destruct (env_app Γ Γp) eqn:Happ, (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=. apply wand_intro_l, sep_intro_True_l; [apply pure_intro|]. @@ -230,8 +229,7 @@ Proof. 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 _ _ Γp') //. - rewrite big_and_app always_and_sep always_sep (big_sep_and Γ). - solve_sep_entails. + rewrite big_sep_app always_sep. solve_sep_entails. - destruct (env_app Γ Γp) eqn:Happ, (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=. apply wand_intro_l, sep_intro_True_l; [apply pure_intro|]. @@ -428,7 +426,7 @@ Proof. repeat apply sep_mono; try apply always_mono. - rewrite -later_intro; apply pure_mono; destruct 1; constructor; naive_solver eauto using env_Forall2_wf, env_Forall2_fresh. - - induction Hp; rewrite /= ?later_and; auto using and_mono, later_intro. + - induction Hp; rewrite /= ?later_sep; auto using sep_mono, later_intro. - induction Hs; rewrite /= ?later_sep; auto using sep_mono, later_intro. Qed.