upred_big_op.v 4.36 KB
Newer Older
1
From algebra Require Export upred.
2
From prelude Require Import fin_maps fin_collections.
3

4
5
6
7
8
9
10
11
12
13
(** * Big ops over lists *)
(* These are the basic building blocks for other big ops *)
Fixpoint uPred_list_and {M} (Ps : list (uPred M)) : uPred M:=
  match Ps with [] => True | P :: Ps => P  uPred_list_and Ps end%I.
Instance: Params (@uPred_list_and) 1.
Notation "'Π∧' Ps" := (uPred_list_and Ps) (at level 20) : uPred_scope.
Fixpoint uPred_list_sep {M} (Ps : list (uPred M)) : uPred M :=
  match Ps with [] => True | P :: Ps => P  uPred_list_sep Ps end%I.
Instance: Params (@uPred_list_sep) 1.
Notation "'Π★' Ps" := (uPred_list_sep Ps) (at level 20) : uPred_scope.
14

15
16
17
18
19
20
21
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
Class UPredBigSep (M : cmraT) (A B : Type) :=
  uPred_big_sep : A  B  uPred M.
Instance: Params (@uPred_big_sep) 4.
Notation "'Π★{' x } P" := (uPred_big_sep x P)
  (at level 20, x at level 10, format "Π★{ x }  P") : uPred_scope.
22

23
24
25
26
27
28
29
Instance uPred_big_sepM {M} `{FinMapToList K A MA} :
    UPredBigSep M MA (K  A  uPred M) := λ m P,
  uPred_list_sep (curry P <$> map_to_list m).
Instance uPred_big_sepC {M} `{Elements A C} :
  UPredBigSep M C (A  uPred M) := λ X P, uPred_list_sep (P <$> elements X).

(** * Always stability for lists *)
30
31
32
33
34
35
36
37
38
39
40
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 *)
41
Global Instance list_and_proper : Proper (() ==> ()) (@uPred_list_and M).
42
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
43
Global Instance list_sep_proper : Proper (() ==> ()) (@uPred_list_sep M).
44
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
45
Global Instance list_and_perm : Proper (() ==> ()) (@uPred_list_and M).
46
47
48
49
50
51
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
  * by rewrite IH.
  * by rewrite !assoc (comm _ P).
  * etransitivity; eauto.
Qed.
52
Global Instance list_sep_perm : Proper (() ==> ()) (@uPred_list_sep M).
53
54
55
56
57
58
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
  * by rewrite IH.
  * by rewrite !assoc (comm _ P).
  * etransitivity; eauto.
Qed.
59
Lemma list_and_app Ps Qs : (Π (Ps ++ Qs))%I  (Π Ps  Π Qs)%I.
60
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
61
Lemma list_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I  (Π★ Ps  Π★ Qs)%I.
62
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
63
Lemma list_sep_and Ps : (Π★ Ps)  (Π Ps).
64
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
65
Lemma list_and_elem_of Ps P : P  Ps  (Π Ps)  P.
66
Proof. induction 1; simpl; auto with I. Qed.
67
Lemma list_sep_elem_of Ps P : P  Ps  (Π★ Ps)  P.
68
69
Proof. induction 1; simpl; auto with I. Qed.

70
71
72
73
(* Big ops over finite maps *)
Section fin_map.
  Context `{FinMap K Ma} {A} (P : K  A  uPred M).

74
75
  Lemma big_sepM_empty : (Π★{} P)%I  True%I.
  Proof. by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_empty. Qed.
76
  Lemma big_sepM_insert (m : Ma A) i x :
77
78
79
80
81
    m !! i = None  (Π★{<[i:=x]> m} P)%I  (P i x  Π★{m} P)%I.
  Proof.
    intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert.
  Qed.
  Lemma big_sepM_singleton i x : (Π★{{[i  x]}} P)%I  (P i x)%I.
82
83
84
85
86
87
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
End fin_map.

88
89
90
(* Always stable *)
Local Notation AS := AlwaysStable.
Local Notation ASL := AlwaysStableL.
91
Global Instance list_and_always_stable Ps : ASL Ps  AS (Π Ps).
92
Proof. induction 1; apply _. Qed.
93
Global Instance list_sep_always_stable Ps : ASL Ps  AS (Π★ Ps).
94
95
96
97
98
99
100
101
102
103
104
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.
105
End big_op.