The Coq mailing list

[Julien Narboux <jnarboux AT narboux.fr>]

Hi,

Thanks you for your interest in GeoCoq.

2015-12-08 11:11 GMT+01:00 Mandy Martino <tesleft AT hotmail.com>:

Hi,

1.would like to data mining new geometry theorems with geo coq github's coq script

       is there an example  script  about  this?

Currently there is no such script in GeoCoq. I only have some maple scripts to find properties of triangle centers and generate Coq scripts (https://hal.inria.fr/hal-01174131 ).

 

2. is there an  example to  translate proof into a polynomials system ?

There is an early prototype tactic "convert_to_algebra", with an example using the Euler circle at the end of this file:

https://github.com/GeoCoq/GeoCoq/blob/master/Tarski_dev/Ch16_coordinates_with_functions.v

This tactic use the proofs of the algebraic characterizations of geometric predicates to convert a geometric statement into an algebraic one. For the moment the following predicates are supported: length equality, midpoint, collinearity, 

perpendicularity parallelism equality of points.

 

3. would like to translate tactics proof result into type programming language, is there example  about this?

I don't understand what you mean. Can you please tell me a bit more ? 

4.is there any existing language can call Coq or automate Coq ? can haskell or F# or java do these?

There is the tactic language of Coq called Ltac. 

5. how can display geometric graph with geogebra from Coq in linux and window  respectively?

There is no automated tool for that. In the past there were GeoView by Bertot, Guilhot and Pottier (https://www-sop.inria.fr/lemme/geoview/geoview.ps) but this tool is no longer maintained.

Regards,

Julien Narboux