Type class inference with parameters

Stream: new members

[Alastair Horn]

Lean doesn't seem to be able to infer types when parameters are involved, so while trying to implement my own version of the integers mod n, I'm having to specify all type classes explicitly. Is there a fix/workaround?
Here's a (ridiculous) example of the kind of stuff that causes problems:

section test

parameter n : ℕ

def inv_wrt_n (a : ℕ) : ℕ := a + n

instance: has_inv ℕ := ⟨inv_wrt_n⟩

#check n⁻¹ -- Fails

end test

[Scott Morrison]

Sorry, I don't have much experience with parameters (mostly because I decided long ago I didn't like them, hiding too much, and prefer to use variables). So my suggestion would be to learn to love variables instead!

[Reid Barton]

I think you'll encounter other serious problems with this approach anyways, unless you only planned to ever use this instance within the scope of the parameter.

[Alastair Horn]

Okay I'll go back to variables, thanks for the advice

[Reid Barton]

variables will make the problems clearer. How do you expect to ever specify n?

[Alastair Horn]

But I want to create a quotient that depends on a value n - the integers mod n

[Alastair Horn]

But type class resolution won't work with variables either because the instance depends on n

[Alastair Horn]

Is there a way to feed lean my specific setoid?

[Mario Carneiro]

You can put the n in the type

[Mario Carneiro]

If you have an instance instance (n : nat) : setoid (mytype n) there are no problems

[Mario Carneiro]

(also, setoids often don't need to be instances)

[Kevin Buzzard]

Or you can not use type class resolution. Mathlib has a whole collection of primed quotient stuff where the equivalence relation is found via unification.

[Kevin Buzzard]

#check @quotient.eq
-- quotient.eq : ∀ {α : Sort u_1} [r : setoid α] {x y : α}, ⟦x⟧ = ⟦y⟧ ↔ x ≈ y
#check @quotient.eq'
-- quotient.eq' : ∀ {α : Sort u_1} {s₁ : setoid α} {a b : α}, quotient.mk' a = quotient.mk' b ↔ setoid.r a b

[Kevin Buzzard]

Note [setoid] v {setoid}

[Kevin Buzzard]

You lose notation this way though, as you can see from the example.

[Alastair Horn]

@Mario Carneiro but if I'm trying to get type class resolution for setoid int (although I'm actually using setoid myint, as I'm using my own implementation of integers) I can't put n in the type

[Alastair Horn]

@Kevin Buzzard that, or explicitly stating everything might be the only way

[Alastair Horn]

But it's not ideal

[Kevin Buzzard]

import tactic
import data.int.modeq

section

parameter (n : ℕ)

def r : ℤ → ℤ → Prop := int.modeq n

open int.modeq quotient

def s : setoid ℤ := { r := r,
  iseqv := ⟨int.modeq.refl, λ _ _, int.modeq.symm, λ _ _ _, int.modeq.trans⟩ }

example : add_semigroup (quotient s) :=
{ add := λ q r, quotient.lift_on₂' q r (λ a b, quotient.mk' (a + b))
  begin
    intros a₁ b₁ a₂ b₂ ha hb,
    show quotient.mk' (a₁ + b₁) = quotient.mk' (a₂ + b₂),
    sorry
  end,
  add_assoc := sorry }

end

[Mario Carneiro]

@Alastair Horn You can, you can define foo n := int and then put the typeclass on foo n

[Alastair Horn]

Okay that seems to get rid of the errors somehow :joy:. I'll see how far I get with that and fall back on Kevin's method otherwise. Thanks