The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 09/26/2016 11:30 AM, Daniel de Rauglaudre wrote:
> Question: I was even not able to prove it with pen and paper!
> How did nsatz do it? Is it possible to see its proof, except
> by typing "Show Proof"?

nsatz just implements the test for ideal membership using grobner basis.

Given polynomials P1.. Pn and Q, it checks if Q is in the ideal 
generated by P1 .. Pn, ie if Q can be written as Q = \sum_i Pi * Ri for 
some arbitrary polynomials Ri.
This solves exactly your problem that is P1= 0 -> ... -> Pn= 0 -> Q = 0.

The problem is decided by building a "canonical" base for the ideal 
(P1,..Pn) using a completion à la Knuth-Bendix.
What you have when you do Show Proof is mainly the Ri. Of course this is 
a bit obfuscated by the reification process.
Anyway this output is usually not for human consumption, nsatz does not 
try to get the "smallest" certificate....

Hope this helps

--
Laurent