inductive Thesis.MultisetExt1 {α : Type u_1} (r : Rel α α) : Multiset α → Multiset α → Prop

We define a multiset extension of a relation r, which is generally expected to be a strict order. The idea behind the extension is that a multiset is "one-step" smaller than another if it is obtained by replacing an element in the larger multiset by any amount of smaller (by r) elements.

MultisetExt1 defines the "one-step" relation. The full extension is formed by taking the transitive closure over MultisetExt1.

• rel: ∀ {α : Type u_1} {r : Rel α α} (M M' : Multiset α) (s : α), (∀ m ∈ M', r m s) → Thesis.MultisetExt1 r (M + M') (s ::ₘ M)

@[reducible, inline]

abbrev Thesis.MultisetExt {α : Type u_1} (r : Rel α α) : Rel (Multiset α) (Multiset α)

Equations

• Thesis.MultisetExt r = (Thesis.MultisetExt1 r)⁺

inductive Thesis.MSESeq {α : Type u_1} (r : Rel α α) : List (Multiset α) → Multiset α → Multiset α → Prop

MSESeq r l M N represents a sequence of smaller-than steps between M and N, with all intermediate steps in l. This is isomorphic to MultisetExt; see MSESeq.iff_multiset_ext.

• single: ∀ {α : Type u_1} {r : Rel α α} {M N : Multiset α}, Thesis.MultisetExt1 r M N → Thesis.MSESeq r [M, N] M N
• step: ∀ {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N O : Multiset α}, Thesis.MultisetExt1 r M N → Thesis.MSESeq r l N O → Thesis.MSESeq r (M :: l) M O

theorem Thesis.MSESeq.l_nonempty {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} (h : Thesis.MSESeq r l M N) : l.length > 0

theorem Thesis.MSESeq.l_expand {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} (h : Thesis.MSESeq r l M N) : ∃ (l' : List (Multiset α)), l = M :: l'

theorem Thesis.MSESeq.iff_multiset_ext {α : Type u_1} {r : Rel α α} {M N : Multiset α} : Thesis.MultisetExt r M N ↔ ∃ (l : List (Multiset α)), Thesis.MSESeq r l M N

There is a sequence of MSE1 steps iff MultisetExt r M N holds.

def Thesis.MSESeq.get_step {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} (hseq : Thesis.MSESeq r l M N) (n : ℕ) (hlen : n < l.length - 1) : Thesis.MultisetExt1 r l[n] l[n + 1]

Every index in l represents a step l[n] <# l[n+1].

Equations

• ⋯ = ⋯

def Thesis.never_increased_elem {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} (hseq : Thesis.MSESeq r l M N) (x : α) : Prop

An element has never increased if for all steps M <# N, the count of x is no higher in M than in N

Equations

• Thesis.never_increased_elem hseq x = ∀ (n : ℕ) (hlen : n < l.length - 1), Multiset.count x l[n] ≤ Multiset.count x l[n + 1]

def Thesis.decreased_elem1 {α : Type u_1} (M N : Multiset α) (m : α) : Prop

An element has decreased in a step if the count in M is one less than the count in N.

Equations

• Thesis.decreased_elem1 M N m = (Multiset.count m M + 1 = Multiset.count m N)

def Thesis.decreased_elem {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} (hseq : Thesis.MSESeq r l M N) (x : α) : Prop

An element has decreased if there is some step M <# N in which it has decreased.

Equations

• Thesis.decreased_elem hseq x = ∃ (n : ℕ) (h : n < l.length - 1), Thesis.decreased_elem1 l[n] l[n + 1] x

theorem Thesis.never_increased_elem.overall {α : Type u_1} {l : List (Multiset α)} {M N : Multiset α} {r : Rel α α} (hseq : Thesis.MSESeq r l M N) (x : α) (hni : Thesis.never_increased_elem hseq x) : Multiset.count x M ≤ Multiset.count x N

If an element has never increased, in particular the count at the end is no larger than at the start.

theorem Thesis.decreased_elem1.is_s {α : Type u_1} {M M' : Multiset α} {s m : α} (hde : Thesis.decreased_elem1 (M + M') (s ::ₘ M) m) : m = s

If an element has decreased between (M + M') and (M + {s}), it must be s.

theorem Thesis.decreased_elem1.unique {α : Type u_1} {r : Rel α α} {M N : Multiset α} {m : α} (h : Thesis.MultisetExt1 r M N) (hde : Thesis.decreased_elem1 M N m) (k : α) : Thesis.decreased_elem1 M N k → k = m

Two elements that have decreased in a single step must be equal, i.e. a one-step decreased element is unique.

def Thesis.is_largest_decreased_elem {α : Type u_1} {l : List (Multiset α)} {M N : Multiset α} {r : Rel α α} (hseq : Thesis.MSESeq r l M N) (m : α) : Prop

An element is the largest decreased element (LDE) if it has decreased, and no decreased element is larger than it.

Equations

• Thesis.is_largest_decreased_elem hseq m = (Thesis.decreased_elem hseq m ∧ ∀ (m' : α), Thesis.decreased_elem hseq m' → ¬r m m')

theorem Thesis.is_largest_decreased_elem.cons_larger {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N O : Multiset α} {m m' : α} (hseq : Thesis.MSESeq r l N O) (hlde : Thesis.is_largest_decreased_elem hseq m) (h : Thesis.MultisetExt1 r M N) (hde : Thesis.decreased_elem1 M N m') (hlt : ¬r m m') : Thesis.is_largest_decreased_elem ⋯ m

Extending a MSESeq with a step that has a larger decreased elem makes that element the sequence's LDE.

theorem Thesis.MultisetExt1.nonempty {α : Type u_1} {r : Rel α α} {M N : Multiset α} (h : Thesis.MultisetExt1 r M N) : N ≠ 0

theorem Thesis.MultisetExt.erase_multiple {α : Type u_1} {r : Rel α α} {M N : Multiset α} (K : Multiset α) (hm : M + K = N) (hk : K ≠ 0) : Thesis.MultisetExt r M N

theorem Thesis.is_largest_decreased_elem.cons_smaller {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N O : Multiset α} {m m' : α} [sor : IsStrictOrder α r] (hseq : Thesis.MSESeq r l N O) (hlde : Thesis.is_largest_decreased_elem hseq m) (h : Thesis.MultisetExt1 r M N) (hde : Thesis.decreased_elem1 M N m') (hlt : r m m') : Thesis.is_largest_decreased_elem ⋯ m'

Extending a MSESeq with a step that has a smaller decreased elem doesn't change the sequence's LDE.

theorem Thesis.MultisetExt1.has_dec_elem {α : Type u_1} {r : Rel α α} {M N : Multiset α} [sor : IsStrictOrder α r] (h : Thesis.MultisetExt1 r M N) : ∃ (m : α), Thesis.decreased_elem1 M N m

An element decreases in every step.

theorem Thesis.MultisetExt1.inc_req_dec {α : Type u_1} {r : Rel α α} {M N : Multiset α} [sor : IsStrictOrder α r] (h : Thesis.MultisetExt1 r M N) (m : α) : Multiset.count m M > Multiset.count m N → ∃ (n : α), r m n ∧ Thesis.decreased_elem1 M N n

If an element increases in a step, a larger element must decrease.

theorem Thesis.MSESeq.has_largest_decreased_elem {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} [sor : IsStrictOrder α r] (hseq : Thesis.MSESeq r l M N) : ∃ (m : α), Thesis.is_largest_decreased_elem hseq m

A sequence always has a largest decreased element.

theorem Thesis.MSESeq.largest_decreased_elem_never_increased {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} [sor : IsStrictOrder α r] (hseq : Thesis.MSESeq r l M N) (m : α) : Thesis.is_largest_decreased_elem hseq m → Thesis.never_increased_elem hseq m

The largest decreased element has never increased; if it had, there must be a larger element which has decreased, yielding a contradiction.

theorem Thesis.MSESeq.largest_decreased_elem_has_lower_multiplicity {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M N : Multiset α} [sor : IsStrictOrder α r] (hseq : Thesis.MSESeq r l M N) (m : α) : Thesis.is_largest_decreased_elem hseq m → Multiset.count m M < Multiset.count m N

The largest decreased element has never increased, and therefore has lower multiplicity at the end of the sequence than at the beginning.

theorem Thesis.MSESeq.irrefl {α : Type u_1} {r : Rel α α} {l : List (Multiset α)} {M : Multiset α} [sor : IsStrictOrder α r] : ¬Thesis.MSESeq r l M M

MSESeq is irreflexive; this follows trivially from MSESeq.has_largest_decreased_elem and MSESeq.largest_decreased_elem_has_lower_multiplicity

instance Thesis.MultisetExt.strict_order {α : Type u_1} {r : Rel α α} [i : IsStrictOrder α r] : IsStrictOrder (Multiset α) (Thesis.MultisetExt r)

Equations

• ⋯ = ⋯

theorem Thesis.less_add {α : Type u_1} {r : Rel α α} {M M' N : Multiset α} {m : α} (h : Thesis.MultisetExt1 r N M) (hM : M = m ::ₘ M') : (∃ (M : Multiset α), Thesis.MultisetExt1 r M M' ∧ N = m ::ₘ M) ∨ ∃ (K : Multiset α), (∀ b ∈ K, r b m) ∧ N = M' + K

If N <¹# M, and M consists of a ::ₘ M0, then either

• some other element is deleted, so a appears in N
• a is deleted and replaced by a set of reducts K

theorem Thesis.all_accessible {α : Type u_1} {r : Rel α α} (hwf : WellFounded r) (M : Multiset α) : Acc (Thesis.MultisetExt1 r) M

instance Thesis.MultisetExt.wf {α : Type u_1} {r : Rel α α} [IsWellFounded α r] : IsWellFounded (Multiset α) (Thesis.MultisetExt r)

Equations

• ⋯ = ⋯