Commit 96184edb authored by Robbert Krebbers's avatar Robbert Krebbers

Better statement of posivitity of option.

parent 46ca1ffc
...@@ -1033,14 +1033,11 @@ Section option. ...@@ -1033,14 +1033,11 @@ Section option.
(** Misc *) (** Misc *)
Global Instance Some_cmra_monotone : CMRAMonotone Some. Global Instance Some_cmra_monotone : CMRAMonotone Some.
Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed. 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. Lemma op_is_Some mx my : is_Some (mx my) is_Some mx is_Some my.
Proof. Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
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.
Global Instance Some_persistent (x : A) : Persistent x Persistent (Some x). Global Instance Some_persistent (x : A) : Persistent x Persistent (Some x).
Proof. by constructor. Qed. Proof. by constructor. Qed.
......
...@@ -147,11 +147,11 @@ Proof. ...@@ -147,11 +147,11 @@ Proof.
+ destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor]. + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
rewrite -Hx; apply (proj2_sig (f i)). rewrite -Hx; apply (proj2_sig (f i)).
+ destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [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''. move: (Hm12' i). rewrite Hx -!timeless_iff.
by symmetry; apply option_op_positive_dist_l with (m2 !! i). rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
+ destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. move: (Hm12' i). rewrite Hx -!timeless_iff.
by symmetry; apply option_op_positive_dist_r with (m1 !! i). rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
Qed. Qed.
Canonical Structure gmapR := Canonical Structure gmapR :=
CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin. CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
......
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