# Circular order hierarchy #

This file defines circular preorders, circular partial orders and circular orders.

## Hierarchy #

- A ternary "betweenness" relation
`btw : α → α → α → Prop`

forms a`CircularOrder`

if it is- reflexive:
`btw a a a`

- cyclic:
`btw a b c → btw b c a`

- antisymmetric:
`btw a b c → btw c b a → a = b ∨ b = c ∨ c = a`

- total:
`btw a b c ∨ btw c b a`

along with a strict betweenness relation`sbtw : α → α → α → Prop`

which respects`sbtw a b c ↔ btw a b c ∧ ¬ btw c b a`

, analogously to how`<`

and`≤`

are related, and is - transitive:
`sbtw a b c → sbtw b d c → sbtw a d c`

.

- reflexive:
- A
`CircularPartialOrder`

drops totality. - A
`CircularPreorder`

further drops antisymmetry.

The intuition is that a circular order is a circle and `btw a b c`

means that going around
clockwise from `a`

you reach `b`

before `c`

(`b`

is between `a`

and `c`

is meaningless on an
unoriented circle). A circular partial order is several, potentially intersecting, circles. A
circular preorder is like a circular partial order, but several points can coexist.

Note that the relations between `CircularPreorder`

, `CircularPartialOrder`

and `CircularOrder`

are subtler than between `Preorder`

, `PartialOrder`

, `LinearOrder`

. In particular, one cannot
simply extend the `Btw`

of a `CircularPartialOrder`

to make it a `CircularOrder`

.

One can translate from usual orders to circular ones by "closing the necklace at infinity". See
`LE.toBtw`

and `LT.toSBtw`

. Going the other way involves "cutting the necklace" or
"rolling the necklace open".

## Examples #

Some concrete circular orders one encounters in the wild are `ZMod n`

for `0 < n`

, `Circle`

,
`Real.Angle`

...

## Main definitions #

## Notes #

There's an unsolved diamond on `OrderDual α`

here. The instances `LE α → Btw αᵒᵈ`

and
`LT α → SBtw αᵒᵈ`

can each be inferred in two ways:

`LE α`

→`Btw α`

→`Btw αᵒᵈ`

vs`LE α`

→`LE αᵒᵈ`

→`Btw αᵒᵈ`

`LT α`

→`SBtw α`

→`SBtw αᵒᵈ`

vs`LT α`

→`LT αᵒᵈ`

→`SBtw αᵒᵈ`

The fields are propeq, but not defeq. It is temporarily fixed by turning the circularizing instances into definitions.

## TODO #

Antisymmetry is quite weak in the sense that there's no way to discriminate which two points are
equal. This prevents defining closed-open intervals `cIco`

and `cIoc`

in the neat `=`

-less way. We
currently haven't defined them at all.

What is the correct generality of "rolling the necklace" open? At least, this works for `α × β`

and
`β × α`

where `α`

is a circular order and `β`

is a linear order.

What's next is to define circular groups and provide instances for `ZMod n`

, the usual circle group
`Circle`

, and `RootsOfUnity M`

. What conditions do we need on `M`

for this last one
to work?

We should have circular order homomorphisms. The typical example is
`days_to_month : days_of_the_year →c months_of_the_year`

which relates the circular order of days
and the circular order of months. Is `α →c β`

a good notation?

## References #

## Tags #

circular order, cyclic order, circularly ordered set, cyclically ordered set

A circular preorder is the analogue of a preorder where you can loop around. `≤`

and `<`

are
replaced by ternary relations `btw`

and `sbtw`

. `btw`

is reflexive and cyclic. `sbtw`

is transitive.

- btw : α → α → α → Prop
- sbtw : α → α → α → Prop
- btw_refl : ∀ (a : α), btw a a a
`a`

is between`a`

and`a`

. If

`b`

is between`a`

and`c`

, then`c`

is between`b`

and`a`

. This is motivated by imagining three points on a circle.Strict betweenness is given by betweenness in one direction and non-betweenness in the other.

