Zulip Chat Archive

Stream: new members

Topic: 'eliminator' elaboration was not used


view this post on Zulip 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 ?
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?

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:46):

Do you understand what "fully applied" means here?

view this post on Zulip mth (Oct 12 2019 at 08:48):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:52):

This is the user-friendly solution.

view this post on Zulip mth (Oct 12 2019 at 08:54):

ah, thank you!

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:55):

I hope the exercise comes after introducing match

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:55):

@Jeremy Avigad?

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:56):

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

view this post on Zulip mth (Oct 12 2019 at 08:58):

match is introduced later in 8.8

view this post on Zulip mth (Oct 12 2019 at 08:58):

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

view this post on Zulip Patrick Massot (Oct 12 2019 at 09:03):

Yes it is a bit friendlier

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 12 2019 at 09:06):

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

view this post on Zulip Patrick Massot (Oct 12 2019 at 09:06):

Now I need to go.

view this post on Zulip mth (Oct 12 2019 at 09:07):

ok, thanks a lot

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 16 2019 at 10:54):

You can help it using a type ascription

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 16 2019 at 10:55):

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

view this post on Zulip mth (Oct 16 2019 at 10:58):

Yes, its pretty pointless on its own


Last updated: May 16 2021 at 22:14 UTC