Zulip Chat Archive

Stream: general

Topic: rewriting and type class inference


Kevin Buzzard (Sep 25 2019 at 21:55):

Mario said (regarding whether variables should be implicit or explicit in an iff statement)

The rule is that if it's an iff then it should be implicit if it appears on both sides of the iff. That is, iffs are treated as a pair of implications, and are implicit if they would be implicit in both one-directional versions

But what about the following session? I only use mathlib to get a topological group; I don't know how far into the hierarchy one needs to go in order to see this phenomenon:

import topology.algebra.uniform_group

lemma silly {G : Type} [group G] [topological_space G] [topological_group G] :
  nonempty G  nonempty G := iff.rfl

example {G : Type} [group G] [topological_space G] [topological_group G]: nonempty G :=
begin
  --rw silly, -- fails
  --rw @silly, -- fails
  -- rw @silly _, -- fails
  /- All fail with this error:
  invalid rewrite tactic, failed to synthesize type class instance
  -/
--  rw @silly _ _ _, -- fails
  /-
  invalid rewrite tactic, failed to synthesize type class instance
state:
4 goals
G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ nonempty G

G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ Type

G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ group ?m_1

G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ topological_space ?m_1
-/
  rw @silly _ _ _ _, -- works but now we have four goals e.g. ⊢ group G
  repeat {sorry}
end

-- explicit G version
lemma silly2 (G : Type) [group G] [topological_space G] [topological_group G] :
  nonempty G  nonempty G := iff.rfl

example {G : Type} [group G] [topological_space G] [topological_group G]: nonempty G :=
begin
  rw silly2 _,
  /-
  4 goals
G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ nonempty G

G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ group G

G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ topological_space G

G : Type,
_inst_1 : group G,
_inst_2 : topological_space G,
_inst_3 : topological_group G
⊢ topological_group G
-/
  repeat {sorry}
end

example {G : Type} [group G] [topological_space G] [topological_group G]: nonempty G :=
begin
  rw silly2 G, -- works -- only one goal.
  sorry
end

Is this evidence that G should be explicit in silly?

Reid Barton (Sep 25 2019 at 22:00):

I think it's evidence that something is wrong with rw: it should just work in all cases. Why doesn't it automatically deal with those side goals? I've seen behavior like this before, and I would love to know what's going on.

Reid Barton (Sep 25 2019 at 22:01):

Could it have something to do with the fact that nonempty is itself a class?

Kevin Buzzard (Sep 25 2019 at 22:01):

mathlib-free version:

class foo (G : Type)

class bar (G : Type) [foo G]

lemma silly {G : Type} [foo G] [bar G] :
  nonempty G  nonempty G := iff.rfl

example (G : Type) [foo G] [bar G] : nonempty G :=
begin
--  rw silly, -- fails
--  rw @silly G, -- fails
  rw @silly G _, -- works
  sorry
end

lemma silly2 (G : Type) [foo G] [bar G] :
  nonempty G  nonempty G := iff.rfl

example (G : Type) [foo G] [bar G] : nonempty G :=
begin
-- rw silly2, -- fails
--  rw @silly2 G, -- fails
  rw silly2 G, -- works -- perhaps different elaboration strat to the previous line?
  sorry
end

Kevin Buzzard (Sep 25 2019 at 22:05):

The issue isn't that nonempty is a class. Maybe it's a bug in rw? I've also seen it before, but catching out a student; it's now catching me out though.

class foo (G : Type)

class bar (G : Type) [foo G]

def P : Type  Prop := sorry
def Q : Type  Prop := sorry

lemma silly {G : Type} [foo G] [bar G] :
  P G  Q G := iff.rfl -- rofl

example (G : Type) [foo G] [bar G] : P G :=
begin
--  rw silly, -- fails
--  rw @silly G, -- fails
  rw @silly G _, -- works
  sorry
end

lemma silly2 (G : Type) [foo G] [bar G] :
  P G  Q G := iff.rfl

example (G : Type) [foo G] [bar G] : P G :=
begin
-- rw silly2, -- fails
--  rw @silly2 G, -- fails
  rw silly2 G, -- works -- perhaps different elaboration strat to the previous line?
  sorry
end

Reid Barton (Sep 25 2019 at 22:07):

Maybe related: in the first example, apply silly.mp succeeds but creates side goals for foo G and bar G, while refine silly.mp _ works correctly

Kevin Buzzard (Sep 25 2019 at 22:09):

I am rather surprised that rw @silly2 G fails at the end but rw silly2 G works. I know that the @ can cause some stuff to be elaborated differently but that fact is not in the context of a rewrite. It would be great if this were a bug in rw, because I like Mario's rule; perhaps there needs to be an exception for when iterated typeclasses are involved though?

