Divide and conquer for sorting networks

Stream: general

[Daniel Weber]

I'm trying to formalize sorting networks, and it's important to be able to do divide and conquer easily for constructions on it. What's the best way to do that? This is my current definition for sorting networks:

import Mathlib.Order.MinMax
import Mathlib.Tactic
import Mathlib.Order.PropInstances

set_option autoImplicit false

variable {α β γ : Type*} [LinearOrder α] [LinearOrder β] [LinearOrder γ]

def ComparatorNetwork.Layer (α : Type*) := {a : α → α // Function.Involutive a}

def ComparatorNetwork.Layer.perm' (l : ComparatorNetwork.Layer α) (v : α → β) (x : α) : α :=
  if v (min x (l.1 x)) < v (max x (l.1 x)) then x else l.1 x

/-
Thanks to
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lattice.20tactics/near/453730734
-/
attribute [aesop unsafe apply 10%] le_trans
attribute [aesop unsafe apply 10%] lt_trans
attribute [aesop safe forward] le_of_lt
attribute [aesop safe forward] lt_of_le_of_lt
attribute [aesop safe forward] lt_of_lt_of_le

lemma ComparatorNetwork.Layer.perm'_involutive (l : ComparatorNetwork.Layer α) (v : α → β) :
    Function.Involutive (l.perm' v) := by
  intro a
  unfold ComparatorNetwork.Layer.perm'
  have : ∀ x, l.1 (l.1 x) = x := l.2
  split
  · rfl
  · rename_i h
    simp_all only [not_lt, ite_eq_right_iff]
    intro h2
    rw [min_comm, max_comm] at h2
    exact (h.trans_lt h2).false.elim

def ComparatorNetwork.Layer.perm (l : ComparatorNetwork.Layer α) (v : α → β) : Equiv.Perm α := (l.perm'_involutive v).toPerm

def ComparatorNetwork.Layer.apply (l : ComparatorNetwork.Layer α) (v : α → β) : α → β :=
  v ∘ (l.perm v)

def ComparatorNetwork.Layer.apply_eq (l : ComparatorNetwork.Layer α) (v : α → β) (x : α) :
    l.apply v x = if x < l.1 x then min (v x) (v (l.1 x)) else max (v x) (v (l.1 x)) := by
  unfold ComparatorNetwork.Layer.apply ComparatorNetwork.Layer.perm ComparatorNetwork.Layer.perm'
  aesop

lemma ComparatorNetwork.Layer.apply_comm (s : ComparatorNetwork.Layer α) (v : α → β) (f : β → γ) (hf : Monotone f) :
    f ∘ (s.apply v) = s.apply (f ∘ v) := by
  ext x
  simp only [Function.comp_apply, apply_eq, apply_ite f, hf.map_min, hf.map_max]

def ComparatorNetwork := List ∘ ComparatorNetwork.Layer

def ComparatorNetwork.apply (s : ComparatorNetwork α) (v : α → β) := s.foldl (fun v l ↦ l.apply v) v

lemma ComparatorNetwork.apply_comm (s : ComparatorNetwork α) (v : α → β) (f : β → γ) (hf : Monotone f) :
    f ∘ (s.apply v) = s.apply (f ∘ v) := by
  unfold ComparatorNetwork.apply
  induction s generalizing v
  case nil => simp
  case cons a s h =>
    simp only [List.foldl_cons]
    rw [h, ComparatorNetwork.Layer.apply_comm]
    exact hf

def SortingNetwork (α : Type*) [LinearOrder α] := {a : ComparatorNetwork α // ∀ v : α → Prop, Monotone (a.apply v)}

def SortingNetwork.apply (s : SortingNetwork α) (v : α → β) := s.1.apply v

@[simp]
def SortingNetwork.coe_apply (s : SortingNetwork α) (v : α → β) : (s.1.apply v) = s.apply v := rfl

lemma zero_one_principle (s : SortingNetwork α) (v : α → β) : Monotone (s.apply v) := by
  intro a b h
  by_contra! nh
  have := s.2 ((fun x ↦ s.apply v a ≤ x) ∘ v) h
  rw [← ComparatorNetwork.apply_comm] at this
  simp only [SortingNetwork.coe_apply, Function.comp_apply, le_refl, le_Prop_eq, true_implies] at this
  exact (nh.trans_le this).false
  intro x y hx
  simp only [le_Prop_eq]
  exact fun h ↦ h.trans hx

[Daniel Weber]

I think I figured it out - I show how to construct something on α ⊕ₗ α by that structure on α. Now I'm trying to formalize Bitonic sequences (a sequence which increases then decreases, or vice vesra). I came up with a few definitions - which one seems best, or are there other good alternatives?

• Bitonic (f : α → β) := ∃ a : α, (MonotoneOn f (Set.Iic a) ∧ AntitoneOn f (Set.Ici a)) ∨(AntitoneOn f (Set.Iic a) ∧ MonotoneOn f (Set.Ici a)) - a rather direct translation of the definition. I'm having trouble with it because it requires to explicitly provide the a.
• Bitonic (f : α → Prop) := ∃ a b : α, (a ≤ b) ∧ ((∀ x, f x ↔ a ≤ x ∧ x ≤ b) ∨ (∀ x, f x ↔ x < a ∨ b < x)) - this is only for Props, as by the zero-one principle it suffices to prove stuff for them. I'm having trouble with it because I'm not sure how to handle intervals which aren't closed using it.
• Bitonic (f : α → β) := ∀ a b c d, a ≤ b → b ≤ c → c ≤ d → ( (f a ≤ f b ∧ f b ≤ f c) ∨ (f a ≥ f b ∧ f b ≥ f c) ∨ (f b ≤ f c ∧ v c ≤ v d) ∨ (f b ≥ f c ∧ v c ≥ v d) ) - I think this is the simplest definition, but it requires too much case analysis to actually use.