## Stream: new members

### Topic: Failed to synthesize type class instance

#### Patrick Stevens (May 11 2020 at 18:39):

Defining the set of all powers of p dividing n:

def times_p (p : nat) (pos : 0 < p) : nat ↪ nat :=
{ to_fun := λ i, i * p,
inj := begin intros x y prod, dsimp at prod, exact (nat.mul_right_inj pos).mp prod, end
}

def powers_dividing : nat → Π (p : nat) [nat.prime p], finset nat
| n p is_prime := have n / p < n, from sorry,
if p ∣ n then
insert 1 (finset.map (times_p p (nat.prime.pos is_prime)) (powers_dividing (n / p) p is_prime))
else
finset.singleton 1


But Lean fails at the recursive call to powers_dividing to synthesise the type class instance that results in nat.prime p, even though it's right there in scope, it's is_prime. Can I tell it any harder to use is_prime?

#### Patrick Stevens (May 11 2020 at 18:40):

Actually now I type this, I realise I can probably look at the Sylow theorems to find something like this

#### Reid Barton (May 11 2020 at 18:42):

Patrick Stevens said:

Can I tell it any harder to use is_prime?

Yes, several ways

#### Reid Barton (May 11 2020 at 18:43):

But the easiest is to move the (p) [nat.prime p] left of the colon

#### Reid Barton (May 11 2020 at 18:43):

since it doesn't seem to be changing anyways

#### Kevin Buzzard (May 11 2020 at 18:44):

Stuff like [nat.prime p] to the right of the colon is not added to the typeclass database.

#### Reid Barton (May 11 2020 at 18:45):

The [] only affects how somebody calls your function and not what is available for instance search.

#### Patrick Stevens (May 11 2020 at 18:45):

Ah, of course - thanks

#### Kevin Buzzard (May 11 2020 at 18:45):

def powers_dividing (n : nat) (p : nat) [nat.prime p] : finset nat := ...

#### Patrick Stevens (May 11 2020 at 18:46):

In this case I do need things on the right of the colon, because I need to recurse, I think - but I can certainly move the prime bits over

#### Reid Barton (May 11 2020 at 18:46):

If you're really committed to this order of function arguments, then there are other options

#### Patrick Stevens (May 11 2020 at 18:46):

My next question was "suppose I do need to change p as I go, what do I do then", which comes under the same banner

#### Kevin Buzzard (May 11 2020 at 18:47):

You can use letI and haveI to register instances

#### Patrick Stevens (May 11 2020 at 18:47):

But def powers_dividing (p : nat) [is_prime : nat.prime p] : nat → finset nat is perfect for my current function

#### Reid Barton (May 11 2020 at 18:47):

by exactI is one (this will make all local variables available as instances), otherwise @ can help you out

Thanks!

#### Reid Barton (May 11 2020 at 18:48):

I assume @ also works with recursive calls although I'm not sure I ever tried it.

#### Eric Wieser (Jun 17 2020 at 12:32):

Hi - I'm using the instance keyword for the first time, and don't really understand what the error message is telling me. My #mve is

import tactic
import group_theory.subgroup algebra.pi_instances

def Δ (G : Type*) : set (G × G) := { g : G × G | g.fst = g.snd }

instance subgroup_Δ (G : Type*) [group G] : is_subgroup (Δ G) :=
⟨ begin
simp_rw prod.forall,
intros a b,
rw prod.inv_mk,
intros h,
rw Δ at *,
simp at *,
exact h,
end ⟩


which gives

failed to synthesize type class instance for
G : Type ?,
_inst_1 : group G
⊢ is_submonoid (Δ G)


I can't work out what I'm being asked to add here. Could you show me where to insert a sorry to make the error go away, so that I can work out what I'm supposed to do?

#### Kevin Buzzard (Jun 17 2020 at 12:39):

I think is_subgroup might be deprecated, and I don't use it, but if it's a class then after := you might want to type {! !}, click on the bulb, select the bottom but one option (the one about structures) and see what lean wants you to prove

#### Kevin Buzzard (Jun 17 2020 at 12:40):

I think the correct thing to do nowadays though is to make a term of type subgroup (G \times G) with Delta as the carrier

#### Eric Wieser (Jun 17 2020 at 12:52):

