'eliminator' elaboration was not used

Stream: new members

[mth]

I'm trying to define composition of partial functions as suggested in chapter 7 of Theorem Proving in Lean and I'm curious as to why this works:

def comp (f : β → option γ) (g : α → option β) : α → option γ :=
(λ b, option.rec option.none f b) ∘ g

but this doesn't:

def comp (f : β → option γ) (g : α → option β) : α → option γ :=
(option.rec option.none f) ∘ g -- error: type mismatch at application 'option.rec none'

I'm also getting

term
  none
has type
  option ?m_1 : Type ?
but is expected to have type
  ?m_1 none : Sort ?
Additional information:
context: 'eliminator' elaboration was not used for 'option.rec' because it is not fully applied, #3 explicit arguments expected

What is Lean trying to tell me? Why can't I use the partial application here?

[Patrick Massot]

Do you understand what "fully applied" means here?

[mth]

that I didn't pass all the arguments the function expected?

[Patrick Massot]

Yes, in the first version, option.rec gets as many arguments as it could hope for, but not in the second version.

[Mario Carneiro]

Right. From a pure type theory point of view this should be alright, but lean's type inference isn't smart enough for this unless you explicitly give it all the arguments

[Patrick Massot]

Now, the elaboration process (which is the crucial step where Lean tries to fill in everything the user let implicit) is pretty subtle, and the recursor case is special, it needs more hand-holding.

[Patrick Massot]

But this is clearly not the intended solution to the exercise. Using recursors directly is not something I would recommend doing.

[Patrick Massot]

def comp (f : β → option γ) (g : α → option β) : α → option γ :=
λ a, match g a with
| (some b) := f b
| none := none
end

[Patrick Massot]

This is the user-friendly solution.

[mth]

ah, thank you!

[Patrick Massot]

I hope the exercise comes after introducing match

[Patrick Massot]

@Jeremy Avigad?

[Patrick Massot]

Otherwise I don't know what was the intended solution.

[mth]

match is introduced later in 8.8

[mth]

maybe the intended solution was to use cases_on? is that any friendlier?

[Patrick Massot]

Yes it is a bit friendlier

[Patrick Massot]

def comp' (f : β → option γ) (g : α → option β) : α → option γ :=
λ a, option.cases_on (g a) none f

def comp'' (f : β → option γ) (g : α → option β) : α → option γ :=
λ a, do b ← g a, c ← f b, return c

I'll let your decide which solution you prefer. I think the match one is by far the easiest to read.

[Patrick Massot]

Quickly reading back that chapter, the cases_on solution is clearly the one Jeremy intended.

[Patrick Massot]

Now I need to go.

[mth]

ok, thanks a lot

[mth]

Why does the elaborator complain here?

example (f: γ → option δ) (g : β → option γ) (h : α → option β) :
comp f (comp g h) = λ a, option.cases_on (option.cases_on (h a) none g) none f := rfl

error: invalid option.cases_on application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables: option ?m_1

(Sorry to annoy you again.)

[Patrick Massot]

The elaborator complains it doesn't know the type expected in the big parenthesis. It is not being smart enough.

[Patrick Massot]

You can help it using a type ascription

[Patrick Massot]

example (f: γ → option δ) (g : β → option γ) (h : α → option β) :
comp f (comp g h) = λ a, option.cases_on (option.cases_on (h a) none g : option γ) none f := rfl

[Patrick Massot]

But I'm not sure I understand the point of this statement.

[mth]

Yes, its pretty pointless on its own