Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Dear Georges,

thanks a lot for the explanation.

Georges Gonthier 
<>
 writes:

>  The reason many mathematical definitions in mathcomp are opaque is
> that the heuristics implemented by the Coq type checker for comparing
> inferred and expected types tends to handle even moderately nested
> transparent definitions very poorly. Specifically, Coq uses a
> combination of lazy constant expansion and call-by-need head (weak)
> reduction.
[...]

I see this problem mentioned often,

- has any solution to this problem been proposed/researched? What would,
  in your opinion, improve the situation?

- do other provers behave better in this aspect?

I hope these are no silly question, excuse my unfamiliarity with the
topic.

> Hence the compute in your proof attempts to create a huge term.

Jacques-Henri Jourdan has successfully used his memory profiler with
Coq, so it would be possible to have a bit fun profiling such diverging
computations; even if is is obvious that a huge term is created, the
profiling could reveal interesting.

Best regards,
Emilio