feat(Data.Prod.Lex): port file (#783)

mathlib3 SHA: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

porting notes: there are several issues here that should probably be fixed before this gets merged
1. `Prod.Lex` is not protect in core, so when you have this namespace open and try to refer to `Lex`, Lean finds `Prod.Lex` instead of `_root_.Lex`. This is not a huge deal since we have notation `α ×ₗ β`, but we should probably ask for it to be protected in core. See leanprover/lean4#1895
2. on the declarations `toLex_mono` and `toLex_strictMono`, Lean sees right through the type synonym `α ×ₗ β` to `α × β` and uses the wrong `Preorder` instance, which is why I had to provide them manually. I think this is a bug and should be fixed, otherwise it will cause loads of other issues down the road (for other type synonyms) and the errors will be hard to diagnose. EDIT: Hopefully leanprover/lean4#1891 will provide a fix.
3. I had to provide the definitions of `min` and `max` for the `LinearOrder` instance manually because in Lean 4 we have the classes `Min` and `Max` which have no counterpart in Lean 3. In this case it's a bit annoying because `ite` requires decidability, so I effectively had to provide that three times in this instance declaration. Surely there should be a better way?

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: j-loreaux

.github/workflows/bors.yml

@@ -21,7 +21,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -42,7 +42,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -60,7 +60,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - name: install elan
         run: |

.github/workflows/build.yml

@@ -27,7 +27,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -48,7 +48,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -66,7 +66,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - name: install elan
         run: |

.github/workflows/build.yml.in

@@ -7,7 +7,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -28,7 +28,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -46,7 +46,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - name: install elan
         run: |

.github/workflows/build_fork.yml

@@ -25,7 +25,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -46,7 +46,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - uses: actions/checkout@v2
 
@@ -64,7 +64,7 @@ jobs:
     steps:
       - name: cleanup
         run: |
-          rm -rf *
+          find . -name . -o -prune -exec rm -rf -- {} +
 
       - name: install elan
         run: |

Mathlib.lean

@@ -96,6 +96,7 @@ import Mathlib.Data.Option.NAry
 import Mathlib.Data.PNat.Defs
 import Mathlib.Data.Pi.Algebra
 import Mathlib.Data.Prod.Basic
+import Mathlib.Data.Prod.Lex
 import Mathlib.Data.Prod.PProd
 import Mathlib.Data.Quot
 import Mathlib.Data.Rat.Defs

Mathlib/Data/Prod/Basic.lean

@@ -175,7 +175,7 @@ theorem fst_eq_iff : ∀ {p : α × β} {x : α}, p.1 = x ↔ p = (x, p.2)
 theorem snd_eq_iff : ∀ {p : α × β} {x : β}, p.2 = x ↔ p = (p.1, x)
   | ⟨a, b⟩, x => by simp
 
-theorem Lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :
+theorem lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :
     Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
   ⟨fun h ↦ by cases h <;> simp [*], fun h ↦
     match p, q, h with
@@ -185,7 +185,7 @@ theorem Lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × 
 instance Lex.decidable [DecidableEq α]
     (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] :
     DecidableRel (Prod.Lex r s) :=
-  fun _ _ ↦ decidable_of_decidable_of_iff (Lex_def r s).symm
+  fun _ _ ↦ decidable_of_decidable_of_iff (lex_def r s).symm
 
 @[refl]
 theorem Lex.refl_left (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] : ∀ x, Prod.Lex r s x x

Mathlib/Data/Prod/Lex.lean

@@ -0,0 +1,204 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Minchao Wu
+-/
+import Mathlib.Order.BoundedOrder
+
+/-!
+# Lexicographic order
+
+This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.
+
+## Main declarations
+
+* `Prod.Lex.<pre/partial/linear>Order`: Instances lifting the orders on `α` and `β` to `α ×ₗ β`.
+
+## Notation
+
+* `α ×ₗ β`: `α × β` equipped with the lexicographic order
+
+## See also
+
+Related files are:
+* `Data.Finset.CoLex`: Colexicographic order on finite sets.
+* `Data.List.Lex`: Lexicographic order on lists.
+* `Data.Pi.Lex`: Lexicographic order on `Πₗ i, α i`.
+* `Data.PSigma.Order`: Lexicographic order on `Σ' i, α i`.
+* `Data.Sigma.Order`: Lexicographic order on `Σ i, α i`.
+-/
+
+
+variable {α β γ : Type _}
+
+namespace Prod.Lex
+
+-- porting note: `Prod.Lex` is not protected in core, hence the `_root_.` prefix
+-- This will be fixed in nightly-2022-11-30
+@[inherit_doc] notation:35 α " ×ₗ " β:34 => _root_.Lex (Prod α β)
+
+instance decidableEq (α β : Type _) [DecidableEq α] [DecidableEq β] : DecidableEq (α ×ₗ β) :=
+  instDecidableEqProd
+#align prod.lex.decidable_eq Prod.Lex.decidableEq
+
+instance inhabited (α β : Type _) [Inhabited α] [Inhabited β] : Inhabited (α ×ₗ β) :=
+  instInhabitedProd
+#align prod.lex.inhabited Prod.Lex.inhabited
+
+/-- Dictionary / lexicographic ordering on pairs.  -/
+instance instLE (α β : Type _) [LT α] [LE β] : LE (α ×ₗ β) where le := Prod.Lex (· < ·) (· ≤ ·)
+#align prod.lex.has_le Prod.Lex.instLE
+
+instance instLT (α β : Type _) [LT α] [LT β] : LT (α ×ₗ β) where lt := Prod.Lex (· < ·) (· < ·)
+#align prod.lex.has_lt Prod.Lex.instLT
+
+theorem le_iff [LT α] [LE β] (a b : α × β) :
+    toLex a ≤ toLex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 ≤ b.2 :=
+  Prod.lex_def (· < ·) (· ≤ ·)
+#align prod.lex.le_iff Prod.Lex.le_iff
+
+theorem lt_iff [LT α] [LT β] (a b : α × β) :
+    toLex a < toLex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 < b.2 :=
+  Prod.lex_def (· < ·) (· < ·)
+#align prod.lex.lt_iff Prod.Lex.lt_iff
+
+example (x : α) (y : β) : toLex (x, y) = toLex (x, y) := rfl
+
+/-- Dictionary / lexicographic preorder for pairs. -/
+instance preorder (α β : Type _) [Preorder α] [Preorder β] : Preorder (α ×ₗ β) :=
+  { Prod.Lex.instLE α β, Prod.Lex.instLT α β with
+    le_refl := refl_of <| Prod.Lex _ _,
+    le_trans := fun _ _ _ => trans_of <| Prod.Lex _ _,
+    lt_iff_le_not_le := fun x₁ x₂ =>
+      match x₁, x₂ with
+      | (a₁, b₁), (a₂, b₂) => by
+        constructor
+        · rintro (⟨_, _, hlt⟩ | ⟨_, hlt⟩)
+          · constructor
+            · exact left _ _ hlt
+            · rintro ⟨⟩
+              · apply lt_asymm hlt; assumption
+              · exact lt_irrefl _ hlt
+          · constructor
+            · right
+              rw [lt_iff_le_not_le] at hlt
+              exact hlt.1
+            · rintro ⟨⟩
+              · apply lt_irrefl a₁
+                assumption
+              · rw [lt_iff_le_not_le] at hlt
+                apply hlt.2
+                assumption
+        · rintro ⟨⟨⟩, h₂r⟩
+          · left
+            assumption
+          · right
+            rw [lt_iff_le_not_le]
+            constructor
+            · assumption
+            · intro h
+              apply h₂r
+              right
+              exact h }
+#align prod.lex.preorder Prod.Lex.preorder
+
+section Preorder
+
+variable [PartialOrder α] [Preorder β]
+
+-- porting note: type class search sees right through the type synonrm for `α ×ₗ β` and uses the
+-- `Preorder` structure for `α × β` instead
+-- This is hopefully the same problems as in https://github.com/leanprover/lean4/issues/1891
+-- and will be fixed in nightly-2022-11-30
+theorem toLex_mono : @Monotone _ _ _ (Prod.Lex.preorder α β) (toLex : α × β → α ×ₗ β) := by
+  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha, hb⟩
+  obtain rfl | ha : a₁ = a₂ ∨ _ := ha.eq_or_lt
+  · exact right _ hb
+  · exact left _ _ ha
+#align prod.lex.to_lex_mono Prod.Lex.toLex_mono
+
+-- porting note: type class search sees right through the type synonrm for `α ×ₗ β` and uses the
+-- `Preorder` structure for `α × β` instead
+-- This is hopefully the same problems as in https://github.com/leanprover/lean4/issues/1891
+-- and will be fixed in nightly-2022-11-30
+theorem toLex_strictMono : @StrictMono _ _ _ (Prod.Lex.preorder α β) (toLex : α × β → α ×ₗ β) := by
+  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
+  obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
+  · exact right _ (Prod.mk_lt_mk_iff_right.1 h)
+  · exact left _ _ ha
+
+#align prod.lex.to_lex_strict_mono Prod.Lex.toLex_strictMono
+
+end Preorder
+
+/-- Dictionary / lexicographic partial order for pairs. -/
+instance partialOrder (α β : Type _) [PartialOrder α] [PartialOrder β] : PartialOrder (α ×ₗ β) :=
+  { Prod.Lex.preorder α β with
+    le_antisymm := by
+      haveI : IsStrictOrder α (· < ·) := { irrefl := lt_irrefl, trans := fun _ _ _ => lt_trans }
+      haveI : IsAntisymm β (· ≤ ·) := ⟨fun _ _ => le_antisymm⟩
+      exact @antisymm _ (Prod.Lex _ _) _ }
+#align prod.lex.partial_order Prod.Lex.partialOrder
+
+/-- Dictionary / lexicographic linear order for pairs. -/
+instance linearOrder (α β : Type _) [LinearOrder α] [LinearOrder β] : LinearOrder (α ×ₗ β) :=
+  { Prod.Lex.partialOrder α β with
+    le_total := total_of (Prod.Lex _ _),
+    decidable_le := Prod.Lex.decidable _ _,
+    decidable_lt := Prod.Lex.decidable _ _,
+    decidable_eq := Lex.decidableEq _ _, }
+#align prod.lex.linear_order Prod.Lex.linearOrder
+
+instance orderBot [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] : OrderBot (α ×ₗ β) where
+  bot := toLex ⊥
+  bot_le _ := toLex_mono bot_le
+#align prod.lex.order_bot Prod.Lex.orderBot
+
+instance orderTop [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] : OrderTop (α ×ₗ β) where
+  top := toLex ⊤
+  le_top _ := toLex_mono le_top
+#align prod.lex.order_top Prod.Lex.orderTop
+
+instance boundedOrder [PartialOrder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :
+    BoundedOrder (α ×ₗ β) :=
+  { Lex.orderBot, Lex.orderTop with }
+#align prod.lex.bounded_order Prod.Lex.boundedOrder
+
+instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :
+    DenselyOrdered (α ×ₗ β) where
+  dense := by
+    rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩)
+    · obtain ⟨c, h₁, h₂⟩ := exists_between h
+      exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
+    · obtain ⟨c, h₁, h₂⟩ := exists_between h
+      exact ⟨(a, c), right _ h₁, right _ h₂⟩
+
+instance noMaxOrder_of_left [Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α ×ₗ β) where
+  exists_gt := by
+    rintro ⟨a, b⟩
+    obtain ⟨c, h⟩ := exists_gt a
+    exact ⟨⟨c, b⟩, left _ _ h⟩
+#align prod.lex.no_max_order_of_left Prod.Lex.noMaxOrder_of_left
+
+instance noMinOrder_of_left [Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (α ×ₗ β) where
+  exists_lt := by
+    rintro ⟨a, b⟩
+    obtain ⟨c, h⟩ := exists_lt a
+    exact ⟨⟨c, b⟩, left _ _ h⟩
+#align prod.lex.no_min_order_of_left Prod.Lex.noMinOrder_of_left
+
+instance noMaxOrder_of_right [Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (α ×ₗ β) where
+  exists_gt := by
+    rintro ⟨a, b⟩
+    obtain ⟨c, h⟩ := exists_gt b
+    exact ⟨⟨a, c⟩, right _ h⟩
+#align prod.lex.no_max_order_of_right Prod.Lex.noMaxOrder_of_right
+
+instance noMinOrder_of_right [Preorder α] [Preorder β] [NoMinOrder β] : NoMinOrder (α ×ₗ β) where
+  exists_lt := by
+    rintro ⟨a, b⟩
+    obtain ⟨c, h⟩ := exists_lt b
+    exact ⟨⟨a, c⟩, right _ h⟩
+#align prod.lex.no_min_order_of_right Prod.Lex.noMinOrder_of_right
+
+end Prod.Lex

Mathlib/Init/Algebra/Order.lean

@@ -226,6 +226,8 @@ class LinearOrder (α : Type u) extends PartialOrder α, Min α, Max α :=
   /-- In a linearly ordered type, we assume the order relations are all decidable. -/
   decidable_lt : DecidableRel (. < . : α → α → Prop) :=
     @decidableLt_of_decidableLe _ _ decidable_le
+  min := fun a b => if a ≤ b then a else b
+  max := fun a b => if a ≤ b then b else a
   /-- The minimum function is equivalent to the one you get from `minOfLe`. -/
   min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
   /-- The minimum function is equivalent to the one you get from `maxOfLe`. -/