Commit e4090611 by Robbert Krebbers

### Remove uPred_big_and, it only use just complicates stuff.

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