Is {! equivalent to a unicode character?

no

#### Eric Wieser (Jun 17 2020 at 12:53):

Just tried it out - that was super helpful, thanks @kbuzzard!

#### Jalex Stark (Jun 17 2020 at 12:54):

suggest should also give you the the thing that {! !} gives you, in addition to lemmas that let you do the construction with fewer arguments

#### Reid Barton (Jun 17 2020 at 12:55):

If you have a super recent Lean (maybe even too recent for mathlib? not sure) then I hear you can use _ in place of this {! !} thing.

#### Eric Wieser (Jun 17 2020 at 13:03):

A follow-up question - given my definition of subgroup_Δ above, how can I construct a normal_subgroup? Do I have to copy the fields over elementwise?

#### Kevin Buzzard (Jun 17 2020 at 13:04):

I think Yury bundled normal_subgroup recently so you might want to look at any constructors he made for that

#### Eric Wieser (Jun 17 2020 at 13:06):

Here's what I'm trying that is giving me a type mismatch:

theorem normal_Δ_iff_comm (G : Type*) [group G] : normal_subgroup (Δ G) ↔ ∀ g h : G, g * h = h * g :=
begin
split,
{
sorry
},
{
intro h_comm,
have j : ∀ (n : G × G), n ∈ Δ G → ∀ (g : G × G), g * n * g⁻¹ ∈ Δ G := by {
sorry
},
have h : is_subgroup (Δ G) := subgroup_Δ G,
exact { one_mem := h.one_mem,
mul_mem := h.mul_mem,
inv_mem := h.inv_mem,
normal := j },
}

end


#### Eric Wieser (Jun 17 2020 at 13:06):

It seems unhappy with the have h : line.

#### Kevin Buzzard (Jun 17 2020 at 13:24):

I think begin/end is a bad way to make terms of a structure

#### Eric Wieser (Jun 17 2020 at 13:25):

Right, but the structure here is a term in a larger proof

#### Kevin Buzzard (Jun 17 2020 at 13:25):

Oh I see you're doing something else. I'm not at lean right now. I would look at the definition of normal subgroup in the library and find the constructor you need

#### Eric Wieser (Jun 17 2020 at 13:29):

I think my issue now is less that my piecewise constructor is ugly, and more that I can't work out how to leverage my previous subgroup_Δ instance.

#### Reid Barton (Jun 17 2020 at 13:30):

Did you fix that instance? Earlier Lean was complaining.

#### Eric Wieser (Jun 17 2020 at 13:31):

Yes, I fixed that.

#### Eric Wieser (Jun 17 2020 at 13:31):

But we can pretend it's just implemented as sorry, right?

#### Reid Barton (Jun 17 2020 at 13:31):

Well, something appears to be introducing an extra universe parameter

#### Eric Wieser (Jun 17 2020 at 13:33):

Oh, you're right. Replacing my instance delcaration with sorry makes the error go away

#### Reid Barton (Jun 17 2020 at 13:34):

so, it sounds like the issue is in code you haven't shown us :upside_down:

#### Eric Wieser (Jun 17 2020 at 13:36):

Indeed. Here's the reduced case:

instance subgroup_Δ (G : Type*) [group G] : is_subgroup (Δ G) :=
{ one_mem := sorry,
mul_mem :=
begin
simp_rw prod.forall,
intros a b,
simp_rw prod.forall,
intros c d,
intros hab hcd,
-- rw prod.mk_mul_mk,
sorry,
end,
inv_mem := sorry
}
#check subgroup_Δ


Uncommenting that commented line introduces the unwanted universe parameter

#### Eric Wieser (Jun 17 2020 at 13:39):

It looks like prod.mk_mul_mk is not inferring the type arguments in the way I want. Passing G G explicitly solves it.

#### Reid Barton (Jun 17 2020 at 13:39):

I don't know what's going on but combining your snippets doesn't work for me.

#### Eric Wieser (Jun 17 2020 at 13:40):

Let me try and reduce the whole thing to just the bit that can't infer arguments to mk_mul_mk

#mwe

Indeed

#### Kenny Lau (Jun 17 2020 at 13:54):

ok I seem to have found the issue, and it is a real issue that needs fixing; let me gather my thoughts

#### Eric Wieser (Jun 17 2020 at 13:55):

Wonderful, thanks. I got distracted fighting with an outdated lean on codewars which does not consider ∈ and set.mem as equivalent...

#### Kenny Lau (Jun 17 2020 at 14:00):

import tactic
import group_theory.subgroup algebra.pi_instances

def Δ (G : Type*) : set (G × G) := { g : G × G | g.fst = g.snd }
set_option pp.universes true
instance is_subgroup_Δ (G : Type*) [group G] : is_subgroup (Δ G) :=
{ one_mem := rfl,
mul_mem := λ p q hp hq, show p.1 * q.1 = p.2 * q.2, by congr',
inv_mem := begin
simp_rw prod.forall,
intros a b, -- (a, b) ∈ Δ.{?l_1} G → (a, b)⁻¹ ∈ Δ.{?l_1} G
rw prod.inv_mk, -- (a, b) ∈ Δ.{(max ?l_1 ?l_2)} G → (a⁻¹, b⁻¹) ∈ Δ.{(max ?l_1 ?l_2)} G
-- intros h,
-- rw Δ at *,
-- simp at *,
-- exact h,
sorry
end }
#check @prod.inv_mk
/-
prod.inv_mk.{u_1 u_2} :
∀ {G : Type u_1} {H : Type u_2} [_inst_1 : has_inv.{u_1} G] [_inst_2 : has_inv.{u_2} H] (a : G) (b : H),
(a, b)⁻¹ = (a⁻¹, b⁻¹)
-/


#### Kenny Lau (Jun 17 2020 at 14:00):

somehow rw prod.inv_mk brought into existence a new universe variable

#### Kenny Lau (Jun 17 2020 at 14:01):

(it is noteworthy that avoiding Type* and using explicit universe variables avoids the problem completely

@Mario Carneiro

#### Reid Barton (Jun 17 2020 at 14:02):

Oh right, so one perhaps surprising thing is that instance is treated as a def even when (as here) we're proving a Prop; and this means that the body is used to elaborate the statement

#### Reid Barton (Jun 17 2020 at 14:03):

and Type* makes no claim about the universe level

#### Kenny Lau (Jun 17 2020 at 14:04):

for the time being OP can use this (use haveI for instances instead of have):

import tactic
import group_theory.subgroup algebra.pi_instances

def Δ (G : Type*) : set (G × G) := { g : G × G | g.fst = g.snd }

instance is_subgroup_Δ (G : Type*) [group G] : is_subgroup (Δ G) :=
{ one_mem := rfl,
mul_mem := λ p q hp hq, show p.1 * q.1 = p.2 * q.2, by congr',
inv_mem := λ p hp, show p.1⁻¹ = p.2⁻¹, by congr' }

theorem normal_Δ_iff_comm (G : Type*) [group G] : normal_subgroup (Δ G) ↔ ∀ g h : G, g * h = h * g :=
begin
split,
{
sorry
},
{
intro h_comm,
have j : ∀ (n : G × G), n ∈ Δ G → ∀ (g : G × G), g * n * g⁻¹ ∈ Δ G := by {
sorry
},
haveI h : is_subgroup (Δ G) := is_subgroup_Δ G,
exact { normal := j },
}

end


#### Reid Barton (Jun 17 2020 at 14:05):

Type* is asking for trouble really

#### Eric Wieser (Jun 17 2020 at 14:05):

Note that the definition of Δ came from https://www.codewars.com/kata/5eb806b4e7c54e00246f70e1

#### Reid Barton (Jun 17 2020 at 14:09):

I think using Type* in top-level variables should be "safe", although it probably won't be in Lean 4 from what I hear

#### Reid Barton (Jun 17 2020 at 14:13):

Indeed, if you move (G : Type*) from instance is_subgroup_Δ to a top-level variables, then the extra universes disappear.

#### Reid Barton (Jun 17 2020 at 14:17):

That said, the behavior Kenny showed also looks quite odd to me.

#### Reid Barton (Jun 17 2020 at 14:19):

Oh, here's another thing I don't understand. If you put your cursor on the prod.inv_mk at the end of Kenny's file, it displays

prod.inv_mk : ∀ {G : Type u_3} {H : Type u_4} [_inst_1 : has_inv.{u_3} G] [_inst_2 : has_inv.{u_4} H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)


but the one in the line rw prod.inv_mk gives

prod.inv_mk : ∀ {G H : Type (max u_1 u_2)} [_inst_1 : has_inv.{(max u_1 u_2)} G] [_inst_2 : has_inv.{(max u_1 u_2)} H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)


#### Reid Barton (Jun 17 2020 at 14:24):

this is actually two things I don't understand, namely?

• why doesn't Lean just always show me the type of the declaration prod.inv_mk? what kind of local processing does it do?
• how did it arrive at this idea of using the universe max u_1 u_2, but not unifying G and H or u_1 and u_2?

#### Donald Sebastian Leung (Jun 18 2020 at 12:40):

@Eric Wieser Note that you can request for the latest Lean version over at Codewars/codewars-runner-cli

#### Donald Sebastian Leung (Jun 18 2020 at 12:52):

BTW we have a #Codewars stream for Codewars-specific questions, if you'd like to take a look. I also created a topic there on upgrading Lean on Codewars to the latest version.

Last updated: May 17 2021 at 22:15 UTC