Semi-automate proofs of nonzero conditions in `field`

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components

33 stars 2 forks source link

Semi-automate proofs of nonzero conditions in `field` #22

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

Closes #20.

For F : numFieldType, it attempts to turn e != 0 :> F into e' != 0 :> int by Z-ifying e : F to e' : int, and then invoke lia on that. This Z-ification is done by the "How to make ad hoc proof automation less ad hoc" approach.

pi8027 commented 3 years ago

Questions:

Is it still better to go through rat instead of directly translate F to int? If we will have ratmul in MathComp at some point, I think this will be useful.
Should we be able to switch from lia to nia sometimes?

pi8027 commented 3 years ago

Is it still better to go through rat instead of directly translate F to int? If we will have ratmul in MathComp at some point, I think this will be useful.

In fact, MathComp has ratr of type forall R : unitRingType, rat -> R. So it seems better to go through rat instead.

pi8027 commented 3 years ago

We provide 4 automation tactics (lia|nia)_(ring|field), and field does not invoke them for now. Users may invoke them as they need.