## Stream: new members

### Topic: Inductive definition with many base cases

#### Anatole Dedecker (Aug 13 2020 at 12:52):

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 (Aug 13 2020 at 13:09):

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

#### Yakov Pechersky (Aug 13 2020 at 13:15):

(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 (Aug 13 2020 at 13:19):

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 (Aug 13 2020 at 13:25):

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

#### Kevin Buzzard (Aug 13 2020 at 13:26):

that doesn't answer the question though

#### Kevin Buzzard (Aug 13 2020 at 13:28):

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 (Aug 13 2020 at 13:31):

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 (Aug 13 2020 at 13:32):

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 (Aug 13 2020 at 13:45):

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

#### Anatole Dedecker (Aug 13 2020 at 13:46):

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

#### Mario Carneiro (Aug 13 2020 at 13:47):

You can define this by well founded recursion too

#### Mario Carneiro (Aug 13 2020 at 13:56):

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 (Aug 13 2020 at 13:57):

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 (Aug 13 2020 at 13:58):

you misspelt omega

#### Anatole Dedecker (Aug 13 2020 at 13:59):

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 (Aug 13 2020 at 14:01):

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)


(deleted)

#### Kevin Buzzard (Aug 13 2020 at 14:02):

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

#### Kevin Buzzard (Aug 13 2020 at 14:03):

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

#### Kevin Buzzard (Aug 13 2020 at 14:03):

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 (Aug 13 2020 at 14:04):

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 (Aug 13 2020 at 14:05):

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

#### Mario Carneiro (Aug 13 2020 at 14:06):

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 (Aug 13 2020 at 14:07):

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 (Aug 13 2020 at 14:08):

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 (Aug 13 2020 at 14:08):

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

#### Anatole Dedecker (Aug 13 2020 at 14:09):

Oooooh that's clever too. Thanks to everyone !

you misspelt 37

#### Patrick Massot (Aug 13 2020 at 20:45):

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 (Aug 13 2020 at 21:25):

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

#### Patrick Massot (Aug 13 2020 at 21:25):

Of course rewriting it would be even better!

#### Mario Carneiro (Aug 13 2020 at 21:25):

it obviously fills an important use case

#### Patrick Massot (Aug 13 2020 at 21:26):

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

#### Mario Carneiro (Aug 13 2020 at 21:26):

avoiding it also requires time and skills though

#### Patrick Massot (Aug 13 2020 at 21:29):

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

Last updated: May 11 2021 at 12:15 UTC