Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Q.real(x) does not lead to Q.finite(x) being true #17113

Open
oscargus opened this issue Jun 27, 2019 · 4 comments · May be fixed by #17118
Open

Q.real(x) does not lead to Q.finite(x) being true #17113

oscargus opened this issue Jun 27, 2019 · 4 comments · May be fixed by #17118

Comments

@oscargus
Copy link
Contributor

It may be that I have no idea about how the assumption system is supposed to work, but I was under the impression that ask(Q.finite(x), Q.real(x)) should evaluate to True.

@jksuom
Copy link
Member

jksuom commented Jun 27, 2019

It looks like the implication Q.finite(x) | ~Q.real(x) is missing from known facts:

Q.finite | ~Q.algebraic,
Q.finite | ~Q.irrational,
Q.finite | ~Q.rational,
Q.finite | ~Q.transcendental,

@oscargus
Copy link
Contributor Author

Yes, that was my conclusion as well. That is Implies(Q.real, Q.finite), right?

@jksuom
Copy link
Member

jksuom commented Jun 27, 2019

I think so. In ask.py. Then ask_generated.py will have to be regenerated.

@oscarbenjamin
Copy link
Contributor

I think I thought this was already the case in the new assumptions. Yes that implication should be added and then ask_generated should be rebuilt.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants