# Zulip Chat Archive

## Stream: new members

### Topic: Build a sequence (N → X) by strong induction

#### Ryan Lahfa (Mar 22 2020 at 20:07):

I'm trying to build a strictly increasing sequence of elements, by using some hypothesis on Inf/Sup:

def seq_strictly_increasing [linear_order X] [has_Inf X] {S: set X} (Hinf: set.infinite S) (Hinf: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)): ℕ → X | zero := Inf S | (nat.succ n) := Inf (S \ { x : X | ∃ k ≤ n, x = seq_strictly_increasing k})

But I'm getting the following error:

failed to prove recursive application is decreasing, well founded relation @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof) Possible solutions: - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs. - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions. The nested exception contains the failure state for the decreasing tactic. nested exception message: failed state: X : Type, _inst_5 : has_Inf X, S : set X, Hinf : infinite S, Hinf : ∀ (M : set X), M ⊆ S → set.nonempty M → Inf M ∈ M, seq_strictly_increasing : ℕ → X, n : ℕ, x : X, k : ℕ, H : k ≤ n ⊢ k < nat.succ n

Which I'm not sure how to solve, I guess I have to prove that the `k < nat.succ n`

, i.e. `k ≤ n`

, that's by H, but unsure how to do it?

Is there a general way to build objects (i.e. sequences, functions, etc.) by induction? I tried to read, re-read mathlib & its docs and the Lean reference, but found nothing except toy examples with naturals, fibonacci, etc.

#### Johan Commelin (Mar 22 2020 at 20:13):

Does https://github.com/leanprover-community/mathlib/pull/1952/files#diff-3cf2529e763503ec4f444b4a282b272eR30 help as an example?

#### Ryan Lahfa (Mar 22 2020 at 20:18):

It makes a lot clearer, @Johan Commelin!

#### Ryan Lahfa (Mar 22 2020 at 20:21):

So now, I'm reduced to:

def increasing_seq [linear_order X] [has_Inf X] {S: set X} (Hinf: set.infinite S) (Hinf: ∀ M ⊆ S, M.nonempty → (Inf M ∈ M)): ℕ → X := well_founded.fix nat.lt_wf (λ n increasing_seq, Inf (S \ { x : X | ∃ k < n, x = increasing_seq k (by admit)})

So instead of `by admit`

, I should use the fact that some hypothesis `H: k < n`

is added to my context and give it to `increasing_seq`

, so I've done `begin, exact H, end`

, could I do something shorter?

#### Ryan Lahfa (Mar 22 2020 at 20:22):

`by assumption`

(but isn't this slow?)

#### Patrick Massot (Mar 22 2020 at 20:24):

`begin exact H end`

can always be replaced by `H`

.

#### Ryan Lahfa (Mar 22 2020 at 20:27):

Thank you @Patrick Massot ! Was not sure about it because it seemed like implicit hypothesis appearing out of nowhere

#### Patrick Massot (Mar 22 2020 at 20:35):

Oh, I didn't see `H`

was such a weird assumption. It comes from your `∃ k < n,`

. This is a really weird way to play here.

#### Patrick Massot (Mar 22 2020 at 20:37):

If you want to avoid relying on automatic names you can desugar the notation to `Inf (S \ { x : X | ∃ (k : ℕ) (Hyp : k < n), x = increasing_seq k Hyp })`

#### Patrick Massot (Mar 22 2020 at 20:37):

But I think `by assumption`

is fine here.

#### Patrick Massot (Mar 22 2020 at 20:38):

If it feels too long you can use Swiss quotes.

#### Patrick Massot (Mar 22 2020 at 20:38):

`Inf (S \ { x : X | ∃ k < n, x = increasing_seq k ‹_› })`

#### Mario Carneiro (Mar 22 2020 at 20:56):

should we change the shorthand for `\f<`

`\f>`

, now that the french are rejecting the "single french quotes"?

#### Patrick Massot (Mar 22 2020 at 20:57):

I'm not sure I can speak for all French people.

#### Ryan Lahfa (Mar 22 2020 at 21:03):

:D

#### Ryan Lahfa (Mar 22 2020 at 21:04):

Thank you for the desugared notation, anyway @Patrick Massot — makes a lot more sense to me now

Last updated: May 06 2021 at 20:13 UTC