From ed0670be2022bf0825262fd57edaa65699d5007f Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl> Date: Sat, 22 Jul 2023 13:30:58 +0000 Subject: [PATCH] simplify proofs and tweak lemma names --- iris/algebra/cmra.v | 20 ++++---------------- iris/algebra/local_updates.v | 2 +- 2 files changed, 5 insertions(+), 17 deletions(-) diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v index afdb92332..2dfb4a3d7 100644 --- a/iris/algebra/cmra.v +++ b/iris/algebra/cmra.v @@ -1524,25 +1524,13 @@ Section option. Lemma Some_included_is_Some x mb : Some x ≼ mb → is_Some mb. Proof. rewrite option_included. naive_solver. Qed. - Lemma Some_includedN_alt n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc. + Lemma Some_includedN_opM n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc. Proof. - rewrite Some_includedN. split. - - intros [Heq|[c Heq]]. - + exists None. auto. - + exists (Some c). auto. - - intros [[c|] Heq]. - + right. exists c. auto. - + left. auto. + rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM. Qed. - Lemma Some_included_alt a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc. + Lemma Some_included_opM a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc. Proof. - rewrite Some_included. split. - - intros [Heq|[c Heq]]. - + exists None. auto. - + exists (Some c). auto. - - intros [[c|] Heq]. - + right. exists c. auto. - + left. auto. + rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM. Qed. Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b. diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v index 429e93e5b..9c722d4d8 100644 --- a/iris/algebra/local_updates.v +++ b/iris/algebra/local_updates.v @@ -84,7 +84,7 @@ Section updates. - apply (cmra_validN_le n); last lia. move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l. - eapply (cmra_includedN_le n); last lia. - apply Some_includedN_alt. eauto. + apply Some_includedN_opM. eauto. Qed. Lemma local_update_valid `{!CmraDiscrete A} x y x' y' : (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y'). -- GitLab