unfolding notation in theorem vs def/instance

Stream: general

[Kenny Lau]

instance pi.comm_ring_i {I : Type*} {f : I → Type*} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
⊢ ∀ (a b c : Π (i : I), f i),
    (λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i))
        ((λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) a b)
        c =
      (λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) a
        ((λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) b c)
-/

theorem pi.comm_ring_t {I : Type*} {f : I → Type*} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
⊢ ∀ (a b c : Π (i : I), f i), a * b * c = a * (b * c)
-/

[Kenny Lau]

The extra unfolding in def and instance is making things harder (I did not include example of def)

[Kenny Lau]

i.e. the * becoming semigroup.mul

[Kenny Lau]

how can I avoid this? is this a bug?

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

@Sebastian Ullrich

[Kenny Lau]

thanks

[Kenny Lau]

temporary workaround: change it to theorem where it doesn't unfold, copy the goal, use change/show, and then switch back to def

[Sebastian Ullrich]

I'm not sure what is happening just by looking at it... but I'll leave for a short trip until Sunday soon

[Patrick Massot]

I see that all the time. It's indeed a bit annoying

[Kenny Lau]

@Sebastian Ullrich

[Kenny Lau]

@Mario Carneiro

[Sebastian Ullrich]

I'd have to go back to a debug build of Lean 3 to diagnose this, but it won't be fixed for Lean 3 anyway...

[Kevin Buzzard]

So just to be clear -- there is no point noting this down as an issue anywhere on github, because we all know it won't be fixed in Lean 3, and because Lean 4 is a complete rewrite it's very unlikely that the issue will remain in Lean 4? Or could it be the case that when Lean 4 comes, exactly the same issue will be there because chunks of code were basically copied from Lean 3, and then this issue should be marked as something which should be fixed in the future. What I'm trying to establish is whether this trickle of minor Lean 3 points which will not be fixed in Lean 3 should be recorded somewhere anyway, just to check Lean 4 does not suffer from the same problems. If the chances of Lean 4 suffering from the same problem is 0% then in this case there is no point recording anything formally.

[Sebastian Ullrich]

It's hard to say in general. There seems to be some bug somewhere in the elaborator here, which may very well survive into Lean 4 if we don't fix it specifically. _However_, Kenny's example will likely work because Lean 4 will elaborate the type and body of a def/instance separately if the former is given explicitly - so just like for theorem.

[Kenny Lau]

holy mother I found a workaround

[Kenny Lau]

universes u v

instance pi.comm_ring_i {I : Type*} {f : I → Type*} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
⊢ ∀ (a b c : Π (i : I), f i),
    (λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i))
        ((λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) a b)
        c =
      (λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) a
        ((λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) b c)
-/

instance pi.comm_ring_i_uv {I : Type u} {f : I → Type v} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
⊢ ∀ (a b c : Π (i : I), f i), a * b * c = a * (b * c)
-/

theorem pi.comm_ring_t {I : Type*} {f : I → Type*} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
⊢ ∀ (a b c : Π (i : I), f i), a * b * c = a * (b * c)
-/

[Kenny Lau]

@Patrick Massot @Sebastian Ullrich @Mario Carneiro it can be avoided by using universes instead of Type*

[Sebastian Ullrich]

Wow, nice find. Then I can probably explain it - there is some tricky code in the structure notation elaborator that needs to unfold terms that contain metavariables - apparently it also does that for universe mvars, which it probably shouldn't do. As I said above, when you use theorem, the body is elaborated separately from the type, so the mvars have already been solved.

[Mario Carneiro]

well, that was unexpected

[Kenny Lau]

finally something unexpected :P

[Johan Commelin]

I'm going to check if this will also simplify my code, and if it removes some of the issues that I've been have lately.

[Johan Commelin]

But it will have to wait till Monday before I get back to Lean.

[Kevin Buzzard]

I write all my code just using Type. I believe in ZFC!

[Kenny Lau]

Can we solve this 2-year-old problem now by changing the C++ code?

[Kenny Lau]

recap:

universes u v

instance pi.comm_ring_i {I : Type*} {f : I → Type*} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
I : Type ?,
f : I → Type ?,
_inst_1 : Π (i : I), semigroup (f i)
⊢ ∀ (a b c : Π (i : I), f i),
    (λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i))
        ((λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) a b)
        c =
      (λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) a
        ((λ (x y : Π (i : I), f i) (i : I), semigroup.mul (x i) (y i)) b c)
-/

instance pi.comm_ring_i_uv {I : Type u} {f : I → Type v} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
I : Type u,
f : I → Type v,
_inst_1 : Π (i : I), semigroup (f i)
⊢ ∀ (a b c : Π (i : I), f i), a * b * c = a * (b * c)
-/

theorem pi.comm_ring_t {I : Type*} {f : I → Type*} [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := λ x y i, x i * y i,
  mul_assoc := _, }

/-
I : Type u_1,
f : I → Type u_2,
_inst_1 : Π (i : I), semigroup (f i)
⊢ ∀ (a b c : Π (i : I), f i), a * b * c = a * (b * c)
-/

[Kevin Buzzard]

Open an issue in the forked Lean repo.

[Kenny Lau]

https://github.com/leanprover-community/lean/issues/214

[Kenny Lau]

push