theorem Thesis.InfReductionSeq.trans_chain {α : Type u_1} {r : Rel α α} {a b : α} : r⁺ a b → ∃ (l : List α), l.getLast? = some b ∧ List.Chain r a l

A single transitive step r⁺ a b can be expanded to a list of reducts l, ending in b, such that List.Chain r a l.

noncomputable def Thesis.InfReductionSeq.trans_chain' {α : Type u_1} {r : Rel α α} {a b : α} : r⁺ a b → List α

trans_chain' chooses a list that has the properties given by trans_chain.

Equations

• Thesis.InfReductionSeq.trans_chain' h = Classical.choose ⋯

theorem Thesis.InfReductionSeq.trans_chain'.spec {α : Type u_1} {r : Rel α α} {a b : α} (h : r⁺ a b) : (Thesis.InfReductionSeq.trans_chain' h).getLast? = some b ∧ List.Chain r a (Thesis.InfReductionSeq.trans_chain' h)

The list returned by trans_chain' has the properties given by trans_chain.

theorem Thesis.InfReductionSeq.trans_chain'.nonempty {α : Type u_1} {r : Rel α α} {a b : α} {h : r⁺ a b} : Thesis.InfReductionSeq.trans_chain' h ≠ []

trans_chain' h is nonempty.

noncomputable def Thesis.InfReductionSeq.inf_trans_lists {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) : ℕ → List α

An infinite r⁺-reduction sequence can be turned into an infinite sequence of lists of reducts, as given by trans_chain'.

Equations

• Thesis.InfReductionSeq.inf_trans_lists f hf x = Thesis.InfReductionSeq.trans_chain' ⋯

theorem Thesis.InfReductionSeq.inf_trans_lists.nonempty {α : Type u_1} {r : Rel α α} {f : ℕ → α} {hf : Thesis.reduction_seq r⁺ ⊤ f} (n : ℕ) : Thesis.InfReductionSeq.inf_trans_lists f hf n ≠ []

Each of the lists in inf_trans_lists f hf is nonempty.

@[irreducible]

def Thesis.InfReductionSeq.aux {α : Type u_1} (l_seq : ℕ → List α) (hne : ∀ (n : ℕ), l_seq n ≠ []) (list_idx elem_idx : ℕ) : α

Starting at list no. list_idx, get the elem_idxth element, going to the next list if elem_idx ≥ (l_seq list_idx).length.

This definition is largely due to Edward van de Meent on the Lean Zulip.

Equations

• One or more equations did not get rendered due to their size.

theorem Thesis.InfReductionSeq.aux_skip {α : Type u_1} (l_seq : ℕ → List α) (hne : ∀ (n : ℕ), l_seq n ≠ []) (m k : ℕ) : ∃ (n : ℕ), Thesis.InfReductionSeq.aux l_seq hne m (k + n) = Thesis.InfReductionSeq.aux l_seq hne (m + 1) k

If x := aux l_seq hne (m + 1) k, i.e. the kth element starting from list m + 1, we can get the same element starting from the previous list m by adding some n, which is the length of list m.

theorem Thesis.InfReductionSeq.aux_skip_i {α : Type u_1} (l_seq : ℕ → List α) (hne : ∀ (n : ℕ), l_seq n ≠ []) (i m k : ℕ) : ∃ (n : ℕ), Thesis.InfReductionSeq.aux l_seq hne m (k + n) = Thesis.InfReductionSeq.aux l_seq hne (m + i) k

An extension of aux_skip; we can get the kth element starting from list m + i by starting from list m and getting the k + nth element, where n is the sum of the lengths of the intermediate lists.

theorem Thesis.InfReductionSeq.aux_elem' {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) (n : ℕ) (hn : n > 0) : let ls := Thesis.InfReductionSeq.inf_trans_lists f hf; f n = Thesis.InfReductionSeq.aux ls ⋯ (n - 1) ((ls (n - 1)).length - 1)

If f is an infinite transitive reduction sequence, each element > 0 appears as the last element of the n - 1th list in the sequence generated by aux ....

theorem Thesis.InfReductionSeq.aux_elem {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) (n : ℕ) (hn : n > 0) : ∃ (n' : ℕ), f n = Thesis.InfReductionSeq.aux (Thesis.InfReductionSeq.inf_trans_lists f hf) ⋯ 0 n'

By aux_skip_i, aux_elem' can be modified to prove each element of f is reachable from the first list. Given that aux _ _ 0 is the basis of our eventual sequence, this essentially proves that all elements in f (except f 0) appear in the expanded sequence.

theorem Thesis.InfReductionSeq.aux_inf_reduction_seq {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) : Thesis.reduction_seq r ⊤ (Thesis.InfReductionSeq.aux (Thesis.InfReductionSeq.inf_trans_lists f hf) ⋯ 0)

noncomputable def Thesis.InfReductionSeq.seq {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) : ℕ → α

We form our expanded sequence by starting with f 0, and then continuing with all reducts of f 0 in the infinite transitive sequence, as generated by aux.

Equations

• Thesis.InfReductionSeq.seq f hf 0 = f 0
• Thesis.InfReductionSeq.seq f hf n.succ = Thesis.InfReductionSeq.aux (Thesis.InfReductionSeq.inf_trans_lists f hf) ⋯ 0 n

theorem Thesis.InfReductionSeq.seq_contains_elems {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) (n : ℕ) : ∃ (m : ℕ), f n = Thesis.InfReductionSeq.seq f hf m

seq contains all elements of the infinite transitive sequence.

theorem Thesis.InfReductionSeq.seq_inf_reduction_seq {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) : Thesis.reduction_seq r ⊤ (Thesis.InfReductionSeq.seq f hf)

seq f hf forms an infinite r-reduction sequence.

theorem Thesis.InfReductionSeq.exists_regular_of_trans {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r⁺ ⊤ f) : ∃ (f' : ℕ → α), Thesis.reduction_seq r ⊤ f' ∧ (∀ (n : ℕ), ∃ (m : ℕ), f n = f' m) ∧ f 0 = f' 0

Any infinite r⁺-reduction sequence has a corresponding infinite r-reduction sequence, which contains all of the elements of the transitive sequence and starts with the same element.

def Thesis.reduction_seq.degenerate {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hseq : Thesis.reduction_seq r ⊤ f) : Prop

We call an infinite reduction sequence degenerate if, from some point onwards, it only contains steps from one element to itself.

Equations

• hseq.degenerate = ∃ (n : ℕ), ∀ m ≥ n, f m = f (m + 1)

def Thesis.InfReductionSeq.transitive_step_guarantee {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hseq : Thesis.reduction_seq r ⊤ f) : Prop

Equations

• Thesis.InfReductionSeq.transitive_step_guarantee hseq = ∀ (n : ℕ), ∃ m ≥ n, f m ≠ f (m + 1) ∧ ∀ m' ∈ Set.Icc n m, f n = f m'

theorem Thesis.InfReductionSeq.tsg_of_not_degenerate {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hseq : Thesis.reduction_seq r ⊤ f) (hndeg : ¬hseq.degenerate) : Thesis.InfReductionSeq.transitive_step_guarantee hseq

noncomputable def Thesis.InfReductionSeq.trans_idx_step {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (n : ℕ) : ℕ

From some index n we step to a next index choose (htsg n) + 1, which is the end of a transitive step.

Equations

• Thesis.InfReductionSeq.trans_idx_step hf htsg n = Classical.choose ⋯ + 1

noncomputable def Thesis.InfReductionSeq.trans_idxs {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (n : ℕ) : ℕ

By iterating trans_idx_step, we can generate a sequence of indices into f which represent all transitive steps in f.

Equations

• Thesis.InfReductionSeq.trans_idxs hf htsg n = (Thesis.InfReductionSeq.trans_idx_step hf htsg)^[n] 0

noncomputable def Thesis.InfReductionSeq.trans_seq {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (n : ℕ) : α

We form the sequence by getting the element at each index given by trans_idxs

Equations

• Thesis.InfReductionSeq.trans_seq hf htsg n = f (Thesis.InfReductionSeq.trans_idxs hf htsg n)

theorem Thesis.InfReductionSeq.trans_idx_step_inc {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (k : ℕ) : k < Thesis.InfReductionSeq.trans_idx_step hf htsg k

Taking a step from index k yields an index greater than k.

theorem Thesis.InfReductionSeq.trans_idxs_inc {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (k : ℕ) : Thesis.InfReductionSeq.trans_idxs hf htsg k < Thesis.InfReductionSeq.trans_idxs hf htsg (k + 1)

Doing an extra iteration of trans_idx_step yields a larger index.

theorem Thesis.InfReductionSeq.trans_idxs_tends_to_infty {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (n : ℕ) : ∃ (k : ℕ), n < Thesis.InfReductionSeq.trans_idxs hf htsg k

For all n, there is an element of trans_idxs that is larger than n.

theorem Thesis.InfReductionSeq.trans_idxs_inbetween {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (k n : ℕ) : n ∈ Set.Ico (Thesis.InfReductionSeq.trans_idxs hf htsg k) (Thesis.InfReductionSeq.trans_idxs hf htsg (k + 1)) → f (Thesis.InfReductionSeq.trans_idxs hf htsg k) = f n

If n is inbetween trans_idxs f hgs k and trans_idxs f hgs (k + 1), then f n must be equal to f (trans_idxs f hgs k). Hence f n is an element of trans_seq f hgs.

theorem Thesis.InfReductionSeq.trans_idxs_sandwich {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (n : ℕ) : ∃ (k : ℕ), n ∈ Set.Ico (Thesis.InfReductionSeq.trans_idxs hf htsg k) (Thesis.InfReductionSeq.trans_idxs hf htsg (k + 1))

All n are sandwiched by two subsequent elements in trans_idxs f hgs. Combining this lemma with trans_idxs_inbetween above yields the proof that trans_seq f hgs contains all elements of f.

theorem Thesis.InfReductionSeq.trans_seq_inf_reduction_seq {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) : Thesis.reduction_seq r⁺ ⊤ (Thesis.InfReductionSeq.trans_seq hf htsg)

trans_seq f hgs is an infinite r⁺-reduction sequence.

theorem Thesis.InfReductionSeq.trans_seq_contains_elems {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (htsg : Thesis.InfReductionSeq.transitive_step_guarantee hf) (n : ℕ) : ∃ (m : ℕ), Thesis.InfReductionSeq.trans_seq hf htsg m = f n

trans_seq f hgs contains all elements of f.

theorem Thesis.InfReductionSeq.exists_inf_regular_seq_of_not_degenerate {α : Type u_1} {r : Rel α α} {f : ℕ → α} (hf : Thesis.reduction_seq r∗ ⊤ f) (hnd : ¬hf.degenerate) : ∃ (f' : ℕ → α), Thesis.reduction_seq r ⊤ f' ∧ (∀ (n : ℕ), ∃ (m : ℕ), f n = f' m) ∧ f 0 = f' 0

If hf is not degenerate, there must be an infinite r-reduction sequence which contains all elements of f and starts with f 0.

This lemma first translates hf to an infinite r⁺-reduction sequence, and then uses the techniques for transitive reduction sequences developed above.

theorem Thesis.InfReductionSeq.finite_of_degenerate {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r∗ ⊤ f) (hdg : hf.degenerate) : ∃ (N : ℕ) (f' : ℕ → α), Thesis.reduction_seq r∗ (↑N) f' ∧ (∀ (n : ℕ), ∃ m ≤ N, f' m = f n) ∧ f' 0 = f 0

If the infinite r∗-reduction sequence is degenerate, there must be some finite r∗-reduction sequence which contains all of the elements of the infinite r∗-reduction sequence, and starts with the same element.

theorem Thesis.InfReductionSeq.finite_seq_flatten {α : Type u_1} {r : Rel α α} (N : ℕ) (f : ℕ → α) (hrs : Thesis.reduction_seq r∗ (↑N) f) : ∃ (N' : ℕ) (f' : ℕ → α), Thesis.reduction_seq r (↑N') f' ∧ f' 0 = f 0 ∧ ∀ n ≤ N, ∃ m < N' + 1, f' m = f n

We can flatten a finite r∗-reduction sequence, by round-tripping through the inductive ReductionSeq definition.

theorem Thesis.InfReductionSeq.regular_seq_of_rt_seq {α : Type u_1} {r : Rel α α} (f : ℕ → α) (hf : Thesis.reduction_seq r∗ ⊤ f) : ∃ (N : ℕ∞) (f' : ℕ → α), Thesis.reduction_seq r N f' ∧ (∀ (n : ℕ), ∃ (m : ℕ) (_ : ↑m < N + 1), f n = f' m) ∧ f 0 = f' 0

A statement that is "obvious" when written down in a pen-and-paper proof, but which is non-trivial to formalize:

If we have an infinite r∗-reduction sequence a₀ ->* a₁ ->* a₂ ... there must be some (finite or infinite) reduction sequence a₀ -> ... -> a₁ -> ... -> a₂ -> ...