[NicholasBHubbard]

This PR adds to List.v a lemma: Lemma length_app_comm : forall l l' : list A, length (l++l') = length (l'++l).

I'd like to preface by saying that I am new to Coq so may be ignorant of many things. However, I was in need of such a lemma in one of my proofs and was surprised that an obvious fact such as this did not already exist in the stdlib. I hope that length_app_comm is a good name for this. I read over rocq-prover/rocq#18564 where the naming convention of these lemmas was discussed, and I believe that I followed it correctly.

One thing I am unsure about is if I was correct to add the new lemma under the Global Hint Rewrite here:

Global Hint Rewrite
  rev_involutive (* rev (rev l) = l *)
  rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
  map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
  length_map (* length (map f l) = length l *)
  length_seq (* length (seq start len) = len *)
  length_app (* length (l ++ l') = length l + length l' *)
  length_app_comm (* length (l ++ l') = length (l' ++ l) *)
  length_rev (* length (rev l) = length l *)
  app_nil_r (* l ++ nil = l *)
  : list.

Was this the correct thing to do?

Please let me know if you believe length_app_comm would be a good addition to List.v, and if anything else needs to be done. Thanks!

• Added changelog.

[NicholasBHubbard]

Not sure why the CI fails but will look into it.

[Zimmi48]

Coq-Elpi error is:

 File "etc/version_parser.ml", line 4, characters 14-43:
4 |   let a,b,c = Elpi.API.Utils.version_parser ~what:"elpi" v in
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Elpi.API.Utils.version_parser

Very unclear for Rewriter (idem for Fiat-crypto-legacy).

Equations-test error looks like a GitHub Action issue (unclear what happened from the log). Idem for Metacoq-template-coq.

@proux01 Any idea what is going on here? Should we just relaunch the failed jobs?

[proux01]

Elpi is known to be currently broken. Fiat-crypto and rewriter might be actual overlays needed, not sure for the others.

[proux01]

@NicholasBHubbard CI in other PR confirms that coq-elpi is unrelated but you need to investigate more the other CI failures.

[Zimmi48]

Something is a bit strange though: why did all these jobs fail after 45-47 minutes?

I suspect something was wrong with the GitHub Action runners (especially given that the logs do not give any clue). I will restart these jobs.

[Zimmi48]

The failures still happen and this time, I identified the cause of at least one of them:

       > make[2]: *** [Makefile:818: STLC.vo] Killed

Now, my guess is that this comes from having adding this lemma to a rewrite hint database. Probably this creates an infinite loop and that's also the reason why these jobs take such a long time to fail.

[NicholasBHubbard]

Looks like removing the lemma from the rewrite hint database fixed it

[proux01]

Rebased to relaunch CI now that it's fixed, just to be on the safe side.

[proux01]

Thanks to both of you for the contrib and the debuging