Build a sequence (N → X) by strong induction

Stream: new members

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

It makes a lot clearer, @Johan Commelin!

[Ryan Lahfa]

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]

by assumption (but isn't this slow?)

[Patrick Massot]

begin exact H end can always be replaced by H.

[Ryan Lahfa]

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

[Patrick Massot]

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]

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]

But I think by assumption is fine here.

[Patrick Massot]

If it feels too long you can use Swiss quotes.

[Patrick Massot]

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

[Mario Carneiro]

should we change the shorthand for \f< \f>, now that the french are rejecting the "single french quotes"?

[Patrick Massot]

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

[Ryan Lahfa]

:D

[Ryan Lahfa]

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