sandialabs / Prove-It

A tool for proving and organizing general theorems using Python.
http://pyproveit.org
Other
27 stars 10 forks source link

Need to check 'is_applicable' for known_memberships in linear_algebra and quantum algebra packages #320

Open wwitzel opened 9 months ago

wwitzel commented 9 months ago

InClass.yield_known_memberships does this properly where it checks 'is_applicable'. However, this doesn't appear done properly for yield_known_hilbert_spaces in the linear_algebra package or when using MatrixSpace.known_memberships in qmult.py. This can cause funny behavior when assumptions change. There may be other places where this is done incorrectly.

wwitzel commented 8 months ago

As an addendum to this Issue, I'd like to like to add further InClass.conclude (and thereby InSet.conclude) automation, checking to see if the element has a "readily_provable_membership" method. If so, and if it returns True when given the domain for the membership we are trying to prove in "conclude", than call the element's "deduce_membership" method, letting the element handle things. Other automation works from the domain side, but sometimes it is better to handle it on the element side.