apply not working with Quotient.inductionOn?

Stream: general

[Sina]

I have the following ad-hoc example where i want to prove the associativity of addition modulo some fixed integer. Somehow exact works but not apply and i don't understand the error message failed to elaborate eliminator, expected type is not available. The relevant line is the field add_assoc in the instance of AddMonoid below.

import Mathlib.Data.Int.ModEq
open Int

abbrev Z (n : ℤ) := ℤ

instance mod_cong_setoid (n : ℤ) : Setoid (Z n) :=
{
  r := Int.ModEq n,
  iseqv := ⟨ModEq.refl, ModEq.symm, ModEq.trans⟩
}

abbrev CMod (n : ℤ) := Quotient (mod_cong_setoid n)

namespace CMod

@[simp]
def add_aux (n : ℤ) : Z n → Z n → CMod n := fun x y => ⟦ x + y ⟧

@[simp]
lemma add_aux_resp_cong (n : ℤ) : ∀ (a b a' b': Z n) ,  a ≈ a' → b ≈ b' →  (⟦ a + b ⟧ : CMod n)  = ⟦ a' + b' ⟧ :=
by
  sorry

instance add (n : ℤ) : Add (CMod n) where
  add := Quotient.lift₂ (CMod.add_aux n) (add_aux_resp_cong n)

lemma add_assoc_aux (n : ℤ) : ∀ (a b c : Z n), (⟦ a ⟧ : CMod n) + ⟦ b ⟧  + ⟦ c ⟧ = ⟦ a ⟧  + (⟦ b ⟧ + ⟦ c ⟧) :=
by
  sorry

instance mod_cong_add_monoid (n : ℤ) : AddMonoid (CMod n) where
  add := Add.add
  add_assoc := by intro a b c; exact Quotient.inductionOn₃ a b c (add_assoc_aux n)
  --simp; apply Quotient.inductionOn₃ a b c;
  zero := _
  zero_add := _
  add_zero := _
  nsmul := _
  nsmul_zero := _
  nsmul_succ := _

end CMod

[Eric Wieser]

Use refine instead

[Kyle Miller]

The function Quotient.inductionOn₃ is handled specially -- it's got a complicated argument (motive) that needs help filling in when elaborating. To do this, it needs to know the expected type at this point. However, the apply tactic elaborates its argument without an expected type (this is because the way apply works is that it attempts to figure out how many additional arguments to apply, so it can't supply an expected type without knowing this number, which would be needed before elaborating). Other tactics, like exact or refine, do elaborate their arguments with the expected type.

[Kyle Miller]

(I suppose there could be an apply! f x y z tactic that re-elaborates with every guess...)

[Mario Carneiro]

Kyle Miller said:

(I suppose there could be an apply! f x y z tactic that re-elaborates with every guess...)

apply does that

[Sina]

@Kyle Miller
I see, thanks for explaining this. In my mind apply could do everything that exact was capable of but your explanation indicates I had a wrong presumption.

[Kyle Miller]

@Mario Carneiro Huh? apply f x y z elaborates f x y z exactly once, and it tacks on new metavariables using mkAppN on the elaborated expression.

[Mario Carneiro]

well it elaborates only once, yes, but it does try different settings for the mvars

[Kyle Miller]

Ok, but the point is that apply! could re-elaborate with varying numbers of trailing holes with the expected type -- you can't do that by elaborating f x y z once ahead of time.

[Mario Carneiro]

In theory this should be sufficient provided that the eliminator defers when it doesn't know how to create the motive