elab_as_eliminator

Stream: general

[Reid Barton]

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]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

something like quot.rec_on would be better

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Reid Barton]

Oh hmm, I see

[Reid Barton]

but even then the problem is not necessarily trivial

[Mario Carneiro]

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

[Mario Carneiro]

and that becomes the motive

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

this works