search

math-comp / algebra-tactics

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

Morphisms #8

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

Closes #4 Closes #6

It internally produces equality proofs for pushing down morphisms and also converting _%:R to _%:~R (e.g., f (a + b * 10%:R) = f a + f b * 10%:~R). Performance issues related to constants have been fixed. However, a produced proof term can be (I guess, quadratically) large in the size of the input, and it causes a serious performance issue in Lemma from_sander. It should be possible to make the size of the proof term linear by factoring out common subterms using let-ins.

pi8027 commented 3 years ago

In the end, I managed to address the performance issue by using reflection for pushing down morphisms (see inductive/fixpoint definitions in ring.v). This PR also fixes the performance issue with _%:R.