search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Performance issue of reflection and support for morphisms #4

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

I have an idea to address the performance issue of reflection (below) and also to support morphisms (including additive-to-multiplicative ones) at the same time. Concretizing and implementing it will take some time though. https://github.com/math-comp/algebra-tactics/blob/6e2eb23641df592793ed0603a186300a104e8908/examples/ring_examples.v#L589-L595

pi8027 commented 3 years ago

Roughly, the solution I propose is as follows:

Lemma rat_constants : 200%:R * 30%:R = 6000%:R :> rat.
rewrite -![_%:R]/((Posz _)%:~R).
ring.
Qed.