Dershowitz-Manna ordering

In this file we define the Dershowitz-Manna ordering on multisets. Specifically, for two multisets M and N in a partial order (S, <), M is smaller than N in the Dershowitz-Manna ordering if M can be obtained from N by replacing one or more elements in N by some finite number of elements from S, each of which is smaller (in the underling ordering over S) than one of the replaced elements from N. We prove that, given a well-founded partial order on the underlying set, the Dershowitz-Manna ordering defined over multisets is also well-founded.

Main results

• Multiset.IsDershowitzMannaLT : the standard definition fo the Dershowitz-Manna ordering.
• Multiset.wellFounded_isDershowitzMannaLT : the main theorem about the Dershowitz-Manna ordering being well-founded.

References

• [Wikipedia, Dershowitz–Manna ordering*] (https://en.wikipedia.org/wiki/Dershowitz%E2%80%93Manna_ordering)

• CoLoR, a Coq library on rewriting theory and termination. Our code here is inspired by their formalization and the theorem is called mOrd_wf in the file MultisetList.v.

def Multiset.IsDershowitzMannaLT {α : Type u_1} [Preorder α] (M N : Multiset α) : Prop

The standard Dershowitz–Manna ordering.

Equations

• M.IsDershowitzMannaLT N = ∃ (X : Multiset α) (Y : Multiset α) (Z : Multiset α), Z ≠ ∅ ∧ M = X + Y ∧ N = X + Z ∧ ∀ y ∈ Y, ∃ z ∈ Z, y < z

theorem Multiset.IsDershowitzMannaLT.trans {α : Type u_1} [Preorder α] {M N P : Multiset α} : M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P

IsDershowitzMannaLT is transitive.

theorem Multiset.wellFounded_isDershowitzMannaLT {α : Type u_1} [Preorder α] [WellFoundedLT α] : WellFounded Multiset.IsDershowitzMannaLT

Over a well-founded order, the Dershowitz-Manna order on multisets is well-founded.

instance Multiset.instWellFoundedisDershowitzMannaLT {α : Type u_1} [Preorder α] [WellFoundedLT α] : WellFoundedRelation (Multiset α)

Equations

• Multiset.instWellFoundedisDershowitzMannaLT = { rel := Multiset.IsDershowitzMannaLT, wf := ⋯ }