Reid Barton (Sep 25 2019 at 22:09):

If silly only depends on foo G and not bar G then rw silly works in the first example but apply silly.mp still creates a side goal foo G

Reid Barton (Sep 25 2019 at 22:10):

Also if bar G doesn't depend on foo G then rw silly succeeds. That seems to suggest that rw might be trying to solve the goals in the wrong order?

Kevin Buzzard (Sep 25 2019 at 22:11):

Yes, if bar doesn't depend on foo then everything seems to work exactly as one might expect it to.

Kevin Buzzard (Sep 25 2019 at 22:13):

Side issue: debugging is hard because in contrast to the usual situation where you can see exactly which instance Lean failed to infer, here we just get this generic message failed to synthesize type class instance. Is there any way of looking at the trace of a rewrite like there is for simp?

Mario Carneiro (Sep 25 2019 at 22:14):

I would have just written apply silly.1 in most of these cases

Floris van Doorn (Sep 25 2019 at 22:14):

I also feel that the problem is that rw does type-class inference in the wrong order. If you provide underscores, then type-class inference will fire for those arguments before rewrite does anything.

Reid Barton (Sep 25 2019 at 22:15):

Mario I'm sure you would have noticed that you don't even have to apply silly

Mario Carneiro (Sep 25 2019 at 22:15):

that's fair

Kevin Buzzard (Sep 25 2019 at 22:15):

I would have just written apply silly.1 in most of these cases

Yes, that's what we did to work around it, but I figured it was worth getting to the bottom of.

Mario Carneiro (Sep 25 2019 at 22:16):

the rule that I gave is optimized for using .1 and .2 to apply bidirectional theorems

Mario Carneiro (Sep 25 2019 at 22:17):

Does it work if you use = instead of <->?

Kevin Buzzard (Sep 25 2019 at 22:17):

One could imagine a big chain of rewrites though, where you don't want to stop and apply something.

Kevin Buzzard (Sep 25 2019 at 22:21):

Does it work if you use = instead of <->?

Nope:

class foo (G : Type)

class bar (G : Type) [foo G]

def P : Type  Prop := λ _, true
def Q : Type  Prop := λ _, true

lemma silly {G : Type} [foo G] [bar G] :
  P G = Q G := rfl

example (G : Type) [foo G] [bar G] : P G :=
begin
  rw silly,
  /-
invalid rewrite tactic, failed to synthesize type class instance
state:
G : Type,
_inst_1 : foo G,
_inst_2 : bar G
⊢ P G
-/
end

Floris van Doorn (Sep 25 2019 at 22:22):

don't forget to use refine silly.1 _ to avoid the apply bug :)

Floris van Doorn (Sep 25 2019 at 22:22):

I think I can explain all behavior except rw @silly _ _:

class foo (G : Type)
class bar (G : Type) [foo G]

constant P : Type  Prop
constant Q : Type  Prop

lemma silly {G : Type} [foo G] [bar G] : P G  Q G := sorry

example (G : Type) [foo G] [bar G] : P G :=
begin
  -- rw @silly, -- fails: rw infers arguments in wrong order?
  -- rw @silly G, -- fails: rw infers arguments in wrong order?
  -- rw @silly G _, -- succeeds: `foo` is inferred before rw is called
  -- rw @silly G _ _, -- succeeds: `foo` and `bar` are inferred before rw is called
  -- rw @silly _, -- fails: rw infers arguments in wrong order?
  -- rw @silly _ _, -- fails?
  -- rw @silly _ _ _, -- works, but generates too many new goals: couldn't infer type-class arguments before rw
  -- rw silly, -- presumably same as `rw @silly` because names are treated differently than expressions
  -- rw id silly, -- same as `rw @silly _ _ _`
  -- refine silly.mpr _, -- preferred solution
end

Floris van Doorn (Sep 25 2019 at 22:24):

Oh rw @silly _ _ probably fails for the same reason: it tries to synthesize bar G when foo G has not been synthesized yet.

Kevin Buzzard (Sep 25 2019 at 22:24):

rw @silly _ _ is failing to synthesize bar G because when it tries it's bar ?m_1 right?

Mario Carneiro (Sep 25 2019 at 22:24):

what is the error rw infers arguments in wrong order?

Floris van Doorn (Sep 25 2019 at 22:24):

that is my human-written reason that rw fails.

Kevin Buzzard (Sep 25 2019 at 22:24):

invalid rewrite tactic, failed to synthesize type class instance
state:
G : Type,
_inst_1 : foo G,
_inst_2 : bar G
⊢ P G

Mario Carneiro (Sep 25 2019 at 22:24):

I know, but what exactly is happening by your estimation

