Inductive definition with many base cases

Stream: new members

[Anatole Dedecker]

Is it possible to make a inductive definition with arbitrarily many "base cases" ? I'm trying to define the constant recursive sequence of order d : ℕ with coefficients c : fin d → α and whose first d terms are given by i : fin d → α but I can't find how to do this since

[Mario Carneiro]

I don't really understand the problem statement, but yes it is possible to formulate recursions like this

[Yakov Pechersky]

(not at computer keyboard atm), but for a proof of that definition later, something like obtain d, hd from d, then rcases d with _|_|_|d for four base cases, then induction d for the rest

[Anatole Dedecker]

Oh sorry if that wasn't clear, let me make a more concrete example : let's say I want to define superfib (d : ℕ) : ℕ → ℕ such that ∀ i : fin d, superfib d i = i and ∀ n,superfib d (n+d) = ∑ i in range d, superfib d (n+i). I know how to define superfib 2 or superfib 37 by making as much base constructors as I need and then the recursive one. But how can I define superfib d for any d since I can't write d constructors for every d

[Yakov Pechersky]

I'd use the proposition that i < d instead of relying on the fin to nat coercion

[Kevin Buzzard]

that doesn't answer the question though

[Kevin Buzzard]

I guess you define an auxiliary function first sending i to [superfib i, superfib (i+1), ..., superfib (i + d - 1)] by usual recursion

[Kevin Buzzard]

import tactic

def superfib_aux (d) : ℕ → fin d → ℕ
| 0 := λ x, x.1
| (n + 1) := λ x, if h : x.1 < d - 1 then superfib_aux n ⟨x.1 + 1, by omega⟩ else Σ i in fin d, superfib_aux n i

[Kevin Buzzard]

I don't know how that Sigma notation works, I've never used it before -- this doesn't compile but should be fixable easily

[Anatole Dedecker]

Ok so this works and looks incredibly clever, now I just need to understand what is going on :sweat_smile:

[Anatole Dedecker]

Btw, the fix is : ∑ i : fin d (the big sigma is \sum)

[Mario Carneiro]

You can define this by well founded recursion too

[Mario Carneiro]

import algebra.big_operators data.fintype.basic

open_locale big_operators

def superfib (d) : ℕ → ℕ
| n := if h : n < d then n else
  ∑ i : fin d,
    have n - d + i < n, from
      nat.add_lt_of_lt_sub_right $
        (nat.sub_lt_sub_left_iff $ le_of_not_gt h).2 i.2,
    superfib (n - d + i)

theorem superfib_lt_d {d n} (h : n < d) :
  superfib d n = n := by rw [superfib, if_pos h]
theorem superfib_sum {d n} (h : d ≤ n) :
  superfib d n = ∑ (i : fin d), superfib d (n - d + ↑i) :=
by rw [superfib, if_neg (not_lt_of_ge h)]

[Mario Carneiro]

you have to supply a proof of decreasing in the middle of the definition but as you can see from the lemmas it doesn't appear there

[Kevin Buzzard]

you misspelt omega

[Anatole Dedecker]

Ok I think I just understood @Kevin Buzzard 's approach, it seems less mysterious now : it is basically like working on the vectors of d consecutive terms to go back to usual recursion.

[Mario Carneiro]

here I fixed the typo

def superfib (d) : ℕ → ℕ
| n := if h : n < d then n else
  ∑ i : fin d,
    have n - d + i.1 < n, by have := i.2; omega,
    superfib (n - d + i)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

I am annoyed that my version doesn't work for d=0 and yours does

[Kevin Buzzard]

def superfib' (d n : ℕ) (hd : d > 0) := superfib'_aux d n ⟨0, hd⟩

[Kevin Buzzard]

import algebra.big_operators data.fintype.basic
import tactic

open_locale big_operators

def superfib'_aux (d) : ℕ → fin d → ℕ
| 0 := λ x, x.1
| (n + 1) := λ x, if h : x.1 < d - 1 then superfib'_aux n ⟨x.1 + 1, by omega⟩ else ∑ i : fin d, superfib'_aux n i

def superfib' (d n : ℕ) (hd : d > 0) := superfib'_aux d n ⟨0, hd⟩

#eval superfib' 3 4 (dec_trivial) -- 6

[Anatole Dedecker]

You know what ? I'm dumb. I tried the exact same approach as Mario, except I didn't explicitly say i : fin d, so the type of i depended on the proof being present (nat) or not (fin d)

[Mario Carneiro]

no that's actually a really subtle part of the definition, I'm not surprised

[Mario Carneiro]

ideally we would be able to just sum over i in range d like you did but my approach requires that you be able to prove that the argument is well defined when it is used, which is often inconvenient

[Anatole Dedecker]

Oh yeah I posted range and tried fin later for this exact reason, but it didn't work anyway cause I'm relying too much on type inferencce

[Mario Carneiro]

here's another way to do it using only range:

def superfib (d) : ℕ → ℕ
| n := if n < d then n else ∑ i in finset.range d,
  if h : n - d + i < n then superfib (n - d + i) else 0

[Mario Carneiro]

This works to make the definition decreasing and punts on proving that the else 0 never happens until the equational theorem

[Anatole Dedecker]

Oooooh that's clever too. Thanks to everyone !

[Kevin Buzzard]

you misspelt 37

[Patrick Massot]

Kevin Buzzard said:

you misspelt omega

Kevin, we have a problem with omega. As you know, this tactic has some bugs and the author is no longer interested in maintaining it (or documenting it). Unless he suddenly comes back to it, we know for sure that omega won't survive the Lean4 migration. So we don't insist too much on using it more in mathlib.

[Mario Carneiro]

I wouldn't go that far. I think we should try to rewrite omega, not drop it

[Patrick Massot]

Of course rewriting it would be even better!

[Mario Carneiro]

it obviously fills an important use case

[Patrick Massot]

But that requires a lot of time and skills than avoiding to use it.

[Mario Carneiro]

avoiding it also requires time and skills though

[Patrick Massot]

It certainly needs a lot less skills, but it could need a lot more total time if we do it long enough.