rewriting and type class inference

Stream: general

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Floris van Doorn]

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]

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

[Mario Carneiro]

that's fair

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Floris van Doorn]

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]

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]

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

[Mario Carneiro]

what is the error rw infers arguments in wrong order?

[Floris van Doorn]

that is my human-written reason that rw fails.

[Kevin Buzzard]

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

[Mario Carneiro]

I know, but what exactly is happening by your estimation

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Floris van Doorn]

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

[Mario Carneiro]

it shouldn't do that

[Kevin Buzzard]

Aah floris' suggestion is more refined than mine.

[Reid Barton]

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

[Floris van Doorn]

it shouldn't do that

Agreed, but does it do that?

[Mario Carneiro]

what's the error message?

[Kevin Buzzard]

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]

what's the error message?

Still the one I quoted.

[Reid Barton]

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]

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]

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

[Mario Carneiro]

ah, synth_instances() works in reverse order

[Reid Barton]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

if only Leo were active right now...

[Kevin Buzzard]

don't even think about it.

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

Well, the core library built successfully at least

[Mario Carneiro]

do Kevin's tests work?

[Reid Barton]

Yes

[Mario Carneiro]

PR?

[Reid Barton]

though apply still generates side conditions

[Mario Carneiro]

I think that's something else

[Bryan Gin-ge Chen]

Can you build mathlib? :rolling_on_the_floor_laughing:

[Reid Barton]

Can you build mathlib? :rolling_on_the_floor_laughing:

in progress

[Reid Barton]

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]

Could you give a simple example of the apply behavior?

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

Yep, with the main goal nonempty G first

[Reid Barton]

Actually, hang on

[Reid Barton]

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]

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

[Reid Barton]

PR?

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

[Reid Barton]

but of course it's potentially breaking compatibility

[Mario Carneiro]

if mathlib builds, I think this should be safe

[Mario Carneiro]

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

[Mario Carneiro]

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]

Mathlib did build

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

yes

[Reid Barton]

OK, right

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

(deleted)