Need help with class instance resolution

Stream: general

[Yury G. Kudryashov]

Hi, I'm trying to make algebra work with semirings and semimodules, see #2303. Lean fails to find an instance of algebra R (matrix n R) in lie_algebra.lean. I've enables trace.class_instances, see build log. It seems that matrix_algebra fails defeq. Why could this happen?

[Kevin Buzzard]

import algebra.lie_algebra

example (R : Type) [comm_ring R] (n : ℕ) :
  algebra R (matrix (fin n) (fin n) R) :=
by apply_instance -- works

example (R : Type) [comm_ring R] (n : Type) [fintype n] :
  algebra R (matrix n n R) :=
by apply_instance -- fails

What definition of matrix are you using? (what you posted doesn't typecheck for me)

[Yury G. Kudryashov]

I'm talking about the bottom of lie_algebra.lean

[Kevin Buzzard]

matrix n n R

[Yury G. Kudryashov]

It compiles with master but fails in my branch, probably because of some semiring vs ring or semimodule vs module issues.

[Yury G. Kudryashov]

In the build log you can see that it tries to apply matrix_algebra but fails.

[Kevin Buzzard]

The above doesn't compile for me on master:

failed to synthesize type class instance for
R : Type,
_inst_1 : comm_ring R,
n : Type,
_inst_2 : fintype n
⊢ ring (matrix n n R)

[Yury G. Kudryashov]

That's interesting.

[Kevin Buzzard]

import algebra.lie_algebra

def X : ℕ := 3

open_locale classical

noncomputable example (R : Type) [comm_ring R] (n : Type) [fintype n] :
  algebra R (matrix n n R) := by apply_instance

[Kevin Buzzard]

Need decidable equality on n

[Kevin Buzzard]

(the def to work around open_locale bug)

[Yury G. Kudryashov]

Don't we have a decidable equality on fin n? And we have it at the bottom of lie_algebra

[Yury G. Kudryashov]

You've posted code snippet with fin n, then error for {n : Type*} [fintype n]

[Kevin Buzzard]

Yes, I was confused by n. I'll fix. Thanks.

[Yury G. Kudryashov]

And this doesn't help with the original question: why lie_algebra fails to compile in my branch?

[Yury G. Kudryashov]

Probably this issue is similar to what @Sebastien Gouezel had when he tried to make linear_maps work with semimodules

[Yury G. Kudryashov]

Ping here...

[Yury G. Kudryashov]

@Reid Barton I'd prefer some hint...

[Sebastien Gouezel]

I have tried (again) to refactor things to replace module by semimodule everywhere, hoping that Lean 3.7 would help. I run into issues I don't understand (mostly with product types), with class instance resolution as usual. I have tracked down the source of my problem to the following example. Open current mathlib master, and put the following lines at Line 85 in algebra/pi_instances.lean (after the semimodule instance, but before the module instance)

lemma ok (α : Type) [ring α] (β : Type) :
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@pi.add_comm_monoid.{0 0} β (λ (a : β), α)
  (λ (i : β), @semiring.to_add_comm_monoid.{0} α (@ring.to_semiring.{0} α _inst_1)))  := by apply_instance -- ok

lemma not_ok (α : Type) [ring α] (β : Type) :
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@add_comm_group.to_add_comm_monoid.{0} (β → α)
  (@pi.add_comm_group.{0 0} β (λ (a : β), α)
  (λ (i : β), @ring.to_add_comm_group.{0} α _inst_1))) := by apply_instance -- fails

lemma but_same (α : Type) [ring α] (β : Type) :
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@pi.add_comm_monoid.{0 0} β (λ (a : β), α)
  (λ (i : β), @semiring.to_add_comm_monoid.{0} α (@ring.to_semiring.{0} α _inst_1)))
  =
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@add_comm_group.to_add_comm_monoid.{0} (β → α)
  (@pi.add_comm_group.{0 0} β (λ (a : β), α)
  (λ (i : β), @ring.to_add_comm_group.{0} α _inst_1))) := rfl

In ok and not_ok, I am asking if the same type, but presented in two different ways, is a semimodule. The first one works, the second one fails. The last lemma in the snippet is to show that the types are really the same. In current master, the following module instance saves the day, because it can then be used to show that not_ok is a semimodule, so when this class instance question appears later on it is solved. In my refactoring, I remove modules, so I remove the pi_instance for modules, and now this instance fails. Of course, I could add it back (with semimodules), but it doesn't feel like a real solution. Do you understand what is going on, and what I should do here?

[Sebastien Gouezel]

Anyone on this typeclass issue? Maybe I should try to bring @Daniel Selsam here.

[Kevin Buzzard]

(@add_comm_group.to_add_comm_monoid.{0} (β → α)
  (@pi.add_comm_group.{0 0} β (λ (a : β), α)
  (λ (i : β), @ring.to_add_comm_group.{0} α _inst_1)))

has type add_comm_monoid (β → α), whereas

(@pi.add_comm_monoid.{0 0} β (λ (a : β), α)
  (λ (i : β), @semiring.to_add_comm_monoid.{0} α (@ring.to_semiring.{0} α _inst_1)))

has type add_comm_monoid (Π (i : β), (λ (a : β), α) i)

[Sebastien Gouezel]

And these are the same thing, right?

[Kevin Buzzard]

Maybe not to the unifier

[Sebastien Gouezel]

At least some parts of Lean know it is the same thing:

lemma foo {α : Type*} {β : Type*} : (β → α) = (Π (i : β), (λ (a : β), α) i) := rfl

[Kevin Buzzard]

For sure, but you know that rw doesn't think they're the same thing

[Kevin Buzzard]

I don't know the answer, I've just taken to looking at the output of

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

recently.

[Kevin Buzzard]

foo is iota reduction or eta expansion or whatever it is called by the CS people, and that's part of rfl but maybe not part of the unifier. But also it might be nothing to do with the problem :-(

[Kevin Buzzard]

Actually rw seems to work fine too

[Kevin Buzzard]

I don't know how to check to see if two terms are syntactically equal in Lean

[Kevin Buzzard]

example (α : Type) [ring α] (β : Type) : β → α :=
begin
  have h : (Π (i : β), (λ (a : β), α) i) = (Π (i : β), (λ (a : β), α) i) := rfl,
  rw h, -- works
  sorry
