[Merged by Bors] - feat(algebra/order/to_interval_mod): add circular_order instance for add_circle

[eric-wieser]

This also provides us with the same instance for real.angle.

---

• depends on: [Merged by Bors] - chore(algebra/order/to_interval_mod): add equiv versions extracted from add_circle #17739
• depends on: [Merged by Bors] - feat(algebra/order/to_interval_mod): lemmas about changing the base of the period #17741
• depends on: [Merged by Bors] - feat(algebra/order/to_interval_mod): more relations between to_Ixx_{mod/div} definitions #17933
• depends on: [Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod #18912
• depends on: [Merged by Bors] - feat(algebra/order/to_interval_mod): symmetric variants of lemmas #18942
• depends on: [Merged by Bors] - feat(algebra/order/to_interval_mod): notation for add_comm_group.modeq #18955
• depends on: [Merged by Bors] - refactor(algebra): Redefine a ≡ b [PMOD p] #18958

Note the only modification to a synchronized file is removing a TODO comment.

[alreadydone]

I think the following are also equivalent characterizations of betweenness, and may facilitate verifying the circular order axioms. I'll use {a} to denote the "fractional part" of a, i.e. a modulo the period:

• {c-b} + {b-a} ≤ period
• {c-b} + {b-a} + {a-c} ≤ period
• {c-b} + {b-a} + {a-c} = period (when a, b, c are not all the same)
• {c-a} = {c-b} + {b-a} (when a ≠ c or a = b = c)

should all be equivalent to btw a b c, and {c-b} + {b-a} < period + a,b,c all distinct should be equivalent to sbtw a b c (edit: btw a b c + a,b,c all distinct should be equivalent to sbtw a b c), though I'm not sure I've taken all degenerate cases into account.

I thought maybe some existing lemmas involving int.fract could be used, but I realized it's about linear_ordered_semiring which is more restrictive than (archimedean) linear_ordered_add_comm_group here. Does it mean we could generalize some floor_ring results to "floor_add_comm_group"?

By the way, we don't have an analogue of partial_order.lift for circular_order yet, right? We'll need it if we want to deduce that all zmod n (n > 0) admits a circular order from this PR.

[eric-wieser]

Unfortunately none of the int.fract lemmas can be used because translating to the language of int.fract requires a period of 1 and therefore division.

[eric-wieser]

It's not what you asked for, but I was able to show that {b-a} + {a-c} ≤ period was equivalent:

lemma to_Ico_mod_eq_sub (hb : 0 < b)  (x₁ x₂ : α) :
  to_Ico_mod x₁ hb x₂ =  to_Ico_mod 0 hb (x₂ - x₁) + x₁ :=
begin
  rw [to_Ico_mod_sub', zero_add, sub_add_cancel],
end

lemma to_Ioc_mod_eq_sub (hb : 0 < b) (x₁ x₂ : α) :
  to_Ioc_mod x₁ hb x₂ =  to_Ioc_mod 0 hb (x₂ - x₁) + x₁ :=
begin
  rw [to_Ioc_mod_sub', zero_add, sub_add_cancel],
end

private lemma to_Ixx_mod_iff (hb : 0 < b) (x₁ x₂ x₃ : α) :
  to_Ico_mod x₁ hb x₂ ≤ to_Ioc_mod x₁ hb x₃ ↔
  to_Ico_mod 0 hb (x₂ - x₁)  + to_Ico_mod 0 hb (x₁ - x₃) ≤ b :=
begin
  rw [to_Ico_mod_eq_sub, to_Ioc_mod_eq_sub _ x₁, add_le_add_iff_right],
  rw ←neg_sub x₁ x₃,
  rw to_Ioc_mod_neg,
  rw neg_zero,
  rw le_sub_iff_add_le,
end

[alreadydone]

Unfortunately none of the int.fract lemmas can be used because translating to the language of int.fract requires a period of 1 and therefore division.

Yes, there isn't a way to produce a semiring just from a add_comm_group. I just want to observe that multiplication seems not essential in floor_semiring.

I also realized that we don't need something like partial_order.lift, but can just apply the result of this PR to the linear_ordered_add_comm_group ℤ with period n > 0 to get the cyclic order on zmod n.

I'm glad that {c-b} + {b-a} ≤ period is indeed unconditionally equivalent to btw a b c. From this I think it's a lot easier to verify the axioms; another essential ingredient is the lemma saying {a-b} + {b-a} = period if a ≠ b (and = 0 if a = b). Thus if a ≠ b and b ≠ c then ({a-b} + {b-c}) + ({c-b} + {b-a}) = 2 * period, so one of {a-b} + {b-c} and {c-b} + {b-a} must be ≤ period, proving btw_total; if both are ≤ period then both are equal to period, which implies a = c, proving btw_antisymm. To prove cyclicity (btw_cyclic_left), it's best to prove the {c-b} + {b-a} + {a-c} ≤ period characterization which is invariant under cyclic permutations.

For sbtw_trans_left, the easiest proof I worked out is as follows:

• from btw a b c get {a-c} + {c-b} ≤ period (using cyclicity);
• from btw b d c get {b-c} + {c-d} ≤ period (again using cyclicity);
• from either sbtw a b c or sbtw b d c, get b ≠ c, so {b-c} + {c-b} = period;
• subtract this equality from the sum of the two inequalities, get {a-c} + {c-d} ≤ period, therefore btw a d c by cyclicity;
• from sbtw a b c get a ≠ c;
• from sbtw b d c get d ≠ c;
• if a = d, then btw a b c and btw b d c = btw b a c implies a,b,c are not all distinct by antisymmetry, contradicting strict betweenness;
• so a,d,c are all distinct, which implies sbtw a d c given btw a d c.

[alreadydone]

Unfortunately none of the int.fract lemmas can be used because translating to the language of int.fract requires a period of 1 and therefore division.

Actually we should be able to define division with remainder in any archimedean linear_ordered_add_comm_group with the quotient taking value in Z and remainder in the add_comm_group itself.

[eric-wieser]

Yes, those operations already exists and are what I'm using in this PR; they're called to_Ico_div and to_Ico_mod respectively.

[eric-wieser]

I'm glad that {c-b} + {b-a} ≤ period is indeed unconditionally equivalent to btw a b c.

That's not what I said; I showed that

• {b-a} + {a-c} ≤ period is equivalent to btw a b c, aka
• {c-b} + {b-a} ≤ period is equivalent to btw b c a

Maybe the difference doesn't matter.

[jcommelin]

@YaelDillies @eric-wieser so... what do we do? There still seem to be several different threads running around in this PR...

[eric-wieser]

#18958 is now on the queue, so I think all that remains is a final review of this PR.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(algebra/order/to_interval_mod): add equiv versions extracted from add_circle #17739
• [Merged by Bors] - feat(algebra/order/to_interval_mod): lemmas about changing the base of the period #17741
• [Merged by Bors] - feat(algebra/order/to_interval_mod): more relations between to_Ixx_{mod/div} definitions #17933
• [Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod #18912
• [Merged by Bors] - feat(algebra/order/to_interval_mod): symmetric variants of lemmas #18942
• [Merged by Bors] - feat(algebra/order/to_interval_mod): notation for add_comm_group.modeq #18955
• [Merged by Bors] - refactor(algebra): Redefine a ≡ b [PMOD p] #18958
  By Dependent Issues (🤖). Happy coding!

[kim-em]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests