search

math-comp / algebra-tactics

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

Semi-automating proofs of nonzero conditions in `field` #20

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

I'm planning to make it work as follows:

  1. For any F : numFieldType, e1 = e2 :> F can be turned into e1' = e2' :> rat by reflection, if e1 and e2 are clearly in the rational subfield of F,
  2. e1' = e2' :> rat can (usually?) be turned into an integer equation, and then
  3. it attempts to solve the integer (dis)equation by Micromega.

This scheme seems to work for inequations in many cases. But, if e1 and/or e2 contain the multiplicative inverse, it would be problematic. What should I do?

pi8027 commented 3 years ago

One in apery seems more restrictive. IIUC, it works only with the case of F = rat and does nothing with the multiplicative inverse. https://github.com/math-comp/apery/blob/c484e1f869526b78a81f0a10e1a657096eac35bb/theories/lia_tactics.v#L186-L239

pi8027 commented 3 years ago

Indeed, the nonzero conditions do not contain any multiplicative inverse. Also, we don't have ratmul in MathComp. So the above restriction seems to make sense. https://github.com/coq/coq/blob/21518abcd16854525f40ed6e524c9d9148c396f0/theories/setoid_ring/Field_theory.v#L1046-L1093