Zulip Chat Archive

Stream: new members

Topic: Inductive definition with many base cases


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 13:26):

that doesn't answer the question though

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Anatole Dedecker (Aug 13 2020 at 13:46):

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

view this post on Zulip Mario Carneiro (Aug 13 2020 at 13:47):

You can define this by well founded recursion too

view this post on Zulip 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)]

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 13:58):

you misspelt omega

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:01):

(deleted)

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:02):

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

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:03):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Aug 13 2020 at 14:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Aug 13 2020 at 14:09):

Oooooh that's clever too. Thanks to everyone !

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:16):

you misspelt 37

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:25):

Of course rewriting it would be even better!

view this post on Zulip Mario Carneiro (Aug 13 2020 at 21:25):

it obviously fills an important use case

view this post on Zulip Patrick Massot (Aug 13 2020 at 21:26):

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

view this post on Zulip Mario Carneiro (Aug 13 2020 at 21:26):

avoiding it also requires time and skills though

view this post on Zulip 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