## Stream: new members

### Topic: 'eliminator' elaboration was not used

#### mth (Oct 12 2019 at 08:44):

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 ?
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 (Oct 12 2019 at 08:46):

Do you understand what "fully applied" means here?

#### mth (Oct 12 2019 at 08:48):

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

#### Patrick Massot (Oct 12 2019 at 08:50):

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

#### Mario Carneiro (Oct 12 2019 at 08:51):

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 (Oct 12 2019 at 08:51):

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 (Oct 12 2019 at 08:52):

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

#### Patrick Massot (Oct 12 2019 at 08:52):

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


#### Patrick Massot (Oct 12 2019 at 08:52):

This is the user-friendly solution.

ah, thank you!

#### Patrick Massot (Oct 12 2019 at 08:55):

I hope the exercise comes after introducing match

#### Patrick Massot (Oct 12 2019 at 08:56):

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

#### mth (Oct 12 2019 at 08:58):

match is introduced later in 8.8

#### mth (Oct 12 2019 at 08:58):

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

#### Patrick Massot (Oct 12 2019 at 09:03):

Yes it is a bit friendlier

#### Patrick Massot (Oct 12 2019 at 09:04):

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 (Oct 12 2019 at 09:06):

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

#### Patrick Massot (Oct 12 2019 at 09:06):

Now I need to go.

ok, thanks a lot

#### mth (Oct 16 2019 at 10:38):

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 (Oct 16 2019 at 10:54):

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

#### Patrick Massot (Oct 16 2019 at 10:54):

You can help it using a type ascription

#### Patrick Massot (Oct 16 2019 at 10:54):

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 (Oct 16 2019 at 10:55):

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

#### mth (Oct 16 2019 at 10:58):

Yes, its pretty pointless on its own

Last updated: May 16 2021 at 22:14 UTC