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'

core/LabeledNet.v

@@ -371,15 +371,15 @@ Section LabeledStepOrderFailure.
     invcs H_st.
     - set net' := {| onwPackets := _ ; onwState := _ |}.
       apply (@refl_trans_1n_trace_trans _ _ _ _ (failed', net)) => //.
-      rewrite (app_nil_end (map2fst _ _)).
+      rewrite -(app_nil_r (map2fst _ _)).
       apply: (@RT1nTStep _ _ _ _ (failed', net')); last exact: RT1nTBase.
       apply: (StepOrderedFailure_deliver _ _ _ H3) => //.
       rewrite /net_handlers /= /unlabeled_net_handlers /=.
       repeat break_let.
       by tuple_inversion.
     - set net' := {| onwPackets := _ ; onwState := _ |}.
       apply (@refl_trans_1n_trace_trans _ _ _ _ (failed', net)) => //.
-      rewrite (app_nil_end (_ :: _)).
+      rewrite -(app_nil_r (_ :: _)).
       apply: (@RT1nTStep _ _ _ _ (failed', net')); last exact: RT1nTBase.
       apply: StepOrderedFailure_input => //; first by [].
       rewrite /input_handlers /= /unlabeled_input_handlers /=.
@@ -436,15 +436,15 @@ Section LabeledStepOrderDynamic.
     invcs H_st.
     - set net' := {| odnwNodes := _ ; odnwPackets := _ ; odnwState := _ |}.
       apply (@refl_trans_1n_trace_trans _ _ _ _ net) => //.
-      rewrite (app_nil_end (map2fst _ _)).
+      rewrite -(app_nil_r (map2fst _ _)).
       apply: (@RT1nTStep _ _ _ _ net'); last exact: RT1nTBase.
       apply: (StepOrderedDynamic_deliver _ _ _ H0 H1) => //.
       rewrite /net_handlers /= /unlabeled_net_handlers /=.
       repeat break_let.
       by tuple_inversion.
     - set net' := {| odnwNodes := _ ; odnwPackets := _ ; odnwState := _ |}.
       apply (@refl_trans_1n_trace_trans _ _ _ _ net) => //.
-      rewrite (app_nil_end (_ :: _)).
+      rewrite -(app_nil_r (_ :: _)).
       apply: (@RT1nTStep _ _ _ _ net'); last exact: RT1nTBase.
       apply: (StepOrderedDynamic_input _ _ H0) => //.
       rewrite /input_handlers /= /unlabeled_input_handlers /=.
@@ -504,15 +504,15 @@ Section LabeledStepOrderDynamicFailure.
     invcs H_st.
     - set net' := {| odnwNodes := _ ; odnwPackets := _ ; odnwState := _ |}.
       apply (@refl_trans_1n_trace_trans _ _ _ _ (failed', net)) => //.
-      rewrite (app_nil_end (map2fst _ _)).
+      rewrite -(app_nil_r (map2fst _ _)).
       apply: (@RT1nTStep _ _ _ _ (failed', net')); last exact: RT1nTBase.
       apply: (StepOrderedDynamicFailure_deliver _ _ _ _ _ H5 H6) => //.
       rewrite /net_handlers /= /unlabeled_net_handlers /=.
       repeat break_let.
       by tuple_inversion.
     - set net' := {| odnwNodes := _ ; odnwPackets := _ ; odnwState := _ |}.
       apply (@refl_trans_1n_trace_trans _ _ _ _ (failed', net)) => //.
-      rewrite (app_nil_end (_ :: _)).
+      rewrite -(app_nil_r (_ :: _)).
       apply: (@RT1nTStep _ _ _ _ (failed', net')); last exact: RT1nTBase.
       apply: (StepOrderedDynamicFailure_input _ _ _ _ H5) => //.
       rewrite /input_handlers /= /unlabeled_input_handlers /=.

core/Net.v

@@ -123,7 +123,7 @@ Section StepRelations.
     intros.
     induction H; simpl; auto.
     concludes.
-    rewrite app_ass.
+    rewrite <- app_assoc.
     constructor 2 with x'; auto.
   Qed.
 
@@ -208,7 +208,7 @@ Section StepRelations.
       constructor.
       auto.
     - concludes.
-      rewrite <- app_ass.
+      rewrite app_assoc.
       econstructor; eauto.
   Qed.
 
@@ -232,7 +232,7 @@ Section StepRelations.
     intros.
     induction H.
     - simpl. rewrite <- app_nil_r. econstructor; eauto. constructor.
-    - concludes. rewrite app_ass.
+    - concludes. rewrite <- app_assoc.
       econstructor; eauto.
   Qed.
 

core/PartialExtendedMapSimulations.v

@@ -246,7 +246,7 @@ case: H => H.
   exists (tr' ++ tr'').
   have H_trans := refl_trans_1n_trace_trans H_star.
   apply: H_trans.
-  have ->: tr'' = tr'' ++ [] by rewrite -app_nil_end.
+  have ->: tr'' = tr'' ++ [] by rewrite app_nil_r.
   apply: (@RT1nTStep _ _ _ _ (pt_ext_map_net x'')) => //.
   exact: RT1nTBase.
 move: H => [H_eq H_eq'].
@@ -361,7 +361,7 @@ case: H => H.
   exists (tr' ++ tr'').
   have H_trans := refl_trans_1n_trace_trans H_star.
   apply: H_trans.
-  have ->: tr'' = tr'' ++ [] by rewrite -app_nil_end.
+  have ->: tr'' = tr'' ++ [] by rewrite app_nil_r.
   apply: (@RT1nTStep _ _ _ _ (pt_ext_map_onet x'')) => //.
   exact: RT1nTBase.
 move: H => [H_eq H_eq'].
@@ -506,7 +506,7 @@ case: H => H.
   exists (tr' ++ tr'').
   have H_trans := refl_trans_1n_trace_trans H_star.
   apply: H_trans.
-  have ->: tr'' = tr'' ++ [] by rewrite -app_nil_end.
+  have ->: tr'' = tr'' ++ [] by rewrite app_nil_r.
   apply: (@RT1nTStep _ _ _ _ (map tot_map_name failed'', pt_ext_map_onet net'')) => //.
   exact: RT1nTBase.  
 move: H => [H_eq_n H_eq_f].
@@ -741,7 +741,7 @@ case: H => H.
   exists (tr' ++ tr'').
   have H_trans := refl_trans_1n_trace_trans H_star.
   apply: H_trans.
-  have ->: tr'' = tr'' ++ [] by rewrite -app_nil_end.
+  have ->: tr'' = tr'' ++ [] by rewrite app_nil_r.
   apply: (@RT1nTStep _ _ _ _ (map tot_map_name failed'', pt_ext_map_odnet net'')) => //.
   exact: RT1nTBase.  
 move: H => [H_eq_n H_eq_f].

core/PartialMapSimulations.v

@@ -341,7 +341,7 @@ case: H => H.
   split.
   * have H_trans := refl_trans_1n_trace_trans H_star.
     apply: H_trans.
-    rewrite (app_nil_end (filterMap pt_map_trace_occ _)).
+    rewrite -(app_nil_r (filterMap pt_map_trace_occ _)).
     apply: (@RT1nTStep _ _ _ _ (pt_map_net x'')) => //.
     exact: RT1nTBase.
   * by rewrite 2!filterMap_app H_eq_tr filterMap_app.
@@ -351,7 +351,7 @@ move: IHH_step1 => [tr' [H_star H_tr]].
 exists tr'.
 split => //.
 rewrite 2!filterMap_app.
-by rewrite H_eq' -app_nil_end.
+by rewrite H_eq' app_nil_r.
 Qed.
 
 Context {fail_fst : FailureParams multi_fst}.
@@ -506,7 +506,7 @@ case: H => H.
   split.
   * have H_trans := refl_trans_1n_trace_trans H_star.
     apply: H_trans.
-    rewrite (app_nil_end (filterMap pt_map_trace_occ _)).
+    rewrite -(app_nil_r (filterMap pt_map_trace_occ _)).
     apply: (@RT1nTStep _ _ _ _ (map tot_map_name failed'', pt_map_net net'')) => //.
     exact: RT1nTBase.
   * by rewrite 3!filterMap_app H_eq_tr.
@@ -516,7 +516,7 @@ move: IHH_step1 => [tr' [H_star H_tr]].
 exists tr'.
 split => //.
 rewrite 2!filterMap_app.
-by rewrite H_eq -app_nil_end.
+by rewrite H_eq app_nil_r.
 Qed.
 
 Definition pt_map_onet (onet : @ordered_network _ multi_fst) : @ordered_network _ multi_snd :=
@@ -572,7 +572,7 @@ case H_m: pt_map_msg => [m'|] /=.
   by rewrite H_eq_f.
 rewrite pt_map_msg_update2 /= filterMap_app /=.
 case H_m': (pt_map_msg _) => [m'|]; first by rewrite H_m' in H_m.
-rewrite -app_nil_end.
+rewrite app_nil_r.
 set f1 := update2 _ _ _ _ _.
 set f2 := fun _ _ => _ _.
 have H_eq_f: f1 = f2.
@@ -731,11 +731,11 @@ apply step_ordered_pt_mapped_simulation_1 in H.
 case: H => H.
   have H_trans := refl_trans_1n_trace_trans IHH_step1.
   apply: H_trans.
-  rewrite (app_nil_end (filterMap pt_map_trace_ev _)).
+  rewrite -(app_nil_r (filterMap pt_map_trace_ev _)).
   apply: (@RT1nTStep _ _ _ _ (pt_map_onet x'')) => //.
   exact: RT1nTBase.
 move: H => [H_eq H_eq'].
-by rewrite H_eq H_eq' -app_nil_end.
+by rewrite H_eq H_eq' app_nil_r.
 Qed.
 
 Lemma pt_msg_in_map :
@@ -1136,11 +1136,11 @@ rewrite filterMap_app.
 case: H => H.
   have H_trans := refl_trans_1n_trace_trans IHH_step1.
   apply: H_trans.
-  rewrite (app_nil_end (filterMap pt_map_trace_ev _)).
+  rewrite -(app_nil_r (filterMap pt_map_trace_ev _)).
   apply: (@RT1nTStep _ _ _ _ (map tot_map_name failed'', pt_map_onet net'')) => //.
   exact: RT1nTBase.
 move: H => [H_eq_n [H_eq_f H_eq]].
-by rewrite H_eq_n -H_eq_f H_eq -app_nil_end.
+by rewrite H_eq_n -H_eq_f H_eq app_nil_r.
 Qed.
 
 Context {new_msg_fst : NewMsgParams multi_fst}.
@@ -1380,11 +1380,11 @@ rewrite filterMap_app.
 case: H => H.
   have H_trans := refl_trans_1n_trace_trans IHH_step1.
   apply: H_trans.
-  rewrite (app_nil_end (filterMap pt_map_trace_ev _)).
+  rewrite -(app_nil_r (filterMap pt_map_trace_ev _)).
   apply: (@RT1nTStep _ _ _ _ (map tot_map_name l0, pt_map_odnet o0)) => //.
   exact: RT1nTBase.
 move: H => [H_eq_n [H_eq_f H_eq]].
-by rewrite H_eq_n -H_eq_f H_eq -app_nil_end.
+by rewrite H_eq_n -H_eq_f H_eq app_nil_r.
 Qed.
 
 Lemma in_msg_filterMap_pt_map_msg :

core/SingleSimulations.v

@@ -106,7 +106,7 @@ case: H_st => H_st; first by rewrite -H_st; exists tr'.
 have [tr'' H_st'] := H_st.
 exists (tr' ++ tr'').
 apply: (refl_trans_1n_trace_trans H_star).
-have ->: tr'' = tr'' ++ [] by rewrite -app_nil_end.
+have ->: tr'' = tr'' ++ [] by rewrite app_nil_r.
 apply RT1nTStep with (x' := (tot_s_map_data (onwState net'' me))) => //.
 exact: RT1nTBase.
 Qed.
@@ -227,7 +227,7 @@ case: H_st => H_st; first by rewrite -H_st; exists tr'.
 have [tr'' H_st'] := H_st.
 exists (tr' ++ tr'').
 apply: (refl_trans_1n_trace_trans H_star).
-have ->: tr'' = tr'' ++ [] by rewrite -app_nil_end.
+have ->: tr'' = tr'' ++ [] by rewrite app_nil_r.
 apply RT1nTStep with (x' := (tot_s_map_data d)) => //.
 exact: RT1nTBase.
 Qed.

core/TotalMapSimulations.v

@@ -296,7 +296,7 @@ rewrite map_app.
 match goal with
 | H : step_async_star _ _ _ |- _ => apply: (refl_trans_1n_trace_trans H)
 end.
-rewrite (app_nil_end (map _ _)).
+rewrite -(app_nil_r (map _ _)).
 apply: (@RT1nTStep _ _ _ _ (tot_map_net x'')) => //.
 exact: RT1nTBase.
 Qed.
@@ -571,7 +571,7 @@ rewrite map_app.
 match goal with
 | H : step_failure_star _ _ _ |- _ => apply: (refl_trans_1n_trace_trans H)
 end.
-rewrite (app_nil_end (map tot_map_trace_occ _)).
+rewrite -(app_nil_r (map tot_map_trace_occ _)).
 apply (@RT1nTStep _ _ _ _ (map tot_map_name l0, tot_map_net n0)) => //.
 exact: RT1nTBase.
 Qed.
@@ -1455,7 +1455,7 @@ rewrite map_app.
 match goal with
 | H : step_ordered_failure_star _ _ _ |- _ => apply: (refl_trans_1n_trace_trans H)
 end.
-rewrite (app_nil_end (map tot_map_trace _)).
+rewrite -(app_nil_r (map tot_map_trace _)).
 apply (@RT1nTStep _ _ _ _ (map tot_map_name l0, tot_map_onet o0)) => //.
 exact: RT1nTBase.
 Qed.
@@ -1668,7 +1668,7 @@ find_apply_lem_hyp step_ordered_dynamic_failure_tot_mapped_simulation_1.
   match goal with
   | H : step_ordered_dynamic_failure_star _ _ _ |- _ => apply: (refl_trans_1n_trace_trans H)
   end.
-  rewrite (app_nil_end (map tot_map_trace _)).
+  rewrite -(app_nil_r (map tot_map_trace _)).
   apply (@RT1nTStep _ _ _ _ (map tot_map_name l0, tot_map_odnet o0)) => //.
   exact: RT1nTBase.
 move: H_step1.

meta.yml

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

systems/LiveLockServ.v

@@ -131,7 +131,7 @@ Section LockServ.
   Proof using.
     unfold Nodes, list_Clients.
     apply NoDup_cons.
-    - in_crush. discriminate.
+    - in_crush_tac (intuition auto). discriminate.
     - apply NoDup_map_injective.
       + intros. congruence.
       + apply all_fin_NoDup.
@@ -1285,7 +1285,7 @@ Section LockServ.
           -- subst. rewrite update_nop_ext.
              find_apply_lem_hyp IHrefl_trans_n1_trace; auto; [idtac].
              repeat find_rewrite.
-             in_crush.
+             in_crush_tac (intuition auto with datatypes).
              discriminate.
           -- subst.
              find_apply_lem_hyp refl_trans_n1_1n_trace.
@@ -1310,15 +1310,15 @@ Section LockServ.
                 do 2 insterU IHrefl_trans_n1_trace.
                 repeat conclude_using eauto.
                 intuition.
-                ** in_crush. discriminate.
-                ** in_crush. discriminate.
+                ** in_crush_tac (intuition auto with datatypes). discriminate.
+                ** in_crush_tac (intuition auto with datatypes). discriminate.
           -- congruence.
           -- break_exists. intuition. subst. simpl.
              repeat find_rewrite. find_inversion. auto.
           -- subst. simpl.
              find_apply_hyp_hyp. intuition.
-             ++ repeat find_rewrite. in_crush. discriminate.
-             ++ repeat find_rewrite. in_crush.
+             ++ repeat find_rewrite. in_crush_tac (intuition auto with datatypes). discriminate.
+             ++ repeat find_rewrite. in_crush_tac (intuition auto with datatypes).
       + find_apply_lem_hyp InputHandler_cases.
         intuition.
         * break_exists. break_and. subst.

systems/LogCorrect.v

@@ -245,7 +245,7 @@ Section LogCorrect.
     | H : IOStreamWriter.unwrap _ = IOStreamWriter.unwrap _ |- _ => rewrite H
     end.
     rewrite nat_serialize_deserialize_id.
-    rewrite (app_nil_end (IOStreamWriter.unwrap _)).
+    rewrite <- (app_nil_r (IOStreamWriter.unwrap _)).
     rewrite list_serialize_deserialize_id_rec.
     find_rewrite.
     reflexivity.

systems/PrimaryBackup.v

@@ -304,7 +304,7 @@ Section PrimaryBackup.
     intros. induction tr1; simpl.
     - auto.
     - repeat break_match; subst; auto.
-      rewrite app_ass. auto using f_equal.
+      rewrite <- app_assoc. auto using f_equal.
   Qed.
 
   Lemma correspond_preserved_primary_same_no_outputs :
@@ -374,7 +374,7 @@ Section PrimaryBackup.
     simpl in *.
     repeat break_match. repeat find_inversion.
     find_rewrite. find_inversion.
-    rewrite app_ass. auto.
+    rewrite <- app_assoc. auto.
   Qed.
 
   Lemma inputs_m_inr_singleton :
@@ -475,7 +475,7 @@ Section PrimaryBackup.
     intros.
     rewrite outputs_m_app, outputs_1_app in *.
     repeat break_match.
-    rewrite app_ass.
+    rewrite <- app_assoc.
     simpl.
     repeat find_rewrite.
     rewrite processInputs_app in *.
@@ -484,7 +484,7 @@ Section PrimaryBackup.
     simpl in *. break_match. tuple_inversion.
     break_and. subst.
     find_rewrite. tuple_inversion.
-    rewrite <- app_ass.
+    rewrite app_assoc.
     find_rewrite.
     auto.
   Qed.
@@ -942,7 +942,7 @@ Section PrimaryBackup.
     - rewrite IHtr1.
       repeat break_match; subst.
       + auto.
-      + rewrite app_ass. auto.
+      + rewrite <- app_assoc. auto.
   Qed.
 
   Lemma simulation :
@@ -1270,7 +1270,7 @@ Section PrimaryBackup.
       rewrite revert_trace_app.
       rewrite inputs_1_app.
       rewrite IHrefl_trans_n1_trace.
-      repeat rewrite app_ass.
+      repeat rewrite <- app_assoc.
       f_equal.
       invc H1; simpl in *.
       + find_apply_lem_hyp PB_net_defn.

systems/SeqNumCorrect.v

@@ -660,7 +660,7 @@ Section SeqNumCorrect.
       break_or_hyp.
       * exists (tr' ++ tr2); split.
         + eapply refl_trans_1n_trace_trans; eauto.
-          rewrite (app_nil_end tr2).
+          rewrite <- (app_nil_r tr2).
           eapply RT1nTStep; eauto.
           apply RT1nTBase.
         + rewrite filterMap_app.
@@ -675,12 +675,12 @@ Section SeqNumCorrect.
           rewrite <- H
         end.
         rewrite filterMap_app.
-        destruct tr2; simpl in *; [ rewrite <- app_nil_end | idtac ]; auto.
+        destruct tr2; simpl in *; [ rewrite app_nil_r | idtac ]; auto.
         match goal with
         | [H : _ = [] |- _ ] =>
           rewrite H
         end.
-        rewrite <- app_nil_end; auto.
+        rewrite app_nil_r; auto.
   Qed.
 
   Theorem reachable_revert :