Zulip Chat Archive

Stream: general

Topic: Lean unfolds projections


Yury G. Kudryashov (Apr 12 2020 at 02:57):

In the following example in inv_mem' Lean unfolds many projections making simp unusable. Doesn't happen with old_structure_cmd.

import data.set.lattice

namespace hidden

universes u v

variables (M : Type u) (G : Type v) [monoid M] [group G]

structure submonoid :=
(carrier : set M)
(one_mem' : (1:M)  carrier)
(mul_mem' :  (x  carrier) (y  carrier), x * y  carrier)

structure subgroup extends submonoid G :=
(inv_mem' :  x  carrier, x⁻¹  carrier)

variables {M G}

instance : has_coe (subgroup G) (set G) := ⟨λ S, S.carrier

instance : has_mem G (subgroup G) := ⟨λ x S, x  (S : set G)

instance : has_Inf (subgroup G) :=
⟨λ S, { carrier :=  s  S, s,
  one_mem' := by { trace_state, sorry },
  mul_mem' := by { trace_state, sorry },
  inv_mem' := by { trace_state, sorry } }

end hidden

Scott Morrison (Apr 12 2020 at 04:59):

I've just had a similar issue, and seen similar mysteries earlier. Could you try refine_struct and see what the goals look like there?

Yury G. Kudryashov (Apr 12 2020 at 05:24):

Better luck with refine_struct

Yury G. Kudryashov (Apr 12 2020 at 07:40):

But I don't want to define all instances using refine_struct!

Yury G. Kudryashov (Apr 12 2020 at 07:40):

Who should know how does it work? @Gabriel Ebner ? @Mario Carneiro ?

Mario Carneiro (Apr 12 2020 at 07:41):

Are there any universe metavariables?

Yury G. Kudryashov (Apr 12 2020 at 07:42):

No, see MWE above.

Yury G. Kudryashov (Apr 12 2020 at 07:43):

It has something to do with the new structure cmd.

Mario Carneiro (Apr 12 2020 at 07:44):

This also happens sometimes when you haven't finished the proof for the first part of the structure

Yury G. Kudryashov (Apr 12 2020 at 07:44):

Let me try.

Mario Carneiro (Apr 12 2020 at 07:44):

If you replace the proofs of one_mem' and mul_mem' with sorry then inv_mem' does not unfold to set.mem

Yury G. Kudryashov (Apr 12 2020 at 07:50):

Here it does:

instance : has_Inf (subgroup G) :=
⟨λ S, { carrier :=  s  S, s,
  one_mem' := mem_bInter $ λ s hs, s.one_mem',
  mul_mem' := by { simp only [mem_bInter_iff], intros x hx y hy s hs, exact s.to_submonoid.mul_mem' _ (hx _ hs) _ (hy _ hs) },
  inv_mem' := by { trace_state, sorry } }

Yury G. Kudryashov (Apr 12 2020 at 07:52):

With sorry for one_mem' and mul_mem' it says

29:20: G : Type w,
_inst_3 : group G,
S : set (subgroup G)
  (x : G),
    x  {carrier :=  (s : subgroup G) (H : s  S), s, one_mem' := _, mul_mem' := _}.carrier 
    x⁻¹  {carrier :=  (s : subgroup G) (H : s  S), s, one_mem' := _, mul_mem' := _}.carrier

Mario Carneiro (Apr 12 2020 at 07:54):

right

Mario Carneiro (Apr 12 2020 at 07:54):

that's good, yes?

Mario Carneiro (Apr 12 2020 at 07:55):

Understand that when you define a composite structure all in one go, the complete first half of the structure appears in the type of the second half

Yury G. Kudryashov (Apr 12 2020 at 07:55):

But with actual proofs (see above) it's still

29:20: G : Type w,
_inst_3 : group G,
S : set (subgroup G)
  (x : G),
    set.mem x ( (s : subgroup G) (H : s  S), s)  set.mem x⁻¹ ( (s : subgroup G) (H : s  S), s)

Yury G. Kudryashov (Apr 12 2020 at 07:56):

I think that Lean tries to get rid of { carrier := ..., .. }.carrier and unfolds all projections instead.

Mario Carneiro (Apr 12 2020 at 07:56):

I think the problem in your example is that the two by are making lean delay elaboration of the first half of the structure when it needs the type of the second half

Mario Carneiro (Apr 12 2020 at 07:57):

If you used term mode for the proof of mul_mem', you should see the version that doesn't unfold \in

Mario Carneiro (Apr 12 2020 at 08:02):

This works:

instance : has_Inf (subgroup G) :=
⟨λ S, {
  carrier :=  s  S, s,
  one_mem' := mem_bInter $ λ s hs, s.one_mem',
  mul_mem' := λ x hx y hy, by {
    simp only [mem_bInter_iff] at hx hy ,
    intros s hs,
    exact s.to_submonoid.mul_mem' _ (hx _ hs) _ (hy _ hs) },
  inv_mem' := _ }

Yury G. Kudryashov (Apr 12 2020 at 08:02):

What's the difference?

Kevin Buzzard (Apr 12 2020 at 08:02):

That's a workaround rather than a solution, isn't it?

Yury G. Kudryashov (Apr 12 2020 at 08:03):

Introduction of x .. hy before tactic mode?

Mario Carneiro (Apr 12 2020 at 08:03):

yes

Mario Carneiro (Apr 12 2020 at 08:04):

Yes, this is all a workaround for a bug in lean

Kevin Buzzard (Apr 12 2020 at 08:04):

Would another workaround be to roll your own constructor?

Mario Carneiro (Apr 12 2020 at 08:05):

If you defined the structure in two stages it should also work

Kevin Buzzard (Apr 12 2020 at 08:05):

But maybe Yury doesn't want to define all instances using the custom constructor either.

Mario Carneiro (Apr 12 2020 at 08:05):

that is, define the submonoid, then use that definition to define the subgroup

Mario Carneiro (Apr 12 2020 at 08:06):

there is usually also a good mathematical reason to not skip steps when defining these structures

Mario Carneiro (Apr 12 2020 at 08:07):

for example, in this case presumably submonoid should also has_Inf

Mario Carneiro (Apr 12 2020 at 08:07):

and you could refer to that construction here

Yury G. Kudryashov (Apr 12 2020 at 08:10):

In this case I'd loose defeq.

Yury G. Kudryashov (Apr 12 2020 at 08:11):

Because of the way \bigcap works

Mario Carneiro (Apr 12 2020 at 08:11):

No

Mario Carneiro (Apr 12 2020 at 08:11):

It is the same function you are already defining

Yury G. Kudryashov (Apr 12 2020 at 08:12):

I can say to_submonoid = ⨅ s ∈ S, s.to_submonoid but this will not be defeq to my definition.

Yury G. Kudryashov (Apr 12 2020 at 08:13):

Because on the way to carrier we'll have the "set.range" four times instead of twice.

Yury G. Kudryashov (Apr 12 2020 at 08:13):

As far as I understand, that's why filters have to use lattice.copy

Mario Carneiro (Apr 12 2020 at 08:15):

You can at least do this:

def Inf_submonoid (S : set (subgroup G)) : submonoid G :=
{ carrier :=  s  S, s,
  one_mem' := mem_bInter $ λ s hs, s.one_mem',
  mul_mem' := by {
    intros x hx y hy,
    simp only [mem_bInter_iff] at hx hy ,
    intros s hs,
    exact s.mul_mem' _ (hx _ hs) _ (hy _ hs) } }

instance : has_Inf (subgroup G) :=
⟨λ S, {
  to_submonoid := Inf_submonoid S,
  inv_mem' := _ }

Scott Morrison (Apr 20 2020 at 14:25):

Did anyone ever get to the bottom of this?

Scott Morrison (Apr 20 2020 at 14:25):

The same bug seems to be biting me again.

Bryan Gin-ge Chen (Apr 20 2020 at 15:18):

Is there an open issue for the bug in the Lean repository?

Scott Morrison (Apr 21 2020 at 00:23):

I've just opened https://github.com/leanprover-community/lean/issues/197.

Scott Morrison (Apr 21 2020 at 00:23):

I'll try to add more examples as I come across them.

Scott Morrison (Apr 21 2020 at 00:23):

We probably could minimise that example quite a bit further still.


Last updated: Dec 20 2023 at 11:08 UTC