instance synthesis failed

Stream: new members

[Yannick Seurin]

In the code below, I don't understand why the definition of foo is OK, but for bar I get failed to synthesize NeZero (Nat.card G). I noticed that bar does not take [Fintype G] as parameter, but even if I add it the error remains...

import Mathlib

variable (G : Type) [Fintype G] [CommGroup G]
         (g : G) (g_gen_G : ∀ x : G, x ∈ Subgroup.zpowers g)

instance : NeZero (Fintype.card G) where
  out := Fintype.card_ne_zero

instance : NeZero (Nat.card G) where
  out := by
    apply Nat.card_ne_zero.mpr
    constructor
    · exact Nonempty.intro g
    apply Fintype.finite
    infer_instance

noncomputable section

def uniform_zmod (n : ℕ) [NeZero n] : PMF (ZMod n) :=
  PMF.uniformOfFintype (ZMod n)

def foo : PMF G := do
  let x ← uniform_zmod (Fintype.card G)
  pure (g ^ x.val)

#check foo -- foo (G : Type) [CommGroup G] [Fintype G] (g : G) : PMF G

def bar : PMF G := do
  let x ← uniform_zmod (Nat.card G) -- failed to synthesize NeZero (Nat.card G)
  pure (g ^ x.val)

#check bar -- bar (G : Type) [CommGroup G] (g : G) : PMF G

end

[Kenny Lau]

@Yannick Seurin this is a subtle one.

If you hover over the word instance at the line instance : NeZero (Nat.card G), then you'll see:

«instNeZeroNatCard_external:file:///MathlibDemo/MathlibDemo.lean_1»
(G : Type) [h : Fintype G] (g : G) :
  NeZero (Nat.card G)

[Kenny Lau]

notice how g : G sneakily got inside the type because you used it!

[Yannick Seurin]

OK, but why does it prevent instance synthesis when defining bar? It seems bar does take (g : G) as parameter (sorry my understanding of instance synthesis is very limited).

[Kenny Lau]

@Yannick Seurin when Lean synthesizes instances, it follows a very simple algorithm, where it only fills in the inputs from other instances and the information available in the type. In this case, concretely, Lean cannot guess what to fill in for the input g.

[Yannick Seurin]

OK thanks, I think I kind of get it. The fix I came with is to first declare an instance of Nonempty G and then infer NeZero (Nat.card G), this gets rid of (g : G) in the instance type:

import Mathlib

variable (G : Type) [Fintype G] [CommGroup G]
         (g : G) (g_gen_G : ∀ x : G, x ∈ Subgroup.zpowers g)

instance : NeZero (Fintype.card G) where
  out := Fintype.card_ne_zero

instance : Nonempty G := Nonempty.intro g

instance : NeZero (Nat.card G) where
  out := by
    apply Nat.card_ne_zero.mpr
    constructor
    · infer_instance
    apply Fintype.finite
    infer_instance

noncomputable section

def uniform_zmod (n : ℕ) [NeZero n] : PMF (ZMod n) :=
  PMF.uniformOfFintype (ZMod n)

def foo : PMF G := do
  let x ← uniform_zmod (Fintype.card G)
  pure (g ^ x.val)

def bar : PMF G := do
  let x ← uniform_zmod (Nat.card G) -- OK
  pure (g ^ x.val)

end

[Kenny Lau]

@Yannick Seurin This is an example of right answer but wrong steps :rofl:
if you now hover over instance in instance : Nonempty G, you'll see that g : G is still being used, meaning that the instance of Nonempty G you provided is useless; however, the third instance still works, because Lean actually used another pathway to deduce that G is nonempty!

[Kenny Lau]

If you go to Line 15 and replace infer_instance with show_term infer_instance, then on the right you'll see:

Try this:
  [apply] exact inferInstance

Now don't click the apply, but instead click on the inferInstance, then you'll see the window pop up with:

@inferInstance (Nonempty G) One.instNonempty : Nonempty G

which means that it used the One.instNonempty to infer that G is nonempty, instead of using the instance you provided

[Yannick Seurin]

Oh damn, so I could have used infer_instance at Line 15 since the beginning and it would have worked right away :upside_down:
Instead I used apply? which only suggested exact Nonempty.intro g but not the inference from [CommGroup G]. So I guess the morality is to always use infer_instance rather than trying to come with explicit proofs.

[Kenny Lau]

well, another lesson you could have taken away is to clearly inspect the variables and whether they are used in each instance/definition/theorem

[Yannick Seurin]

@Kenny Lau Actually, I did inspect the variables and noticed that (g : G) was used in my first version of instance : NeZero (Nat.card G). But then I thought: well, bar does take (g : G) and even uses it in pure (g ^ x.val), so this cannot be the problem (and I still don't really understand why Lean class synthesis does not use this (g : G) to synthesize NeZero (Nat.card G); it rather seemed to me that what was missing in my initial example in the parameters of bar was [Fintype G]...)

[Robin Arnez]

The instance you really want is

instance {α : Type u} [Finite α] [Nonempty α] : NeZero (Nat.card α) where
  out := Nat.card_ne_zero.mpr ⟨inferInstance, inferInstance⟩

which doesn't rely on a weird CommGroup G instance requirement