From 0fd2a888543270d9aada90c10b73f357a9724055 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 16 Jun 2024 14:43:48 +0200 Subject: [PATCH] Adapt to Coq PR #18591 which grants "simpl never" on List.app more accuratedly. The change is however indirect: - Coq PR #18591 fixes a lack of refolding of fixpoints; - as a consequence, some calls to "simpl" on subterms start to respect "simpl never" as required; - this impacts "injection" (here the "[]" intro-pattern) as "injection" calls "simpl" on the subterms it generates. --- .../StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v b/theories/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v index c6bdeb7b..7bdd3894 100644 --- a/theories/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v +++ b/theories/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v @@ -603,7 +603,7 @@ Proof. elim: u s. - move=> [|y1 [|y2 s]]. + rewrite ?app_nil_l. move=> <-. right. right. by exists []. - + move=> [] <- <- /=. right. by left. + + move=> []. rewrite [in [] ++ _]/List.app => <- <- /=. right. by left. + move=> [] <- <- ->. left. by exists s. - move=> x1 u IH [|y1 s]. + rewrite ?app_nil_l. move=> <-. right. right. by exists (x1 :: u). @@ -707,7 +707,7 @@ Proof. ** rewrite app_nil_r /= ?map_app. move: (a) => [|?]; first done. move=> Hi [] H1 [<-] H2. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. - inversion Hxy. subst. + inversion Hxy. subst. try rewrite [in LHS]/List.app in H1. eexists (u' ++ [sz]), v', (_ :: _). rewrite -?app_assoc. constructor; [done | by rewrite /= ?map_app H1 H2]. ** rewrite ?map_app filter_app /= app_nil_r /step.