corecursive fibonacci and factorial

Stream: new members

[SnowFox]

Hello world. While experimenting with some Rosetta Code tasks to learn Lean; I've encountered a few obscure type synthesis failures. Can someone shed any light as to why and how often these issues are?

-- corecursive factorial works perfectly
def cofac := stream.corec prod.snd (λ ⟨a, b⟩, (a + 1, a * b)) (1, 1)
-- corecursive fibonacci however, fails to synthesize the type of the first function
def cofib := stream.corec prod.fst (λ ⟨a, b⟩, (b, a + b)) (0, 1)
-- which requires annotating it as either `(prod.fst : prod \nat \nat -> \nat)` or the
-- second lambda body as `(b + 0, a + b)` (adding `+ 0`)
-- or rewriting to use `corec_on` where `(0, 1)` is passed before the lambdas
def cofib' := stream.corec_on (0, 1) prod.fst (λ ⟨a, b⟩, (b, a + b))

I also hit these inconsistencies.

-- `multiset` can be constructed with `{}` but `finset` cannot
#check ({} : multiset nat)
#check ({} : finset nat)
-- `finset` has `finset.empty` but `multiset` does not have `multiset.empty`

[Mario Carneiro]

multiset uses additive notation, so it is (0 : multiset nat)

[Mario Carneiro]

as for the lambda match, those require the type to be known when reading left to right. I think that from the pattern stream.corec prod.fst _ _ you can't determine that the first _ has type A x B -> C which is necessary to interpret (λ ⟨a, b⟩, ...)

[SnowFox]

Mario Carneiro said:

as for the lambda match, those require the type to be known when reading left to right. I think that from the pattern stream.corec prod.fst _ _ you can't determine that the first _ has type A x B -> C which is necessary to interpret (λ ⟨a, b⟩, ...)

I suspected as much; but then I tried stream.unfolds (0, 1) .. because this pushes the type of (0,1) all the way to the left, but this has the same issue.

[SnowFox]

Mario Carneiro said:

multiset uses additive notation, so it is (0 : multiset nat)

The weird detail there is that ({} : multiset nat) does work but ({} : finset nat) does not. I did notice \empty works for both.. but why doesn't {}?

[Mario Carneiro]

Because multiset doesn't have insert, I think

[Mario Carneiro]

insert is kind of a weird operation for multisets

[Mario Carneiro]

actually correction, insert works for multiset, it's just cons

[Mario Carneiro]

also

#check ({} : multiset ℕ)

works for me and produces ∅ : multiset ℕ

[SnowFox]

Right, but try finset.

[Mario Carneiro]

oh, the error is weirder than I thought

[Mario Carneiro]

#check ({} : finset ℕ)
-- invalid structure value { ... }, field 'val' was not provided
-- invalid structure value { ... }, field 'nodup' was not provided

[Mario Carneiro]

It has interpreted the {} as an empty structure literal

[Mario Carneiro]

because finset is a structure

[SnowFox]

Yeah.. I should have included this. Sorry.

[Mario Carneiro]

and multiset isn't

[SnowFox]

Ah!

[Mario Carneiro]

I should note that we don't usually write {} for the empty set

[Mario Carneiro]

we're all about the unicode here

[SnowFox]

Heh, noted.

[SnowFox]

Any idea why the corecursive fib doesn't work when using the unfolds variant?

[SnowFox]

The alpha type is as far left as it gets; yet still fails

[SnowFox]

Well; without being explicitly provided.

[Mario Carneiro]

#mwe?

[SnowFox]

Er, I misremembered. That was a different thing I tried. It was stream.corec_on which pushes the (0, 1) to the start and works as expected.

import data.stream
def cofib := stream.corec prod.fst (λ ⟨a, b⟩, (b + 0, a + b)) (0, 1)
def cofib2 := stream.corec_on (0, 1) prod.fst (λ ⟨a, b⟩, (b, a + b))
def cofib3 := stream.unfolds prod.fst (λ ⟨a, b⟩, (b, a + b)) (0, 1)

[SnowFox]

The first one works because of the + 0, the second works because (0, 1) is first, and the 3rd fails along with s/unfolds/corec, so is the same problem. Except I suspected unfolds might work where corec didn't because unfolds puts all bindings on the left-hand-side of the colon in the type. Unsure if that'd make any difference. It didn't.

[Mario Carneiro]

here's another trick for the toolbox:

def cofib3 := stream.unfolds prod.fst (by exact λ ⟨a, b⟩, (b, a + b)) (0, 1)

[Mario Carneiro]

by exact is a way to say "elaborate this last"

[Mario Carneiro]

also you can (should) just give more type ascriptions when this happens

[SnowFox]

Huh! Nice to know. Thanks. Though I'll just go with the corec_on variant for simplicity.

[Mario Carneiro]

def cofib3 := stream.unfolds prod.fst (λ ⟨a, b⟩, (b, a + b) : ℕ × ℕ → ℕ × ℕ) (0, 1)

[SnowFox]

Yeah, as I had earlier, I annotated the prod.fst part, as that was where the error was.

[SnowFox]

Thanks again. I need to take a break, have a headache due to insufficient sleep. TTYL. o/