## Stream: new members

### Topic: reduce sin

#### Joseph Corneli (Jan 30 2019 at 15:03):

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?

no

#### Reid Barton (Jan 30 2019 at 15:08):

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 (Jan 30 2019 at 15:12):

True, I did mean that.

#### Kenny Lau (Jan 30 2019 at 15:14):

I thought you can reduce noncomputable things

#### Kenny Lau (Jan 30 2019 at 15:14):

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

#### Joseph Corneli (Jan 30 2019 at 15:17):

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

#### Reid Barton (Jan 30 2019 at 15:17):

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

#### Johan Commelin (Jan 30 2019 at 18:50):

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 (Jan 30 2019 at 18:54):

That could be arranged

#### Johan Commelin (Jan 30 2019 at 18:57):

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

Last updated: May 12 2021 at 04:19 UTC