move(order/synonym): Group order_dual and lex (#13769)

Move `to_dual`, `of_dual`, `to_lex`, `of_lex` to a new file `order.synonym`. This does not change the import tree, because `order.lexicographic` had slightly higher imports than `order.order_dual`, but those weren't used for `lex` itself.
leanprover-community · May 10, 2022 · c892622 · c892622
1 parent 37c691f
commit c892622
Show file tree

Hide file tree

Showing 15 changed files with 116 additions and 101 deletions.
diff --git a/src/algebra/group/type_tags.lean b/src/algebra/group/type_tags.lean
@@ -16,6 +16,10 @@ We define two type tags:
   multiplicative structure on `multiplicative α`.
 
 We also define instances `additive.*` and `multiplicative.*` that actually transfer the structures.
+
+## See also
+
+This file is similar to `order.synonym`.
 -/
 
 universes u v

diff --git a/src/algebra/order/group.lean b/src/algebra/order/group.lean
@@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.abs
 import algebra.order.sub
-import order.order_dual
 
 /-!
 # Ordered groups

diff --git a/src/algebra/order/rearrangement.lean b/src/algebra/order/rearrangement.lean
@@ -5,6 +5,7 @@ Authors: Mantas Bakšys
 -/
 import algebra.order.module
 import group_theory.perm.support
+import order.lexicographic
 import order.monovary
 import tactic.abel
 

diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, François Dupuis
 -/
 import analysis.convex.basic
-import order.order_dual
 import tactic.field_simp
 import tactic.linarith
 import tactic.ring

diff --git a/src/data/finset/lattice.lean b/src/data/finset/lattice.lean
@@ -8,7 +8,7 @@ import data.finset.option
 import data.finset.prod
 import data.multiset.lattice
 import order.complete_lattice
-import order.lexicographic
+
 /-!
 # Lattice operations on finsets
 -/

diff --git a/src/data/psigma/order.lean b/src/data/psigma/order.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Minchao Wu
 -/
 import data.sigma.lex
-import order.lexicographic
+import order.synonym
 
 /-!
 # Lexicographic order on a sigma type

diff --git a/src/data/sigma/order.lean b/src/data/sigma/order.lean
@@ -5,7 +5,6 @@ Authors: Yaël Dillies
 -/
 import data.sigma.lex
 import order.bounded_order
-import order.lexicographic
 
 /-!
 # Orders on a sigma type

diff --git a/src/data/sum/order.lean b/src/data/sum/order.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import order.hom.basic
-import order.lexicographic
 
 /-!
 # Orders on a sum type

diff --git a/src/group_theory/group_action/fixing_subgroup.lean b/src/group_theory/group_action/fixing_subgroup.lean
@@ -6,7 +6,6 @@ Authors: Antoine Chambert-Loir
 
 import group_theory.subgroup.basic
 import group_theory.group_action.basic
-import order.order_dual
 
 /-!
 

diff --git a/src/order/compare.lean b/src/order/compare.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import order.order_dual
+import order.synonym
 
 /-!
 # Comparison

diff --git a/src/order/galois_connection.lean b/src/order/galois_connection.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import order.complete_lattice
-import order.order_dual
+import order.synonym
+
 /-!
 # Galois connections, insertions and coinsertions
 

diff --git a/src/order/lexicographic.lean b/src/order/lexicographic.lean
@@ -3,9 +3,7 @@ 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 data.prod
-import logic.equiv.basic
-import tactic.basic
+import order.synonym
 
 /-!
 # Lexicographic order
@@ -31,28 +29,7 @@ Related files are:
 * `data.sigma.order`: Lexicographic order on `Σ i, α i`.
 -/
 
-universes u v
-
-/-- A type synonym to equip a type with its lexicographic order. -/
-def lex (α : Type u) := α
-
-variables {α : Type u} {β : Type v} {γ : Type*}
-
-/-- `to_lex` is the identity function to the `lex` of a type.  -/
-@[pattern] def to_lex : α ≃ lex α := ⟨id, id, λ h, rfl, λ h, rfl⟩
-
-/-- `of_lex` is the identity function from the `lex` of a type.  -/
-@[pattern] def of_lex : lex α ≃ α := to_lex.symm
-
-@[simp] lemma to_lex_symm_eq : (@to_lex α).symm = of_lex := rfl
-@[simp] lemma of_lex_symm_eq : (@of_lex α).symm = to_lex := rfl
-@[simp] lemma to_lex_of_lex (a : lex α) : to_lex (of_lex a) = a := rfl
-@[simp] lemma of_lex_to_lex (a : α) : of_lex (to_lex a) = a := rfl
-@[simp] lemma to_lex_inj {a b : α} : to_lex a = to_lex b ↔ a = b := iff.rfl
-@[simp] lemma of_lex_inj {a b : lex α} :  of_lex a = of_lex b ↔ a = b := iff.rfl
-
-/-- A recursor for `lex`. Use as `induction x using lex.rec`. -/
-protected def lex.rec {β : lex α → Sort*} (h : Π a, β (to_lex a)) : Π a, β a := λ a, h (of_lex a)
+variables {α β γ : Type*}
 
 namespace prod.lex
 

diff --git a/src/order/max.lean b/src/order/max.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Yury Kudryashov, Yaël Dillies
 -/
-import order.order_dual
+import order.synonym
 
 /-!
 # Minimal/maximal and bottom/top elements

diff --git a/src/order/order_dual.lean b/src/order/order_dual.lean
diff --git a/src/order/synonym.lean b/src/order/synonym.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2020 Johan Commelin, Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Damiano Testa, Yaël Dillies
+-/
+import logic.equiv.basic
+import logic.nontrivial
+import order.basic
+
+/-!
+# Type synonyms
+
+This file provides two type synonyms for order theory:
+* `order_dual α`: Type synonym of `α` to equip it with the dual order (`a ≤ b` becomes `b ≤ a`).
+* `lex α`: Type synonym of `α` to equip it with its lexicographic order. The precise meaning depends
+  on the type we take the lex of. Examples include `prod`, `sigma`, `list`, `finset`.
+
+## Notation
+
+`αᵒᵈ` is notation for `order_dual α`.
+
+The general rule for notation of `lex` types is to append `ₗ` to the usual notation.
+
+## Implementation notes
+
+One should not abuse definitional equality between `α` and `αᵒᵈ`/`lex α`. Instead, explicit
+coercions should be inserted:
+* `order_dual`: `order_dual.to_dual : α → αᵒᵈ` and `order_dual.of_dual : αᵒᵈ → α`
+* `lex`: `to_lex : α → lex α` and `of_lex : lex α → α`.
+
+In fact, those are bundled as `equiv`s to put goals in the right syntactic form for rewriting with
+the `equiv` API (`⇑to_lex a` where `⇑` is `coe_fn : (α ≃ lex α) → α → lex α`, instead of a bare
+`to_lex a`).
+
+## See also
+
+This file is similar to `algebra.group.type_tags`.
+-/
+
+variables {α β γ : Type*}
+
+/-! ### Order dual -/
+
+namespace order_dual
+
+instance [h : nontrivial α] : nontrivial (αᵒᵈ) := h
+
+/-- `to_dual` is the identity function to the `order_dual` of a linear order.  -/
+def to_dual : α ≃ αᵒᵈ := equiv.refl _
+
+/-- `of_dual` is the identity function from the `order_dual` of a linear order.  -/
+def of_dual : αᵒᵈ ≃ α := equiv.refl _
+
+@[simp] lemma to_dual_symm_eq : (@to_dual α).symm = of_dual := rfl
+@[simp] lemma of_dual_symm_eq : (@of_dual α).symm = to_dual := rfl
+@[simp] lemma to_dual_of_dual (a : αᵒᵈ) : to_dual (of_dual a) = a := rfl
+@[simp] lemma of_dual_to_dual (a : α) : of_dual (to_dual a) = a := rfl
+@[simp] lemma to_dual_inj {a b : α} : to_dual a = to_dual b ↔ a = b := iff.rfl
+@[simp] lemma of_dual_inj {a b : αᵒᵈ} : of_dual a = of_dual b ↔ a = b := iff.rfl
+
+@[simp] lemma to_dual_le_to_dual [has_le α] {a b : α} : to_dual a ≤ to_dual b ↔ b ≤ a := iff.rfl
+@[simp] lemma to_dual_lt_to_dual [has_lt α] {a b : α} : to_dual a < to_dual b ↔ b < a := iff.rfl
+@[simp] lemma of_dual_le_of_dual [has_le α] {a b : αᵒᵈ} : of_dual a ≤ of_dual b ↔ b ≤ a := iff.rfl
+@[simp] lemma of_dual_lt_of_dual [has_lt α] {a b : αᵒᵈ} : of_dual a < of_dual b ↔ b < a := iff.rfl
+lemma le_to_dual [has_le α] {a : αᵒᵈ} {b : α} : a ≤ to_dual b ↔ b ≤ of_dual a := iff.rfl
+lemma lt_to_dual [has_lt α] {a : αᵒᵈ} {b : α} : a < to_dual b ↔ b < of_dual a := iff.rfl
+lemma to_dual_le [has_le α] {a : α} {b : αᵒᵈ} : to_dual a ≤ b ↔ of_dual b ≤ a := iff.rfl
+lemma to_dual_lt [has_lt α] {a : α} {b : αᵒᵈ} : to_dual a < b ↔ of_dual b < a := iff.rfl
+
+/-- Recursor for `αᵒᵈ`. -/
+@[elab_as_eliminator]
+protected def rec {C : αᵒᵈ → Sort*} (h₂ : Π a : α, C (to_dual a)) : Π a : αᵒᵈ, C a := h₂
+
+@[simp] protected lemma «forall» {p : αᵒᵈ → Prop} : (∀ a, p a) ↔ ∀ a, p (to_dual a) := iff.rfl
+@[simp] protected lemma «exists» {p : αᵒᵈ → Prop} : (∃ a, p a) ↔ ∃ a, p (to_dual a) := iff.rfl
+
+alias to_dual_le_to_dual ↔ _ has_le.le.dual
+alias to_dual_lt_to_dual ↔ _ has_lt.lt.dual
+alias of_dual_le_of_dual ↔ _ has_le.le.of_dual
+alias of_dual_lt_of_dual ↔ _ has_lt.lt.of_dual
+
+end order_dual
+
+/-! ### Lexicographic order -/
+
+/-- A type synonym to equip a type with its lexicographic order. -/
+def lex (α : Type*) := α
+
+/-- `to_lex` is the identity function to the `lex` of a type.  -/
+@[pattern] def to_lex : α ≃ lex α := equiv.refl _
+
+/-- `of_lex` is the identity function from the `lex` of a type.  -/
+@[pattern] def of_lex : lex α ≃ α := equiv.refl _
+
+@[simp] lemma to_lex_symm_eq : (@to_lex α).symm = of_lex := rfl
+@[simp] lemma of_lex_symm_eq : (@of_lex α).symm = to_lex := rfl
+@[simp] lemma to_lex_of_lex (a : lex α) : to_lex (of_lex a) = a := rfl
+@[simp] lemma of_lex_to_lex (a : α) : of_lex (to_lex a) = a := rfl
+@[simp] lemma to_lex_inj {a b : α} : to_lex a = to_lex b ↔ a = b := iff.rfl
+@[simp] lemma of_lex_inj {a b : lex α} :  of_lex a = of_lex b ↔ a = b := iff.rfl
+
+/-- A recursor for `lex`. Use as `induction x using lex.rec`. -/
+protected def lex.rec {β : lex α → Sort*} (h : Π a, β (to_lex a)) : Π a, β a := λ a, h (of_lex a)