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):

#mwe

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