I.e., if

`b`

is between`a`

and`c`

but not between`c`

and`a`

, then we say`b`

is strictly between`a`

and`c`

.For any fixed

`c`

,`fun a b ↦ sbtw a b c`

is a transitive relation.I.e., given

`a`

`b`

`d`

`c`

in that "order", if we have`b`

strictly between`a`

and`c`

, and`d`

strictly between`b`

and`c`

, then`d`

is strictly between`a`

and`c`

.

## Instances

`a`

is between `a`

and `a`

.

If `b`

is between `a`

and `c`

, then `c`

is between `b`

and `a`

.
This is motivated by imagining three points on a circle.

Strict betweenness is given by betweenness in one direction and non-betweenness in the other.

I.e., if `b`

is between `a`

and `c`

but not between `c`

and `a`

, then we say `b`

is strictly
between `a`

and `c`

.

For any fixed `c`

, `fun a b ↦ sbtw a b c`

is a transitive relation.

I.e., given `a`

`b`

`d`

`c`

in that "order", if we have `b`

strictly between `a`

and `c`

, and `d`

strictly between `b`

and `c`

, then `d`

is strictly between `a`

and `c`

.

A circular partial order is the analogue of a partial order where you can loop around. `≤`

and
`<`

are replaced by ternary relations `btw`

and `sbtw`

. `btw`

is reflexive, cyclic and
antisymmetric. `sbtw`

is transitive.

- btw : α → α → α → Prop
- sbtw : α → α → α → Prop
- btw_refl : ∀ (a : α), btw a a a
If

`b`

is between`a`

and`c`

and also between`c`

and`a`

, then at least one pair of points among`a`

,`b`

,`c`

are identical.

## Instances

A circular order is the analogue of a linear order where you can loop around. `≤`

and `<`

are
replaced by ternary relations `btw`

and `sbtw`

. `btw`

is reflexive, cyclic, antisymmetric and total.
`sbtw`

is transitive.

- btw : α → α → α → Prop
- sbtw : α → α → α → Prop
- btw_refl : ∀ (a : α), btw a a a
For any triple of points, the second is between the other two one way or another.

## Instances

For any triple of points, the second is between the other two one way or another.

### Circular preorders #

**Alias** of `btw_cyclic_right`

.

The order of the `↔`

has been chosen so that `rw [btw_cyclic]`

cycles to the right while
`rw [← btw_cyclic]`

cycles to the left (thus following the prepended arrow).

**Alias** of `btw_of_sbtw`

.

**Alias** of `not_btw_of_sbtw`

.

**Alias** of `not_sbtw_of_btw`

.

**Alias** of `sbtw_of_btw_not_btw`

.

**Alias** of `sbtw_cyclic_left`

.

**Alias** of `sbtw_cyclic_right`

.

The order of the `↔`

has been chosen so that `rw [sbtw_cyclic]`

cycles to the right while
`rw [← sbtw_cyclic]`

cycles to the left (thus following the prepended arrow).

**Alias** of `sbtw_trans_right`

.

**Alias** of `sbtw_asymm`

.

### Circular partial orders #

### Circular orders #

### Circular intervals #

### Circularizing instances #

The circular preorder obtained from "looping around" a preorder. See note [reducible non-instances].

## Equations

- Preorder.toCircularPreorder α = CircularPreorder.mk ⋯ ⋯ ⋯ ⋯

## Instances For

The circular partial order obtained from "looping around" a partial order. See note [reducible non-instances].

## Equations

## Instances For

The circular order obtained from "looping around" a linear order. See note [reducible non-instances].

## Equations

## Instances For

### Dual constructions #

## Equations

- OrderDual.btw α = { btw := fun (a b c : α) => btw c b a }

## Equations

- OrderDual.sbtw α = { sbtw := fun (a b c : α) => sbtw c b a }

## Equations

- OrderDual.circularPreorder α = CircularPreorder.mk ⋯ ⋯ ⋯ ⋯