end

[Sebastien Gouezel]

This is the kind of problem where I feel completely helpless. When even with pp.all I can't see anything bad, I just need to call for help...

[Kevin Buzzard]

Yeah I am interested in learning how to debug these issues. mv_polynomial is defined to be some finsupp after some unfolding, and I saw an mv_polynomial zero and a finsupp zero which add_zero got upset about because of some unification issue but refl worked fine.

[Kevin Buzzard]

pp.all just shows these defeq terms. The question is what the type class inference algorithm is I guess.

[Kevin Buzzard]

With set_option trace.class_instances true, the success

def ok :
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@pi.add_comm_monoid.{0 0} β (λ (a : β), α)
  (λ (i : β), @semiring.to_add_comm_monoid.{0} α (@ring.to_semiring.{0} α _inst_1)))  := begin apply_instance end -- ok

has log

[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) := @pi.semimodule ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6

[class_instances] (1) ?x_6 i : @semimodule α α (@ring.to_semiring α _inst_1) (@semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1)) := @semiring.to_semimodule (?x_15 i) (?x_16 i)

[Kevin Buzzard]

(I skipped a couple of steps and just showed the successful route to the success) and the failure has a longer log.

[Kevin Buzzard]

The very first line of the gist is

[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @pi.semimodule ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq

so it tries to use pi.semimodule but here it fails.

[Kevin Buzzard]

I think this is the precise point where the typeclass algorithm decides to go in two different ways for your two different questions.

[Kevin Buzzard]

variables (α : Type) [ring α] (β : Type)

def ok' : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) :=
begin
  refine @pi.semimodule _ _ _ _ _ _,
  -- Proof complete!
end

def not_ok' : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
begin
  refine @pi.semimodule _ _ _ _ _ _, -- fails
  /-
  invalid type ascription, term has type
  semimodule ?m_1 (Π (i : ?m_2), ?m_3 i) : Type (max ? ? ?)
but is expected to have type
  semimodule α (β → α) : Type
  -/
end

[Kevin Buzzard]

I think @Reid Barton and @Gabriel Ebner were talking about this kind of unification issue quite recently.

[Kevin Buzzard]

The types of ok' and not_ok' are defeq.

[Kevin Buzzard]

Of course I am in no position to be able to tell you what to do about it, I'm just observing that with set_option trace.class_instances true you can diagnose what is going on even if you know as little about computers as me.

[Kevin Buzzard]

The first difference in the trace.type_context.is_def_eq true logs is that in the OK case, we have

[type_context.is_def_eq] semimodule ?m_1 (Π (i : ?m_2), ?m_3 i) =?= semimodule α (β → α) ... success  (approximate mode)

and in the not OK case, we have

[type_context.is_def_eq] semimodule ?m_1 (Π (i : ?m_2), ?m_3 i) =?= semimodule α (β → α) ... failed  (approximate mode)

So that is a diagnosis of the failure, which might help someone else to tell you how to fix it.

[Reid Barton]

These lines are the same up to success/failed, right?

[Kevin Buzzard]

Yes, but I didn't have the detailed version on

[Reid Barton]

are these logs with pp.all? is that what you mean?

[Kevin Buzzard]

oh no, i have pp.all off

[Kevin Buzzard]

I meant I didn't have trace.type_context.is_def_eq_detail on

[Reid Barton]

Well, I imagine/hope there must be some difference between the pp.all versions.

[Reid Barton]

Ah.

[Kevin Buzzard]

Here is the pp.all unification failure:

[type_context.is_def_eq] @semimodule.{?l_1 (max ?l_2 ?l_3)} ?m_4 (Π (i : ?m_5), ?m_6 i) ?m_7
  (@pi.add_comm_monoid.{?l_2 ?l_3} ?m_5 (λ (i : ?m_5), ?m_6 i) (λ (i : ?m_5), ?m_8 i)) =?= @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@add_comm_group.to_add_comm_monoid.{0} (β → α)
     (@pi.add_comm_group.{0 0} β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group.{0} α _inst_1))) ... failed  (approximate mode)

and here is the success:

[type_context.is_def_eq] @semimodule.{?l_1 (max ?l_2 ?l_3)} ?m_4 (Π (i : ?m_5), ?m_6 i) ?m_7
  (@pi.add_comm_monoid.{?l_2 ?l_3} ?m_5 (λ (i : ?m_5), ?m_6 i) (λ (i : ?m_5), ?m_8 i)) =?= @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@pi.add_comm_monoid.{0 0} β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid.{0} α (@ring.to_semiring.{0} α _inst_1))) ... success  (approximate mode)

[Kevin Buzzard]

So now you can all play the unification game at home

[Reid Barton]

Okay so there is a diamond here, when putting an add_comm_monoid structure on a product of rings.

[Reid Barton]

we could (1) forget from ring to add_comm_group, (2) use the pi instance, (3) forget from add_comm_group to add_comm_monoid.
Or (1) forget from ring to semiring, (2) forget from ring to add_comm_monoid, (3) use the pi instance.

[Reid Barton]

question 1: are these defeq?

[Reid Barton]

I'm pretty sure the answer will be yes

[Reid Barton]

question 2: are they defeq using "instance transparency", that is, only looking into the definitions of things which are either reducible or instances (and not, for example, the definition of id)

[Reid Barton]

I imagine the answer will be no, otherwise both should succeed (or fail).

[Reid Barton]

I see from #print pi.add_comm_monoid:

add := λ (a a_1 : Π (i : I), f i), id (λ (i : I), add_comm_monoid.add (a i) (a_1 i)),

[Kevin Buzzard]

-- the full semimodule instance
example : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
  @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
rfl -- succeeds

-- instance transparency version for the full semimodule instance
example : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
  @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
by tactic.reflexivity tactic.transparency.reducible -- succeeds

-- But now let's look at the subterms giving the add_comm_monoid structure
example : (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
rfl -- succeeds

example : (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
by tactic.reflexivity tactic.transparency.reducible -- fails!

[Reid Barton]

oh, actually that field is probably not a problem, since pi.add_comm_group's add has id in the same place.

[Reid Barton]

zero := eq.mpr pi.add_comm_group._proof_2 (λ (_x : I), add_comm_group.zero (f _x)),

This certainly looks silly

[Kevin Buzzard]

Reid I think my snippet shows that the semimodule terms are defeq even using instance transparency, but they have defeq subterms which are not defeq using instance transparency. I am pretty much at the boundary of my understanding here, I am just posting stuff like by tactic.reflexivity tactic.transparency.reducible copying from posts Gabriel made earlier this week and am not even 100% sure that I am checking what you are asking.

[Reid Barton]

I think you want tactic.transparency.instances not reducible

[Kevin Buzzard]

Eveything succeeds if I change reducible to instances

[Reid Barton]

@Gabriel Ebner help

[Kevin Buzzard]

example : (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
by tactic.reflexivity tactic.transparency.instances -- works

[Gabriel Ebner]

@Reid Barton MWE please.

[Kevin Buzzard]

I'll do it

[Reid Barton]

I'm really confused about your 2nd and 4th examples. Isn't semimodule just a constant? How can adding it turn a failing unification problem into one which succeeds?

[Reid Barton]

Actually these examples are "easier" than the original failing instance search problem, because here we gave Lean both sides

[Reid Barton]

Not to sound like a broken record, but life would be simpler if we didn't allow diamonds and add_comm_group.to_add_comm_monoid wasn't an instance.

[Kevin Buzzard]

import algebra.pi_instances

variables (α : Type) [ring α] (β : Type)

def ok' : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) :=
by apply_instance -- succeeds

def not_ok' : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
sorry
--by apply_instance -- fails

example : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
     @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)))
     := by tactic.reflexivity tactic.transparency.reducible -- succeeds

[Gabriel Ebner]

The second apply_instance works for me.

[Kevin Buzzard]

curses, I might be using some modified mathlib

[Kevin Buzzard]

oh yeah, you need to add an #exit in algebra.pi_instances :-/

[Gabriel Ebner]

Is this meant seriously? Where should I put it?

[Kevin Buzzard]

How about

import order.basic
import algebra.group.prod
import algebra.module
import data.finset
import ring_theory.subring
import tactic.pi_instances

namespace pi
universes u v w
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances
variables (x y : Π i, f i) (i : I)

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ i, 0⟩
@[simp] lemma zero_apply [∀ i, has_zero $ f i] : (0 : Π i, f i) i = 0 := rfl

instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ i, 1⟩
@[simp] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl

attribute [to_additive] pi.has_one
attribute [to_additive] pi.one_apply

instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ x y, λ i, x i + y i⟩
@[simp] lemma add_apply [∀ i, has_add $ f i] : (x + y) i = x i + y i := rfl

instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ x y, λ i, x i * y i⟩
@[simp] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl

attribute [to_additive] pi.has_mul
attribute [to_additive] pi.mul_apply

instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ x, λ i, (x i)⁻¹⟩
@[simp] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl

instance has_neg [∀ i, has_neg $ f i] : has_neg (Π i : I, f i) := ⟨λ x, λ i, -(x i)⟩
@[simp] lemma neg_apply [∀ i, has_neg $ f i] : (-x) i = -x i := rfl

attribute [to_additive] pi.has_inv
attribute [to_additive] pi.inv_apply

instance has_scalar {α : Type*} [∀ i, has_scalar α $ f i] : has_scalar α (Π i : I, f i) := ⟨λ s x, λ i, s • (x i)⟩
@[simp] lemma smul_apply {α : Type*} [∀ i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl

instance semigroup          [∀ i, semigroup          $ f i] : semigroup          (Π i : I, f i) := by pi_instance
instance comm_semigroup     [∀ i, comm_semigroup     $ f i] : comm_semigroup     (Π i : I, f i) := by pi_instance
instance monoid             [∀ i, monoid             $ f i] : monoid             (Π i : I, f i) := by pi_instance
instance comm_monoid        [∀ i, comm_monoid        $ f i] : comm_monoid        (Π i : I, f i) := by pi_instance
instance group              [∀ i, group              $ f i] : group              (Π i : I, f i) := by pi_instance
instance comm_group         [∀ i, comm_group         $ f i] : comm_group         (Π i : I, f i) := by pi_instance
instance add_semigroup      [∀ i, add_semigroup      $ f i] : add_semigroup      (Π i : I, f i) := by pi_instance
instance add_comm_semigroup [∀ i, add_comm_semigroup $ f i] : add_comm_semigroup (Π i : I, f i) := by pi_instance
instance add_monoid         [∀ i, add_monoid         $ f i] : add_monoid         (Π i : I, f i) := by pi_instance
instance add_comm_monoid    [∀ i, add_comm_monoid    $ f i] : add_comm_monoid    (Π i : I, f i) := by pi_instance
instance add_group          [∀ i, add_group          $ f i] : add_group          (Π i : I, f i) := by pi_instance
instance add_comm_group     [∀ i, add_comm_group     $ f i] : add_comm_group     (Π i : I, f i) := by pi_instance
instance semiring           [∀ i, semiring           $ f i] : semiring           (Π i : I, f i) := by pi_instance
instance ring               [∀ i, ring               $ f i] : ring               (Π i : I, f i) := by pi_instance
instance comm_ring          [∀ i, comm_ring          $ f i] : comm_ring          (Π i : I, f i) := by pi_instance

instance mul_action     (α) {m : monoid α}                                      [∀ i, mul_action α $ f i]     : mul_action α (Π i : I, f i) :=
{ smul := λ c f i, c • f i,
  mul_smul := λ r s f, funext $ λ i, mul_smul _ _ _,
  one_smul := λ f, funext $ λ i, one_smul α _ }

instance distrib_mul_action (α) {m : monoid α}         [∀ i, add_monoid $ f i]      [∀ i, distrib_mul_action α $ f i] : distrib_mul_action α (Π i : I, f i) :=
{ smul_zero := λ c, funext $ λ i, smul_zero _,
  smul_add := λ c f g, funext $ λ i, smul_add _ _ _,
  ..pi.mul_action _ }

instance semimodule     (α) {r : semiring α}       [∀ i, add_comm_monoid $ f i] [∀ i, semimodule α $ f i]     : semimodule α (Π i : I, f i) :=
{ add_smul := λ c f g, funext $ λ i, add_smul _ _ _,
  zero_smul := λ f, funext $ λ i, zero_smul α _,
  ..pi.distrib_mul_action _ }

variables (α : Type) [ring α] (β : Type)

def ok' : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) :=
by apply_instance -- succeeds

def not_ok' : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) :=
sorry
--by apply_instance -- fails

example : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@pi.add_comm_monoid β (λ (a : β), α)
     (λ (i : β), @semiring.to_add_comm_monoid α (@ring.to_semiring α _inst_1))) =
     @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1)))
     := by tactic.reflexivity tactic.transparency.reducible -- succeeds

