destructuring existentials in proofs

Stream: new members

[Jacob Weightman]

I'm working on a formalization of a string rewriting system, and some of the literature on the topic uses this "strong" notion of divergence — intuitively, string rewriting diverges on a string A if for any string length n, there is a "point of no return" i such that for any subsequent step the length is greater than n. That is, after i steps, we never get a short string.

def diverges (A : List α) : Prop :=
  ∀n : ℕ, ∃i : ℕ, ∀j > i, (T.next^[j] A).length > n

I'd like to prove that this "seemingly weaker" notion of divergence is equivalent — intuitively, if string rewriting diverges on A, then we always eventually get a longer string.

def diverges' (A : List α) : Prop :=
  ∀i : ℕ, ∃j : ℕ, j > i ∧ (T.next^[j] A).length > (T.next^[i] A).length

The T.diverges A → T.diverges' A part of the proof is easy, I have that formalized already. Formalizing the other direction is a bit trickier. I'm able to get up to this point with contraposition:

α : Type u
inst✝ : Inhabited α
T : TagSystem α
A : List α
n : ℕ
h : ∀ (i : ℕ), ∃ j, i < j ∧ (next^[j] A).length ≤ n
⊢ ∃ i, ∀ (j : ℕ), i < j → (next^[j] A).length ≤ (next^[i] A).length

Now the rest of the argument I'd like to make goes something like this: starting with h 0, there is a jthat gives us a string shorter than n. Proceed with h j to obtain another such j, and by repeating we can find infinitely many such js. However, there are less than #α^(n+1) strings shorter than n, so at that point we must have repeated a string which means we have either halted or gotten stuck in a loop. Let i be the last j if it halted, or look forward and find the largest string in that loop. All j > i have length less than or equal to n by construction.

The part of this that has me stumped is "by repeating we can find infinitely many such js." In the context of a proof, I can "extract" the value of an existential with e.g. let ⟨j, _⟩ := h 0, but I cannot do this in the context of a function because of proof irrelevance. How can I do this style of iteration in my proof?

[suhr]

You can try using this functions:

Classical.choose.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α
Classical.choose_spec.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (Classical.choose h)

[Kyle Miller]

There's a tactic choose j h' using h that will create a j function from h with a fixed set of cohices.

[Jacob Weightman]

the choose tactic was exactly what I was looking for, but I learned something useful from both of these answers. Thanks :blush: