TODOs in `lra`

[pi8027]

Short term:

• Avoid hypotheses search triggered by exact. This can be a source of a significant slowdown.
  • Done in Avoid search for hypotheses and use refine instead #74, but does not fix the slowdown.
• Better error messages (things like "Cannot find witness" are shown as debug messages, which is weird).
  • Done in Improve the error message of lra #75.
• Implement an option to use exact_no_check.
• Support zmodType homomorphisms (additive functions) and subexpressions.
  • Done in Port to Hierarchy Builder #71.
• Support nat subexpressions.
  • Done in Port to Hierarchy Builder #71.
• Support the real subset (Num.real) of any numDomainType and numFieldType.
• Reimplement vm_of_list.
• Implement a preprocessing mechanism for interval memberships.

Long term:

• For the moment, a reified term should be re-parsed by the wlra_Q or wnra_Q tactic provided by the Micromega plugin. Can we do it better? Reimplementing the witness generator as a built-in predicate of Coq-Elpi might be a solution, but it would be nice if we could do that from another Coq plugin.

[pi8027]

Better error messages (things like "Cannot find witness" are shown as debug messages, which is weird).

To do error handling properly, we have to call a witness generator (like wlra_Q) and a reflection tactic separately. But, since the former puts the witness in the context, it is unclear how to retrieve it.

[proux01]

Support the real subset (Num.real) of any numDomainType and numFieldType.

FTR, I thought a bit about this but since we loose (~ (x <= y) -> y < x) this requires changes in the checker (there is a limitation on the number of negations per clause (we can only handl Horn clauses)) and/or we have to keep track of Num.real hypotheses. Either way it would probably be better to have the witness generator be aware of it.

[pi8027]

I think that Num.real is closed under any operator handled by lra. Then:

Goal forall (R : numDomainType) (x y : R),
    x \in Num.real -> y \in Num.real -> (~~ (x <= y) -> y < x)%R.
Proof. by move=> R x y xr yr; case: real_ltgtP. Qed.

[CohenCyril]

Another way to say it is that we have :

• forall R : numDomainType, {x | x \in Num.real R} : realDomainType
• forall R : numFieldType, {x | x \in Num.real R} : realFieldType

[pi8027]

Yes, and these instances preserve the operators of R.