Kevin Buzzard (Sep 25 2019 at 22:25):

I think that type class inference fails on foo ?m_1 before it has decided that ?m_1=G

Kevin Buzzard (Sep 25 2019 at 22:25):

but this is just a guess and I don't know how to find out if I'm right.

Floris van Doorn (Sep 25 2019 at 22:25):

my estimation is that rw tries to infer @bar G ?m and fails before inferring ?m : foo G.

Mario Carneiro (Sep 25 2019 at 22:26):

it shouldn't do that

Kevin Buzzard (Sep 25 2019 at 22:26):

Aah floris' suggestion is more refined than mine.

Reid Barton (Sep 25 2019 at 22:26):

I think Kevin's guess is wrong because it doesn't happen if bar is not involved

Floris van Doorn (Sep 25 2019 at 22:27):

it shouldn't do that

Agreed, but does it do that?

Mario Carneiro (Sep 25 2019 at 22:27):

what's the error message?

Kevin Buzzard (Sep 25 2019 at 22:27):

I think Kevin's guess is wrong because it doesn't happen if bar is not involved

My guess can't be right because if it were right then we would have noticed this much much earlier

Kevin Buzzard (Sep 25 2019 at 22:28):

what's the error message?

Still the one I quoted.

Reid Barton (Sep 25 2019 at 22:28):

it shouldn't do that

Agreed, but does it do that?

This you can test with set_option trace.class_instances true, the first output is

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @bar G ?m__fresh.293.7708 := _inst_2
failed is_def_eq

Kevin Buzzard (Sep 25 2019 at 22:28):

It's the "rubbish" version of the failed to synthesize type class instance error, when it doesn't tell you the type of the instance it failed to syntheize

Reid Barton (Sep 25 2019 at 22:28):

In fact, that's the only relevant output because rw just gives up when that fails

Mario Carneiro (Sep 25 2019 at 22:29):

ah, synth_instances() works in reverse order

Reid Barton (Sep 25 2019 at 22:29):

Also if bar doesn't depend on foo, then you can see in the trace it solves bar first and then foo

Mario Carneiro (Sep 25 2019 at 22:30):

that's what gets called in rewrite_core() after the pattern matches (so G is unified) with the list of instance metavariables that were inserted in order to fill the pis in the equation

Kevin Buzzard (Sep 25 2019 at 22:30):

You should never be solving the instances in reverse order -- things wouldn't even typecheck if I fed them to Lean in reverse order when I was defining the function.

Mario Carneiro (Sep 25 2019 at 22:31):

https://github.com/leanprover-community/lean/blob/master/src/library/tactic/apply_tactic.cpp#L96-L97

Mario Carneiro (Sep 25 2019 at 22:32):

I don't know if it's an optimization or what

Kevin Buzzard (Sep 25 2019 at 22:32):

It certainly looks like a conscious decision though doesn't it ;-)

Mario Carneiro (Sep 25 2019 at 22:33):

if only Leo were active right now...

Kevin Buzzard (Sep 25 2019 at 22:34):

don't even think about it.

Kevin Buzzard (Sep 25 2019 at 22:34):

I'm going to go to bed before I snap and just ask him :-/

Bryan Gin-ge Chen (Sep 25 2019 at 22:36):

Looks like that code was added in this commit: https://github.com/leanprover-community/lean/commit/f7fe2a775c1492184278931dc223648b95d9ce64#diff-cd4a348ea2537f9e3471d8c015145d5eR80-R91

I couldn't find any issue that corresponded to the commit message though.

Reid Barton (Sep 25 2019 at 22:36):

It was effectively moved from elsewhere in that commit though, so you'd have look farther back

Reid Barton (Sep 25 2019 at 22:37):

I'll just change it to forwards and find out what breaks

Mario Carneiro (Sep 25 2019 at 22:40):

It's been there since the beginning: https://github.com/leanprover-community/lean/commit/61a845c0050c7617ce9df7e2071883d1c24f3a27

Reid Barton (Sep 25 2019 at 22:44):

Well, the core library built successfully at least

Mario Carneiro (Sep 25 2019 at 22:48):

do Kevin's tests work?

Reid Barton (Sep 25 2019 at 22:50):

Yes

Mario Carneiro (Sep 25 2019 at 22:50):

PR?

Reid Barton (Sep 25 2019 at 22:50):

though apply still generates side conditions

Mario Carneiro (Sep 25 2019 at 22:50):

I think that's something else

Bryan Gin-ge Chen (Sep 25 2019 at 22:50):

Can you build mathlib? :rolling_on_the_floor_laughing:

Reid Barton (Sep 25 2019 at 22:51):

Can you build mathlib? :rolling_on_the_floor_laughing:

