# Zulip Chat Archive

## 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

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

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