doc-next-gen

Mathlib.Data.Sigma.Lex

Module docstring

{"# Lexicographic order on a sigma type

This defines the lexicographical order of two arbitrary relations on a sigma type and proves some lemmas about PSigma.Lex, which is defined in core Lean.

Given a relation in the index type and a relation on each summand, the lexicographical order on the sigma type relates a and b if their summands are related or they are in the same summand and related by the summand's relation.

See also

Related files are: * Combinatorics.CoLex: Colexicographic order on finite sets. * Data.List.Lex: Lexicographic order on lists. * Data.Sigma.Order: Lexicographic order on Σ i, α i per say. * Data.PSigma.Order: Lexicographic order on Σ' i, α i. * Data.Prod.Lex: Lexicographic order on α × β. Can be thought of as the special case of Sigma.Lex where all summands are the same ","### PSigma "}

Sigma.Lex inductive
(r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) : ∀ _ _ : Σ i, α i, Prop
Full source 
/-- The lexicographical order on a sigma type. It takes in a relation on the index type and a
relation for each summand. `a` is related to `b` iff their summands are related or they are in the
same summand and are related through the summand's relation. -/
inductive Lex (r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) : ∀ _ _ : Σ i, α i, Prop
  | left {i j : ι} (a : α i) (b : α j) : r i j → Lex r s ⟨i, a⟩ ⟨j, b⟩
  | right {i : ι} (a b : α i) : s i a b → Lex r s ⟨i, a⟩ ⟨i, b⟩
Lexicographical order on a dependent sum type
Informal description
Given an index type $\iota$ with a relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with a relation $s_i$, the lexicographical order on the dependent sum type $\Sigma i, \alpha_i$ is defined as follows: for two elements $(i, a)$ and $(j, b)$, $(i, a)$ is lexicographically less than $(j, b)$ if either $i$ is related to $j$ under $r$, or $i = j$ and $a$ is related to $b$ under $s_i$.
Sigma.lex_iff theorem
: Lex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec a.2) b.2
Full source 
theorem lex_iff : LexLex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec a.2) b.2 := by
  constructor
  · rintro (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩
  · obtain ⟨i, a⟩ := a
    obtain ⟨j, b⟩ := b
    dsimp only
    rintro (h | ⟨rfl, h⟩)
    · exact Lex.left _ _ h
    · exact Lex.right _ _ h
Characterization of Lexicographical Order on Dependent Sum Types
Informal description
Let $\iota$ be an index type with a relation $r$, and for each $i \in \iota$, let $\alpha_i$ be a type with a relation $s_i$. For two elements $(i, a)$ and $(j, b)$ in the dependent sum type $\Sigma i, \alpha_i$, the lexicographical order $\text{Lex}(r, s)$ relates $(i, a)$ to $(j, b)$ if and only if either: 1. $i$ is related to $j$ under $r$ (i.e., $r(i, j)$ holds), or 2. $i = j$ and $a$ is related to $b$ under $s_i$ (i.e., $s_i(a, b)$ holds).
Sigma.Lex.decidable instance
(r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) [DecidableEq ι] [DecidableRel r] [∀ i, DecidableRel (s i)] : DecidableRel (Lex r s)
Full source 
instance Lex.decidable (r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) [DecidableEq ι]
    [DecidableRel r] [∀ i, DecidableRel (s i)] : DecidableRel (Lex r s) := fun _ _ =>
  decidable_of_decidable_of_iff lex_iff.symm
Decidability of Lexicographical Order on Dependent Sum Types
Informal description
For an index type $\iota$ with a decidable equality and a decidable relation $r$, and for each $i \in \iota$ a type $\alpha_i$ with a decidable relation $s_i$, the lexicographical order on the dependent sum type $\Sigma i, \alpha_i$ is decidable. That is, given two elements $(i, a)$ and $(j, b)$, it is decidable whether $(i, a)$ is lexicographically less than $(j, b)$ under the relations $r$ and $s_i$.
Sigma.Lex.mono theorem
(hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ i, α i} (h : Lex r₁ s₁ a b) : Lex r₂ s₂ a b
Full source 
theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ i, α i}
    (h : Lex r₁ s₁ a b) : Lex r₂ s₂ a b := by
  obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h
  · exact Lex.left _ _ (hr _ _ hij)
  · exact Lex.right _ _ (hs _ _ _ hab)
