diff --git a/algebra/cmra.v b/algebra/cmra.v index 1b5323bb2e15f6171691f43d780ac661051a72e6..87f4f717be9238d500ee282647a6362102e6d33d 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -1033,14 +1033,11 @@ Section option. (** Misc *) Global Instance Some_cmra_monotone : CMRAMonotone Some. Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed. + + Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None. + Proof. destruct mx, my; naive_solver. Qed. Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my. - Proof. - destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver. - Qed. - Lemma option_op_positive_dist_l n mx my : mx ⋅ my ≡{n}≡ None → mx ≡{n}≡ None. - Proof. by destruct mx, my; inversion_clear 1. Qed. - Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None. - Proof. by destruct mx, my; inversion_clear 1. Qed. + Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed. Global Instance Some_persistent (x : A) : Persistent x → Persistent (Some x). Proof. by constructor. Qed. diff --git a/algebra/gmap.v b/algebra/gmap.v index 5b5c3bad882af46c564ac69ca72ace690800bbbf..c9858eba7755b01a9258b98ff8ea8f9bcb4eff6e 100644 --- a/algebra/gmap.v +++ b/algebra/gmap.v @@ -147,11 +147,11 @@ Proof. + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor]. rewrite -Hx; apply (proj2_sig (f i)). + destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|]. - pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. - by symmetry; apply option_op_positive_dist_l with (m2 !! i). + move: (Hm12' i). rewrite Hx -!timeless_iff. + rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto. + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. - pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. - by symmetry; apply option_op_positive_dist_r with (m1 !! i). + move: (Hm12' i). rewrite Hx -!timeless_iff. + rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto. Qed. Canonical Structure gmapR := CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.