Jakobs' order is the Dershowitz–Manna order

On a linear order, Mathlib's Dershowitz–Manna order on multisets (Multiset.IsDershowitzMannaLT) coincides with Jakobs' order "lexicographic from the largest element".

Main results

• isDershowitzMannaLT_iff_jakobsLT, jakobsLT_total, jakobsLT_add_right;
• wellFounded_min_jakobsLE: the WellFounded.min used in DGH.Basic is a minimum for Jakobs' order.

Related

The Dershowitz–Manna order and its well-foundedness are Mathlib's Multiset.IsDershowitzMannaLT and Multiset.wellFounded_isDershowitzMannaLT (Mathlib.Data.Multiset.DershowitzManna); this file adds its characterization, on a linear order, as the lexicographic order from the largest element.

References

• F. Jakobs, PhD thesis, 2019, Thm. 1.1.3; Dubrovin–Gräter–Hanke, Prop. 2.1.
• N. Dershowitz, Z. Manna, Proving termination with multiset orderings, Comm. ACM 22 (1979), 465–476.

def DGH.jakobsLT {α : Type u_1} [LinearOrder α] (s t : Multiset α) : Prop

Jakobs' order: s <_J t iff at some x the count in s is smaller than in t, and the counts agree at every y > x.

Equations

• DGH.jakobsLT s t = ∃ (x : α), Multiset.count x s < Multiset.count x t ∧ ∀ (y : α), x < y → Multiset.count y s = Multiset.count y t

def DGH.jakobsLE {α : Type u_1} [LinearOrder α] (s t : Multiset α) : Prop

Reflexive closure of jakobsLT.

Equations

• DGH.jakobsLE s t = (s = t ∨ DGH.jakobsLT s t)

theorem DGH.exists_max_count_ne {α : Type u_1} [LinearOrder α] {s t : Multiset α} (h : s ≠ t) : ∃ (m : α), Multiset.count m s ≠ Multiset.count m t ∧ ∀ (y : α), m < y → Multiset.count y s = Multiset.count y t

If s ≠ t, there is a largest element where the counts differ.

theorem DGH.max_notMem {α : Type u_1} [LinearOrder α] {Y Z : Multiset α} (hZ : Z.toFinset.Nonempty) (hYZ : ∀ y ∈ Y, ∃ z ∈ Z, y < z) : Z.toFinset.max' hZ ∉ Y

Helper: under the DM hypothesis on Y, Z, the maximum of Z is not in Y.

theorem DGH.jakobsLT_of_isDershowitzMannaLT {α : Type u_1} [LinearOrder α] {s t : Multiset α} (h : s.IsDershowitzMannaLT t) : jakobsLT s t

(1, ⇒) Dershowitz–Manna implies Jakobs.

theorem DGH.isDershowitzMannaLT_of_jakobsLT {α : Type u_1} [LinearOrder α] {s t : Multiset α} (h : jakobsLT s t) : s.IsDershowitzMannaLT t

(1, ⇐) Jakobs implies Dershowitz–Manna.

theorem DGH.isDershowitzMannaLT_iff_jakobsLT {α : Type u_1} [LinearOrder α] {s t : Multiset α} : s.IsDershowitzMannaLT t ↔ jakobsLT s t

(1) On a linear order, Dershowitz–Manna = Jakobs' lexicographic order.

theorem DGH.jakobsLT_total {α : Type u_1} [LinearOrder α] {s t : Multiset α} (h : s ≠ t) : jakobsLT s t ∨ jakobsLT t s

(2) Totality.

theorem DGH.jakobsLT_irrefl {α : Type u_1} [LinearOrder α] (s : Multiset α) : ¬jakobsLT s s

Irreflexivity.

theorem DGH.jakobsLT_add_right {α : Type u_1} [LinearOrder α] {s t : Multiset α} (u : Multiset α) (h : jakobsLT s t) : jakobsLT (s + u) (t + u)

(3) Translation invariance: s <_J t → s + u <_J t + u.

theorem DGH.wellFounded_min_jakobsLE {α : Type u_1} [LinearOrder α] [WellFoundedLT α] (S : Set (Multiset α)) (hS : S.Nonempty) {t : Multiset α} (ht : t ∈ S) : jakobsLE (⋯.min S hS) t

(4) Over a well-founded linear order, the Dershowitz–Manna WellFounded.min of a nonempty set S is ≤_J every element of S (a minimum, not merely minimal).