Monotonicity of Lexicographical Order on Dependent Sum Types
Informal description
Let $\iota$ be an index type with two relations $r_1$ and $r_2$, and for each $i \in \iota$, let $\alpha_i$ be a type with two relations $s_1^i$ and $s_2^i$. Suppose that: 1. $r_1$ is pointwise weaker than $r_2$ (i.e., $r_1(a, b)$ implies $r_2(a, b)$ for all $a, b \in \iota$), and 2. For each $i \in \iota$, $s_1^i$ is pointwise weaker than $s_2^i$ (i.e., $s_1^i(a, b)$ implies $s_2^i(a, b)$ for all $a, b \in \alpha_i$). Then for any two elements $(i, a)$ and $(j, b)$ in the dependent sum type $\Sigma i, \alpha_i$, if $(i, a)$ is lexicographically less than $(j, b)$ under the relations $r_1$ and $s_1^i$, then it is also lexicographically less than $(j, b)$ under the relations $r_2$ and $s_2^i$.
Sigma.Lex.mono_left theorem
(hr : ∀ a b, r₁ a b → r₂ a b) {a b : Σ i, α i} (h : Lex r₁ s a b) : Lex r₂ s a b
Full source 
theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) {a b : Σ i, α i} (h : Lex r₁ s a b) :
    Lex r₂ s a b :=
  h.mono hr fun _ _ _ => id
Monotonicity of Lexicographical Order in Index Relation
Informal description
Let $\iota$ be an index type with two relations $r_1$ and $r_2$ such that $r_1$ is pointwise weaker than $r_2$ (i.e., $r_1(a, b) \to r_2(a, b)$ for all $a, b \in \iota$). Then for any elements $(i, a)$ and $(j, b)$ in the dependent sum type $\Sigma i, \alpha_i$, if $(i, a)$ is lexicographically less than $(j, b)$ under $r_1$ and $s_i$, then it is also lexicographically less under $r_2$ and $s_i$.
Sigma.Lex.mono_right theorem
(hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ i, α i} (h : Lex r s₁ a b) : Lex r s₂ a b
Full source 
theorem Lex.mono_right (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ i, α i} (h : Lex r s₁ a b) :
    Lex r s₂ a b :=
  h.mono (fun _ _ => id) hs
Monotonicity of Lexicographical Order in Value Relations
Informal description
Let $\iota$ be an index type with a relation $r$, and for each $i \in \iota$, let $\alpha_i$ be a type with two relations $s_1^i$ and $s_2^i$ such that $s_1^i$ is pointwise weaker than $s_2^i$ (i.e., $s_1^i(a, b) \to s_2^i(a, b)$ for all $a, b \in \alpha_i$). Then for any elements $(i, a)$ and $(j, b)$ in the dependent sum type $\Sigma i, \alpha_i$, if $(i, a)$ is lexicographically less than $(j, b)$ under $r$ and $s_1^i$, then it is also lexicographically less under $r$ and $s_2^i$.
Sigma.lex_swap theorem
: Lex (Function.swap r) s a b ↔ Lex r (fun i => Function.swap (s i)) b a
Full source 
theorem lex_swap : LexLex (Function.swap r) s a b ↔ Lex r (fun i => Function.swap (s i)) b a := by
  constructor <;>
    · rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
      · exact Lex.left _ _ h
      · exact Lex.right _ _ h
