diff --git a/_CoqProject b/_CoqProject index 822e634b756d7f8973aed347407d5538ac8dee89..0f71e25dabb9259c7cfd8473a4e08fc8df003803 100644 --- a/_CoqProject +++ b/_CoqProject @@ -50,6 +50,7 @@ algebra/excl.v algebra/iprod.v algebra/functor.v algebra/upred.v +algebra/upred_big_op.v program_logic/model.v program_logic/adequacy.v program_logic/hoare_lifting.v diff --git a/algebra/upred.v b/algebra/upred.v index f2a8a55e548fa13af8b63a7882ca378d0f066d54..d0a4d6f676be333bf5462c2a6c6c4d002d66da73 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -219,29 +219,15 @@ Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope. Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I. Infix "↔" := uPred_iff : uPred_scope. -Fixpoint uPred_big_and {M} (Ps : list (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)) := - match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I. -Instance: Params (@uPred_big_sep) 1. -Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope. - Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False). Arguments timelessP {_} _ {_} _ _ _ _. Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P. Arguments always_stable {_} _ {_} _ _ _ _. -Class AlwaysStableL {M} (Ps : list (uPred M)) := - always_stableL : Forall AlwaysStable Ps. -Arguments always_stableL {_} _ {_}. - Module uPred. Section uPred_logic. Context {M : cmraT}. Implicit Types φ : Prop. Implicit Types P Q : uPred M. -Implicit Types Ps Qs : list (uPred M). Implicit Types A : Type. Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *) Arguments uPred_holds {_} !_ _ _ /. @@ -849,36 +835,6 @@ Proof. done. Qed. Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False. Proof. by intros; rewrite ownM_valid valid_elim. Qed. -(* Big ops *) -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_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). - * etransitivity; 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. - * by rewrite IH. - * by rewrite !assoc (comm _ P). - * etransitivity; eauto. -Qed. -Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I. -Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. -Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I. -Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. -Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps). -Proof. by induction Ps as [|P Ps IH]; simpl; auto. Qed. -Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P. -Proof. induction 1; simpl; auto. Qed. -Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P. -Proof. induction 1; simpl; auto. Qed. - (* Timeless *) Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x. Proof. @@ -967,23 +923,6 @@ Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) AS P → (∀ x, AS (Q x)) → AS (default P mx Q). Proof. destruct mx; apply _. Qed. -(* Always stable for lists *) -Local Notation ASL := AlwaysStableL. -Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps). -Proof. induction 1; apply _. Qed. -Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps). -Proof. induction 1; apply _. Qed. - -Global Instance nil_always_stable : ASL (@nil (uPred M)). -Proof. constructor. Qed. -Global Instance cons_always_stable P Ps : AS P → ASL Ps → ASL (P :: Ps). -Proof. by constructor. Qed. -Global Instance app_always_stable Ps Ps' : ASL Ps → ASL Ps' → ASL (Ps ++ Ps'). -Proof. apply Forall_app_2. Qed. -Global Instance zip_with_always_stable {A B} (f : A → B → uPred M) xs ys : - (∀ x y, AS (f x y)) → ASL (zip_with f xs ys). -Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. - (* Derived lemmas for always stable *) Lemma always_always P `{!AlwaysStable P} : (□ P)%I ≡ P. Proof. apply (anti_symm (⊑)); auto using always_elim. Qed. diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v new file mode 100644 index 0000000000000000000000000000000000000000..a52a96d5ff3901608cc1eaf8b5aadc3c48fb0951 --- /dev/null +++ b/algebra/upred_big_op.v @@ -0,0 +1,69 @@ +From algebra Require Export upred. + +Fixpoint uPred_big_and {M} (Ps : list (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)) := + match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I. +Instance: Params (@uPred_big_sep) 1. +Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope. + +Class AlwaysStableL {M} (Ps : list (uPred M)) := + always_stableL : Forall AlwaysStable Ps. +Arguments always_stableL {_} _ {_}. + +Section big_op. +Context {M : cmraT}. +Implicit Types P Q : uPred M. +Implicit Types Ps Qs : list (uPred M). +Implicit Types A : Type. + +(* Big ops *) +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_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). + * etransitivity; 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. + * by rewrite IH. + * by rewrite !assoc (comm _ P). + * etransitivity; eauto. +Qed. +Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I. +Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. +Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I. +Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. 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. + +(* Always stable *) +Local Notation AS := AlwaysStable. +Local Notation ASL := AlwaysStableL. +Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps). +Proof. induction 1; apply _. Qed. +Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps). +Proof. induction 1; apply _. Qed. + +Global Instance nil_always_stable : ASL (@nil (uPred M)). +Proof. constructor. Qed. +Global Instance cons_always_stable P Ps : AS P → ASL Ps → ASL (P :: Ps). +Proof. by constructor. Qed. +Global Instance app_always_stable Ps Ps' : ASL Ps → ASL Ps' → ASL (Ps ++ Ps'). +Proof. apply Forall_app_2. Qed. +Global Instance zip_with_always_stable {A B} (f : A → B → uPred M) xs ys : + (∀ x y, AS (f x y)) → ASL (zip_with f xs ys). +Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed. +End big_op. \ No newline at end of file