[Kevin Buzzard]

That is like the first third of algebra.pi_instances

[Gabriel Ebner]

Ok, fails for me now.

[Kevin Buzzard]

I stop just before the line

instance module         (α) {r : ring α}           [∀ i, add_comm_group $ f i]  [∀ i, module α $ f i]         : module α (Π i : I, f i)       := {..pi.semimodule I f α}

[Sebastien Gouezel]

In the first message of the thread, I said to put it just before the module instance.

[Kevin Buzzard]

The reason I stop here is that Sebastien is trying to remove module from this part of the story and use only semimodule.

[Gabriel Ebner]

Why is there an eq.mpr in the 0 in pi.add_comm_monoid?

@[instance]
protected def pi.add_comm_monoid : Π {I : Type u} {f : I → Type v} [_inst_1 : Π (i : I), add_comm_monoid (f i)], add_comm_monoid (Π (i : I), f i) :=
λ {I : Type u} {f : I → Type v} [_inst_1 : Π (i : I), add_comm_monoid (f i)],
  {add := λ (a a_1 : Π (i : I), f i), id (λ (i : I), add_comm_monoid.add (a i) (a_1 i)),
   add_assoc := _,
   zero := eq.mpr add_comm_monoid._proof_2 (λ (_x : I), add_comm_monoid.zero (f _x)),
   zero_add := _,
   add_zero := _,
   add_comm := _}

[Gabriel Ebner]

With this modifications, the not_ok' works for me:

instance add_comm_monoid    [∀ i, add_comm_monoid    $ f i] : add_comm_monoid    (Π i : I, f i) :=
{ add := λ a b i, a i + b i,
  zero := λ i, 0,
  add_assoc := by simp,
  add_comm := by intros a b; ext; simp; cc,
  zero_add := by intro a; ext; simp,
  add_zero := by intro a; ext; simp, }

instance semimodule
    (α) {r : semiring α}
           [m : ∀ i, add_comm_monoid $ f i]
           [∀ i, semimodule α $ f i]     :
           @semimodule α (Π i : I, f i) r (@pi.add_comm_monoid I f m)
            :=
{ add_smul := λ c f g, funext $ λ i, add_smul _ _ _,
  zero_smul := λ f, funext $ λ i, zero_smul α _,
  ..pi.distrib_mul_action _ }

[Gabriel Ebner]

Previously, there was an eq.mpr in the 0 of pi.add_comm_monoid (this is bad for unification, don't do that). There were also the η-expansions λ i, f i and λ i, m i in pi.semimodule, try to avoid those as well.

[Mario Carneiro]

I'm not sure what in pi_instance is causing that. Would apply insert id terms in the goal?

[Yury G. Kudryashov]

I tried to understand the magic in by pi_instance some time ago, and failed.

[Yury G. Kudryashov]

Could someone explain me what happens in derive_field in tactic/pi_instances (the "else" branch)?

[Yury G. Kudryashov]

BTW, the following fails (tried to write this instead of the current instance):

instance add_comm_group     [∀ i, add_comm_group     $ f i] : add_comm_group     (Π i : I, f i) :=
{ .. pi.add_comm_monoid, .. show add_comm_group (Π i, f i), by pi_instance }

[Yury G. Kudryashov]

Here is the code of the else branch:

     field ← get_current_field,
     e ← mk_const field,
     expl_arity ← get_expl_arity e,
     xs ← (iota expl_arity).mmap $ λ _, intro1,
     x ← intro1,
     applyc field,
     xs.mmap' (λ h, try $
      () <$ (apply (h x) <|> apply h) <|>
      refine ``(set.image ($ %%x) %%h)) <|> fail "args",
     return ()

[Yury G. Kudryashov]

Rewriting pi-instances by hand doesn't help.

[Yury G. Kudryashov]

I tried the following:

import order.basic
import algebra.group.prod
import algebra.module
import data.finset
import ring_theory.subring
import tactic.pi_instances

namespace pi
universes u v w
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances
variables (x y : Π i, f i) (i : I)

@[to_additive]
instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ i, 1⟩
@[to_additive, simp] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl

@[to_additive] instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) :=
⟨λ x y, λ i, x i * y i⟩
@[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl

@[to_additive] instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ x, λ i, (x i)⁻¹⟩
@[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl

instance has_scalar {α : Type*} [∀ i, has_scalar α $ f i] : has_scalar α (Π i : I, f i) :=
⟨λ s x, λ i, s • (x i)⟩
@[simp] lemma smul_apply {α : Type*} [∀ i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl

@[to_additive add_semigroup]
instance semigroup          [∀ i, semigroup          $ f i] : semigroup          (Π i : I, f i) :=
by refine_struct { mul := (*) }; tactic.derive_field

@[to_additive add_comm_semigroup]
instance comm_semigroup     [∀ i, comm_semigroup     $ f i] : comm_semigroup     (Π i : I, f i) :=
by refine_struct { mul := (*) }; tactic.derive_field

@[to_additive add_monoid]
instance monoid             [∀ i, monoid             $ f i] : monoid             (Π i : I, f i) :=
by refine_struct { one := (1 : Π i, f i), mul := (*) }; tactic.derive_field

@[to_additive add_comm_monoid]
instance comm_monoid        [∀ i, comm_monoid        $ f i] : comm_monoid        (Π i : I, f i) :=
by refine_struct { one := (1 : Π i, f i), mul := (*) }; tactic.derive_field

@[to_additive add_group]
instance group              [∀ i, group              $ f i] : group              (Π i : I, f i) :=
by refine_struct { inv := has_inv.inv, one := (1 : Π i, f i), mul := (*) }; tactic.derive_field

@[to_additive add_comm_group]
instance comm_group         [∀ i, comm_group         $ f i] : comm_group         (Π i : I, f i) :=
by refine_struct { inv := has_inv.inv, one := (1 : Π i, f i), mul := (*) }; tactic.derive_field

instance semiring           [∀ i, semiring           $ f i] : semiring           (Π i : I, f i) :=
by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*) }; tactic.derive_field

instance ring               [∀ i, ring               $ f i] : ring               (Π i : I, f i) :=
by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), neg := has_neg.neg }; tactic.derive_field