Lexicographical Order Swap: $\text{Lex}(\text{swap}(r), s) \leftrightarrow \text{Lex}(r, \text{swap}(s))$
Informal description
For any relations $r$ on an index type $\iota$ and $s_i$ on each $\alpha_i$, and for any elements $a, b$ in the dependent sum type $\Sigma i, \alpha_i$, the lexicographical order with swapped relations $r$ and $s_i$ relates $a$ and $b$ if and only if the original lexicographical order relates $b$ and $a$ with the original relations. In other words, $(a, b) \in \text{Lex}(\text{swap}(r), s)$ if and only if $(b, a) \in \text{Lex}(r, \text{swap}(s))$, where $\text{swap}(r)(i,j) = r(j,i)$ and $\text{swap}(s_i)(x,y) = s_i(y,x)$ for each $i \in \iota$.
Sigma.instIsReflLex instance
[∀ i, IsRefl (α i) (s i)] : IsRefl _ (Lex r s)
Full source 
instance [∀ i, IsRefl (α i) (s i)] : IsRefl _ (Lex r s) :=
  ⟨fun ⟨_, _⟩ => Lex.right _ _ <| refl _⟩
Reflexivity of Lexicographical Order on Dependent Sum Types
Informal description
For any index type $\iota$ with relations $r$ on $\iota$ and $s_i$ on each $\alpha_i$, if each $s_i$ is reflexive, then the lexicographical order on the dependent sum type $\Sigma i, \alpha_i$ is also reflexive.
Sigma.instIsIrreflLex instance
[IsIrrefl ι r] [∀ i, IsIrrefl (α i) (s i)] : IsIrrefl _ (Lex r s)
Full source 
instance [IsIrrefl ι r] [∀ i, IsIrrefl (α i) (s i)] : IsIrrefl _ (Lex r s) :=
  ⟨by
    rintro _ (⟨a, b, hi⟩ | ⟨a, b, ha⟩)
    · exact irrefl _ hi
    · exact irrefl _ ha
      ⟩
Irreflexivity of Lexicographic Order on Sigma Types
Informal description
For any index type $\iota$ with an irreflexive relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with an irreflexive relation $s_i$, the lexicographical order $\text{Lex}(r, s)$ on the dependent sum type $\Sigma i, \alpha_i$ is irreflexive.
Sigma.instIsTransLex instance
[IsTrans ι r] [∀ i, IsTrans (α i) (s i)] : IsTrans _ (Lex r s)
Full source 
instance [IsTrans ι r] [∀ i, IsTrans (α i) (s i)] : IsTrans _ (Lex r s) :=
  ⟨by
    rintro _ _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, c, hk⟩ | ⟨_, c, hc⟩)
    · exact Lex.left _ _ (_root_.trans hij hk)
    · exact Lex.left _ _ hij
    · exact Lex.left _ _ hk
    · exact Lex.right _ _ (_root_.trans hab hc)⟩
Transitivity of Lexicographic Order on Sigma Types
Informal description
For any index type $\iota$ with a transitive relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with a transitive relation $s_i$, the lexicographical order $\text{Lex}(r, s)$ on the dependent sum type $\Sigma i, \alpha_i$ is transitive.
Sigma.instIsSymmLex instance
[IsSymm ι r] [∀ i, IsSymm (α i) (s i)] : IsSymm _ (Lex r s)
Full source 
instance [IsSymm ι r] [∀ i, IsSymm (α i) (s i)] : IsSymm _ (Lex r s) :=
  ⟨by
    rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
    · exact Lex.left _ _ (symm hij)
    · exact Lex.right _ _ (symm hab)
      ⟩
Symmetry of Lexicographic Order on Sigma Types
Informal description
For any index type $\iota$ with a symmetric relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with a symmetric relation $s_i$, the lexicographical order $\text{Lex}(r, s)$ on the dependent sum type $\Sigma i, \alpha_i$ is symmetric.
Sigma.instIsAntisymmLexOfIsAsymm instance
[IsAsymm ι r] [∀ i, IsAntisymm (α i) (s i)] : IsAntisymm _ (Lex r s)
Full source 
instance [IsAsymm ι r] [∀ i, IsAntisymm (α i) (s i)] : IsAntisymm _ (Lex r s) :=
  ⟨by
    rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)
    · exact (asymm hij hji).elim
    · exact (irrefl _ hij).elim
    · exact (irrefl _ hji).elim
    · exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba⟩
