Update proofs

theories/algebra/auth.v

@@ -366,14 +366,13 @@ Lemma auth_update a b a' b' :
   (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
 Proof.
   intros Hup; apply cmra_total_update.
-  move=> n [[[??]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
-  + exfalso. move : VL => /frac_valid'.
-    rewrite frac_op'. by apply Qp_not_plus_q_ge_1.
-  + split; [done|]. apply (inj to_agree) in Eq.
-    move: Ha; rewrite !left_id -assoc => Ha.
-    destruct (Hup n (Some (bf1 ⋅ bf2))); [by rewrite Eq..|]. simpl in *.
-    exists a'. split; [done|]. split; [|done]. exists bf2.
-    by rewrite left_id -assoc.
+  move=> n [[qa|] bf1] [/= Hq [a0 [Haa0 [[bf2 Ha] Ha0]]]]; do 2 red; simpl in *.
+  { by apply (exclusiveN_l _ _) in Hq. }
+  split; [done|]. apply (inj to_agree) in Haa0.
+  move: Ha; rewrite !left_id -assoc=> Ha.
+  destruct (Hup n (Some (bf1 ⋅ bf2))); [by rewrite Haa0..|]; simpl in *.
+  exists a'. split_and!; [done| |done].
+  exists bf2. by rewrite left_id -assoc.
 Qed.
 
 Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
@@ -388,16 +387,14 @@ Qed.
 Lemma auth_update_core_id q a b `{!CoreId b} :
   b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
 Proof.
-  intros Heq%core_id_extract; last done. apply cmra_total_update.
-  move=> n [[[q' ag]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
-  + split; first done.
-    exists a0. split; last split; try done. exists bf2.
-    assert (a ≡{n}≡ a0) as Eq2. { apply to_agree_includedN. exists ag. done. }
-    by rewrite left_id -Eq2 -assoc -comm Heq Eq2 Ha left_id.
-  + split; first done. exists a0.
-    split; first done. split; last done. exists bf2.
-    apply (inj to_agree) in Eq.
-    by rewrite left_id -Eq -assoc -comm Heq Eq Ha left_id.
+  intros Ha%(core_id_extract _ _). apply cmra_total_update.
+  move=> n [[[q' ag]|] bf1] [Hq [a0 [Haa0 [Hbf1 Ha0]]]]; do 2 red; simpl in *.
+  + split; [done|]. exists a0. split_and!; [done| |done].
+    assert (a ≡{n}≡ a0) as Haa0' by (apply to_agree_includedN; by exists ag).
+    rewrite -Haa0' Ha Haa0' -assoc (comm _ b) assoc. by apply cmra_monoN_r.
+  + split; [done|]. exists a0. split_and!; [done| |done].
+    apply (inj to_agree) in Haa0.
+    rewrite -Haa0 Ha Haa0 -assoc (comm _ b) assoc. by apply cmra_monoN_r.
 Qed.
 
 Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ● a ⋅ ◯ b ~~> ● a'.