reintroduce a type for angle (wip)

[affeldt-aist]

No description provided.

[CohenCyril]

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]

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]

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]

could it be the definition of angle?

[CohenCyril]

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]

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

[affeldt-aist]

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]

could this also be handled by some general alternating property

f x = 0, alternating f p -> there exists  0 <= x <p /\ f x = 0
``.

[affeldt-aist]

Thank you for your comments. This one I hadn't it time to address it today.
See 2a5197b

[thery]

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.