feat: Colex order on pi types (#29080)

We define an order instance on `Colex (∀ i, β i)`, so that its `<` relation is `Pi.Lex (· > ·) (· < ·)`.

Author: vihdzp

Mathlib/Order/PiLex.lean

@@ -9,8 +9,12 @@ import Mathlib.Tactic.Common
 /-!
 # Lexicographic order on Pi types
 
-This file defines the lexicographic order for Pi types. `a` is less than `b` if `a i = b i` for all
-`i` up to some point `k`, and `a k < b k`.
+This file defines the lexicographic and colexicographic orders for Pi types.
+
+* In the lexicographic order, `a` is less than `b` if `a i = b i` for all `i` up to some point
+  `k`, and `a k < b k`.
+* In the colexicographic order, `a` is less than `b` if `a i = b i` for all `i` above some point
+  `k`, and `a k < b k`.
 
 ## Notation
 
@@ -33,7 +37,10 @@ variable {ι : Type*} {β : ι → Type*} (r : ι → ι → Prop) (s : ∀ {i},
 namespace Pi
 
 /-- The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`,
-  and each `β i` is ordered by `s`. -/
+and each `β i` is ordered by `s`.
+
+The `<` relation on `Lex (∀ i, β i)` is `Pi.Lex (· < ·) (· < ·)`, while the `<` relation on
+`Colex (∀ i, β i)` is `Pi.Lex (· > ·) (· < ·)`. -/
 protected def Lex (x y : ∀ i, β i) : Prop :=
   ∃ i, (∀ j, r j i → x j = y j) ∧ s (x i) (y i)
 
@@ -57,7 +64,7 @@ theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (β i)] {r} (hwf : WellFounded
   ⟨i, fun j hj => ⟨h'.1 j, not_not.1 fun h => hl j (lt_of_le_not_ge (h'.1 j) h) hj⟩, hi⟩
 
 theorem lex_lt_of_lt [∀ i, PartialOrder (β i)] {r} (hwf : WellFounded r) {x y : ∀ i, β i}
-    (hlt : x < y) : Pi.Lex r (@fun _ => (· < ·)) x y := by
+    (hlt : x < y) : Pi.Lex r (· < ·) x y := by
   simp_rw [Pi.Lex, le_antisymm_iff]
   exact lex_lt_of_lt_of_preorder hwf hlt
 
@@ -78,7 +85,10 @@ theorem isTrichotomous_lex [∀ i, IsTrichotomous (β i) s] (wf : WellFounded r)
           Or.inr <| Or.inr <| ⟨i, fun j hj => (hri j hj).symm, hi.resolve_left hne⟩] }
 
 instance [LT ι] [∀ a, LT (β a)] : LT (Lex (∀ i, β i)) :=
-  ⟨Pi.Lex (· < ·) @fun _ => (· < ·)⟩
+  ⟨Pi.Lex (· < ·) (· < ·)⟩
+
+instance [LT ι] [∀ a, LT (β a)] : LT (Colex (∀ i, β i)) :=
+  ⟨Pi.Lex (· > ·) (· < ·)⟩
 
 instance Lex.isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] :
     IsStrictOrder (Lex (∀ i, β i)) (· < ·) where
@@ -90,16 +100,28 @@ instance Lex.isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] :
       ⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩,
       ⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩]
 
+instance Colex.isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] :
+    IsStrictOrder (Colex (∀ i, β i)) (· < ·) :=
+  Lex.isStrictOrder (ι := ιᵒᵈ)
+
 instance [LinearOrder ι] [∀ a, PartialOrder (β a)] : PartialOrder (Lex (∀ i, β i)) :=
   partialOrderOfSO (· < ·)
 
-/-- `Πₗ i, α i` is a linear order if the original order is well-founded. -/
-noncomputable instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, LinearOrder (β a)] :
-    LinearOrder (Lex (∀ i, β i)) :=
+instance [LinearOrder ι] [∀ a, PartialOrder (β a)] : PartialOrder (Colex (∀ i, β i)) :=
+  partialOrderOfSO (· < ·)
+
+/-- `Lex (∀ i, α i)` is a linear order if the original order has well-founded `<`. -/
+noncomputable instance Lex.linearOrder [LinearOrder ι] [WellFoundedLT ι]
+    [∀ a, LinearOrder (β a)] : LinearOrder (Lex (∀ i, β i)) :=
   @linearOrderOfSTO (Πₗ i, β i) (· < ·)
     { trichotomous := (isTrichotomous_lex _ _ IsWellFounded.wf).1 } (Classical.decRel _)
 
-section PartialOrder
+/-- `Colex (∀ i, α i)` is a linear order if the original order has well-founded `>`. -/
+noncomputable instance Colex.linearOrder [LinearOrder ι] [WellFoundedGT ι]
+    [∀ a, LinearOrder (β a)] : LinearOrder (Colex (∀ i, β i)) :=
+  Lex.linearOrder (ι := ιᵒᵈ)
+
+section Lex
 
 variable [LinearOrder ι] [WellFoundedLT ι] [∀ i, PartialOrder (β i)] {x : ∀ i, β i} {i : ι}
   {a : β i}
@@ -151,21 +173,64 @@ theorem le_toLex_update_self_iff : toLex x ≤ toLex (update x i a) ↔ x i ≤
 theorem toLex_update_le_self_iff : toLex (update x i a) ≤ toLex x ↔ a ≤ x i := by
   simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]
 
-end PartialOrder
+end Lex
+
+section Colex
+
+variable [LinearOrder ι] [WellFoundedGT ι] [∀ i, PartialOrder (β i)] {x : ∀ i, β i} {i : ι}
+  {a : β i}
+
+open Function
+
+theorem toColex_monotone : Monotone (@toColex (∀ i, β i)) :=
+  toLex_monotone (ι := ιᵒᵈ)
+
+theorem toColex_strictMono : StrictMono (@toColex (∀ i, β i)) :=
+  toLex_strictMono (ι := ιᵒᵈ)
+
+@[simp]
+theorem lt_toColex_update_self_iff : toColex x < toColex (update x i a) ↔ x i < a :=
+  lt_toLex_update_self_iff (ι := ιᵒᵈ)
+
+@[simp]
+theorem toColex_update_lt_self_iff : toColex (update x i a) < toColex x ↔ a < x i :=
+  toLex_update_lt_self_iff (ι := ιᵒᵈ)
+
+@[simp]
+theorem le_toColex_update_self_iff : toColex x ≤ toColex (update x i a) ↔ x i ≤ a :=
+  le_toLex_update_self_iff (ι := ιᵒᵈ)
+
+@[simp]
+theorem toColex_update_le_self_iff : toColex (update x i a) ≤ toColex x ↔ a ≤ x i :=
+  toLex_update_le_self_iff (ι := ιᵒᵈ)
+
+end Colex
 
 instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderBot (β a)] :
     OrderBot (Lex (∀ a, β a)) where
   bot := toLex ⊥
   bot_le _ := toLex_monotone bot_le
 
+instance [LinearOrder ι] [WellFoundedGT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderBot (β a)] :
+    OrderBot (Colex (∀ a, β a)) where
+  bot := toColex ⊥
+  bot_le _ := toColex_monotone bot_le
+
 instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderTop (β a)] :
     OrderTop (Lex (∀ a, β a)) where
   top := toLex ⊤
   le_top _ := toLex_monotone le_top
 
+instance [LinearOrder ι] [WellFoundedGT ι] [∀ a, PartialOrder (β a)] [∀ a, OrderTop (β a)] :
+    OrderTop (Colex (∀ a, β a)) where
+  top := toColex ⊤
+  le_top _ := toColex_monotone le_top
+
 instance [LinearOrder ι] [WellFoundedLT ι] [∀ a, PartialOrder (β a)]
-    [∀ a, BoundedOrder (β a)] : BoundedOrder (Lex (∀ a, β a)) :=
-  { }
+    [∀ a, BoundedOrder (β a)] : BoundedOrder (Lex (∀ a, β a)) where
+
+instance [LinearOrder ι] [WellFoundedGT ι] [∀ a, PartialOrder (β a)]
+    [∀ a, BoundedOrder (β a)] : BoundedOrder (Colex (∀ a, β a)) where
 
 instance [Preorder ι] [∀ i, LT (β i)] [∀ i, DenselyOrdered (β i)] :
     DenselyOrdered (Lex (∀ i, β i)) :=
@@ -181,6 +246,10 @@ instance [Preorder ι] [∀ i, LT (β i)] [∀ i, DenselyOrdered (β i)] :
       · rw [Function.update_of_ne hj.ne a]
       · rwa [Function.update_self i a]⟩
 
+instance [Preorder ι] [∀ i, LT (β i)] [∀ i, DenselyOrdered (β i)] :
+    DenselyOrdered (Colex (∀ i, β i)) :=
+  inferInstanceAs (DenselyOrdered (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))
+
 theorem Lex.noMaxOrder' [Preorder ι] [∀ i, LT (β i)] (i : ι) [NoMaxOrder (β i)] :
     NoMaxOrder (Lex (∀ i, β i)) :=
   ⟨fun a => by
@@ -189,23 +258,42 @@ theorem Lex.noMaxOrder' [Preorder ι] [∀ i, LT (β i)] (i : ι) [NoMaxOrder (
     exact ⟨Function.update a i b, i, fun j hj =>
       (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩⟩
 
+theorem Colex.noMaxOrder' [Preorder ι] [∀ i, LT (β i)] (i : ι) [NoMaxOrder (β i)] :
+    NoMaxOrder (Colex (∀ i, β i)) :=
+  Lex.noMaxOrder' (ι := ιᵒᵈ) i
+
 instance [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [∀ i, PartialOrder (β i)]
     [∀ i, NoMaxOrder (β i)] : NoMaxOrder (Lex (∀ i, β i)) :=
   ⟨fun a =>
     let ⟨_, hb⟩ := exists_gt (ofLex a)
     ⟨_, toLex_strictMono hb⟩⟩
 
+instance [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [∀ i, PartialOrder (β i)]
+    [∀ i, NoMaxOrder (β i)] : NoMaxOrder (Colex (∀ i, β i)) :=
+  inferInstanceAs (NoMaxOrder (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))
+
 instance [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [∀ i, PartialOrder (β i)]
     [∀ i, NoMinOrder (β i)] : NoMinOrder (Lex (∀ i, β i)) :=
   ⟨fun a =>
     let ⟨_, hb⟩ := exists_lt (ofLex a)
     ⟨_, toLex_strictMono hb⟩⟩
 
+instance [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [∀ i, PartialOrder (β i)]
+    [∀ i, NoMinOrder (β i)] : NoMinOrder (Colex (∀ i, β i)) :=
+  inferInstanceAs (NoMinOrder (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))
+
 /-- If we swap two strictly decreasing values in a function, then the result is lexicographically
 smaller than the original function. -/
 theorem lex_desc {α} [Preorder ι] [DecidableEq ι] [LT α] {f : ι → α} {i j : ι} (h₁ : i ≤ j)
     (h₂ : f j < f i) : toLex (f ∘ Equiv.swap i j) < toLex f :=
   ⟨i, fun _ hik => congr_arg f (Equiv.swap_apply_of_ne_of_ne hik.ne (hik.trans_le h₁).ne), by
     simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂⟩
 
+/-- If we swap two strictly increasing values in a function, then the result is colexicographically
+smaller than the original function. -/
+theorem colex_asc {α} [Preorder ι] [DecidableEq ι] [LT α] {f : ι → α} {i j : ι} (h₁ : i ≤ j)
+    (h₂ : f i < f j) : toColex (f ∘ Equiv.swap i j) < toColex f := by
+  rw [Equiv.swap_comm]
+  exact lex_desc (ι := ιᵒᵈ) h₁ h₂
+
 end Pi