From 76812039acf60ee3e64cbb5e6794be28cab051ec Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 14 Jun 2018 01:00:48 +0200 Subject: [PATCH] Separating big operator over two lists. --- theories/bi/big_op.v | 278 ++++++++++++++++++++++++++++++++++++++++- theories/bi/notation.v | 7 ++ 2 files changed, 284 insertions(+), 1 deletion(-) diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v index 5d10c244..db7dccbb 100644 --- a/theories/bi/big_op.v +++ b/theories/bi/big_op.v @@ -4,6 +4,21 @@ From stdpp Require Import countable fin_collections functions. Set Default Proof Using "Type". Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi. +(** A version of the separating big operator that ranges over two lists. This +version also ensures that both lists have the same length. Although this version +can be defined in terms of the unary using a [zip] (see [big_sepL2_alt]), we do +not define it that way to get better computational behavior (for [simpl]). *) +Fixpoint big_sepL2 {PROP : bi} {A B} + (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) : PROP := + match l1, l2 with + | [], [] => emp + | x1 :: l1, x2 :: l2 => Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2 + | _, _ => False + end%I. +Instance: Params (@big_sepL2) 3. +Arguments big_sepL2 {PROP A B} _ !_ !_ /. +Typeclasses Opaque big_sepL2. + (* Notations *) Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l) : bi_scope. @@ -12,6 +27,11 @@ Notation "'[∗' 'list]' x ∈ l , P" := Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope. +Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" := + (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope. +Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" := + (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope. + Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l) : bi_scope. Notation "'[∧' 'list]' x ∈ l , P" := @@ -185,7 +205,7 @@ Section sep_list. Proof. induction 1; simpl; apply _. Qed. End sep_list. -Section sep_list2. +Section sep_list_more. Context {A : Type}. Implicit Types l : list A. Implicit Types Φ Ψ : nat → A → PROP. @@ -199,6 +219,217 @@ Section sep_list2. - by rewrite big_sepL_emp left_id. - by rewrite IH. Qed. +End sep_list_more. + +Lemma big_sepL2_alt {A B} (Φ : nat → A → B → PROP) l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) + ⊣⊢ ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ y ∈ zip l1 l2, Φ k (y.1) (y.2). +Proof. + apply (anti_symm _). + - apply and_intro. + + revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2] /=; + auto using pure_intro, False_elim. + rewrite IH sep_elim_r. apply pure_mono; auto. + + revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2] /=; + auto using pure_intro, False_elim. + by rewrite IH. + - apply pure_elim_l=> /Forall2_same_length Hl. revert Φ. + induction Hl as [|x1 l1 x2 l2 _ _ IH]=> Φ //=. by rewrite -IH. +Qed. + +(** ** Big ops over two lists *) +Section sep_list2. + Context {A B : Type}. + Implicit Types Φ Ψ : nat → A → B → PROP. + + Lemma big_sepL2_nil Φ : ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2) ⊣⊢ emp. + Proof. done. Qed. + Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2. + Proof. apply (affine _). Qed. + + Lemma big_sepL2_cons Φ x1 x2 l1 l2 : + ([∗ list] k↦y1;y2 ∈ x1 :: l1; x2 :: l2, Φ k y1 y2) + ⊣⊢ Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2, Φ (S k) y1 y2. + Proof. done. Qed. + Lemma big_sepL2_cons_inv_l Φ x1 l1 l2 : + ([∗ list] k↦y1;y2 ∈ x1 :: l1; l2, Φ k y1 y2) -∗ + ∃ x2 l2', ⌜ l2 = x2 :: l2' ⌝ ∧ + Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2', Φ (S k) y1 y2. + Proof. + destruct l2 as [|x2 l2]; simpl; auto using False_elim. + by rewrite -(exist_intro x2) -(exist_intro l2) pure_True // left_id. + Qed. + Lemma big_sepL2_cons_inv_r Φ x2 l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1; x2 :: l2, Φ k y1 y2) -∗ + ∃ x1 l1', ⌜ l1 = x1 :: l1' ⌝ ∧ + Φ 0 x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1';l2, Φ (S k) y1 y2. + Proof. + destruct l1 as [|x1 l1]; simpl; auto using False_elim. + by rewrite -(exist_intro x1) -(exist_intro l1) pure_True // left_id. + Qed. + + Lemma big_sepL2_singleton Φ x1 x2 : + ([∗ list] k↦y1;y2 ∈ [x1];[x2], Φ k y1 y2) ⊣⊢ Φ 0 x1 x2. + Proof. by rewrite /= right_id. Qed. + + Lemma big_sepL2_length Φ l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) -∗ ⌜ length l1 = length l2 ⌝. + Proof. by rewrite big_sepL2_alt and_elim_l. Qed. + + Lemma big_sepL2_app Φ l1 l2 l1' l2' : + ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) -∗ + ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k) y1 y2) -∗ + ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2). + Proof. + apply wand_intro_r. revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /=. + - by rewrite left_id. + - rewrite left_absorb. apply False_elim. + - rewrite left_absorb. apply False_elim. + - by rewrite -assoc IH. + Qed. + Lemma big_sepL2_app_inv_l Φ l1' l1'' l2 : + ([∗ list] k↦y1;y2 ∈ l1' ++ l1''; l2, Φ k y1 y2) -∗ + ∃ l2' l2'', ⌜ l2 = l2' ++ l2'' ⌝ ∧ + ([∗ list] k↦y1;y2 ∈ l1';l2', Φ k y1 y2) ∗ + ([∗ list] k↦y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2). + Proof. + rewrite -(exist_intro (take (length l1') l2)) + -(exist_intro (drop (length l1') l2)) take_drop pure_True // left_id. + revert Φ l2. induction l1' as [|x1 l1' IH]=> Φ -[|x2 l2] /=; + [by rewrite left_id|by rewrite left_id|apply False_elim|]. + by rewrite IH -assoc. + Qed. + Lemma big_sepL2_app_inv_r Φ l1 l2' l2'' : + ([∗ list] k↦y1;y2 ∈ l1; l2' ++ l2'', Φ k y1 y2) -∗ + ∃ l1' l1'', ⌜ l1 = l1' ++ l1'' ⌝ ∧ + ([∗ list] k↦y1;y2 ∈ l1';l2', Φ k y1 y2) ∗ + ([∗ list] k↦y1;y2 ∈ l1'';l2'', Φ (length l2' + k) y1 y2). + Proof. + rewrite -(exist_intro (take (length l2') l1)) + -(exist_intro (drop (length l2') l1)) take_drop pure_True // left_id. + revert Φ l1. induction l2' as [|x2 l2' IH]=> Φ -[|x1 l1] /=; + [by rewrite left_id|by rewrite left_id|apply False_elim|]. + by rewrite IH -assoc. + Qed. + + Lemma big_sepL2_mono Φ Ψ l1 l2 : + (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) → + ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2. + Proof. + intros H. rewrite !big_sepL2_alt. f_equiv. apply big_sepL_mono=> k [y1 y2]. + rewrite lookup_zip_with=> ?; simplify_option_eq; auto. + Qed. + Lemma big_sepL2_proper Φ Ψ l1 l2 : + (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊣⊢ Ψ k y1 y2) → + ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2. + Proof. + intros; apply (anti_symm _); + apply big_sepL2_mono; auto using equiv_entails, equiv_entails_sym. + Qed. + + Global Instance big_sepL2_ne n : + Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n))) + ==> (=) ==> (=) ==> (dist n)) + (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)). + Proof. + intros Φ1 Φ2 HΦ x1 ? <- x2 ? <-. rewrite !big_sepL2_alt. f_equiv. + f_equiv=> k [y1 y2]. apply HΦ. + Qed. + Global Instance big_sepL2_mono' : + Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢))) + ==> (=) ==> (=) ==> (⊢)) + (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)). + Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_mono; intros; apply Hf. Qed. + Global Instance big_sepL2_proper' : + Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢))) + ==> (=) ==> (=) ==> (⊣⊢)) + (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)). + Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_proper; intros; apply Hf. Qed. + + Lemma big_sepL2_lookup_acc Φ l1 l2 i x1 x2 : + l1 !! i = Some x1 → l2 !! i = Some x2 → + ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ + Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)). + Proof. + intros Hl1 Hl2. rewrite big_sepL2_alt. apply pure_elim_l=> Hl. + rewrite {1}big_sepL_lookup_acc; last by rewrite lookup_zip_with; simplify_option_eq. + by rewrite pure_True // left_id. + Qed. + + Lemma big_sepL2_lookup Φ l1 l2 i x1 x2 `{!Absorbing (Φ i x1 x2)} : + l1 !! i = Some x1 → l2 !! i = Some x2 → + ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ Φ i x1 x2. + Proof. intros. rewrite big_sepL2_lookup_acc //. by rewrite sep_elim_l. Qed. + + Lemma big_sepL2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) l1 l2 : + ([∗ list] k↦y1;y2 ∈ f <\$> l1; l2, Φ k y1 y2) + ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k (f y1) y2). + Proof. + rewrite !big_sepL2_alt fmap_length zip_with_fmap_l zip_with_zip big_sepL_fmap. + by f_equiv; f_equiv=> k [??]. + Qed. + Lemma big_sepL2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1; g <\$> l2, Φ k y1 y2) + ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 (g y2)). + Proof. + rewrite !big_sepL2_alt fmap_length zip_with_fmap_r zip_with_zip big_sepL_fmap. + by f_equiv; f_equiv=> k [??]. + Qed. + + Lemma big_sepL2_sepL2 Φ Ψ l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2) + ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2). + Proof. + rewrite !big_sepL2_alt big_sepL_sepL !persistent_and_affinely_sep_l. + rewrite -assoc (assoc _ _ ( _)%I). rewrite -(comm bi_sep ( _)%I). + rewrite -assoc (assoc _ _ ( _)%I) -!persistent_and_affinely_sep_l. + by rewrite affinely_and_r persistent_and_affinely_sep_l idemp. + Qed. + + Lemma big_sepL2_and Φ Ψ l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∧ Ψ k y1 y2) + ⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∧ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2). + Proof. auto using and_intro, big_sepL2_mono, and_elim_l, and_elim_r. Qed. + + Lemma big_sepL2_persistently `{BiAffine PROP} Φ l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) + ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, (Φ k y1 y2). + Proof. + by rewrite !big_sepL2_alt persistently_and persistently_pure big_sepL_persistently. + Qed. + + Lemma big_sepL2_impl Φ Ψ l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗ + □ (∀ k x1 x2, + ⌜l1 !! k = Some x1⌝ → ⌜l2 !! k = Some x2⌝ → Φ k x1 x2 -∗ Ψ k x1 x2) -∗ + [∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2. + Proof. + apply wand_intro_l. revert Φ Ψ l2. + induction l1 as [|x1 l1 IH]=> Φ Ψ [|x2 l2] /=; [by rewrite sep_elim_r..|]. + rewrite intuitionistically_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. + apply sep_mono. + - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2) !pure_True // !True_impl. + by rewrite intuitionistically_elim wand_elim_l. + - rewrite comm -(IH (Φ ∘ S) (Ψ ∘ S)) /=. + apply sep_mono_l, affinely_mono, persistently_mono. + apply forall_intro=> k. by rewrite (forall_elim (S k)). + Qed. + + Global Instance big_sepL2_nil_persistent Φ : + Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2). + Proof. simpl; apply _. Qed. + Global Instance big_sepL2_persistent Φ l1 l2 : + (∀ k x1 x2, Persistent (Φ k x1 x2)) → + Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2). + Proof. rewrite big_sepL2_alt. apply _. Qed. + + Global Instance big_sepL2_nil_affine Φ : + Affine ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2). + Proof. simpl; apply _. Qed. + Global Instance big_sepL2_affine Φ l1 l2 : + (∀ k x1 x2, Affine (Φ k x1 x2)) → + Affine ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2). + Proof. rewrite big_sepL2_alt. apply _. Qed. End sep_list2. Section and_list. @@ -757,6 +988,51 @@ Section list. End plainly. End list. +Section list2. + Context {A B : Type}. + Implicit Types Φ Ψ : nat → A → B → PROP. + + Lemma big_sepL2_later_2 Φ l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2. + Proof. + rewrite !big_sepL2_alt bi.later_and big_sepL_later_2. + auto using and_mono, later_intro. + Qed. + + Lemma big_sepL2_laterN_2 Φ n l1 l2 : + ([∗ list] k↦y1;y2 ∈ l1;l2, ▷^n Φ k y1 y2) ⊢ ▷^n [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2. + Proof. + rewrite !big_sepL2_alt bi.laterN_and big_sepL_laterN_2. + auto using and_mono, laterN_intro. + Qed. + + Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ : + Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2). + Proof. simpl; apply _. Qed. + Global Instance big_sepL2_timeless `{!Timeless (emp%I : PROP)} Φ l1 l2 : + (∀ k x1 x2, Timeless (Φ k x1 x2)) → + Timeless ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2). + Proof. rewrite big_sepL2_alt. apply _. Qed. + + Section plainly. + Context `{!BiPlainly PROP}. + + Lemma big_sepL2_plainly `{!BiAffine PROP} Φ l1 l2 : + ■ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) + ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, ■ (Φ k y1 y2). + Proof. by rewrite !big_sepL2_alt plainly_and plainly_pure big_sepL_plainly. Qed. + + Global Instance big_sepL2_nil_plain `{!BiAffine PROP} Φ : + Plain ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2). + Proof. simpl; apply _. Qed. + + Global Instance big_sepL2_plain `{!BiAffine PROP} Φ l1 l2 : + (∀ k x1 x2, Plain (Φ k x1 x2)) → + Plain ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2). + Proof. rewrite big_sepL2_alt. apply _. Qed. + End plainly. +End list2. + (** ** Big ops over finite maps *) Section gmap. Context `{Countable K} {A : Type}. diff --git a/theories/bi/notation.v b/theories/bi/notation.v index 0b463cee..84afd784 100644 --- a/theories/bi/notation.v +++ b/theories/bi/notation.v @@ -96,6 +96,13 @@ 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 "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" + (at level 200, l1, l2 at level 10, k, x1, x2 at level 1, right associativity, + format "[∗ list] k ↦ x1 ; x2 ∈ l1 ; l2 , P"). +Reserved Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" + (at level 200, l1, l2 at level 10, x1, x2 at level 1, right associativity, + format "[∗ list] x1 ; x2 ∈ l1 ; l2 , P"). + Reserved Notation "'[∗]' Ps" (at level 20). Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P" -- GitLab