Force extra condition with `choice`?

Stream: new members

[Jacob Weightman]

Currently studying a deterministic string rewriting system, and I want to prove that a rewriting system either halts, loops, or produces ever increasingly long strings. I have a "completed" proof, except for a small hole. The idea is that if the system doesn't diverge on a string, there must be a string that repeats since the length of strings is bounded. The problem is that the way I'm applying the axiom of choice and pigeonhole principle doesn't give me a way to prove that j i₁ ≠ j i₂. I wonder if there's a way to make a "better" choice without loss of generality, or maybe there's a way to use a different PHP theorem like Finite.exists_infinite_fiber to obtain the stronger condition I need. Perhaps one of the kind Lean experts here could point me in the right direction to fix my proof?

def ShortList (α : Type u) (n : ℕ) :=
  { l : List α // l.length ≤ n }

instance ShortList.finite {α : Type u}{n : ℕ} [Finite α] : Finite (ShortList α n) :=
  List.finite_length_le α n

theorem not_diverges'_halts_or_loops (A : List α)
    : ¬T.diverges' A → T.halts A ∨ T.loops A := by
  -- `T.diverges A := ∀n : ℕ, ∃i : ℕ, ∀j > i, (T.next^[j] A).length > n`
  -- so `¬T.diverges A ↔ ∃n : ℕ, ∀i : ℕ, ∃j > i, (T.next^[j] A).length ≤ n`
  intro h
  simp [diverges'] at h

  have h₁ : ∃i₁ i₂, i₁ ≠ i₂ ∧ T.next^[i₁] A = T.next^[i₂] A := by
    -- `h` says that there's some string length `n` such that after any number of steps `i`, we can
    -- find another number of steps `j > i` such that the length of the resulting string is less
    -- than `n`. Use the axiom of choice to obtain `j : ℕ → ℕ`, which gives the index of a
    -- subsequent short string from a previous one.
    choose n j h using h

    -- With this function j, we have an infinite sequence of indices of strings shorter than `n`, of
    -- which there are finitely many. By the pigeonhole principle, some string must repeat.
    let f : ℕ → ShortList α n := fun (i : ℕ) ↦
      let l := T.next^[j i] A
      have π : l.length ≤ n := (h i).right
      ⟨l, π⟩
    let h3 := Finite.exists_ne_map_eq_of_infinite f
    let ⟨A', h3'⟩ := Finite.exists_infinite_fiber f

    -- Let `i₁ i₂ : ℕ` such that `j i₁` and `j i₂` are indices which produce a repeated string.
    choose i₁ i₂ h3 using h3
    let ⟨h4, h5⟩ := h3; clear h3
    have h6 : T.next^[j i₁] A = T.next^[j i₂] A := by
      simp [f] at h5
      rw [← Subtype.val_inj] at h5
      assumption

    -- TODO: we have that i₁ ≠ i₂, but the current use of axiom of choice and pigeonhole principle
    -- doesn't guarantee j i₁ ≠ j i₂. It should be possible to force such a choice, but I'm not sure
    -- how to do this in Lean...
    have h7 : j i₁ ≠ j i₂ := by sorry

    exists j i₁
    exists j i₂

  clear h
  choose i₁ i₂ h₁ h₂ using h₁
  wlog h₃ : i₁ < i₂
  · simp at h₃; rw [ne_comm] at h₁; rw [eq_comm] at h₂
    apply this A i₂ i₁ h₁ h₂ (Nat.lt_of_le_of_ne h₃ h₁)

  -- At this point, we must have either halted or found a loop. We can tell these cases apart easily
  -- by checking if the length of the string is less than `T.v`.
  cases Nat.lt_or_ge (T.next^[i₁] A).length T.v with
  | inl h₄ => left; exists i₁
  | inr h₄ =>
      right
      exists i₁
      exists i₂ - i₁
      constructor
      · simp; assumption
      · have h₁' : i₁ ≤ i₂ := Nat.le_of_lt h₃
        constructor
        · simp; exact h₃
        · rw [← Function.iterate_add_apply, Nat.sub_add_cancel h₁', h₂]

[Matt Diamond]

Could you include the definition of T and any imports? It's easier for people to help when it's a #mwe

[Aaron Liu]

Could you use Finite.exists_ne_map_eq_of_infinite (f ∘ j) instead and then use that j is strictly monotone (therefore injective) to get that j i₁ ≠ j i₂?

[Aaron Liu]

You have a docs#Filter.extraction_of_frequently_atTop' statement. Extract a function that indexes your short strings, instead of having a function that finds the next one. This will make it easier to prove stuff, because the new function is injective.

[Jacob Weightman]

Thank you so much @Aaron Liu , docs#Filter.extraction_of_frequently_atTop' did exactly what I needed it to do!