Tactic state explosion

Stream: mathlib4

[Patrick Massot]

I am again facing tactic state explosion and I would really like to get an answer because this is a huge pain for teaching. Compare the following Lean 3 code:

import tactic.group
import group_theory.subgroup.basic

variables {G : Type*} [group G]

def conjugate (x : G) (H : subgroup G) : subgroup G :=
{ carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹},
  one_mem' := begin
    use 1,
    split,
    exact H.one_mem,
    group
  end,
  inv_mem' := begin
    rintro - ⟨h, h_in, rfl⟩,
    use [h⁻¹, H.inv_mem h_in],
    group
  end,
  mul_mem' := begin
    rintro - - ⟨h, h_in, rfl⟩ ⟨k, k_in, rfl⟩,
    use [h*k, H.mul_mem h_in k_in],
    group
  end }

lemma conjugate_one (H : subgroup G) : conjugate 1 H = H :=
begin
  ext x,
  unfold conjugate, -- State isn't great, but better than in Mathlib4
  simp
end

with its Lean 4 analogue

import Mathlib.Tactic.Group
import Mathlib.GroupTheory.Subgroup.Basic
variable {G : Type*} [Group G]

def conjugate (x : G) (H : Subgroup G) : Subgroup G where
  carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
  one_mem' := by
    -- Note crazy tactic state here
    dsimp
    use 1
    constructor
    exact H.one_mem
    group
  inv_mem' := by
    -- Note crazy tactic state is becoming even crazier
    dsimp
    rintro - ⟨h, h_in, rfl⟩
    use h⁻¹, H.inv_mem h_in
    group
  mul_mem' := by
    -- But here it's getting better??
    dsimp
    rintro - - ⟨h, h_in, rfl⟩ ⟨k, k_in, rfl⟩
    use h*k, H.mul_mem h_in k_in
    group

lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
  ext x
  unfold conjugate -- crazy crazy tactic state
  simp

[Patrick Massot]

For instance at the beginning of the first proof, you get in Lean 3:

1 ∈ {a : G | ∃ (h : G), h ∈ H ∧ a = x * h * x⁻¹}

which isn't what you would hope for, which is ∃ (h : G), h ∈ H ∧ 1 = x * h * x⁻¹, but is much better than the Lean 4 version:

1 ∈
  { carrier := {a | ∃ h, h ∈ H ∧ a = x * h * x⁻¹},
      mul_mem' :=
        (_ :
          ∀ {a b : G},
            a ∈ {a | ∃ h, h ∈ H ∧ a = x * h * x⁻¹} →
              b ∈ {a | ∃ h, h ∈ H ∧ a = x * h * x⁻¹} → a * b ∈ {a | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}) }.carrier

[Patrick Massot]

And in the last proof, after unfold conjugate, the Lean 3 goal is displayed as

x ∈ {carrier := {a : G | ∃ (h : G), h ∈ H ∧ a = 1 * h * 1⁻¹}, mul_mem' := _, one_mem' := _, inv_mem' := _} ↔ x ∈ H

which again is not perfect, but the Lean 4 version is:

x ∈
    {
      toSubmonoid :=
        {
          toSubsemigroup :=
            { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹},
              mul_mem' :=
                (_ :
                  ∀ {a b : G},
                    a ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                      b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} → a * b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹},
                    mul_mem' :=
                      (_ :
                        ∀ {a b : G},
                          a ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                            b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                              a * b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}) }.carrier) },
      inv_mem' :=
        (_ :
          ∀ {x : G},
            x ∈
                {
                      toSubsemigroup :=
                        { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹},
                          mul_mem' :=
                            (_ :
                              ∀ {a b : G},
                                a ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                  b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                    a * b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}) },
                      one_mem' :=
                        (_ :
                          1 ∈
                            { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹},
                                mul_mem' :=
                                  (_ :
                                    ∀ {a b : G},
                                      a ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                        b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                          a * b ∈
                                            {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}) }.carrier) }.toSubsemigroup.carrier →
              x⁻¹ ∈
                {
                      toSubsemigroup :=
                        { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹},
                          mul_mem' :=
                            (_ :
                              ∀ {a b : G},
                                a ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                  b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                    a * b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}) },
                      one_mem' :=
                        (_ :
                          1 ∈
                            { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹},
                                mul_mem' :=
                                  (_ :
                                    ∀ {a b : G},
                                      a ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                        b ∈ {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹} →
                                          a * b ∈
                                            {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}) }.carrier) }.toSubsemigroup.carrier) } ↔
  x ∈ H

