## 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.

#### 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.

: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