Zulip Chat Archive

Stream: general

Topic: unfolding notation in theorem vs def/instance


view this post on Zulip Kenny Lau (May 31 2018 at 02:35):

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)
-/

view this post on Zulip Kenny Lau (May 31 2018 at 02:35):

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

view this post on Zulip Kenny Lau (May 31 2018 at 02:35):

i.e. the * becoming semigroup.mul

view this post on Zulip Kenny Lau (May 31 2018 at 02:37):

how can I avoid this? is this a bug?

view this post on Zulip Kenny Lau (May 31 2018 at 02:37):

@Mario Carneiro

view this post on Zulip Mario Carneiro (May 31 2018 at 02:39):

@Sebastian Ullrich

view this post on Zulip Kenny Lau (May 31 2018 at 02:39):

thanks

view this post on Zulip Kenny Lau (May 31 2018 at 02:39):

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

view this post on Zulip Sebastian Ullrich (May 31 2018 at 06:49):

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

view this post on Zulip Patrick Massot (May 31 2018 at 07:04):

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

view this post on Zulip Kenny Lau (Jun 13 2018 at 13:52):

@Sebastian Ullrich

view this post on Zulip Kenny Lau (Jun 15 2018 at 00:29):

@Mario Carneiro

view this post on Zulip Sebastian Ullrich (Jun 15 2018 at 09:11):

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...

view this post on Zulip Kevin Buzzard (Jun 15 2018 at 09:30):

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.

view this post on Zulip Sebastian Ullrich (Jun 15 2018 at 10:27):

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.

view this post on Zulip Kenny Lau (Jun 16 2018 at 12:48):

holy mother I found a workaround

view this post on Zulip Kenny Lau (Jun 16 2018 at 12:48):

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)
-/

view this post on Zulip Kenny Lau (Jun 16 2018 at 12:48):

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

view this post on Zulip Sebastian Ullrich (Jun 16 2018 at 12:59):

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.

view this post on Zulip Mario Carneiro (Jun 16 2018 at 13:45):

well, that was unexpected

view this post on Zulip Kenny Lau (Jun 16 2018 at 13:46):

finally something unexpected :P

view this post on Zulip Johan Commelin (Jun 16 2018 at 15:00):

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.

view this post on Zulip Johan Commelin (Jun 16 2018 at 15:01):

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

view this post on Zulip Kevin Buzzard (Jun 16 2018 at 19:32):

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

view this post on Zulip Kenny Lau (May 07 2020 at 00:39):

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

view this post on Zulip Kenny Lau (May 07 2020 at 00:40):

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)
-/

view this post on Zulip Kevin Buzzard (May 07 2020 at 00:43):

Open an issue in the forked Lean repo.

view this post on Zulip Kenny Lau (May 07 2020 at 00:46):

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

view this post on Zulip Kenny Lau (May 27 2020 at 08:45):

push


Last updated: May 11 2021 at 14:11 UTC