The Coq mailing list

[Loïc Pottier <Loic.Pottier AT sophia.inria.fr>]



Chers Coqueurs(euses),

avec Jérôme Creci, nous avons écrit une tactique en coq7.4, nommée Gb (comme Gröbner) qui permet de montrer des égalités de polynômes dans un anneau, en utilisant des égalités de polynômes en hypothèses.

Par exemple, Gb permet de montrer, dans un anneau intègre A:

 

(x,y,a,b,c:A)a*x*x+b*x+c==0-> b==-a*(x+y)-> c==a*x*y ->a*y*y+b*y+c==0

 

Loïc Pottier

 

 

Dear Coqers,

with Jérôme Creci, we wrote a tactic in coq7.4, called Gb (from Gröbner), which proves polynomial equalities in a ring, using polynomial equalities in hypotheses.

For example, Gb allows to prove, in a domain A:

 

(x,y,a,b,c:A)a*x*x+b*x+c==0-> b==-a*(x+y)-> c==a*x*y ->a*y*y+b*y+c==0

 

Loïc Pottier

 

Other traductions (with Babelfish, sorry...):

------------------

In lieber Coqers,

mit Jérôme Creci, schrieben wir eine Taktik coq7.4, benannt Gb (von Gröbner), das polynomische Gleichheiten in einem Ring prüft mit polynomischen Gleichheiten in den Hypothesen.

Z.B. darf GB, in einem Gebiet A prüfen: (x, y, a, b, c:A)a*x*x+b*x+c==0 - > b==-a*(x+y) - > c==a*x*y ->a*y*y+b*y+c==0

-----------------

Caro Coqers,

con Jérôme Creci, abbiamo scritto una tattica in coq7.4, denominato Gb (da Gröbner), in cui dimostra le uguaglianze polinomiali in un anello, usando le uguaglianze polinomiali nelle ipotesi.

Per esempio, il GB concede risultare, in un dominio A: (x, y, a, b, c:A)a*x*x+b*x+c==0 - > b==-a*(x+y) - > c==a*x*y ->a*y*y+b*y+c==0

----------------

貴重なCoqers,

 J3er4ome Creci の, 私達はGb 呼ばれた coq7.4 (Gröbner から), 作戦をリングのpolynomial 平等を証明する書き, polynomial 平等を仮説で使用する。例えば, gb は範囲a で, 証明するために割り当てる: (x, y, a, b, c:A)a*x*x+b*x+c==0 - > b==-a*(x+y) - > c==a*x*y ->a*y*y+b*y+c==0

--------------

Coqers querido,

con Jérôme Creci, escribimos una táctica en coq7.4, llamado Gb (de Gröbner), quien prueba igualdades polinómicas en un anillo, usando igualdades polinómicas en hipótesis.

Por ejemplo, el GB permite para probar, en un dominio A: (x, y, a, b, c:A)a*x*x+b*x+c==0 - > b==-a*(x+y) - > c==a*x*y ->a*y*y+b*y+c==0

-----------------------

etc: http://babelfish.altavista.com/babelfish/tr