search

affeldt-aist / coq-robot

Mathematics of Rigid Body Transformationss using Coq and MathComp
26 stars 2 forks source link

reintroduce a type for angle (wip) #36

Open affeldt-aist opened 2 years ago

CohenCyril commented 2 years ago

I did not read the PR but one should ideally show that the type angle whatever its definition is a ring quotient of R by the ideal 2 * pi * R

affeldt-aist commented 2 years ago

I did not read the PR but one should ideally show that the type angle whatever its definition is a ring quotient of R by the ideal 2pi

Right but using which tooling from MathComp?

CohenCyril commented 2 years ago

I did not read the PR but one should ideally show that the type angle whatever its definition is a ring quotient of R by the ideal 2pi

Right but using which tooling from MathComp?

ring_quotient

thery commented 2 years ago

could it be the definition of angle?

CohenCyril commented 2 years ago

Be careful, you do not need to build angle using a quotient (maybe the arguments of complex numbers was actually the right one), but you can provide a quotient interface and deduce the ring structure from it

CohenCyril commented 2 years ago

It could also be the definition of angle... sure

affeldt-aist commented 2 years ago

This PR is the consequence of an effort to replace the coq-robot definition of trigonometric functions with what is now available in MathComp-Analysis but maybe we should first generalize expR to complex numbers to prove the relation with cos/sin to redefine the already-existing angle as a subtype of R that can finally be endowed afterwards with a ring structure using ring_quotient.

thery commented 2 years ago

Reintroducing the type angle makes life a bit more complicated. Before cos and sin were derived from angle, so we had formula for sin(a + b) directly on angle..... Now, sin is defined on R, and when writting sin(a + b) wirh a and b are of type angle, the + is the addition on angle. I don't know the way to go: lifting all the theorem from R to angle or disabling the Zmodule for angle.