Fix deprecations

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'

meta.yml

@@ -52,6 +52,7 @@ supported_coq_versions:
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.18'
 - version: '8.17'
 - version: '8.16'
 - version: '8.15'

raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v

@@ -264,7 +264,7 @@ Section AppendEntriesRequestReplyCorrespondence.
       match goal with
         | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ =>
           assert (nwPackets net' = xs ++ p :: (ys ++ l))
-            by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto);
+            by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto);
             clear H
       end.
       eapply @RIR_handleMessage with (net := net') (p := p);
@@ -325,7 +325,7 @@ Section AppendEntriesRequestReplyCorrespondence.
       match goal with
         | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ =>
           assert (nwPackets net' = xs ++ p :: (ys ++ l))
-            by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto);
+            by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto);
             clear H
       end.
       eapply @RIR_handleMessage with (net := net') (p := p);
@@ -364,7 +364,7 @@ Section AppendEntriesRequestReplyCorrespondence.
       match goal with
         | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ =>
           assert (nwPackets net' = xs ++ p :: (ys ++ l))
-            by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto);
+            by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto);
             clear H
       end.
       eapply @RIR_handleMessage with (net := net') (p := p);
@@ -401,7 +401,7 @@ Section AppendEntriesRequestReplyCorrespondence.
     match goal with
       | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ =>
         assert (nwPackets net' = xs ++ p :: (ys ++ l))
-          by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto);
+          by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto);
           clear H
     end.
     eapply @RIR_handleMessage with (net := net') (p := p);

raft-proofs/LogsLeaderLogsProof.v

@@ -298,7 +298,7 @@ Section LogsLeaderLogs.
                   simpl in *.
                   rewrite update_elections_data_appendEntries_leaderLogs. auto.
                 * rewrite removeAfterIndex_in_app; auto.
-                  rewrite app_ass. repeat find_rewrite. auto.
+                  rewrite <- app_assoc. repeat find_rewrite. auto.
                 * repeat find_rewrite. do_in_app. intuition; eauto.
               + (* we share an entry with the leader, so we can use
                 log matching to make sure our old entries match. we'll
@@ -318,7 +318,7 @@ Section LogsLeaderLogs.
                   simpl in *.
                   rewrite update_elections_data_appendEntries_leaderLogs. auto.
                 * rewrite removeAfterIndex_in_app; auto.
-                  repeat find_rewrite. rewrite app_ass.
+                  repeat find_rewrite. rewrite <- app_assoc.
                   find_copy_eapply_lem_hyp leaderLogs_sorted_invariant; eauto.
                   f_equal.
                   eapply thing; eauto using lift_logs_sorted;
@@ -343,7 +343,7 @@ Section LogsLeaderLogs.
                   simpl in *.
                   rewrite update_elections_data_appendEntries_leaderLogs. auto.
                 * rewrite removeAfterIndex_in_app; auto.
-                  repeat find_rewrite. rewrite app_ass.
+                  repeat find_rewrite. rewrite <- app_assoc.
                   f_equal.
                   assert (x2 = []).
                   {
@@ -504,7 +504,7 @@ Section LogsLeaderLogs.
              end; intuition.
              + find_higher_order_rewrite; update_destruct; subst; rewrite_update; eauto;
                simpl in *; rewrite update_elections_data_client_request_leaderLogs; eauto.
-             + break_if; eauto using app_ass; do_bool; lia.
+             + break_if; eauto using app_assoc; do_bool; lia.
              + simpl in *. intuition; subst; eauto.
            - find_copy_apply_lem_hyp maxIndex_is_max; eauto using lift_logs_sorted.
              find_apply_hyp_hyp. break_exists_exists; intuition;

raft-proofs/MatchIndexAllEntriesProof.v

@@ -349,7 +349,7 @@ Section MatchIndexAllEntries.
   Proof using. 
     unfold handleAppendEntries, advanceCurrentTerm.
     intros. repeat break_match; repeat find_inversion; simpl in *; repeat do_bool; eauto;
-            eexists; f_equal; eauto using NPeano.Nat.le_antisymm.
+            eexists; f_equal; eauto using Nat.le_antisymm.
   Qed.
 
   Lemma not_empty_true_elim :

raft-proofs/NextIndexSafetyProof.v

@@ -173,7 +173,7 @@ Section NextIndexSafety.
       + destruct (name_eq_dec h' (pSrc p)).
         * subst. rewrite get_set_same_default.
           unfold getNextIndex.
-          apply NPeano.Nat.le_le_pred.
+          apply Nat.le_le_pred.
           auto.
         * rewrite get_set_diff_default by auto.
           auto.
@@ -229,7 +229,7 @@ Section NextIndexSafety.
       intuition; repeat find_rewrite.
       + auto.
       + unfold assoc_default. simpl.
-        auto using NPeano.Nat.le_le_pred.
+        auto using Nat.le_le_pred.
     - auto.
   Qed.
 

raft-proofs/OutputCorrectProof.v

@@ -398,7 +398,7 @@ Section OutputCorrect.
     intuition.
     pose proof (deduplicate_log_app xs ys). break_exists.
     repeat find_rewrite.
-    rewrite app_ass in *. simpl in *.
+    rewrite <- app_assoc in *. simpl in *.
     eexists. eexists. eexists. eexists. eexists.
     intuition eauto.
   Qed.
@@ -880,7 +880,7 @@ Section OutputCorrect.
       pose proof deduplicate_log_app l l'; break_exists; find_rewrite
     end.
     repeat eexists; intuition eauto; repeat find_rewrite; auto.
-    rewrite app_ass. simpl. repeat f_equal.
+    rewrite <- app_assoc. simpl. repeat f_equal.
   Defined.
   Next Obligation.
     unfold in_output_trace in *. intuition.

raft-proofs/RaftMsgRefinementProof.v

@@ -130,7 +130,7 @@ Section RaftMsgRefinement.
            end.
            simpl.
            f_equal; auto.
-           - repeat rewrite app_ass. auto.
+           - repeat rewrite <- app_assoc. auto.
            - apply functional_extensionality.
              intros. repeat break_if; simpl; auto.
            - repeat find_rewrite; auto.
@@ -218,7 +218,7 @@ Section RaftMsgRefinement.
            end.
            simpl.
            f_equal; auto.
-           - repeat rewrite app_ass. auto.
+           - repeat rewrite <- app_assoc. auto.
            - apply functional_extensionality.
              intros. repeat break_if; simpl; auto.
            - repeat find_rewrite; auto.

raft-proofs/StateMachineCorrectProof.v

@@ -917,7 +917,7 @@ Section StateMachineCorrect.
     find_apply_hyp_hyp.
     break_exists. intuition.
     repeat find_rewrite. find_inversion.
-    repeat eexists; eauto using app_ass.
+    repeat eexists; eauto using app_assoc.
   Qed.
 
   Lemma getLastId_clientCache_to_ks_assoc :
@@ -1025,7 +1025,7 @@ Section StateMachineCorrect.
       end.
       repeat find_rewrite.
       repeat eexists; eauto.
-      rewrite app_ass.
+      rewrite <- app_assoc.
       rewrite <- app_comm_cons. eauto.
     - do_bool. repeat find_inversion.
       copy_eapply_prop_hyp applyEntries applyEntries;
@@ -1045,7 +1045,7 @@ Section StateMachineCorrect.
       end.
       repeat find_rewrite.
       repeat eexists; eauto.
-      rewrite app_ass.
+      rewrite <- app_assoc.
       rewrite <- app_comm_cons. eauto.
     - do_bool. subst.
       destruct (clientId_eq_dec (eClient x) client).
@@ -1101,7 +1101,7 @@ Section StateMachineCorrect.
         end.
         repeat find_rewrite.
         repeat eexists; eauto.
-        rewrite app_ass.
+        rewrite <- app_assoc.
         rewrite <- app_comm_cons. eauto.
     - do_bool. subst.
       destruct (clientId_eq_dec (eClient x) client).
@@ -1157,7 +1157,7 @@ Section StateMachineCorrect.
         end.
         repeat find_rewrite.
         repeat eexists; eauto.
-        rewrite app_ass.
+        rewrite <- app_assoc.
         rewrite <- app_comm_cons. eauto.
   Qed.
 
@@ -1223,7 +1223,7 @@ Section StateMachineCorrect.
     intuition.
     pose proof (deduplicate_log_app xs ys). break_exists.
     repeat find_rewrite.
-    rewrite app_ass in *. simpl in *.
+    rewrite <- app_assoc in *. simpl in *.
     eexists. eexists. eexists. eexists. eexists.
     intuition eauto.
   Qed.
@@ -1236,7 +1236,7 @@ Section StateMachineCorrect.
     induction l; intros; simpl in *.
     - find_inversion. auto.
     - repeat break_let.
-      rewrite app_ass.
+      rewrite <- app_assoc.
       eauto.
   Qed.
 
@@ -1603,7 +1603,7 @@ Section StateMachineCorrect.
           (exists (l ++ xs), e, ys)
       end.
       unfold execute_log.
-      repeat rewrite app_ass.
+      repeat rewrite <- app_assoc.
       rewrite execute_log'_app.
       break_let.
       get_invariant_pre state_machine_log_invariant.

raft-proofs/StateMachineSafetyProof.v

@@ -1944,7 +1944,7 @@ Section StateMachineSafetyProof.
                repeat match goal with
                | [ H : _ <= _, H': _ |- _ ] => rewrite H' in H
                end.
-               find_apply_lem_hyp NPeano.Nat.max_le. break_or_hyp.
+               find_apply_lem_hyp Nat.max_le. break_or_hyp.
                + (* my log is just the entries in the incoming AE.
                     so e was in the incoming entries.
                     but eIndex e <= old commit index.
@@ -2016,7 +2016,7 @@ Section StateMachineSafetyProof.
                repeat match goal with
                       | [ H : _ <= _, H': _ |- _ ] => rewrite H' in H
                       end.
-               find_apply_lem_hyp NPeano.Nat.max_le. break_or_hyp.
+               find_apply_lem_hyp Nat.max_le. break_or_hyp.
                + (* eIndex e <= old commit index *)
                  repeat find_rewrite.
                  match goal with