Inductive definition using minimum of some subset of ℕ

Stream: mathlib4

[Tony Ma]

I want to define a sequence inductively, each term depending on the last and is defined as the minimum of some subset of ℕ. I found thatsInf seems not so convenient while using. How shall I simplify Nat.find ⋯ = 3 or should I use something other than sInf instead? (ℕ is well-ordered. Could I utilize this fact?)

import Mathlib

noncomputable def A : ℕ → ℕ
| 0 => 2
| n + 1 => sInf {x | x > A n ∧ Nat.Prime x}
decreasing_by
  apply Nat.lt_succ_self

example : A 1 = 3 := by
  have A0 : A 0 = 2 := by
    simp [A]
  simp [A, sInf]
  have h : ∃ x, x > A 0 ∧ Nat.Prime x := by
    use 3
    simp [A0]
    exact Nat.prime_three
  simp [dif_pos h]

  /-
  A0 : A 0 = 2
  h : ∃ x > A 0, Nat.Prime x
  ⊢ Nat.find ⋯ = 3
  -/

[Matt Diamond]

you might want to take a look at how docs#Nat.Subtype.ofNat does this using docs#Nat.Subtype.succ

[Matt Diamond]

(or just use Nat.Subtype.ofNat itself)

[Matt Diamond]

unless I'm misreading you and you're trying to do something more complex than just enumerating an infinite set (which is how I interpreted your example)

[Tony Ma]

The precise definition I wanted is

noncomputable def A : ℕ → ℕ
| 0 => 1
| n + 1 => sInf {x | x > A n ∧ ∀ i j k : Finset.Icc 0 n, A i + A j ≠ 3 * A k ∧ ∀ i j : Finset.Icc 0 n, A i + A j ≠ 3 * x ∧ ∀ i k :Finset.Icc 0 n, A i + x ≠ 3 * A k}

So, the next element depends on the previous.

[Tony Ma]

@Matt Diamond I guess inductive definition is required in my case.

[Matt Diamond]

Well, there's also docs#Nat.strongRecOn as another option... not sure what the pros or cons here would be

[Tony Ma]

Is there a way to simplify, if I still use sInf?

[Matt Diamond]

I'm not sure... btw it looks like one of your conditions (∀ i j k : Finset.Icc 0 n, A i + A j ≠ 3 * A k) doesn't mention x... is that a typo?

[Tony Ma]

Oh yes. I shall remove that.

[Tony Ma]

What is the way to use strongRecOn?

[Matt Diamond]

This isn't the best explanation, but:

You pass it two arguments, the first being the input and the second argument is the inductive step, which you define as a function like fun n IH => ...

Within that function, you're able to use IH to access previously defined values. The type of IH is (x : Nat) → x < n → motive x, so if you pass in some x along with a proof that x < n, you get back the value of A x (which is what motive x is).

[Tony Ma]

Sorry I think I might be not familiar with how to define something... Could you show me some example that uses strongRecOn in definitino?

[Matt Diamond]

honestly I think I'm leading you down the wrong path here... you should probably just stick with the inductive definition you were working with

[Tony Ma]

Ok. Nevermind and thx a lot. But maybe I could still use the inductive definition with sInf replaced by something better? Should I prove some lemma before or what could I do to avoid the complicated `Nat.find ... = 3

[Violeta Hernández]

What's the issue with using sInf?

[Violeta Hernández]

The natural numbers implement docs#ConditionallyCompleteLinearOrderBot which is a very specific typeclass that interfaces well with them

[Violeta Hernández]

There's even a few lemmas for well-ordered CCLOBs, such as docs#csInf_mem

[Violeta Hernández]

You should only really be using Nat.find if you care about computability. In fact, you can see in docs#Nat.instInfSet that sInf on naturals is defined in terms of Nat.find.