From cbc791781bf4315247ba72f1a74bf0ba7b36c0eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 3 May 2023 16:40:15 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#17564. --- core/PartialExtendedMapSimulations.v | 8 ++++---- core/PartialMapSimulations.v | 18 +++++++++--------- core/TotalMapSimulations.v | 10 +++++----- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/core/PartialExtendedMapSimulations.v b/core/PartialExtendedMapSimulations.v index 6dc1f74e..2af3aeac 100644 --- a/core/PartialExtendedMapSimulations.v +++ b/core/PartialExtendedMapSimulations.v @@ -111,7 +111,7 @@ Proof using name_map_bijective. move => f h d. apply functional_extensionality => n. rewrite /update /=. -case (name_eq_dec _ _) => H_dec; case (name_eq_dec _ _) => H_dec' //. +case: (name_eq_dec _ _) => H_dec; case (name_eq_dec _ _) => H_dec' //. - rewrite -H_dec in H_dec'. by rewrite H_dec. - case: H_dec'. @@ -189,7 +189,7 @@ case => {net net' tr}. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case name_eq_dec => H_dec //. + case: name_eq_dec => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. - move => h net net' out inp d l H_hnd H_eq. @@ -218,7 +218,7 @@ case => {net net' tr}. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case name_eq_dec => H_dec //. + case: name_eq_dec => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. Qed. @@ -594,7 +594,7 @@ invcs H_step. repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=. * by find_apply_lem_hyp not_in_failed_not_in. * by find_apply_lem_hyp in_failed_in. - * case adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + * case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + by rewrite IH. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. diff --git a/core/PartialMapSimulations.v b/core/PartialMapSimulations.v index b8c10328..40ca24c2 100644 --- a/core/PartialMapSimulations.v +++ b/core/PartialMapSimulations.v @@ -200,7 +200,7 @@ Proof using name_map_bijective. move => f h d. apply functional_extensionality => n. rewrite /update /=. -case name_eq_dec => H_dec; case name_eq_dec => H_dec' //. +case: name_eq_dec => H_dec; case name_eq_dec => H_dec' //. rewrite -H_dec in H_dec'. by rewrite tot_map_name_inverse_inv in H_dec'. rewrite H_dec' in H_dec. @@ -274,7 +274,7 @@ case => {net net' tr}. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case (name_eq_dec _ _) => H_dec //. + case: (name_eq_dec _ _) => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. * move {H_eq'}. @@ -308,7 +308,7 @@ case => {net net' tr}. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case (name_eq_dec _ _) => H_dec //. + case: (name_eq_dec _ _) => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. * rewrite /=. @@ -408,7 +408,7 @@ invcs H_step. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case (name_eq_dec _ _) => H_dec //. + case: (name_eq_dec _ _) => H_dec //. by rewrite H_dec. by rewrite H_eq_s. - rewrite /= /pt_map_net /=. @@ -434,7 +434,7 @@ invcs H_step. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case (name_eq_dec _ _) => H_dec //. + case: (name_eq_dec _ _) => H_dec //. by rewrite H_dec H_d. by rewrite H_eq_s. - case H_m: (pt_map_packet p) => [p'|]. @@ -849,7 +849,7 @@ Proof using. move => m m' h. elim => //=. move => n ns IH. -case (adjacent_to_dec _ _) => H_dec /=; last exact: IH. +case: (adjacent_to_dec _ _) => H_dec /=; last exact: IH. case => n' m0 H_eq. rewrite /pt_map_name_msg /=. case H_eq': (pt_map_msg m') => [m1|]; last by rewrite H_eq' in H_eq. @@ -1242,7 +1242,7 @@ invcs H_step. repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=. * by find_apply_lem_hyp not_in_failed_not_in. * by find_apply_lem_hyp in_failed_in. - * case adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + * case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + by rewrite IH. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. @@ -1285,7 +1285,7 @@ invcs H_step. rewrite /nwS1 /nwS2 {nwS1 nwS2}. apply functional_extensionality => n. rewrite /update /=. - case name_eq_dec => H_dec //. + case: name_eq_dec => H_dec //. by rewrite H_dec H5 H_eq_d. have H_eq_p: nwP1 = nwP2. rewrite /nwP1 /nwP2 /=. @@ -1330,7 +1330,7 @@ invcs H_step. rewrite /nwS1 /nwS2 /=. apply functional_extensionality => n. rewrite /update /=. - case name_eq_dec => H_dec //. + case: name_eq_dec => H_dec //. by rewrite H_dec H5 H_d. by rewrite H_eq_n. - left. diff --git a/core/TotalMapSimulations.v b/core/TotalMapSimulations.v index 9fd68999..3c12feb1 100644 --- a/core/TotalMapSimulations.v +++ b/core/TotalMapSimulations.v @@ -867,7 +867,7 @@ Proof using. move => h m. elim => //=. move => n ns IH. -case (adjacent_to_dec _ _) => H_dec /=. +case: (adjacent_to_dec _ _) => H_dec /=. case => n' m' H_in. case: H_in => H_in. by inversion H_in. @@ -994,7 +994,7 @@ elim => //= [|n l IH] failed h n'; first by rewrite remove_all_nil. have H_cn := remove_all_cons name_eq_dec failed n l. break_or_hyp; break_and; find_rewrite; first exact: IH. rewrite /=. -case (adjacent_to_dec _ _) => H_dec' /=. +case: (adjacent_to_dec _ _) => H_dec' /=. move => H_in. case: H_in => H_in. inversion H_in. @@ -1013,7 +1013,7 @@ elim => [|n l IH] failed n' h; first by rewrite remove_all_nil. have H_cn := remove_all_cons name_eq_dec failed n l. break_or_hyp; break_and; find_rewrite; first exact: IH. rewrite /=. -case (adjacent_to_dec _ _) => /= H_dec'. +case: (adjacent_to_dec _ _) => /= H_dec'. move => H_in. case: H_in => H_in. rewrite {1}H_in -{4}H_in. @@ -1161,7 +1161,7 @@ Proof using. move => m. elim => //=. move => n ns IH n' h H_adj H_in. -case (adjacent_to_dec _ _) => H_dec; case: H_in => H_in. +case: (adjacent_to_dec _ _) => H_dec; case: H_in => H_in. - rewrite /=. left. by rewrite H_in. @@ -1572,7 +1572,7 @@ invcs H_step. repeat break_or_hyp; repeat break_and; repeat find_rewrite => //=. * by find_apply_lem_hyp not_in_failed_not_in. * by find_apply_lem_hyp in_failed_in. - * case adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + * case: adjacent_to_dec => H_dec; case adjacent_to_dec => H_dec' => //=. + by rewrite IH. + by find_apply_lem_hyp tot_adjacent_to_fst_snd. + by find_apply_lem_hyp tot_adjacent_to_fst_snd.