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
(** * Big ops over lists *)
(* These are the basic building blocks for other big ops *)
6
7
8
9
10
11
12
13
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.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
14

15
16
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
17
18
19
20
Definition uPred_big_sepM {M} `{FinMapToList K A MA}
    (m : MA) (P : K  A  uPred M) : uPred M :=
  uPred_big_sep (curry P <$> map_to_list m).
Notation "'Π★{map' m } P" := (uPred_big_sepM m P)
21
  (at level 20, m at level 10, format "Π★{map  m }  P") : uPred_scope.
22

23
24
25
Definition uPred_big_sepS {M} `{Elements A C}
  (X : C) (P : A  uPred M) : uPred M := uPred_big_sep (P <$> elements X).
Notation "'Π★{set' X } P" := (uPred_big_sepS X P)
26
  (at level 20, X at level 10, format "Π★{set  X }  P") : uPred_scope.
27
28

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

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

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

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