timeout when #reduce-ing fin n function

Stream: new members

[Alex Reynaldi]

Hi, Whenever I try to #reduce a function defined recursively on fin n, I get a timeout. However using #eval works just fine. The minimal example is the factorial function in the documentation for fin.has_well_founded:

import data.fin

def factorial {n : ℕ} : fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩

#reduce factorial 2 --timeout
#eval @factorial 3 2 --works fine

Am I missing something or doing something wrong?

[Eric Rodriguez]

Kernel computation is slow :(

[Alex Reynaldi]

Is it really just that slow though? because even #reduce factorial 0 seems to timeout

[Yakov Pechersky]

It can't figure out which fin n you mean.

[Yakov Pechersky]

Because 2 is 0 in fin 0, 1, or 2

[Yakov Pechersky]

What happens if you say #reduce factorial (2 : fin 3)?

[Kevin Buzzard]

Can you make this a #mwe ? I just tried this and your code doesn't compile -- you're missing imports or opens or something (you can just edit the original message, no need to repost).

[Alex Reynaldi]

sorry about that, I just forgot to import data.fin

[Kevin Buzzard]

#reduce @factorial 1 0 -- 1
#reduce @factorial 2 0 -- 1

def one : fin 2 := ⟨1, dec_trivial⟩

#reduce factorial one -- nope

[Alex Reynaldi]

@Yakov Pechersky , #reduce factorial (2 : fin 3) also timeouts for me. I can reproduce what @Kevin Buzzard put up though.

[Alex Reynaldi]

#reduce @factorial 3 1 also timeouts on my end

[Gihan Marasingha]

I think the issue is with the code produced by the equation compiler, maybe something to do with the fact that has_well_founded is involved? Anyway, the following works fine.

import data.fin

def factorial {n : ℕ} : fin n → ℕ :=
λ fn, subtype.rec_on fn (λ m p, nat.rec_on m 1 (λ k ih, (k+1)*ih))

#reduce @factorial 3 1

#reduce factorial (5 : fin 6)

[Alex Reynaldi]

Yes this works, thank you!