Failed to synthesize type class instance

Stream: new members

[Patrick Stevens]

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]

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

[Reid Barton]

Patrick Stevens said:

Can I tell it any harder to use is_prime?

Yes, several ways

[Reid Barton]

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

[Reid Barton]

since it doesn't seem to be changing anyways

[Kevin Buzzard]

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

[Reid Barton]

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

[Patrick Stevens]

Ah, of course - thanks

[Kevin Buzzard]

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

[Patrick Stevens]

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]

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

[Patrick Stevens]

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]

You can use letI and haveI to register instances

[Patrick Stevens]

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

[Reid Barton]

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

[Patrick Stevens]

Thanks!

[Reid Barton]

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

[Eric Wieser]

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]

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]

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]

Is {! equivalent to a unicode character?

[Jalex Stark]

no

[Eric Wieser]

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

[Jalex Stark]

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]

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]

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]

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

[Eric Wieser]

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]

It seems unhappy with the have h : line.

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

Did you fix that instance? Earlier Lean was complaining.

[Eric Wieser]

Yes, I fixed that.

[Eric Wieser]

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

[Reid Barton]

Well, something appears to be introducing an extra universe parameter

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Kenny Lau]

#mwe

[Eric Wieser]

Indeed

[Kenny Lau]

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

[Eric Wieser]

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Kenny Lau]

@Mario Carneiro

[Reid Barton]

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]

and Type* makes no claim about the universe level

[Kenny Lau]

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]

Type* is asking for trouble really

[Eric Wieser]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Donald Sebastian Leung]

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]

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?