instance comm_ring          [∀ i, comm_ring          $ f i] : comm_ring          (Π i : I, f i) :=
by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), neg := has_neg.neg }; tactic.derive_field

instance mul_action     (α) {m : monoid α}                                      [∀ i, mul_action α $ f i]     : mul_action α (Π i : I, f i) :=
{ smul := λ c f i, c • f i,
  mul_smul := λ r s f, funext $ λ i, mul_smul _ _ _,
  one_smul := λ f, funext $ λ i, one_smul α _ }

instance distrib_mul_action (α) {m : monoid α}         [∀ i, add_monoid $ f i]      [∀ i, distrib_mul_action α $ f i] : distrib_mul_action α (Π i : I, f i) :=
{ smul_zero := λ c, funext $ λ i, smul_zero _,
  smul_add := λ c f g, funext $ λ i, smul_add _ _ _,
  ..pi.mul_action _ }

variables (I f)

instance semimodule     (α) {r : semiring α}       [∀ i, add_comm_monoid $ f i] [∀ i, semimodule α $ f i]     : semimodule α (Π i : I, f i) :=
{ add_smul := λ c f g, funext $ λ i, add_smul _ _ _,
  zero_smul := λ f, funext $ λ i, zero_smul α _,
  ..pi.distrib_mul_action _ }

variables {I f}

lemma ok (α : Type) [ring α] (β : Type) :
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@pi.add_comm_monoid.{0 0} β (λ (a : β), α)
  (λ (i : β), @semiring.to_add_comm_monoid.{0} α (@ring.to_semiring.{0} α _inst_1)))  := by apply_instance -- ok

lemma not_ok (α : Type) [ring α] (β : Type) :
  @semimodule.{0 0} α (β → α) (@ring.to_semiring.{0} α _inst_1)
  (@add_comm_group.to_add_comm_monoid.{0} (β → α)
  (@pi.add_comm_group.{0 0} β (λ (a : β), α)
  (λ (i : β), @ring.to_add_comm_group.{0} α _inst_1))) := by apply_instance -- fails
end pi

[Yury G. Kudryashov]

And I don't see the difference between my instances and @Gabriel Ebner 's

[Yury G. Kudryashov]

Ah, I didn't apply his patch to semimodule.

[Scott Morrison]

Regarding this eq.mpr ---- I put a lot of effort in the transport tactic to ensure none of these turned up in transported structures.

[Scott Morrison]

I haven't looked at this case, but we should ping @Simon Hudon to ask about pi_instances, I think.

[Scott Morrison]

When writing transport, I found that often the eq.mprs (and even theeq.recs) that were being produced were actually trivial:

[Scott Morrison]

when you looked at the equality you were running eq.mpr along, it was in fact refl, and eq_mpr_refl (only recently inmaster) would reduce it.

[Scott Morrison]

Sometimes it was very hard to avoid the eq.mpr being generated, and you had to intercept it after the fact with the simp_result tactic introduced in #2251.

[Simon Hudon]

I haven't spent much time looking at eq.mp. @Scott Morrison I think you know more than me on the topic

[Yury G. Kudryashov]

How do I add debug output to a tactic script? Do we have something more convenient than trace?

[Yury G. Kudryashov]

I just want to prepend string labels to output strings.

[Simon Hudon]

You could write your own that does:

meta def my_trace (msg : string) : tactic unit := trace ("prefix: " ++ msg)

[Scott Morrison]

Ok, so wrapping pi_instance in simp_result does make the eq.mpr in #print pi.add_comm_monoid go away.

[Scott Morrison]

So I think this counts as a fix to @Sebastien Gouezel's original problem?

[Scott Morrison]

How should we implement it?

[Scott Morrison]

I can make a PR that just patches pi_instances to use simp_result. (Presumably I will play with squeeze_simp to identify exactly which simp lemmas simp_result actually needs.

[Scott Morrison]

And then @Sebastien Gouezel can continue his branch on top of that?

[Yury G. Kudryashov]

Sounds like a good idea.

[Scott Morrison]

We will need to remember to make @Gabriel Ebner's patch to the semimodule instance in pi_instances, but I think this can be done in @Sebastien Gouezel's branch, as this is a separate issue from the automation problem.

[Reid Barton]

This seems super hacky. Couldn't we just build the correct term in the first place using structural recursion on the shape of the operation we want to define?

[Yury G. Kudryashov]

Can you do this? It seems that either applyc or apply generates this eq.mpr.

[Yury G. Kudryashov]

No, for one somehow intro1 closes the goal.

[Yury G. Kudryashov]

And generates eq.mpr.

[Yury G. Kudryashov]

intro_core does the same.

[Yury G. Kudryashov]

How do I print debug current proof state (i.e., what Lean normally prints in "goals" in the tactic proof mode)?

[Scott Morrison]

Dumb eq.mprs seem hard to avoid. :-(

[Scott Morrison]

But maybe we can go into the C++?

[Yury G. Kudryashov]

I found out the difference between 1 and mul.

[Yury G. Kudryashov]

For mul, expl_arity = 2, and after two intro1, the goal is Π i, f i

[Yury G. Kudryashov]

For one, expl_arity = 1, and after one intro1, the goal is f i.

[Reid Barton]

What I had in mind was to just build the required expr directly from the constructors.

[Yury G. Kudryashov]

My tactic programming skills are, let's say, far from being good.

[Reid Barton]

exactly, don't use tactics!

[Yury G. Kudryashov]

What do you propose?

[Yury G. Kudryashov]

Should we have pi_instance tactic or not?

[Yury G. Kudryashov]

Of course, we can leave only Prop branch, and use := by refine_struct { one := (1 : Π i, f i) }; pi_props

[Yury G. Kudryashov]

This will give us all the required defeq's.

[Yury G. Kudryashov]

But if we want to generate all fields automatically, then we need some meta code analyzing the target.

[Yury G. Kudryashov]

The current code works well for unary and binary operations but fails for constants.

[Scott Morrison]

The

xs.mmap' (λ h, try $
      () <$ (apply (h x) <|> apply h) <|>
      refine ``(set.image ($ %%x) %%h)) <|> fail "args",

block deserves some documentation. :-)

[Scott Morrison]

(but I think is unrelated to what we're seeing at the moment)

[Yury G. Kudryashov]

@Scott Morrison I added some traces, and the goal one is closed by x ← intro1

[Scott Morrison]

how does the rest of the tactic not fail, then?

[Scott Morrison]

doesn't applyc choke when there's no goal?

[Scott Morrison]

I'm confused

[Yury G. Kudryashov]

It just exits. At least trace doesn't print anything.

[Reid Barton]

It seems easy to get the target type and appropriate bits of the context and compute by a pure function the term which we should produce.

[Reid Barton]

I can't try right now because I need to prepare a seminar for tomorrow

[Yury G. Kudryashov]

I don't understand how this manages to define pi.monoid:

namespace tactic

open interactive interactive.types lean.parser expr
open functor has_seq list nat tactic.interactive

set_option pp.all true
meta def derive_field' : tactic unit :=
do b ← target >>= is_prop,
   field ← get_current_field,
   if b then do
     field ← get_current_field,
     vs ← introv [] <|> pure [],
     hs ← intros <|> pure [],
     resetI,
     x ← get_unused_name,
     try (() <$ ext1 [rcases_patt.one x] <|> () <$ intro x),
     x' ← try_core (get_local x),
     applyc field,
     hs.mmap (λ h, try $
       () <$ (to_expr ``(congr_fun %%h %%(x'.iget)) >>= apply) <|>
       () <$ apply (h x'.iget) <|>
       () <$ (to_expr ``(set.mem_image_of_mem _ %%h) >>= apply) <|>
       () <$ (solve_by_elim) ),
     return ()
   else focus1 $ do
     field ← get_current_field,
     e ← mk_const field,
     expl_arity ← get_expl_arity e,
     xs ← (iota expl_arity).mmap $ λ _, intro1,
     t ← target >>= whnf,
     if expr.is_pi t then do
       trace field,
       x ← intro1,
       applyc field,
       xs.mmap' (λ h, apply (h x) <|> apply h),
       return ()
     else return ()

/--
`pi_instance` constructs an instance of `my_class (Π i : I, f i)`
where we know `Π i, my_class (f i)`. If an order relation is required,
it defaults to `pi.partial_order`. Any field of the instance that
`pi_instance` cannot construct is left untouched and generated as a new goal.
-/
meta def pi_instance' : tactic unit :=
refine_struct ``( {  ..pi.partial_order, .. } );
  propagate_tags (try (derive_field' ; done))

run_cmd add_interactive [`pi_instance']

end tactic

[Yury G. Kudryashov]

(I put this at the top of algebra/pi_instances.lean to avoid compiling other files)

[Yury G. Kudryashov]

@Reid Barton May I open an issue and assign it to you?

[Scott Morrison]

oh ....

[Scott Morrison]

I think what is going on is that derive_field is actually _failing_ on one.

[Scott Morrison]

Which by itself is fine, it's wrapped in try.

[Scott Morrison]

However we then plough on trying to derive_field the axioms as well.

[Scott Morrison]

And somehow one is solved by unification at a later step.

[Scott Morrison]

But we mess up and introduce the bad answer there?

[Yury G. Kudryashov]

Indeed!

[Yury G. Kudryashov]

Removed try, and now it fails.

[Scott Morrison]

Yes, look at this, from trace_state at the beginning of solving zero_add:

(@has_zero.zero.{(max u v)} (Π (i : I), f i)
            (@has_zero.mk.{(max u v)} (Π (i : I), f i)
               (@eq.mpr.{(max (u+1) (v+1))} (Π (i : I), f i) (Π (i : I), f i)
                  (@id.{0} (@eq.{(max (u+1) (v+1))+1} (Type (max u v)) (Π (i : I), f i) (Π (i : I), f i))
                     (@eq.refl.{(max (u+1) (v+1))+1} (Type (max u v)) (Π (i : I), f i)))
                  ?m_1)))
         a)

We've just got a metavariable for zero!

[Scott Morrison]

Until you turn pp.all on, you can't even see this. It just happily prints as 0...

[Scott Morrison]

Kind of scary that this was working at all. :-)

[Scott Morrison]

Haha...

[Scott Morrison]

it turns out we've already fixed this issue

[Scott Morrison]

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

[Scott Morrison]

This is the reason why we're seeing arity = 1 on zero and one.

[Scott Morrison]

I suspect that when this gets merged, and we move to Lean 3.8, derive_field will no longer fail, the eq.mpr will disappear, and we'll all be happy.

[Yury G. Kudryashov]

I don't think so. The target is Π i, f i, so it actually has arity = 1

[Scott Morrison]

oh, hrm.

[Yury G. Kudryashov]

BTW, now I'm testing on has_zero instead of monoid.

[Scott Morrison]

I don't think that's what expl_arity is meant to mean. Notice that it is 2 for add, and 1 for zero.

[Scott Morrison]

It should be 2 for add, and 0 for zero.

[Scott Morrison]

With has_zero we'll just see it fail at the x <- intro1 line.

[Yury G. Kudryashov]

This works for has_zero but gives eq.mpr in the result:

namespace tactic

open interactive interactive.types lean.parser expr
open functor has_seq list nat tactic.interactive

meta def derive_field' : tactic unit :=
do b ← target >>= is_prop,
   field ← get_current_field,
   if b then do
     field ← get_current_field,
     vs ← introv [] <|> pure [],
     hs ← intros <|> pure [],
     resetI,
     x ← get_unused_name,
     try (() <$ ext1 [rcases_patt.one x] <|> () <$ intro x),
     x' ← try_core (get_local x),
     applyc field,
     hs.mmap (λ h, try $
       () <$ (to_expr ``(congr_fun %%h %%(x'.iget)) >>= apply) <|>
       () <$ apply (h x'.iget) <|>
       () <$ (to_expr ``(set.mem_image_of_mem _ %%h) >>= apply) <|>
       () <$ (solve_by_elim) ),
     return ()
   else focus1 $ do
     field ← get_current_field,
     e ← mk_const field,
     expl_arity ← get_expl_arity e,
     xs ← (iota expl_arity).mmap $ λ _, intro1,
     t ← target >>= whnf,
     if expr.is_pi t then do
       x ← intro1,
       applyc field,
       xs.mmap' (λ h, apply (h x) <|> apply h),
       return ()
     else
       applyc field,
       return ()

/--
`pi_instance` constructs an instance of `my_class (Π i : I, f i)`
where we know `Π i, my_class (f i)`. If an order relation is required,
it defaults to `pi.partial_order`. Any field of the instance that
`pi_instance` cannot construct is left untouched and generated as a new goal.
-/
meta def pi_instance' : tactic unit :=
refine_struct ``( {  ..pi.partial_order, .. } );
  propagate_tags (derive_field' ; done)

run_cmd add_interactive [`pi_instance']

end tactic

[Scott Morrison]

I see. You're saying that the applyc call introduces an eq.mpr all by itself?

[Scott Morrison]

Can we reproduce that in a standalone tactic block, independent of using pi_instance?

[Yury G. Kudryashov]

How do I try to close the goal using apply e, and do something else if it fails?

[Yury G. Kudryashov]

I mean, inside do block

[Scott Morrison]

<|>

[Scott Morrison]

I'm remaining pretty sure the problem is the expl_arity being reported for one is wrong.

[Scott Morrison]

Your last update to derive_field doesn't make sense.

[Scott Morrison]

The else branch of

if expr.is_pi t then do
       x ← intro1,
       applyc field,
       xs.mmap' (λ h, apply (h x) <|> apply h),
       return ()
     else
       applyc field,
       return ()

really needs to have a x ← intro1 to consume the argument of the Pi type

[Scott Morrison]

Your code is working without it because expl_arity is wrong for zero/one because of the explicit argument in has_zero/has_one that is fixed in that PR I linked above.

[Yury G. Kudryashov]

Try to add trace target before expl_arity.

[Yury G. Kudryashov]

Sorry, you're right.

[Yury G. Kudryashov]

e is has_one.one.

[Scott Morrison]

Actually, while I remain convinced expl_arity is being calculated incorrectly, I no longer believe it's because of this implicit/explict argument inhas_one.

[Scott Morrison]

The target before expl_arity in has_add is

(Π (i : I), f i) → (Π (i : I), f i) → Π (i : I), f i

and we get told 2

[Scott Morrison]

The target before expl_arity in has_zero is

Π (i : I), f i

and we get told 1

[Scott Morrison]

These are not consistent.

[Scott Morrison]

I think in the has_add case it should be 3?

[Scott Morrison]

oh, no, it is the PR I was talking about

[Yury G. Kudryashov]

That's why we have x and xs.
P.S.: Please use syntax highlighting.

[Scott Morrison]

it's not the target that matters, it is e that matters.

[Scott Morrison]

and the expl_arity of add_comm_monoid.add.{?l_1} is (correctly) 2

[Yury G. Kudryashov]

This defines pi.has_one but still produces eq.mpr:

meta def derive_field' : tactic unit :=
do b ← target >>= is_prop,
   field ← get_current_field,
   if b then do
     field ← get_current_field,
     vs ← introv [] <|> pure [],
     hs ← intros <|> pure [],
     resetI,
     x ← get_unused_name,
     try (() <$ ext1 [rcases_patt.one x] <|> () <$ intro x),
     x' ← try_core (get_local x),
     applyc field,
     hs.mmap (λ h, try $
       () <$ (to_expr ``(congr_fun %%h %%(x'.iget)) >>= apply) <|>
       () <$ apply (h x'.iget) <|>
       () <$ (to_expr ``(set.mem_image_of_mem _ %%h) >>= apply) <|>
       () <$ (solve_by_elim) ),
     return ()
   else focus1 $ do
     field ← get_current_field,
     e ← mk_const field,
     expl_arity ← if field = `has_one.one then return 0 else get_expl_arity e,
     xs ← (iota expl_arity).mmap $ λ _, intro1,
     x ← intro_core `_,
     applyc field,
     xs.mmap' (λ h, try $
      () <$ (apply (h x) <|> apply h) <|>
      refine ``(set.image ($ %%x) %%h)) <|> fail "args",
     return ()

[Scott Morrison]

and the expl_arity of has_zero.zero.{?l_1} is (suprisingly) 1

[Scott Morrison]

Interesting, let me try that

[Scott Morrison]

Okay, I agree that is sensible code, and still produces an eq.mpr.

[Yury G. Kudryashov]

Here is an MWE:

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) :=
by refine_struct { .. }; intros; apply has_zero.zero

#print pi.has_zero

[Yury G. Kudryashov]

So it is a bug in refine_struct.

[Yury G. Kudryashov]

It works with refine.

[Scott Morrison]

And a completely standalone example:

import tactic.interactive

namespace pi
universes u v
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) :=
by refine_struct { .. }; propagate_tags (do
  tactic.intro1,
  tactic.applyc `has_zero.zero)

set_option pp.all true
#print pi.has_zero

end pi

[Yury G. Kudryashov]

refine_struct produces an eq.mpr, refine doesn't.

[Yury G. Kudryashov]

And refine_struct is too long for me to understand and catch the bug.

[Scott Morrison]

Yeah, I'm looking through it now. Hopefully @Simon Hudon will stop by sometime. :-)

[Scott Morrison]

I'm worried it falls all the way down to meta constant pexpr.mk_structure_instance : structure_instance_info → pexpr.

[Scott Morrison]

no, that makes no sense, it is just producing something with metavariables: @has_zero.mk.{?l_1} ?m_2 ?m_3

[Scott Morrison]

In

import tactic.interactive

namespace pi
universes u v
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances

set_option pp.all true

open tactic

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) :=
begin
  refine_struct { .. },
  result >>= trace,
  (do
  tactic.intro1,
  tactic.applyc `has_zero.zero)
end

#print pi.has_zero

end pi

You can clearly see that the problem has already occurred by the time we leave refine_struct: the eq.mpr is there no matter how we discharge the goal later.

[Yury G. Kudryashov]

Even shorter:

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) :=
by refine_struct { .. }; exact λ _, 0

[Scott Morrison]

You can wrap the whole refine_struct { .. }; exact λ _, 0 with simp_result, and successfully clear the eq.mpr, but it's not possible to fix refine_struct this way: until the metavariables have been filled in simp_result doesn't work.

[Scott Morrison]

Ok, the eq.mpr in the result is introduced in the line

      gs ← with_enable_tags (
        mzip_with (λ (n : name × name) v, do
           set_goals [v],
           try (interactive.unfold (provided.map $ λ ⟨s,f⟩, f.update_prefix s) (loc.ns [none])),
           apply_auto_param
             <|> apply_opt_param
             <|> (set_main_tag [`_field,n.2,n.1]),
           get_goals)
        missing_f' vs),

in meta def refine_one in tactic/interactive.lean.

[Scott Morrison]

(You can trace_result before and after.)

[Scott Morrison]

And if we comment out the line

try (interactive.unfold (provided.map $ λ ⟨s,f⟩, f.update_prefix s) (loc.ns [none])),

then the problem goes away.

[Yury G. Kudryashov]

Why do we need this line?

[Yury G. Kudryashov]

When I read the code, I wish we had much more comments. Why do I forget about this when I write the code?

[Scott Morrison]

I have no idea. :-)

[Scott Morrison]

:-)

[Scott Morrison]

I will go and add extra comments to all my current PRs. I feel exactly the same way at the moment.

[Scott Morrison]

In fact I'm starting to think this is a bug in core again.

[Scott Morrison]

This interactive.unfold should be failing, on the basis that it's not really changing anything. Except, of course, that it is changing something: introducing this pesky eq.mpr!

[Scott Morrison]

It seems we are calling interactive.unfold [] (loc.ns [none]) here, which means simp_core is being called with no lemmas at all.

[Scott Morrison]

So it has no excuse for doing anything.

[Yury G. Kudryashov]

Can you try to turn it into an MWE?

[Yury G. Kudryashov]

I mean, an example without refine_struct.

[Scott Morrison]

Trying... if we just run

import tactic.interactive

namespace pi
universes u v
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances

set_option pp.all true

open tactic

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) :=
begin
  refine { .. },
  tactic.interactive.unfold [] (interactive.loc.ns [none]),
  result >>= trace,
  exact (λ_, 0),
end

#print pi.has_zero

end pi

[Scott Morrison]

Then unfold correctly fails, saying it has nothing to do.

[Scott Morrison]

But somehow inside refine_struct, with apparently the same goal, it succeeds and introduces the eq.mpr.

[Mario Carneiro]

simp does stuff even with no lemmas

[Mario Carneiro]

like unfolding beta redexes

[Scott Morrison]

and apparently introducing eq.mpr along eq.refl _, just for the fun of it. :-(

[Scott Morrison]

We should call it unsimp here. You need to hit the result with simp [eq_mpr_refl] to get something reasonable back...

[Scott Morrison]

@Simon Hudon, when you notice this thread, don't feel the need to read from the top. We can write a good summary now, we're getting much closer to the source.

[Yury G. Kudryashov]

Usually people call simp when the goal is in Prop, so the exact proof term is not important.

[Scott Morrison]

I just tried commenting out that offending line inside refine_struct. All the tests in test/examples.lean succeed, but maybe they don't test enough.

[Yury G. Kudryashov]

I think that the logic of refine_struct should be changed so that if there is no field with a given name among explicitly provided fields, then it doesn't unfold/simp/whatever.

[Simon Hudon]

What is the status here?

[Yury G. Kudryashov]

The following code generates an eq.mpr in the result:

import tactic.interactive

instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) :=
by refine_struct { .. }; exact λ _, 0

[Yury G. Kudryashov]

@Scott Morrison found the offending line in refine_struct

[Yury G. Kudryashov]

It's

try (interactive.unfold (provided.map $ λ ⟨s,f⟩, f.update_prefix s) (loc.ns [none])),

[Yury G. Kudryashov]

That's all I know. May be @Scott Morrison has more details to add

[Yury G. Kudryashov]

I wonder why refine_struct does something to a goal if there is no field with the same name provided in the { .. } block.

[Yury G. Kudryashov]

And how hard would it be to fix this.

[Simon Hudon]

If we use dunfold instead of unfold, does that solve the problem?

[Yury G. Kudryashov]

No eq.mpr but there is id.

[Yury G. Kudryashov]

Don't know how bad is it for class instances.

[Simon Hudon]

I think it's going to be an issue too. Can you skip that line if the goal is not a prop?

[Yury G. Kudryashov]

I don't understand what happens in refine_one.

[Yury G. Kudryashov]

If you insert this after the definition of refine_struct in tactic.interactive, it will tell you whether the problem is fixed or not:

instance pi.has_one {α : Type*} {β : α → Type*} [Π x, has_one (β x)] : has_one (Π x, β x) :=
by refine_struct { .. }; exact λ _, 1

set_option pp.all true
#print pi.has_one

[Simon Hudon]

refine_struct has to work recursively because structures can extend each other and I have to elaborate one instance at a time

[Simon Hudon]

refine_one takes the definition of a struct and an instance, infers the missing fields, tries to fill them up and tag the left-over goals

[Simon Hudon]

Ok, I think I see how we can do things.

[Simon Hudon]

We can create a copy of the current goal, rewrite it using dunfold, get the new statement with target and use it with change in the original goal

[Yury G. Kudryashov]

What are you doing to fields that are not in provided?

[Simon Hudon]

Creating a meta variable with their type and add it to the list of goals

[Yury G. Kudryashov]

Why do you run unfold on them?

[Simon Hudon]

I think it's because otherwise I can get this kind of expression { add := my_add }.add x y ≤ _

[Yury G. Kudryashov]

I see, they can depend on provided fields.

[Yury G. Kudryashov]

(and Props normally do)

[Simon Hudon]

Yes and I'd rather have my_add x y ≤ _

[Simon Hudon]

I'm heading to bed. Good luck with refine_struct

[Scott Morrison]

We may ask for help again tomorrow. :-)

[Yury G. Kudryashov]

Let's see if #2319 works.