recursive function from fin

Stream: new members

[Angela Li]

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]

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]

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]

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]

Which is a custom recursor that Kevin mentioned.

[Kevin Buzzard]

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

[Mario Carneiro]

or \lam i, 37 :D

[Yakov Pechersky]

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

[Eric Wieser]

@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]

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

[Mario Carneiro]

Plus dot notation doesn't work for recursors

[Kevin Buzzard]

oh yeah :-)