in progress

Reid Barton (Sep 25 2019 at 22:52):

I was hoping the apply thing was related just because the code was in tactic_apply.cpp, but it wasn't really consistent with the fact that it also occurred with only one class involved

Mario Carneiro (Sep 25 2019 at 22:52):

Could you give a simple example of the apply behavior?

Reid Barton (Sep 25 2019 at 22:53):

is "replace rw silly with apply silly.1 in Kevin's examples" good enough?

Mario Carneiro (Sep 25 2019 at 22:54):

and you get subgoals |- foo G, |- bar G?

Reid Barton (Sep 25 2019 at 22:55):

Yep, with the main goal nonempty G first

Reid Barton (Sep 25 2019 at 22:56):

Actually, hang on

Reid Barton (Sep 25 2019 at 22:58):

Ah, never mind. I thought I saw something else going on, but it was due to other stuff in the same file (the second example).
The order of the new goals is also the same (nonempty G then foo G then bar G) with both standard Lean and my modified version.

Mario Carneiro (Sep 25 2019 at 23:03):

I get no typeclass instance trace corresponding to a proof of foo G or foo ?m_1

Reid Barton (Sep 25 2019 at 23:05):

PR?

https://github.com/leanprover-community/lean/pull/67

Reid Barton (Sep 25 2019 at 23:06):

but of course it's potentially breaking compatibility

Mario Carneiro (Sep 25 2019 at 23:07):

if mathlib builds, I think this should be safe

Mario Carneiro (Sep 25 2019 at 23:08):

it's apparently rarely exercised but I don't see how this will cause any new errors

Mario Carneiro (Sep 25 2019 at 23:12):

It looks like the problem isn't with apply:

lemma silly {G : Type} [foo G] : Q G  P G := sorry

example (G : Type) [foo G] : P G :=
begin
  -- apply silly, --works
  -- apply @silly, --works
  -- apply (@silly _), --works
  apply (@silly _ _), --leaves |- foo G
end

Reid Barton (Sep 25 2019 at 23:13):

Mathlib did build

Mario Carneiro (Sep 25 2019 at 23:15):

I think the issue is that i_to_expr_for_apply gets called with the pexpr (@silly _ _) first, and no expected type, which generates the subgoal for |- ?m : Type and for |- foo ?m, then apply_core is called with the resulting expr, which unifies ?m := G and leaves the |- foo G goal

Mario Carneiro (Sep 25 2019 at 23:16):

apply itself knows how to handle this when it does its own metavariable instantiations: it delays them until after unification

Mario Carneiro (Sep 25 2019 at 23:16):

but these metavariables are created before apply_core is called so it doesn't know about them

Reid Barton (Sep 25 2019 at 23:19):

So you changed two things: silly has only foo and not bar, and it's no longer a biconditional.

Mario Carneiro (Sep 25 2019 at 23:20):

the biconditional was confusing matters, and the foo/bar thing was exercising the wrong bug

Mario Carneiro (Sep 25 2019 at 23:21):

you get the same result with silly.2 with the earlier version if you fix the synth_instances bug

Reid Barton (Sep 25 2019 at 23:21):

The same result as apply (@silly _ _) you mean?

Mario Carneiro (Sep 25 2019 at 23:21):

yes

Reid Barton (Sep 25 2019 at 23:21):

OK, right

Mario Carneiro (Sep 25 2019 at 23:22):

because synth.2 is elaborated first to (synth ?m ?m').2 with the ?m' subgoal added, then apply is called

Mario Carneiro (Sep 25 2019 at 23:23):

I don't see an obvious way to fix this besides passing the new goals to apply_core so it can include them in the accounting, or maybe trying to infer them again after calling apply_core

Mario Carneiro (Sep 25 2019 at 23:24):

it's not easy to find out if they are pending instance resolution though

Mario Carneiro (Sep 25 2019 at 23:25):

because that depends on the binder on the application that generated them

Mario Carneiro (Sep 25 2019 at 23:26):

you can approximate it by looking at the type and seeing if it's a class, but this will have the wrong behavior for {_ : nonempty A} binders

Reid Barton (Sep 25 2019 at 23:34):

I think I see, apply is going to do the work of guessing how many _s to insert (hopefully correctly), so before that we don't know how to infer metavariables in the given expression from the target type

Jeremy Avigad (Sep 26 2019 at 01:34):

Mario, I'll make you explain all this to me next time we meet. I am guessing is that this might explain the trouble I had when I tried unbundling things in the algebraic hierarchy. IIRC, I wanted to do things like foo {α : Type} [has_mul α] [commutative (@mul α)] and was having similar problems.

Jesse Michael Han (Sep 26 2019 at 03:03):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC