Zulip Chat Archive

Stream: new members

Topic: Failed to synthesize type class instance


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Reid Barton (May 11 2020 at 18:42):

Patrick Stevens said:

Can I tell it any harder to use is_prime?

Yes, several ways

view this post on Zulip Reid Barton (May 11 2020 at 18:43):

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

view this post on Zulip Reid Barton (May 11 2020 at 18:43):

since it doesn't seem to be changing anyways

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 11 2020 at 18:45):

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

view this post on Zulip Patrick Stevens (May 11 2020 at 18:45):

Ah, of course - thanks

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:45):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 11 2020 at 18:46):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:47):

You can use letI and haveI to register instances

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Stevens (May 11 2020 at 18:47):

Thanks!

view this post on Zulip Reid Barton (May 11 2020 at 18:48):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jun 17 2020 at 12:52):

Is {! equivalent to a unicode character?

view this post on Zulip Jalex Stark (Jun 17 2020 at 12:53):

no

view this post on Zulip Eric Wieser (Jun 17 2020 at 12:53):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jun 17 2020 at 13:06):

It seems unhappy with the have h : line.

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 13:24):

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

view this post on Zulip Eric Wieser (Jun 17 2020 at 13:25):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 17 2020 at 13:30):

Did you fix that instance? Earlier Lean was complaining.

view this post on Zulip Eric Wieser (Jun 17 2020 at 13:31):

Yes, I fixed that.

view this post on Zulip Eric Wieser (Jun 17 2020 at 13:31):

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

view this post on Zulip Reid Barton (Jun 17 2020 at 13:31):

Well, something appears to be introducing an extra universe parameter

view this post on Zulip Eric Wieser (Jun 17 2020 at 13:33):

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

view this post on Zulip Reid Barton (Jun 17 2020 at 13:34):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 17 2020 at 13:41):

#mwe

view this post on Zulip Eric Wieser (Jun 17 2020 at 13:41):

Indeed

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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⁻¹)
-/

view this post on Zulip Kenny Lau (Jun 17 2020 at 14:00):

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

view this post on Zulip Kenny Lau (Jun 17 2020 at 14:01):

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

view this post on Zulip Kenny Lau (Jun 17 2020 at 14:01):

@Mario Carneiro

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 17 2020 at 14:03):

and Type* makes no claim about the universe level

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 17 2020 at 14:05):

Type* is asking for trouble really

view this post on Zulip Eric Wieser (Jun 17 2020 at 14:05):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 17 2020 at 14:17):

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

view this post on Zulip 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⁻¹)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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