From 3d1a71bdd7cd394c0b411843adb6bb8276ee569d Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 15 Oct 2023 15:29:36 +0200 Subject: [PATCH 1/3] fix list deprecations --- core/LabeledNet.v | 12 ++++++------ core/Net.v | 6 +++--- core/PartialExtendedMapSimulations.v | 8 ++++---- core/PartialMapSimulations.v | 22 +++++++++++----------- core/SingleSimulations.v | 4 ++-- core/TotalMapSimulations.v | 8 ++++---- systems/LogCorrect.v | 2 +- systems/PrimaryBackup.v | 12 ++++++------ systems/SeqNumCorrect.v | 6 +++--- 9 files changed, 40 insertions(+), 40 deletions(-) diff --git a/core/LabeledNet.v b/core/LabeledNet.v index 7bf5c0ec..196da1a3 100644 --- a/core/LabeledNet.v +++ b/core/LabeledNet.v @@ -371,7 +371,7 @@ 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 /=. @@ -379,7 +379,7 @@ Section LabeledStepOrderFailure. 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,7 +436,7 @@ 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 /=. @@ -444,7 +444,7 @@ Section LabeledStepOrderDynamic. 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,7 +504,7 @@ 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 /=. @@ -512,7 +512,7 @@ Section LabeledStepOrderDynamicFailure. 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 /=. diff --git a/core/Net.v b/core/Net.v index c65e4a60..90a0f6c1 100644 --- a/core/Net.v +++ b/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. diff --git a/core/PartialExtendedMapSimulations.v b/core/PartialExtendedMapSimulations.v index 2af3aeac..55a8bddc 100644 --- a/core/PartialExtendedMapSimulations.v +++ b/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]. diff --git a/core/PartialMapSimulations.v b/core/PartialMapSimulations.v index 40ca24c2..e9a740ac 100644 --- a/core/PartialMapSimulations.v +++ b/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 : diff --git a/core/SingleSimulations.v b/core/SingleSimulations.v index a3d42344..3a6099fb 100644 --- a/core/SingleSimulations.v +++ b/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. diff --git a/core/TotalMapSimulations.v b/core/TotalMapSimulations.v index 3c12feb1..4da74f61 100644 --- a/core/TotalMapSimulations.v +++ b/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. diff --git a/systems/LogCorrect.v b/systems/LogCorrect.v index b70fd020..32cedf11 100644 --- a/systems/LogCorrect.v +++ b/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. diff --git a/systems/PrimaryBackup.v b/systems/PrimaryBackup.v index 5563c5e1..01783cbf 100644 --- a/systems/PrimaryBackup.v +++ b/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. diff --git a/systems/SeqNumCorrect.v b/systems/SeqNumCorrect.v index 0042c8c9..95b8bf04 100644 --- a/systems/SeqNumCorrect.v +++ b/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 : From 3994e622513b9578aa617089d0a3abf80a9ecd81 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 15 Oct 2023 16:05:24 +0200 Subject: [PATCH 2/3] fix intuition deprecations by using in_crush parameters --- systems/LiveLockServ.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/systems/LiveLockServ.v b/systems/LiveLockServ.v index 1b91d3eb..a4bf5d93 100644 --- a/systems/LiveLockServ.v +++ b/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. From ea2c43bd522b43ab673994f450670152e1bca6a4 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 15 Oct 2023 16:07:00 +0200 Subject: [PATCH 3/3] refresh boilerplate --- .github/workflows/docker-action.yml | 1 + meta.yml | 1 + 2 files changed, 2 insertions(+) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 7a0662d0..f59964a2 100644 --- a/.github/workflows/docker-action.yml +++ b/.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' diff --git a/meta.yml b/meta.yml index 56d74aae..0f2e2cff 100644 --- a/meta.yml +++ b/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'