# Zulip Chat Archive

## 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

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

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?

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

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`

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

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

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

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

@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.

#### Xavier Roblot (May 18 2022 at 10:11):

In my quest to learn Lean, I am trying to prove a result from one of my papers. Here is an excerpt of the proof :

```
import group_theory.p_group
import group_theory.subgroup.basic
import group_theory.quotient_group
universes u
variables {G : Type u} [group G] [nontrivial G] [fintype G]
variables {p : ℕ} [hp : fact (nat.prime p)]
include hp
lemma lemma1 (h₁ : is_p_group p G) (h₂ : G ≠ subgroup.center G) :
∃ s : G, (s ∉ subgroup.center G) ∧ (∀ g : G, s*g*s⁻¹*g⁻¹ ∈ subgroup.center G) :=
begin
let Z := subgroup.center G,
let Q := G ⧸ Z,
have t₀ : is_p_group p Q, from is_p_group.to_quotient h₁ Z,
let ZQ := subgroup.center Q,
have tt : nontrivial Q, from sorry,
have rr : fintype Q, from sorry,
have : nontrivial (subgroup.center G) := is_p_group.center_nontrivial h₁,
have zz : nontrivial (subgroup.center Q) := is_p_group.center_nontrivial t₀,
sorry
end
```

The first call to `is_p_group.center_nontrivial`

works fine, but the second one yields an error : failed to synthesize type class instance

The problem seems to be that `nontrivial Q`

is not proved, but I did prove it (well, admit it) just before.

What I am doing wrong?

Last updated: Dec 20 2023 at 11:08 UTC