Proof failures with (unsupported) Coq 8.12

[blaxill]

Some changes in Coq 8.12 tactics break proofs in a few places.

• firstorder is now weaker (related coq change coq/coq#11760), firstorder with bool works in failing cases here
• lia seems to be weaker, failing at coq/PrimitiveProperties.v:354&357 the first being:

  353         * f_equal.
  354           rewrite N.mul_mod_distr_l by (destruct sz; cbn; lia).  
  355           reflexivity.

This can be fixed by an intermediate remember:

  353         * f_equal.               
  354           rewrite N.mul_mod_distr_l ; (destruct sz; cbn; try lia).  
  355           remember (2^(Pos.of_succ_nat sz))%positive; lia

This seems odd to me (I can't find a relevant changelog for lia), does the Koika team think this is a Coq issue?

[cpitclaudel]

Thanks! I tried to make a backwards-compatible fix. Can you give it a try?

[blaxill]

Thanks, I can confirm its building for me now with 8.12 and 8.13. (There are still the errors from #7 from the multiplercorrectness example).

[cpitclaudel]

Thanks a lot. #7 is on my list