Commit c189f3d6 authored by Robbert Krebbers's avatar Robbert Krebbers

Move uPred big_op stuff to separate file.

parent bdfb180a
...@@ -50,6 +50,7 @@ algebra/excl.v ...@@ -50,6 +50,7 @@ algebra/excl.v
algebra/iprod.v algebra/iprod.v
algebra/functor.v algebra/functor.v
algebra/upred.v algebra/upred.v
algebra/upred_big_op.v
program_logic/model.v program_logic/model.v
program_logic/adequacy.v program_logic/adequacy.v
program_logic/hoare_lifting.v program_logic/hoare_lifting.v
......
...@@ -219,29 +219,15 @@ Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope. ...@@ -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. Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%I.
Infix "↔" := uPred_iff : uPred_scope. 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). Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_} _ _ _ _. Arguments timelessP {_} _ {_} _ _ _ _.
Class AlwaysStable {M} (P : uPred M) := always_stable : P P. Class AlwaysStable {M} (P : uPred M) := always_stable : P P.
Arguments always_stable {_} _ {_} _ _ _ _. Arguments always_stable {_} _ {_} _ _ _ _.
Class AlwaysStableL {M} (Ps : list (uPred M)) :=
always_stableL : Forall AlwaysStable Ps.
Arguments always_stableL {_} _ {_}.
Module uPred. Section uPred_logic. Module uPred. Section uPred_logic.
Context {M : cmraT}. Context {M : cmraT}.
Implicit Types φ : Prop. Implicit Types φ : Prop.
Implicit Types P Q : uPred M. Implicit Types P Q : uPred M.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type. Implicit Types A : Type.
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *) Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Arguments uPred_holds {_} !_ _ _ /. Arguments uPred_holds {_} !_ _ _ /.
...@@ -849,36 +835,6 @@ Proof. done. Qed. ...@@ -849,36 +835,6 @@ Proof. done. Qed.
Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False. Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed. 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 *) (* Timeless *)
Lemma timelessP_spec P : TimelessP P x n, {n} x P 0 x P n x. Lemma timelessP_spec P : TimelessP P x n, {n} x P 0 x P n x.
Proof. Proof.
...@@ -967,23 +923,6 @@ Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) ...@@ -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). AS P ( x, AS (Q x)) AS (default P mx Q).
Proof. destruct mx; apply _. Qed. 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 *) (* Derived lemmas for always stable *)
Lemma always_always P `{!AlwaysStable P} : ( P)%I P. Lemma always_always P `{!AlwaysStable P} : ( P)%I P.
Proof. apply (anti_symm ()); auto using always_elim. Qed. Proof. apply (anti_symm ()); auto using always_elim. Qed.
......
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
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