The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

Hi ,

i can not search setoid_rewrite function's implementation

https://github.com/GeoCoq/GeoCoq/search?utf8=%E2%9C%93&q=setoid_rewrite

if  i  would like to  change  setoid 's  transitive to another  definition,  which file can  i edit  to  change  it?

if  i edit  the  file, does  it mean  that  make clean in  geocoq  directory  and  make  and make  install again then  it  can apply  the  new definition?

Regards,

Martin 

---

Date: Mon, 14 Dec 2015 04:24:04 +0000
From: tesleft AT hotmail.com
To: coq-club AT inria.fr; coq-club AT inria.fr
Subject: Re: [Coq-Club] is there an example about data mining new geometry theorems with geo coq github and translate proof into a polynomials system

For question 3, I discover Isabelle's lemma proof result can be translated to function body in f# or Haskell these type language such as reverse function.

So, I guess whether there are tools to do these translate in coq so that it can generate all possible functions based on lemma for type language, no need to discover manually.

I guess the lemma can come from free theorems program.

Sent from Outlook Mobile

On Sun, Dec 13, 2015 at 9:26 AM -0800, "Julien Narboux" <jnarboux AT narboux.fr> wrote:

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