Commit c7164230 authored by Robbert Krebbers's avatar Robbert Krebbers

Big-op `big_orL` for disjunction over lists.

parent 84490edc
......@@ -9,16 +9,20 @@ Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
(big_opL bi_sep (λ k x, P) l) : bi_scope.
Notation "'[∗' 'list]' x ∈ l , P" :=
(big_opL bi_sep (λ _ x, P) l) : bi_scope.
Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
(big_opL bi_and (λ k x, P) l) : bi_scope.
Notation "'[∧' 'list]' x ∈ l , P" :=
(big_opL bi_and (λ _ x, P) l) : bi_scope.
Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.
Notation "'[∨' 'list]' k ↦ x ∈ l , P" :=
(big_opL bi_or (λ k x, P) l) : bi_scope.
Notation "'[∨' 'list]' x ∈ l , P" :=
(big_opL bi_or (λ _ x, P) l) : bi_scope.
Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps) : bi_scope.
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.
......@@ -536,6 +540,104 @@ Section and_list.
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
End and_list.
Section or_list.
Context {A : Type}.
Implicit Types l : list A.
Implicit Types Φ Ψ : nat A PROP.
Lemma big_orL_nil Φ : ([ list] ky nil, Φ k y) False.
Proof. done. Qed.
Lemma big_orL_cons Φ x l :
([ list] ky x :: l, Φ k y) Φ 0 x [ list] ky l, Φ (S k) y.
Proof. by rewrite big_opL_cons. Qed.
Lemma big_orL_singleton Φ x : ([ list] ky [x], Φ k y) Φ 0 x.
Proof. by rewrite big_opL_singleton. Qed.
Lemma big_orL_app Φ l1 l2 :
([ list] ky l1 ++ l2, Φ k y)
([ list] ky l1, Φ k y) ([ list] ky l2, Φ (length l1 + k) y).
Proof. by rewrite big_opL_app. Qed.
Lemma big_orL_mono Φ Ψ l :
( k y, l !! k = Some y Φ k y Ψ k y)
([ list] k y l, Φ k y) [ list] k y l, Ψ k y.
Proof. apply big_opL_forall; apply _. Qed.
Lemma big_orL_proper Φ Ψ l :
( k y, l !! k = Some y Φ k y Ψ k y)
([ list] k y l, Φ k y) ([ list] k y l, Ψ k y).
Proof. apply big_opL_proper. Qed.
Lemma big_orL_submseteq (Φ : A PROP) l1 l2 :
l1 + l2 ([ list] y l1, Φ y) [ list] y l2, Φ y.
Proof.
intros [l ->]%submseteq_Permutation. by rewrite big_orL_app -or_intro_l.
Qed.
Global Instance big_orL_mono' :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
(big_opL (@bi_or PROP) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
Global Instance big_orL_id_mono' :
Proper (Forall2 () ==> ()) (big_opL (@bi_or PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_orL_lookup Φ l i x :
l !! i = Some x Φ i x ([ list] ky l, Φ k y).
Proof.
intros. rewrite -(take_drop_middle l i x) // big_orL_app /=.
rewrite Nat.add_0_r take_length_le;
eauto using lookup_lt_Some, Nat.lt_le_incl, or_intro_l', or_intro_r'.
Qed.
Lemma big_orL_elem_of (Φ : A PROP) l x :
x l Φ x ([ list] y l, Φ y).
Proof.
intros [i ?]%elem_of_list_lookup; eauto using (big_orL_lookup (λ _, Φ)).
Qed.
Lemma big_orL_fmap {B} (f : A B) (Φ : nat B PROP) l :
([ list] ky f <$> l, Φ k y) ([ list] ky l, Φ k (f y)).
Proof. by rewrite big_opL_fmap. Qed.
Lemma big_orL_or Φ Ψ l :
([ list] kx l, Φ k x Ψ k x)
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_op. Qed.
Lemma big_orL_persistently Φ l :
<pers> ([ list] kx l, Φ k x) [ list] kx l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_orL_exist Φ l :
([ list] kx l, Φ k x) ( k x, l !! k = Some x Φ k x).
Proof.
apply (anti_symm _).
{ revert Φ. induction l as [|x l IH]=> Φ.
{ rewrite big_orL_nil. apply False_elim. }
rewrite big_orL_cons. apply or_elim.
- by rewrite -(exist_intro 0) -(exist_intro x) pure_True // left_id.
- rewrite IH. apply exist_elim=> k. by rewrite -(exist_intro (S k)). }
apply exist_elim=> k; apply exist_elim=> x. apply pure_elim_l=> ?.
by apply: big_orL_lookup.
Qed.
Lemma big_orL_sep_l P Φ l :
P ([ list] kx l, Φ k x) ([ list] kx l, P Φ k x).
Proof.
rewrite !big_orL_exist sep_exist_l.
f_equiv=> k. rewrite sep_exist_l. f_equiv=> x.
by rewrite !persistent_and_affinely_sep_l !assoc (comm _ P).
Qed.
Lemma big_orL_sep_r Q Φ l :
([ list] kx l, Φ k x) Q ([ list] kx l, Φ k x Q).
Proof. setoid_rewrite (comm bi_sep). apply big_orL_sep_l. Qed.
Global Instance big_orL_nil_persistent Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_orL_persistent Φ l :
( k x, Persistent (Φ k x)) Persistent ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
End or_list.
(** ** Big ops over finite maps *)
Section map.
Context `{Countable K} {A : Type}.
......@@ -1340,6 +1442,18 @@ Section list.
Global Instance big_andL_plain Φ l :
( k x, Plain (Φ k x)) Plain ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Lemma big_orL_plainly `{!BiPlainlyExist PROP} Φ l :
([ list] kx l, Φ k x) [ list] kx l, (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Global Instance big_orL_nil_plain Φ :
Plain ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_orL_plain Φ l :
( k x, Plain (Φ k x)) Plain ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
End plainly.
End list.
......
......@@ -120,6 +120,15 @@ Reserved Notation "'[∧' 'list]' x ∈ l , P"
Reserved Notation "'[∧]' Ps" (at level 20).
Reserved Notation "'[∨' 'list]' k ↦ x ∈ l , P"
(at level 200, l at level 10, k, x at level 1, right associativity,
format "[∨ list] k ↦ x ∈ l , P").
Reserved Notation "'[∨' 'list]' x ∈ l , P"
(at level 200, l at level 10, x at level 1, right associativity,
format "[∨ list] x ∈ l , P").
Reserved Notation "'[∨]' Ps" (at level 20).
Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[∗ map] k ↦ x ∈ m , P").
......
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