Recursive definition

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I want to define a recursive function g from ℕ to a nonempty linear order type α in such a way that when given a F: Finset α (nonempty), you get for 0 its minimum and for n + 1 you get the minimum of F \ Finset.image g (Finset.Icc 0 n).

My idea is to do something like:

import Mathlib

variable {α: Type*} [Inhabited α] [LinearOrder α]

def Finset.SMC (F: Finset α) (nemp: F ≠ ∅) : ℕ → α
  | 0 => Finset.min' F (Finset.nonempty_iff_ne_empty.mpr nemp)
  | n + 1 => if h: (F \ Finset.image
    (Finset.SMC F nemp) (Finset.Icc 0 n)).Nonempty then
      Finset.min' (F \ Finset.image (Finset.SMC F nemp) (Finset.Icc 0 n)) h
    else default

But it doesn't work. Any ideas?

[Esteban Martínez Vañó]

By making this definition

def Finset.min'' (s: Finset α) := if h: s.Nonempty then Finset.min' s h else default

I can simplify to:

def Finset.SMC (F: Finset α) : ℕ → α
  | 0 => Finset.min'' F
  | n + 1 => Finset.min'' (F \ Finset.image (Finset.SMC F) (Finset.Icc 0 n))

But still doesn't work :/

[Johannes Tantow]

It is not a #mwe you need to add import Mathlib.
You currently need to compute Finset.SMC F nemp in order to compute Finset.SMC F nemp, which is circular. Why would this work on paper?

[Esteban Martínez Vañó]

Of course it works in paper, its simply the recursion theorem. You know the value of the function at 0 and supposing you now the value at all the values less than n you can work the value at n.

[Esteban Martínez Vañó]

It seem it works by defining: (THIS IS WRONG)

def Finset.SMC (F: Finset α) : ℕ → α
  | 0 => Finset.min'' F
  | n + 1 => Finset.min'' (F \ {Finset.SMC F n})

And at the end it should be the same function, but I still would like if is there a way to make the other definition work.

[Johannes Tantow]

In this way Lean definitely sees that n is getting smaller. I guess it needs to know that every argument that is used in in image is smaller than n. It is possible to do it by going a bit more basic:

import Mathlib

variable {α: Type*} [Inhabited α] [LinearOrder α]

def Finset.SMC (F: Finset α) (nemp: F ≠ ∅) (n: ℕ): α :=
  match n with
  | 0 => Finset.min' F (Finset.nonempty_iff_ne_empty.mpr nemp)
  | m + 1 =>
    let image := (Multiset.map (fun ⟨x, _h⟩ => Finset.SMC F nemp x) (Finset.Icc 0 m).attach.1).toFinset
    if h: (F \ image).Nonempty then
      Finset.min' (F \ image) h
    else default
termination_by n
decreasing_by
  simp at _h
  exact Nat.lt_add_one_of_le _h

[Johannes Tantow]

Now we see exactly that it is only called on smaller elements. For that I had to go to Multisets to use map to see more directly what happens.

[Esteban Martínez Vañó]

Okay, I think I get what you have done (although I didn't know that much about Lean) and why the error was ocurring in the first place.
Thank you so much!