Lean unfolds projections

Stream: general

[Yury G. Kudryashov]

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]

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]

Better luck with refine_struct

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

Are there any universe metavariables?

[Yury G. Kudryashov]

No, see MWE above.

[Yury G. Kudryashov]

It has something to do with the new structure cmd.

[Mario Carneiro]

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

[Yury G. Kudryashov]

Let me try.

[Mario Carneiro]

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]

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]

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]

right

[Mario Carneiro]

that's good, yes?

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

What's the difference?

[Kevin Buzzard]

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

[Yury G. Kudryashov]

Introduction of x .. hy before tactic mode?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Kevin Buzzard]

Would another workaround be to roll your own constructor?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

for example, in this case presumably submonoid should also has_Inf

[Mario Carneiro]

and you could refer to that construction here

[Yury G. Kudryashov]

In this case I'd loose defeq.

[Yury G. Kudryashov]

Because of the way \bigcap works

[Mario Carneiro]

No

[Mario Carneiro]

It is the same function you are already defining

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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]

Did anyone ever get to the bottom of this?

[Scott Morrison]

The same bug seems to be biting me again.

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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