Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC