Trouble with simp - failed to assign instance

Stream: lean4

[Tomas Skrivan]

I'm having a problem with simp tactic as it does not want to use certain theorem because of an error failed to assign instance.

I did some investigation and the problem is that I have two instances, SemiHilbert.toVec and instVecℝ, that fails to be proven equal, i.e. isDefEq evaluates to false inside of simp tactic.

The weird thing is that outside of simp tactic the isDefEq evaluates to true. The problem is that whnf inside of the function synthesizeArgs(in Lean/Meta/Tactic/Simp/Rewrite.lean) does not reduce either SemiHilbert.toVec or instVecℝ, but calling whnf on these in a simple file reduces both to:

Vec.mk instVecℝ.proof_1 instVecℝ.proof_2 instVecℝ.proof_3 instVecℝ.proof_4

Therefore there must be some special transparency setting when running simp so that whnf does not reduce these instances. Is that intended behavior? Unfortunately, I was unable simplify this problem to a small example.

[Gabriel Ebner]

#mwe please. In general, type class search uses reducible transparency, so it won't reduce defs but only abbrevs.

[Tomas Skrivan]

Yes I will try to produce MWE, but I was unable to do so without copy pasting few hundreds of lines of code.

[Tomas Skrivan]

I have managed to nail down the problem, here is the mwe:

class Vec (X : Type) extends Add X, Sub X, Inhabited X

class Vec' (X : Type) extends Vec X

instance {X} [Vec X] : Vec' X := ⟨⟩

constant differential {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X) : Y

@[simp]
theorem differential_of_linear {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : differential f x dx = f dx := sorry

example {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : differential f x dx = f dx := by simp

set_option trace.Meta.Tactic.simp true
example {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : @differential _ _ Vec'.toVec _ f x dx = f dx := by simp done -- failed to assign instance

[Tomas Skrivan]

[Tomas Skrivan]

(deleted)

[Gabriel Ebner]

In your example, the two instances are indeed different. inst : Vec X and Vec'.toVec instVec' are not defeq.

[Reid Barton]

Note that in practice this normally won't be a problem because the Vec' instance will be built from the Vec instance in a sensible way, and the definition of differential_of_linear won't be sorry

[Reid Barton]

but it could well be that the simplifier runs with a reducibility setting that doesn't expand the definition of differential_of_linear, yeah

[Tomas Skrivan]

the Vec' instance will be built from the Vec instance in a sensible way

What do you mean by that? Using extends is not a sensible way of doing it?

[Tomas Skrivan]

How can I change the above code such that the second example is solved by simp?

[Reid Barton]

I'm talking about instances of Vec'. Your MWE is too trivial to have interesting examples but in general, if you have instances of both Vec X and Vec' X then you would want to arrange that the fields of the Vec' X instance that came from Vec X are defeq to the corresponding fields of the Vec X instance.

[Reid Barton]

Sorry, it's not differential_of_linear that's the problem, it's differential.

[Reid Barton]

I guess it should work for instance if you make differential a def like def differential {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X) : Y := f x

[Reid Barton]

Maybe simp won't do the rewrite for you, but you could do it by hand at least.

[Tomas Skrivan]

I guess it should work for instance if you make differential a def like def differential {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X) : Y := f x

It does not work for me.

[Reid Barton]

In your current version, the last example is just not provable at all

[Reid Barton]

oh maybe it is provable... sorry, this example is very confusing :face_palm:

[Reid Barton]

OK, let me try again.

[Reid Barton]

simp doesn't do this.

[Tomas Skrivan]

Think about Vec as a vector space and Vec' for example as a finite dimensional vector space. I didn't put full definitions here for brevity.

[Reid Barton]

However, it's usually not a problem because we don't have instances like instance {X} [Vec X] : Vec' X := ⟨⟩ in the real world, and when we want to apply simp to something like add_zero at a specific type T where we might have a funny "non-standard" instance for add_zero_class T, that funny instance will be defeq to the standard one because both of them will reduce to constructor applications with defeq fields.

[Reid Barton]

Not every vector space is finite dimensional, so this is still not a real example

[Tomas Skrivan]

Ohh, the culprit was instance {X} [Vec X] : Vec' X := ⟨⟩ ok then I made incorrect mwe :)

[Reid Barton]

I think for your real situation the question comes down to what reducibility level simp uses to compare instance arguments of lemmas to the synthesized ones. Note that (at least in Lean 3) this is all a bit silly because if you stated your simp lemma using {} binders for the Vec arguments, then simp would just infer their values from the ones that appear in the expression to be simplified, which is generally what you want anyways. I think some of this stuff works differently in Lean 4.

[Tomas Skrivan]

Ok consider this:

class Vec (X : Type) extends Add X, Inhabited X

class Vec' (X : Type) extends Vec X

def differential {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X) : Y := f dx

@[simp]
theorem differential_of_linear {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : differential f x dx = f dx := by simp[differential]

example {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : differential f x dx = f dx := by simp

instance : Vec Float := ⟨⟩
instance : Vec' Float := ⟨⟩

set_option trace.Meta.Tactic.simp true
example {Y : Type} [Vec Y] (f : Float → Y) (x dx : Float)
        : @differential _ _ Vec'.toVec _ f x dx = f dx :=
  by
    simp done

[Reid Barton]

We have some versions of lemmas in mathlib that are formulated to take instance arguments in {} binders rather than [] ones, but usually the reason is that we want to handle cases where the instance that appears in an expression is genuinely different from the synthesized one, or where there is no synthesized one... not where the two instances are actually defeq, but at the wrong reducibility level

[Tomas Skrivan]

It still fails and I do not have a general instance instance {X} [Vec X] : Vec' X := ⟨⟩ but only a specialized one for Float.

[Gabriel Ebner]

Sorry, I think I got some of the stuff wrong here.

1. The instances are defeq after all. The instance [inst : Vec X] : Vec' X := ⟨⟩ is @Vec' X inst under the hood. I mistook it for ⟨⟨⟩⟩.
2. It is weird that simp tries to synthesize this instance in the first place. The instance should have already been assigned via unification. There is an explicit check for this in the simp code.

[Reid Barton]

I don't know, but it works in Lean 3 now:

class Vec (X : Type) -- extends Add X, Inhabited X

class Vec' (X : Type) extends Vec X

def differential {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X) : Y := f dx

@[simp]
theorem differential_of_linear {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : differential f x dx = f dx := by simp[differential]

example {X Y : Type} [Vec X] [Vec Y] (f : X → Y) (x dx : X)
        : differential f x dx = f dx := by simp

instance : Vec nat := ⟨⟩
instance : Vec' nat := ⟨⟩

set_option trace.simplify.rewrite true
example {Y : Type} [Vec Y] (f : nat → Y) (x dx : nat)
        : @differential _ _ Vec'.to_Vec _ f x dx = f dx :=
  by
    simp

[Tomas Skrivan]

Yeah does not work with Lean 4, I'm on nightly-2021-11-10

[Tomas Skrivan]

The simplifier trace:

[Meta.Tactic.simp.discharge] differential_of_linear, failed to assign instance
  Vec Nat

[Tomas Skrivan]

Gabriel Ebner said:

Sorry, I think I got some of the stuff wrong here.

1. The instances are defeq after all. The instance [inst : Vec X] : Vec' X := ⟨⟩ is @Vec' X inst under the hood. I mistook it for ⟨⟨⟩⟩.
2. It is weird that simp tries to synthesize this instance in the first place. The instance should have already been assigned via unification. There is an explicit check for this in the simp code.

The (← isDefEq x val) in the function Lean.Meta.Simp.synthesizeArgs does not seem to produce correct value in this case.

[Gabriel Ebner]

There is an explicit check for this in the simp code.

Oh I take it back. There is a check for "is this mvar already assigned" there. But right above it is: if the argument is instance-implicit, synthesize the instance anyhow...

[Tomas Skrivan]

So is this a bug or a feature? :)

[Tomas Skrivan]

Simply fixing the transparency settings solves the problem.

I do not fully understand the definition of "definitional equality" but should the result of isDefEq depend on transparency settings? If not then the transparency fix should be applied on the level of isDefEq.