feat(data/sum/order): Linear and disjoint sums of orders (#11157)

This defines the disjoint sum of two orders on `α ⊕ β` and the linear (aka lexicographic) sum of two orders on `α ⊕ₗ β` (a type synonym of `α ⊕ β`) in a new file `data.sum.order`.

src/algebra/lie/classical.lean

@@ -330,11 +330,11 @@ begin
   ext i j,
   rcases i with ⟨⟨i₁ | i₂⟩ | i₃⟩;
   rcases j with ⟨⟨j₁ | j₂⟩ | j₃⟩;
-  simp only [indefinite_diagonal, matrix.diagonal, equiv.sum_assoc_apply_in1,
+  simp only [indefinite_diagonal, matrix.diagonal, equiv.sum_assoc_apply_inl_inl,
     matrix.reindex_lie_equiv_apply, matrix.minor_apply, equiv.symm_symm, matrix.reindex_apply,
     sum.elim_inl, if_true, eq_self_iff_true, matrix.one_apply_eq, matrix.from_blocks_apply₁₁,
-    dmatrix.zero_apply, equiv.sum_assoc_apply_in2, if_false, matrix.from_blocks_apply₁₂,
-    matrix.from_blocks_apply₂₁, matrix.from_blocks_apply₂₂, equiv.sum_assoc_apply_in3,
+    dmatrix.zero_apply, equiv.sum_assoc_apply_inl_inr, if_false, matrix.from_blocks_apply₁₂,
+    matrix.from_blocks_apply₂₁, matrix.from_blocks_apply₂₂, equiv.sum_assoc_apply_inr,
     sum.elim_inr];
   congr,
 end

src/data/equiv/basic.lean

@@ -679,21 +679,34 @@ noncomputable def Prop_equiv_bool : Prop ≃ bool :=
 
 /-- Sum of types is commutative up to an equivalence. -/
 @[simps apply]
-def sum_comm (α β : Sort*) : α ⊕ β ≃ β ⊕ α :=
+def sum_comm (α β : Type*) : α ⊕ β ≃ β ⊕ α :=
 ⟨sum.swap, sum.swap, sum.swap_swap, sum.swap_swap⟩
 
 @[simp] lemma sum_comm_symm (α β) : (sum_comm α β).symm = sum_comm β α := rfl
 
 /-- Sum of types is associative up to an equivalence. -/
-def sum_assoc (α β γ : Sort*) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
+def sum_assoc (α β γ : Type*) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
 ⟨sum.elim (sum.elim sum.inl (sum.inr ∘ sum.inl)) (sum.inr ∘ sum.inr),
   sum.elim (sum.inl ∘ sum.inl) $ sum.elim (sum.inl ∘ sum.inr) sum.inr,
   by rintros (⟨_ | _⟩ | _); refl,
   by rintros (_ | ⟨_ | _⟩); refl⟩
 
-@[simp] theorem sum_assoc_apply_in1 {α β γ} (a) : sum_assoc α β γ (inl (inl a)) = inl a := rfl
-@[simp] theorem sum_assoc_apply_in2 {α β γ} (b) : sum_assoc α β γ (inl (inr b)) = inr (inl b) := rfl
-@[simp] theorem sum_assoc_apply_in3 {α β γ} (c) : sum_assoc α β γ (inr c) = inr (inr c) := rfl
+@[simp] lemma sum_assoc_apply_inl_inl {α β γ} (a) : sum_assoc α β γ (inl (inl a)) = inl a := rfl
+
+@[simp] lemma sum_assoc_apply_inl_inr {α β γ} (b) : sum_assoc α β γ (inl (inr b)) = inr (inl b) :=
+rfl
+
+@[simp] lemma sum_assoc_apply_inr {α β γ} (c) : sum_assoc α β γ (inr c) = inr (inr c) := rfl
+
+@[simp] lemma sum_assoc_symm_apply_inl {α β γ} (a) : (sum_assoc α β γ).symm (inl a) = inl (inl a) :=
+rfl
+
+@[simp] lemma sum_assoc_symm_apply_inr_inl {α β γ} (b) :
+  (sum_assoc α β γ).symm (inr (inl b)) = inl (inr b) := rfl
+
+@[simp] lemma sum_assoc_symm_apply_inr_inr {α β γ} (c) :
+  (sum_assoc α β γ).symm (inr (inr c)) = inr c := rfl
+
 
 /-- Sum with `empty` is equivalent to the original type. -/
 @[simps symm_apply] def sum_empty (α β : Type*) [is_empty β] : α ⊕ β ≃ α :=

src/data/sum/basic.lean

@@ -3,8 +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, Yury G. Kudryashov
 -/
-import logic.function.basic
-import tactic.protected
+import data.option.basic
 
 /-!
 # Disjoint union of types
@@ -77,6 +76,14 @@ section get
 | (inl _) := ff
 | (inr _) := tt
 
+variables {x y : α ⊕ β}
+
+lemma get_left_eq_none_iff : x.get_left = none ↔ x.is_right :=
+by cases x; simp only [get_left, is_right, coe_sort_tt, coe_sort_ff, eq_self_iff_true]
+
+lemma get_right_eq_none_iff : x.get_right = none ↔ x.is_left :=
+by cases x; simp only [get_right, is_left, coe_sort_tt, coe_sort_ff, eq_self_iff_true]
+
 end get
 
 /-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
@@ -194,6 +201,56 @@ by rw ← update_inr_comp_inr
 @[simp] lemma swap_left_inverse : function.left_inverse (@swap α β) swap := swap_swap
 @[simp] lemma swap_right_inverse : function.right_inverse (@swap α β) swap := swap_swap
 
+section lift_rel
+
+/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
+`α ⊕ β` and `γ ⊕ δ`. -/
+inductive lift_rel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
+| inl {a c} : r a c → lift_rel (inl a) (inl c)
+| inr {b d} : s b d → lift_rel (inr b) (inr d)
+
+attribute [protected] lift_rel.inl lift_rel.inr
+
+variables {r r₁ r₂ : α → γ → Prop} {s s₁ s₂ : β → δ → Prop} {a : α} {b : β} {c : γ} {d : δ}
+  {x : α ⊕ β} {y : γ ⊕ δ}
+
+@[simp] lemma lift_rel_inl_inl : lift_rel r s (inl a) (inl c) ↔ r a c :=
+⟨λ h, by { cases h, assumption }, lift_rel.inl⟩
+
+@[simp] lemma not_lift_rel_inl_inr : ¬ lift_rel r s (inl a) (inr d) .
+@[simp] lemma not_lift_rel_inr_inl : ¬ lift_rel r s (inr b) (inl c) .
+
+@[simp] lemma lift_rel_inr_inr : lift_rel r s (inr b) (inr d) ↔ s b d :=
+⟨λ h, by { cases h, assumption }, lift_rel.inr⟩
+
+instance [Π a c, decidable (r a c)] [Π b d, decidable (s b d)] :
+  Π (ab : α ⊕ β) (cd : γ ⊕ δ), decidable (lift_rel r s ab cd)
+| (inl a) (inl c) := decidable_of_iff' _ lift_rel_inl_inl
+| (inl a) (inr d) := decidable.is_false not_lift_rel_inl_inr
+| (inr b) (inl c) := decidable.is_false not_lift_rel_inr_inl
+| (inr b) (inr d) := decidable_of_iff' _ lift_rel_inr_inr
+
+lemma lift_rel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
+  (h : lift_rel r₁ s₁ x y) :
+  lift_rel r₂ s₂ x y :=
+by { cases h, exacts [lift_rel.inl (hr _ _ ‹_›), lift_rel.inr (hs _ _ ‹_›)] }
+
+lemma lift_rel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : lift_rel r₁ s x y) :
+  lift_rel r₂ s x y :=
+h.mono hr $ λ _ _, id
+
+lemma lift_rel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b)  (h : lift_rel r s₁ x y) :
+  lift_rel r s₂ x y :=
+h.mono (λ _ _, id) hs
+
+protected lemma lift_rel.swap (h : lift_rel r s x y) : lift_rel s r x.swap y.swap :=
+by { cases h, exacts [lift_rel.inr ‹_›, lift_rel.inl ‹_›] }
+
+@[simp] lemma lift_rel_swap_iff : lift_rel s r x.swap y.swap ↔ lift_rel r s x y :=
+⟨λ h, by { rw [←swap_swap x, ←swap_swap y], exact h.swap }, lift_rel.swap⟩
+
+end lift_rel
+
 section lex
 
 /-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
@@ -217,6 +274,15 @@ variables {r r₁ r₂ : α → α → Prop} {s s₁ s₂ : β → β → Prop}
 
 @[simp] lemma lex_inr_inl : ¬ lex r s (inr b) (inl a) .
 
+instance [decidable_rel r] [decidable_rel s] : decidable_rel (lex r s)
+| (inl a) (inl c) := decidable_of_iff' _ lex_inl_inl
+| (inl a) (inr d) := decidable.is_true (lex.sep _ _)
+| (inr b) (inl c) := decidable.is_false lex_inr_inl
+| (inr b) (inr d) := decidable_of_iff' _ lex_inr_inr
+
+protected lemma lift_rel.lex {a b : α ⊕ β} (h : lift_rel r s a b) : lex r s a b :=
+by { cases h, exacts [lex.inl ‹_›, lex.inr ‹_›] }
+
 lemma lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : lex r₁ s₁ x y) :
   lex r₂ s₂ x y :=
 by { cases h, exacts [lex.inl (hr _ _ ‹_›), lex.inr (hs _ _ ‹_›), lex.sep _ _] }