reduce sin

Stream: new members

[Joseph Corneli]

import data.complex.exponential analysis.exponential

open real
#check sin_pi_div_two
#reduce sin pi/2

(deterministic) timeout

Morally speaking, should #reduce sin pi/2 work?

[Reid Barton]

no

[Reid Barton]

I think the definition of pi is nonconstructive, but even if everything involved was constructive, in the best case this expression would reduce to the equivalence class of some particular Cauchy sequence of rationals, and you still would need to prove a theorem to know whether or not it was equal to 1. (By the way, I guess you mean sin (pi/2)?)

[Joseph Corneli]

True, I did mean that.

[Kenny Lau]

I thought you can reduce noncomputable things

[Kenny Lau]

but you might need to define "work": what output do you expect? an infinite stream of digits?

[Joseph Corneli]

I would have expected "1" but a stream would be interesting too.

[Reid Barton]

I agree "work" should be clarified, but in this case, the answer will turn out to be "no" for any reasonable interpretation.

[Johan Commelin]

Is there some sort of #simp? I imagine that you give it an expression, and it runs the simplifier against it and prints the result.

[Simon Hudon]

That could be arranged

[Johan Commelin]

I would imagine that #simp sin (pi/2) would in fact return 1. (Provided we have the right simp-lemmas in place.)