## Stream: new members

### Topic: recursive function from fin

#### Angela Li (Dec 31 2020 at 16:49):

Hello! I am trying to write a function from fin (to make the goal position a rainbow in Fifteen). Here's a smaller MWE that's equivalent to my issue:

import tactic

def test : fin 37 → nat
| ⟨0,_⟩ := 37
| ⟨n+1,_⟩ := test ⟨n,by linarith⟩


Why does it have ⊢ 0 < 0 and not ⊢ n < n+1?
Thanks!

#### Kevin Buzzard (Dec 31 2020 at 16:52):

I am not an expert in this kind of thing but I suspect that you need to either use some custom recursor (which probably exists?) or you need to prove that what you're doing is well-founded, following the instructions at https://leanprover-community.github.io/extras/well_founded_recursion.html

#### Shing Tak Lam (Dec 31 2020 at 16:53):

following the instructions Kevin posted, something like this works

import tactic

def test : fin 37 → nat
| ⟨0, _⟩ := 37
| ⟨n+1,_⟩ := test ⟨n,by linarith⟩
using_well_founded {rel_tac := λ _ _, [exact ⟨_, measure_wf subtype.val⟩]}


#### Yakov Pechersky (Dec 31 2020 at 17:05):

In this particular case, you can define it like:

def test : fin 37 → nat :=
λ i, fin.induction_on i 37 (λ j x, x)


#### Yakov Pechersky (Dec 31 2020 at 17:05):

Which is a custom recursor that Kevin mentioned.

#### Kevin Buzzard (Dec 31 2020 at 17:05):

that should be called rec_on surely? If it can be used to construct data it's recursion not induction.

#### Mario Carneiro (Dec 31 2020 at 17:06):

or \lam i, 37 :D

#### Yakov Pechersky (Dec 31 2020 at 17:07):

Sure, but the recursor example shows how to access the recursing values

#### Eric Wieser (Dec 31 2020 at 17:16):

@Kevin Buzzard: It can't be called fin.rec_on, because that already exists as subtype.rec_on (I think)

Edit: No, it's just x.rec_on that finds subtype.rec_on

#### Mario Carneiro (Dec 31 2020 at 17:22):

If fin.rec_on existed x.rec_on would find it instead of subtype.rec_on`

#### Mario Carneiro (Dec 31 2020 at 17:23):

Plus dot notation doesn't work for recursors

#### Kevin Buzzard (Dec 31 2020 at 17:39):

oh yeah :-)

Last updated: May 15 2021 at 00:39 UTC