Kazuhiko Sakaguchi

IIUC, the source of this issue is that 1. the `lia` tactic itself does not know the fact that `b : bool` is `true` or `false` (see https://github.com/coq/coq/pull/11906#issuecomment-631191897), 2. the...

And this case analysis is performed here. I see the current implementation is too bad to handle the use of boolean predicates and relations in MathComp. https://github.com/coq/coq/blob/12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f/theories/micromega/ZifyBool.v#L16-L19 https://github.com/coq/coq/blob/12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f/theories/micromega/ZifyBool.v#L155-L161

For example, `p1Dp3: is_true (p1 != p3)` and `sam1C : is_true (codom sam1 \subset [:: pa; p2])` are handled in this way.

Then, could you put the following lines at the beginning of your proof script? (NB: it makes `lia` less powerful in general.) ```coq Ltac Zify.zify_post_hook ::= zify_ssreflect.SsreflectZifyInstances.divZ_modZ_to_equations. ```

Or if you don't use the Euclidean division at all, its RHS can be `idtac`.

I think it is doable, but doing that without changing the Coq side properly seems another source of potential incompatibility issue. I will rather try to obtain better `elim_bool_cstr`.

I think, ultimately, we need an SMT solver (or a rather ad-hoc combination of a SAT solver and a theory solver, at least) to address this kind of exponential blowup....

When I put some thought into this, I didn't think so. But now I don't remember the details. Let me do that later. (Now I'm just making my TODOs explicit...

BTW, Lean's `ring_exp` tactic does not seem to solve `(a * b + a * c) ^ n = a ^ n * (b + c) ^ n` (not tested)....

I can also imagine that writing such a preprocessor (mainly the Elpi part) dealing with side conditions can be a bit more painful. So generating such reflexive tactics is another...