instantiate existential with new inductive function

Stream: new members

[Paul Rowe]

I'm trying to formalize the proof that all terminating relations are normalizing (i.e. no infinite chains of a0 -> a1 -> ... implies every term has a normal form). The mathematician's by-hand proof is by contraposition which means I should be building an infinite chain of reductions anchored at a0 assuming a0 has no normal form. On paper this is easy: You start with a0, since it has no normal form it is reducible to some a1. Since a0 has no normal form, a1 must be reducible to some a2, and so on.

In the above proof, the necessary function from Nat to the domain of the relation is built inductively in tandem with the inductive argument that justifies the existence of each next step. I can't figure out how to do such a thing in Lean, or what else to do instead. I reach the following goal:

A : Type,
r : A → A → Prop,
a0 : A,
ha0 : ∀ (x : A), refl_trans_gen r a0 x → Exists (r x),
G0 : refl_trans_gen r a0 a0
⊢ ∃ (c : achain r a0), true

ha0 is the unfolding of the statement that a0 has no normal form. In Lean I can manually deduce the next step to find a suitable a1. And from there I could find a2, etc. But I don't know how to perform an induction to satisfy the existential with the necessary complete chain.

By the way, achain is a structure defined as follows, if it matters:

structure achain (r : A → A → Prop) (a : A) :=
(seq : ℕ → A)
(link : ∀ (n : ℕ), r (seq n) (seq (n+1)))
(start : seq 0 = a)

[Ruben Van de Velde]

If you can create a ∀ n: ℕ, ∃ a : A, ..., you can use choose to turn it into a function ℕ → A; does that help?

[Paul Rowe]

I don't know what to put in that ... My context has nothing referring to ℕ in it. I do indeed use choose in my attempt to make a single step though.

[Paul Rowe]

What I mean is, I can grow my context, without changing the goal, to get finite chains of any length. But I don't know how to turn that into something of the form ∀ n : ℕ, ∃ a : A, ... because that process doesn't manipulate natural numbers.

[Reid Barton]

You should be able to turn ha0 into something like \all (x : {x // refl_trans_gen r a0 x}), \exists (x' : {x // refl_trans_gen r a0 x}), r x.1 x'.1, use choose on it, and use that to define a sequence of {x // refl_trans_gen r a0 x} by induction

[Paul Rowe]

Update: First, apologies to Ruben. I spaced and said I used choose when I meant I used some which is very different. Second, I followed Reid's idea and I managed to get it to work! I suspect the need to manipulate ha0 into the form suggested means I should consider restructuring some earlier definitions. Instantiating the existential with a structure was also a pain, but largely because I'm not yet comfortable with the {x // ...} notation, and other definitions didn't play nicely enough.

Thanks all around for the help.

[Ruben Van de Velde]

No worries, glad you got it to work