search

sandialabs / Prove-It

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

Order theory and total ordering notation #182

Open wwitzel opened 4 years ago

wwitzel commented 4 years ago

Currently, we have a "relation" package which defines the TransitiveRelation Operation and related things. But "order theory" is a proper "thing" in its own right, abstracted from any specific type of ordering, so we should probably have an "ordering" theory package and move everything from "relation" to there (and delete "relations" which is obsolete).

While we are at it, another idea is to use "style" for total ordering notation (e.g., "a < b <= c") rather than creating special Operation classes for such things. Currently we have LesserSequence and GreaterSequence. It would make things a lot easier if we made this a style option for specific conjunctions. We would need to check that the conjunction satisfies some total ordering criteria in its structure -- e.g., they are consecutive relations where the relations all belong to some compatible set like {<, <=, =} or {>, >=, =} or {subset, subseteq, set_equiv, =}. This would save a lot of work and is fairly natural (though somewhat debatable).

wwitzel commented 3 years ago

The total ordering part of this was implemented along with #180. But creating a theory package for generic ordering theory has yet to be done.