Antisymmetry of Lexicographic Order on Sigma Types with Asymmetric and Antisymmetric Relations
Informal description
For any index type $\iota$ with an asymmetric relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with an antisymmetric relation $s_i$, the lexicographical order $\text{Lex}(r, s)$ on the dependent sum type $\Sigma i, \alpha_i$ is antisymmetric.
Sigma.instIsTotalLexOfIsTrichotomous instance
[IsTrichotomous ι r] [∀ i, IsTotal (α i) (s i)] : IsTotal _ (Lex r s)
Full source 
instance [IsTrichotomous ι r] [∀ i, IsTotal (α i) (s i)] : IsTotal _ (Lex r s) :=
  ⟨by
    rintro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (Lex.left _ _ hij)
    · obtain hab | hba := total_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Lex.right _ _ hba)
    · exact Or.inr (Lex.left _ _ hji)⟩
Totality of Lexicographic Order on Sigma Types with Trichotomous and Total Relations
Informal description
For any index type $\iota$ with a trichotomous relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with a total relation $s_i$, the lexicographical order $\text{Lex}(r, s)$ on the dependent sum type $\Sigma i, \alpha_i$ is total.
Sigma.instIsTrichotomousLex instance
[IsTrichotomous ι r] [∀ i, IsTrichotomous (α i) (s i)] : IsTrichotomous _ (Lex r s)
Full source 
instance [IsTrichotomous ι r] [∀ i, IsTrichotomous (α i) (s i)] : IsTrichotomous _ (Lex r s) :=
  ⟨by
    rintro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (Lex.left _ _ hij)
    · obtain hab | rfl | hba := trichotomous_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Or.inl rfl)
      · exact Or.inr (Or.inr <| Lex.right _ _ hba)
    · exact Or.inr (Or.inr <| Lex.left _ _ hji)⟩
