ConditionSet, ImageSet: Implement formal Set comprehension

[rwst]

In order to be able to express solution sets from SymPy's solveset a set comprehension constructor as equivalent to SymPy's imageset / ConditionSet is needed. As the arguments are symbolic the most natural way to do this would be a formal symbolic function named like set_of_all taking a term argument and a list argument containing element_of(...) function expressions.

This set would convert to a SymPy ImageSet or ConditionSet

Related: ImageManifoldSubset (#31653)

Depends on #24171
Depends on #32013
Depends on #32089
Depends on #32121

CC: @tscrim @mantepse

Component: symbolics

Reviewer: Travis Scrimshaw

Issue created by migration from https://trac.sagemath.org/ticket/24176

[rwst]

Dependencies: #24171

[rwst]

Changed dependencies from #24171 to #24171, pynac-0.7.13

[rwst]

comment:2

Accepting lists requires the function being a GinacFunction.

[rwst]

Branch: u/rws/implement_formal_set_comprehension

[rwst]

Commit: 9c77312

[rwst]

Changed dependencies from #24171, pynac-0.7.13 to #24171, #24262

[rwst]

New commits:

669ea22	24171: Formal set membership function
34c9773	24171: make RealSet inherit from Set_generic
af82717	24171: remove RealSet import; SR set coercion doctests
592ce87	24171: Py3 fixes
82b7c6f	Merge branch 'u/rws/formal_set_membership_function' of git://trac.sagemath.org/sage into t/24176/implement_formal_set_comprehension
ae29895	24176: check set argument of element_of()
9c77312	24176: Implement formal Set comprehension

[rwst]

Changed branch from u/rws/implement_formal_set_comprehension to u/rws/24176

[rwst]

Changed branch from u/rws/24176 to u/rws/implement_formal_set_comprehension

[rwst]

Changed dependencies from #24171, #24262 to #24171, #24329

[rwst]

Author: Ralf Stephan

[mkoeppe]

Changed branch from u/rws/implement_formal_set_comprehension to u/mkoeppe/implement_formal_set_comprehension

[mkoeppe]

Changed commit from 9c77312 to ec39309

[mkoeppe]

Changed dependencies from #24171, #24329 to #24171

[mkoeppe]

comment:8

Rebased on top of rebased #24171

---

New commits:

72565f2	24171: Formal set membership function
71bbf38	24171: Formal set membership function
6811a76	24171: make RealSet inherit from Set_generic
0a66f78	24171: remove RealSet import; SR set coercion doctests
e35349a	24171: Py3 fixes
26ef67d	24176: check set argument of element_of()
ec39309	24176: Implement formal Set comprehension

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. This was a forced push. Last 10 new commits:

51c8152	Merge branch 't/31877/refine_category_of_realset' into t/24171/set-membership-rebased
5e623bb	RealSet.is_finite: Remove, inherited from category
7d19916	Do not use QQ.completion(oo,oo) - not implemented
9b4e224	24176: check set argument of element_of()
5310e04	Function_elementof: Remove use of is_Set
46d9795	24171: Formal set membership function
6995d1e	24171: make RealSet inherit from Set_generic
a41c5fc	24171: remove RealSet import; SR set coercion doctests
2a9c49a	24171: Py3 fixes
24789ba	24176: Implement formal Set comprehension

[sagetrac-git]

Changed commit from ec39309 to 24789ba

[mkoeppe]

comment:10

Rebased on top of updated #24171, which cherry-picked 1 commit from here.

Not sure about the changes on this ticket marked 24171. They are either from a newer or older version of 24171.

[mkoeppe]

comment:11

The fix to RealSet.__bool__ in 6995d1e/2a9c49a can go to #31941 (Make empty RealSet false).

Unclear to me whether 6995d1e (make RealSet inherit from Set_generic) should be done

[mkoeppe]

comment:14

I think the approach on the current branch may be tied a bit too closely to SR functions.

I think it's better to first implement:

• ImageSubset (as an abstract subobject of the codomain) for arbitrary Maps -- this would be a generalization of ImageManifoldSubset (Images of continuous maps and embedded submanifolds as manifold subsets #31653). No relation to SR (but by relaxing the code from Formal set membership function #24171 that only allows some sets to be coerced to SR, one would be able to coerce it to SR).

• ConditionSet (as an abstract subobject of a parent in the Sets category) - defined via the element constructor of the parent and an SR expression with truth value.

[mkoeppe]

comment:16

Replying to @mkoeppe:

• ConditionSet (as an abstract subobject of a parent in the Sets category) - defined via the element constructor of the parent and an SR expression with truth value.

more precisely... an element of CallableSymbolicExpression (see #32008 for making this safer)

[mkoeppe]

Changed dependencies from #24171 to #24171, #32013

[mkoeppe]

Changed dependencies from #24171, #32013 to #24171, #32013, #32089

[mkoeppe]

comment:18

Replying to @mkoeppe:

Replying to @mkoeppe:

• ConditionSet (as an abstract subobject of a parent in the Sets category) - defined via the element constructor of the parent and an SR expression with truth value.

more precisely... an element of CallableSymbolicExpression (see #32008 for making this safer)

This is now implemented in #32089.

[mkoeppe]

comment:19

ImageSet is essentially the same as the (deprecated?) sage.combinat.combinat.MapCombinatorialClass, except that we would not insist that the map is injective.

[mkoeppe]

comment:20

Opened #32121 Replace MapCombinatorialClass

[mkoeppe]

Changed dependencies from #24171, #32013, #32089 to #24171, #32013, #32089, #32121

[mantepse]

comment:22

@mkoeppe: since you put me into the CC list, would this include symbolic roots of polynomials, given by the minimal polynomial?

I am guessing (because I'm not an expert there) that these would really need a special treatment, because one can compute with them quite well.

[mkoeppe]

comment:25

With #32121 merged, this is now finished

[mkoeppe]

Changed author from Ralf Stephan to none

[tscrim]

comment:26

Agreed.

[tscrim]

Reviewer: Travis Scrimshaw

[tscrim]

Changed branch from u/mkoeppe/implement_formal_set_comprehension to none

[tscrim]

Changed commit from 24789ba to none

[mantepse]

comment:27

Does #32121 provide a possibility to specify the set of roots of a polynomial?