The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,
Transitivity is defined in the standard library. Replacing its
definition would break all proofs of transitivity in libraries you are
using, including the standard library. So bad idea.

But you can define another notion of transitivity and prove it
equivalent to the stdlib one. Then each time you want to prove
(stdlib) transitivity you can do it by going to your definition as a
first step.

Hope this helps,
P.



2015-12-14 12:39 GMT+01:00 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
>
>