# Zulip Chat Archive

## Stream: new members

### Topic: instantiate existential with new inductive function

#### Paul Rowe (Aug 01 2020 at 17:23):

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 (Aug 01 2020 at 17:28):

If you can create a `∀ n: ℕ, ∃ a : A, ...`

, you can use `choose`

to turn it into a function `ℕ → A`

; does that help?

#### Paul Rowe (Aug 01 2020 at 17:36):

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 (Aug 01 2020 at 17:48):

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 (Aug 01 2020 at 17:57):

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 (Aug 01 2020 at 22:22):

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 (Aug 01 2020 at 22:36):

No worries, glad you got it to work

Last updated: May 07 2021 at 00:30 UTC