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: Dec 20 2023 at 11:08 UTC