## Stream: general

### Topic: elab_as_eliminator

#### Reid Barton (Jun 27 2018 at 21:41):

Is there an explanation of what elab_as_eliminator actually does somewhere? I once tried reading the source, but wasn't enlightened.
I know there is a selection bias at work here, in that I never notice when it does the right thing, but several times I've found that it fails to infer apparently obvious type parameters, where elab_with_expected_type succeeds.

#### Reid Barton (Jun 27 2018 at 21:52):

Here is a toy example where elab_as_eliminator fails but elab_with_expected_type succeeds:

def equal_mod (n : ℤ) (a b : ℤ) : Prop :=
∃ c, a - b = n * c

def mod_setoid (n : ℤ) : setoid ℤ :=
{ r := equal_mod n, iseqv := sorry }

def Z_mod (n : ℤ) := quotient (mod_setoid n)

local attribute [elab_with_expected_type] quot.lift_on

def mod_dvd (n k : ℤ) : Z_mod (n * k) → Z_mod n :=
λ x, quot.lift_on x
(λ a, quot.mk _ a)
(λ a a' ⟨c, h⟩, quot.sound ⟨k * c, by rw ←mul_assoc; exact h⟩)


#### Mario Carneiro (Jun 27 2018 at 21:57):

elab_as_eliminator is meant for eliminators, where lean has to infer a higher order argument, namely the "motive"

#### Mario Carneiro (Jun 27 2018 at 21:58):

It's not a good fit for nondependent elimination since you can just use the usual first order unification

#### Reid Barton (Jun 27 2018 at 21:59):

OK, that was what I suspected, but wasn't sure. So ideally, methods like lift and lift_on shouldn't have that attribute, since they are nondependent

#### Mario Carneiro (Jun 27 2018 at 22:00):

something like quot.rec_on would be better

#### Reid Barton (Jun 27 2018 at 22:02):

Even then, this strategy is only appropriate when you want to infer the motive from the types of the arguments, rather than from the return type, right?

#### Reid Barton (Jun 27 2018 at 22:02):

Assuming the return type is something like β q, for which the higher-order unification problem is trivial

#### Mario Carneiro (Jun 27 2018 at 22:03):

The motive is inferred from the return type, not the types of the arguments

Oh hmm, I see

#### Reid Barton (Jun 27 2018 at 22:04):

but even then the problem is not necessarily trivial

#### Mario Carneiro (Jun 27 2018 at 22:04):

it finds instances of the value being inducted on and replaces them with a variable

#### Mario Carneiro (Jun 27 2018 at 22:05):

and that becomes the motive

#### Mario Carneiro (Jun 27 2018 at 22:06):

example (x y : ℕ) : x + y = y + x :=
nat.rec_on (x + y)
_ -- ⊢ 0 = y + x
_ -- ⊢ ∀ (n : ℕ), n = y + x → nat.succ n = y + x


#### Reid Barton (Jun 27 2018 at 22:07):

So why does it fail on the mod_dvd example? Wouldn't it conclude that quot.mk _ a : Z_mod n?

#### Mario Carneiro (Jun 27 2018 at 22:09):

vs:

local attribute [elab_with_expected_type] nat.rec_on
example (x y : ℕ) : x + y = y + x :=
nat.rec_on (x + y) _ _
-- unexpected argument at application
--   nat.rec_on (x + y)
-- given argument
--   x + y
-- expected argument
--   y + x


The reason this error is reported is since the output type is C n, without doing higher order unification it matches against eq (x + y) (y + x) so it expects the major premise to be y+x

#### Reid Barton (Jun 27 2018 at 22:09):

it seems to figure this out if I give less detail in the last argument, for example replacing it by (λ a a' h, sorry)

#### Mario Carneiro (Jun 27 2018 at 22:12):

You have to put a by exact in the right place, to delay the elaboration of the let match

#### Mario Carneiro (Jun 27 2018 at 22:12):

def mod_dvd (n k : ℤ) : Z_mod (n * k) → Z_mod n :=
λ x, quot.lift_on x
(λ a, quot.mk _ a)
(by exact λ a a' ⟨c, h⟩, quot.sound ⟨k * c, by rw ←mul_assoc; exact h⟩)


#### Mario Carneiro (Jun 27 2018 at 22:12):

this works

Last updated: Aug 03 2023 at 10:10 UTC