Trichotomy of Lexicographic Order on Sigma Types
Informal description
For any index type $\iota$ with a trichotomous relation $r$ and for each $i \in \iota$ a type $\alpha_i$ with a trichotomous relation $s_i$, the lexicographical order $\text{Lex}(r, s)$ on the dependent sum type $\Sigma i, \alpha_i$ is trichotomous. This means that for any two elements $(i, a)$ and $(j, b)$, exactly one of the following holds: $(i, a)$ is lexicographically less than $(j, b)$, $(i, a) = (j, b)$, or $(j, b)$ is lexicographically less than $(i, a)$.
PSigma.lex_iff theorem
{a b : Σ' i, α i} : Lex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec a.2) b.2
Full source 
theorem lex_iff {a b : Σ' i, α i} :
    LexLex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec a.2) b.2 := by
  constructor
  · rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩
  · obtain ⟨i, a⟩ := a
    obtain ⟨j, b⟩ := b
    dsimp only
    rintro (h | ⟨rfl, h⟩)
    · exact Lex.left _ _ h
    · exact Lex.right _ h
Characterization of Lexicographic Order on Sigma Types
Informal description
For any two elements $a$ and $b$ in the sigma type $\Sigma' i, \alpha i$, the lexicographic order relation $\text{Lex}(r, s)$ holds between $a$ and $b$ if and only if either: 1. The first component of $a$ is related to the first component of $b$ under the relation $r$ (i.e., $r(a.1, b.1)$ holds), or 2. The first components are equal (i.e., $a.1 = b.1$) and the second component of $a$ (transported along this equality) is related to the second component of $b$ under the relation $s$ for the index $b.1$ (i.e., $s(b.1, \text{transport}(a.2), b.2)$ holds).
PSigma.Lex.decidable instance
(r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) [DecidableEq ι] [DecidableRel r] [∀ i, DecidableRel (s i)] : DecidableRel (Lex r s)
Full source 
instance Lex.decidable (r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) [DecidableEq ι]
    [DecidableRel r] [∀ i, DecidableRel (s i)] : DecidableRel (Lex r s) := fun _ _ =>
  decidable_of_decidable_of_iff lex_iff.symm
Decidability of Lexicographic Order on Sigma Types
Informal description
Given a type `ι` with a decidable equality and a decidable relation `r`, and for each `i : ι`, a type `α i` with a decidable relation `s i`, the lexicographic order on the sigma type `Σ' i, α i` is decidable.
PSigma.Lex.mono theorem
{r₁ r₂ : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop} (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ' i, α i} (h : Lex r₁ s₁ a b) : Lex r₂ s₂ a b
Full source 
theorem Lex.mono {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop}
    (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ' i, α i}
    (h : Lex r₁ s₁ a b) : Lex r₂ s₂ a b := by
  obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
  · exact Lex.left _ _ (hr _ _ hij)
  · exact Lex.right _ (hs _ _ _ hab)
Monotonicity of Lexicographic Order on Sigma Types
Informal description
Let $ι$ be a type, and for each $i \in ι$, let $α_i$ be a type. Given two relations $r_1, r_2$ on $ι$ and for each $i \in ι$, two relations $s_1(i), s_2(i)$ on $α_i$, suppose that: 1. For all $a, b \in ι$, if $r_1(a, b)$ holds, then $r_2(a, b)$ holds. 2. For all $i \in ι$ and $a, b \in α_i$, if $s_1(i)(a, b)$ holds, then $s_2(i)(a, b)$ holds. Then for any two elements $(i, x), (j, y)$ in the sigma type $\Sigma' i, α_i$, if $(i, x)$ is lexicographically less than $(j, y)$ with respect to $r_1$ and $s_1$, then $(i, x)$ is also lexicographically less than $(j, y)$ with respect to $r_2$ and $s_2$.
PSigma.Lex.mono_left theorem
{r₁ r₂ : ι → ι → Prop} {s : ∀ i, α i → α i → Prop} (hr : ∀ a b, r₁ a b → r₂ a b) {a b : Σ' i, α i} (h : Lex r₁ s a b) : Lex r₂ s a b
Full source 
theorem Lex.mono_left {r₁ r₂ : ι → ι → Prop} {s : ∀ i, α i → α i → Prop}
    (hr : ∀ a b, r₁ a b → r₂ a b) {a b : Σ' i, α i} (h : Lex r₁ s a b) : Lex r₂ s a b :=
  h.mono hr fun _ _ _ => id
Monotonicity of Lexicographic Order in the Index Relation
Informal description
Let $ι$ be a type, and for each $i \in ι$, let $α_i$ be a type. Given two relations $r_1$ and $r_2$ on $ι$ and for each $i \in ι$, a relation $s(i)$ on $α_i$, suppose that for all $a, b \in ι$, if $r_1(a, b)$ holds, then $r_2(a, b)$ holds. Then for any two elements $(i, x), (j, y)$ in the sigma type $\Sigma' i, α_i$, if $(i, x)$ is lexicographically less than $(j, y)$ with respect to $r_1$ and $s$, then $(i, x)$ is also lexicographically less than $(j, y)$ with respect to $r_2$ and $s$.
PSigma.Lex.mono_right theorem
{r : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop} (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ' i, α i} (h : Lex r s₁ a b) : Lex r s₂ a b
Full source 
theorem Lex.mono_right {r : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop}
    (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ' i, α i} (h : Lex r s₁ a b) : Lex r s₂ a b :=
  h.mono (fun _ _ => id) hs
Monotonicity of Lexicographic Order on Sigma Types (Right Component)
Informal description
Let $ι$ be a type, and for each $i \in ι$, let $α_i$ be a type. Given a relation $r$ on $ι$ and for each $i \in ι$, two relations $s_1(i), s_2(i)$ on $α_i$, suppose that for all $i \in ι$ and $a, b \in α_i$, if $s_1(i)(a, b)$ holds, then $s_2(i)(a, b)$ holds. Then for any two elements $(i, x), (j, y)$ in the sigma type $\Sigma' i, α_i$, if $(i, x)$ is lexicographically less than $(j, y)$ with respect to $r$ and $s_1$, then $(i, x)$ is also lexicographically less than $(j, y)$ with respect to $r$ and $s_2$.