From ac9e1471a329e714f57cee5c9dee57f992d0b9df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 11 Jun 2023 15:41:57 +0200
Subject: [PATCH] Tweak proofs.

---
 iris/algebra/dyn_reservation_map.v | 2 +-
 iris/algebra/gmap.v                | 2 +-
 iris/algebra/reservation_map.v     | 2 +-
 iris/algebra/view.v                | 8 ++++----
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index fd59b3a80..b31404a90 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -243,7 +243,7 @@ Section cmra.
 
   Lemma dyn_reservation_map_data_mono k a b :
     a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
-  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. eauto. Qed.
+  Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.
   Global Instance dyn_reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 4715bdc62..58ce801bb 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -346,7 +346,7 @@ Lemma singleton_included_l m i x :
 Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    exists (x â‹…? m' !! i). rewrite -Some_op_opM. eauto.
+    exists (x â‹…? m' !! i). by rewrite -Some_op_opM.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index ea300bbf5..1be3502ff 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -225,7 +225,7 @@ Section cmra.
   Qed.
   Lemma reservation_map_data_mono k a b :
     a ≼ b → reservation_map_data k a ≼ reservation_map_data k b.
-  Proof. intros [c ->]. rewrite reservation_map_data_op. eauto. Qed.
+  Proof. intros [c ->]. by rewrite reservation_map_data_op. Qed.
   Global Instance reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (reservation_map_data k a) (reservation_map_data k b1) (reservation_map_data k b2).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 5add4f59d..5392eb6f0 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -288,7 +288,7 @@ Section cmra.
   Lemma view_frag_op b1 b2 : â—¯V (b1 â‹… b2) = â—¯V b1 â‹… â—¯V b2.
   Proof. done. Qed.
   Lemma view_frag_mono b1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
-  Proof. intros [c ->]. rewrite view_frag_op. eauto. Qed.
+  Proof. intros [c ->]. by rewrite view_frag_op. Qed.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
   Lemma view_both_core_discarded a b :
@@ -424,8 +424,8 @@ Section cmra.
       + apply equiv_dist=> n.
         by eapply view_auth_dfrac_includedN, cmra_included_includedN.
     - intros [[[dq ->]| ->] ->].
-      + rewrite view_auth_dfrac_op -assoc. eauto.
-      + eauto.
+      + by rewrite view_auth_dfrac_op -assoc.
+      + done.
   Qed.
   Lemma view_auth_includedN n a1 a2 b :
     ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
@@ -448,7 +448,7 @@ Section cmra.
     split.
     - intros [xf [_ Hb]]; simpl in *.
       revert Hb; rewrite left_id. by exists (view_frag_proj xf).
-    - intros [bf ->]. rewrite comm view_frag_op -assoc. eauto.
+    - intros [bf ->]. by rewrite comm view_frag_op -assoc.
   Qed.
 
   (** The weaker [view_both_included] lemmas below are a consequence of the
-- 
GitLab