From d2ac9c4e89d9df391070a541e34a1ebcdc90e9f4 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Fri, 20 Oct 2023 20:26:07 +0200
Subject: [PATCH] consistently use bullets for goals in proofs

---
 raft-proofs/AppendEntriesLeaderProof.v | 14 +++++---------
 raft-proofs/PrefixWithinTermProof.v    |  8 ++++----
 2 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/raft-proofs/AppendEntriesLeaderProof.v b/raft-proofs/AppendEntriesLeaderProof.v
index 12ba056..d20e1bb 100644
--- a/raft-proofs/AppendEntriesLeaderProof.v
+++ b/raft-proofs/AppendEntriesLeaderProof.v
@@ -18,9 +18,7 @@ Section AppendEntriesLeader.
   Context {orig_base_params : BaseParams}.
   Context {one_node_params : OneNodeParams orig_base_params}.
   Context {raft_params : RaftParams orig_base_params}.
-
   Context {rri : raft_refinement_interface}.
-
   Context {aecfli : append_entries_came_from_leaders_interface}.
   Context {ollpti : one_leaderLog_per_term_interface}.
   Context {lltsi : leaderLogs_term_sanity_interface}.
@@ -84,7 +82,6 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved; eauto using handleClientRequest_TTLM.
-        eauto.
       + eauto.
     - find_apply_lem_hyp handleClientRequest_packets.
       subst. simpl in *. intuition.
@@ -113,7 +110,6 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved; eauto using handleTimeout_TTLM.
-        eauto.
       + eauto.
     - do_in_map.
       find_eapply_lem_hyp handleTimeout_packets; eauto.
@@ -141,7 +137,7 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved.
-        2-9:eauto using handleAppendEntries_TTLM.
+        2-7:eauto using handleAppendEntries_TTLM.
         eauto.
       + eauto.
     - find_apply_lem_hyp handleAppendEntries_not_append_entries.
@@ -169,7 +165,7 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved.
-        2-9: eauto using handleAppendEntriesReply_TTLM.
+        2-7: eauto using handleAppendEntriesReply_TTLM.
         eauto.
       + eauto.
     - find_apply_lem_hyp handleAppendEntriesReply_packets.
@@ -197,7 +193,7 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved.
-        2-9:eauto using handleRequestVote_TTLM.
+        2-7:eauto using handleRequestVote_TTLM.
         eauto.
       + eauto.
     - find_apply_lem_hyp handleRequestVote_no_append_entries.
@@ -345,7 +341,7 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved.
-        2-9: eauto using doLeader_TTLM.
+        2-7: eauto using doLeader_TTLM.
         match goal with
         | [ H : nwState ?net ?h = (?gd, ?d) |- _ ] =>
           replace d with (snd (nwState net h)) in * by (rewrite H; auto)
@@ -386,7 +382,7 @@ Section AppendEntriesLeader.
     - repeat find_higher_order_rewrite.
       update_destruct_simplify.
       + eapply appendEntries_leader_predicate_TTLM_preserved.
-        2-9: eauto using doGenericServer_TTLM.
+        2-7: eauto using doGenericServer_TTLM.
         match goal with
         | [ H : nwState ?net ?h = (?gd, ?d) |- _ ] =>
           replace d with (snd (nwState net h)) in * by (rewrite H; auto)
diff --git a/raft-proofs/PrefixWithinTermProof.v b/raft-proofs/PrefixWithinTermProof.v
index 97653ee..8720fdb 100644
--- a/raft-proofs/PrefixWithinTermProof.v
+++ b/raft-proofs/PrefixWithinTermProof.v
@@ -229,7 +229,7 @@ Section PrefixWithinTerm.
         10: { eauto. }
         5: { eauto. }
         4: { eauto. }
-        all:eauto; try lia. repeat find_rewrite; auto.
+        all:eauto; try lia.
       + exfalso.
         find_eapply_lem_hyp Prefix_maxIndex; eauto.
         lia.
@@ -256,7 +256,7 @@ Section PrefixWithinTerm.
         10: { eauto. }
         5: { eauto. }
         4: { eauto. }       
-        all:eauto; try lia. repeat find_rewrite; auto.
+        all:eauto; try lia.
       + exfalso.
         find_eapply_lem_hyp Prefix_maxIndex; eauto.
         lia.
@@ -285,7 +285,7 @@ Section PrefixWithinTerm.
         10: { eauto. }
         5: { eauto. }
         4: { eauto. }
-        all:eauto; try lia. repeat find_rewrite; auto.
+        all:eauto; try lia.
       + exfalso.
         find_eapply_lem_hyp Prefix_maxIndex; eauto.
         lia.
@@ -309,7 +309,7 @@ Section PrefixWithinTerm.
         10: { eauto. }
         5: { eauto. }
         4: { eauto. }       
-        all:eauto; try lia. repeat find_rewrite; auto.
+        all:eauto; try lia.
       + exfalso.
         find_eapply_lem_hyp Prefix_maxIndex; eauto.
         lia.