From a9be19ebf36b6fb3e7a7451757195364aae67619 Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim Date: Wed, 2 Sep 2020 13:49:00 -0400 Subject: [PATCH 1/3] Generalize the type of gmap_equivI. --- theories/algebra/gmap.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index 3cdc9c7bf..a1dbfb08f 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -94,6 +94,9 @@ Global Instance gmap_singleton_discrete i x : Lemma insert_idN n m i x : m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m. Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed. + +Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i. +Proof. by uPred.unseal. Qed. End cofe. Arguments gmapO _ {_ _} _. @@ -232,8 +235,6 @@ Qed. Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin. (** Internalized properties *) -Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i. -Proof. by uPred.unseal. Qed. Lemma gmap_validI {M} m : ✓ m ⊣⊢@{uPredI M} ∀ i, ✓ (m !! i). Proof. by uPred.unseal. Qed. End cmra. -- GitLab From e992caeac1e51a7e8c5b3075a98b214d24980b4a Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim Date: Thu, 3 Sep 2020 10:07:07 -0400 Subject: [PATCH 2/3] Add comment to lemma. --- theories/algebra/gmap.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index a1dbfb08f..6e3b7311a 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -95,6 +95,7 @@ Lemma insert_idN n m i x : m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m. Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed. +(** Internalized properties *) Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i. Proof. by uPred.unseal. Qed. End cofe. -- GitLab From e24d0280711e573a81a13f385c2574ca897a8826 Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim Date: Thu, 3 Sep 2020 10:32:12 -0400 Subject: [PATCH 3/3] Generalize other equivalence lemmas as well. --- theories/algebra/auth.v | 8 +++++--- theories/algebra/csum.v | 24 +++++++++++++----------- theories/algebra/list.v | 6 ++++-- 3 files changed, 22 insertions(+), 16 deletions(-) diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v index f98f368fa..8ae286844 100644 --- a/theories/algebra/auth.v +++ b/theories/algebra/auth.v @@ -69,6 +69,11 @@ Global Instance Auth_discrete a b : Proof. by intros ?? [??] [??]; split; apply: discrete. Qed. Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authO. Proof. intros ? [??]; apply _. Qed. + +(** Internalized properties *) +Lemma auth_equivI {M} x y : + x ≡ y ⊣⊢@{uPredI M} auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y. +Proof. by uPred.unseal. Qed. End ofe. Arguments authO : clear implicits. @@ -329,9 +334,6 @@ Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b : Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed. (** Internalized properties *) -Lemma auth_equivI {M} x y : - x ≡ y ⊣⊢@{uPredI M} auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y. -Proof. by uPred.unseal. Qed. Lemma auth_validI {M} x : ✓ x ⊣⊢@{uPredI M} match auth_auth_proj x with | Some (q, ag) => ✓ q ∧ diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v index 477c3f3e5..e6b483a42 100644 --- a/theories/algebra/csum.v +++ b/theories/algebra/csum.v @@ -107,6 +107,19 @@ Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a). Proof. by inversion_clear 2; constructor; apply (discrete _). Qed. Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b). Proof. by inversion_clear 2; constructor; apply (discrete _). Qed. + +(** Internalized properties *) +Lemma csum_equivI {M} (x y : csum A B) : + x ≡ y ⊣⊢@{uPredI M} match x, y with + | Cinl a, Cinl a' => a ≡ a' + | Cinr b, Cinr b' => b ≡ b' + | CsumBot, CsumBot => True + | _, _ => False + end. +Proof. + uPred.unseal; do 2 split; first by destruct 1. + by destruct x, y; try destruct 1; try constructor. +Qed. End cofe. Arguments csumO : clear implicits. @@ -287,17 +300,6 @@ Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b). Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed. (** Internalized properties *) -Lemma csum_equivI {M} (x y : csum A B) : - x ≡ y ⊣⊢@{uPredI M} match x, y with - | Cinl a, Cinl a' => a ≡ a' - | Cinr b, Cinr b' => b ≡ b' - | CsumBot, CsumBot => True - | _, _ => False - end. -Proof. - uPred.unseal; do 2 split; first by destruct 1. - by destruct x, y; try destruct 1; try constructor. -Qed. Lemma csum_validI {M} (x : csum A B) : ✓ x ⊣⊢@{uPredI M} match x with | Cinl a => ✓ a diff --git a/theories/algebra/list.v b/theories/algebra/list.v index 1abbc20fc..50ceac0f1 100644 --- a/theories/algebra/list.v +++ b/theories/algebra/list.v @@ -93,6 +93,10 @@ Global Instance nil_discrete : Discrete (@nil A). Proof. inversion_clear 1; constructor. Qed. Global Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x :: l). Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed. + +(** Internalized properties *) +Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i. +Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed. End cofe. Arguments listO : clear implicits. @@ -311,8 +315,6 @@ Section cmra. Proof. intros Hyp; by apply list_core_id'. Qed. (** Internalized properties *) - Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i. - Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed. Lemma list_validI {M} l : ✓ l ⊣⊢@{uPredI M} ∀ i, ✓ (l !! i). Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. End cmra. -- GitLab