circular predicate

Stream: maths

[Yaël Dillies]

This is taking the discussion on #9413 off Github as I feel more people can be interested.

@Joseph Myers pointed out in #7329 that we didn't have an appropriate way to state that a polygon is noncrossing. I think the answer to this lies in a carefully crafted ternary predicate on points (something like orientation would probably do it, but I'm not claiming it's right) and some new simple list definitions:

import data.list.defs

inductive list.triwise {α : Sort*} (p : α → α → α → Prop) : list α → Prop
| nil : list.triwise list.nil
| cons {a : α} {l : list α} : l.pairwise (p a) → list.triwise l → list.triwise (a :: l)

def function.cycle_left {α β γ : Sort*} {φ : α → β → γ → Sort*}
  (f : Π (x : α) (y : β) (z : γ), φ x y z) (z : γ) (x : α) (y : β) : φ x y z := f x y z

def function.cycle_right {α β γ : Sort*} {φ : α → β → γ → Sort*}
  (f : Π (x : α) (y : β) (z : γ), φ x y z) (y : β) (z : γ) (x : α) : φ x y z := f x y z

def list.cyclewise {α : Sort*} (p : α → α → α → Prop) (l : list α) : Prop :=
l.triwise p ∧ l.triwise (function.cycle_left p) ∧ l.triwise (function.cycle_right p)

The idea behind is that p represents a betweenness relation and we ask all elements b that are "physically" in between a and c as elements of l to also be "conceptually" in between a and c according to p (translates to p a b c). But that's not enough as the last and first elements of the list is physically in between nothing but should still be conceptually checked. So we have to "cycle the list", which can be done by cycling the arguments of the predicates (have a look at #9413 to see why that works). Another option should be

def list.cyclewise {α : Sort*} (p : α → α → α → Prop) (l : list α) : Prop :=
(l ++ l).triwise p

[Yakov Pechersky]

Why not use an actual cycle? docs#cycle

[Yakov Pechersky]

Define your inductive Prop on lists, and lift it into the quotient

[Yaël Dillies]

Tha could do it.