[Bhavik Mehta]

I think part of this is because Lean 4 is printing the types of proof fields, which is exploding the state. For me that setting is turned off, and I wonder if for teaching it might be an unhelpful option. In particular, in your first example my goal looks like

1 ∈ { carrier := {a | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}, mul_mem' := _ }.carrier

[Patrick Massot]

I don't know whether this is related to new structures vs flat structures or if we are missing a delaborator. But we need to do something. It makes Lean+Mathlib a lot less usable for teaching, and it will also be a problem for ambitious formalization projects.

[Patrick Massot]

Do you mean set_option pp.proofs.withType false?

[Bhavik Mehta]

Yes

[Patrick Massot]

Indeed this already make things a little better.

[Patrick Massot]

Actually a lot better, but still the last tactic state is:

x ∈
    {
      toSubmonoid :=
        { toSubsemigroup := { carrier := {a | ∃ h, h ∈ H ∧ a = 1 * h * 1⁻¹}, mul_mem' := _ }, one_mem' := _ },
      inv_mem' := _ } ↔
  x ∈ H

which looks like nested classes are acting badly.

[Jireh Loreaux]

Is there a pp.etaReduce? that seems like it would fix the extra .carrier?

[Patrick Massot]

No there isn't.

[Patrick Massot]

And I also don't understand why dsimp does nothing after unfold conjugate.

[Patrick Massot]

It does in Lean 3.

[Thomas Murrills]

Would it be a good idea to have something like pp.flattenStructures to handle the nested structures part of the issue? Do we have something like that already somewhere? (I couldn’t find it.)

[Patrick Massot]

Do you understand why dsimp doesn't work?

[Thomas Murrills]

Hmm, no, I don't; I was thinking about how to clean up the appearance of toSubmonoid and toSubSemigroup.

[Thomas Murrills]

Ah, I think I (sort of) figured it out: mathlib3's dsimp can rewrite using subgroup.mem_mk (now docs#Subgroup.mem_mk), whereas mathlib4's dsimp can't.

[Thomas Murrills]

Why this difference exists, I'm not sure yet.

[Thomas Murrills]

I think we're getting closer! It has to do with ↔-theorems marked @[simp] which consist of Iff.rfl. These aren't recognized as dsimp-worthy in Lean 4, but are in Lean 3. Compare:

Lean 4:

def w : Prop → Prop | p => p

example : w a := by dsimp -- dsimp made no progress

@[simp] theorem defthm : w a ↔ a := Iff.rfl

example : w a := by dsimp -- dsimp made no progress

@[simp] theorem defthm' : w a = a := rfl

example : w a := by dsimp -- unsolved goals `⊢ a`

Lean 3:

def w : Prop → Prop := fun p, p

example (a : Prop) : w a := by dsimp -- (no progress) unsolved goals `⊢ w a`

@[simp] theorem defthm (a : Prop) : w a ↔ a := iff.rfl

example (a : Prop) : w a := by dsimp -- unsolved goals `⊢ a`

[Ruben Van de Velde]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/dsimp.20and.20Iff.2Erfl

[Thomas Murrills]

I see! It doesn't look like an issue was ever filed...should one be?

[Thomas Murrills]

I looked around and I think it would be a minor change—we'd just want to mark these theorems as rfl theorems to simp internally, which (I think) amounts to just changing the condition

if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2  then ...

to

if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 ||
    proof.isAppOfArity ``Iff.refl 1 || proof.isAppOfArity ``Iff.rfl 1 then ...

in isRflProofCore (in Lean.Meta.Tactic.Simp.SimpTheorems). (EDIT: actually a couple other small changes need to be made, but the gist is the same.) Though I haven't tested it out.

I'd be happy to make an issue + a draft PR to see if it really is this simple, if there's support. :)

[Yaël Dillies]

Yes please! It's an annoying regression.

[Patrick Massot]

Yes, please.

[Thomas Murrills]

On it. :)

[Thomas Murrills]

Issue: lean4#2678
Draft PR forthcoming...

[Thomas Murrills]

(Subsequent messages moved to #mathlib4 > using Iff rfl proofs in dsimp. Apparently I forgot to tick the box that automates this message... :) )