Zulip Chat Archive

Stream: new members

Topic: reduce sin


view this post on Zulip 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?

view this post on Zulip Reid Barton (Jan 30 2019 at 15:05):

no

view this post on Zulip 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)?)

view this post on Zulip Joseph Corneli (Jan 30 2019 at 15:12):

True, I did mean that.

view this post on Zulip Kenny Lau (Jan 30 2019 at 15:14):

I thought you can reduce noncomputable things

view this post on Zulip 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?

view this post on Zulip Joseph Corneli (Jan 30 2019 at 15:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jan 30 2019 at 18:54):

That could be arranged

view this post on Zulip 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