tactic doesn't change primary goal state

Stream: lean4

[Bhavik Mehta]

I'm in a situation with four goals given to me in the infoview, and applying any tactic only changes the fourth one. I think this is confusing behaviour, especially to newcomers. Here's the example:

class Preorder (α : Type) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := fun a b => a ≤ b ∧ ¬b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl

class PartialOrder (α : Type) extends Preorder α where
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b

instance : PartialOrder Nat where
  le := (· ≤ ·)
  le_refl := Nat.le_refl
  le_trans a b c := Nat.le_trans
  le_antisymm := by
    intro x

Note the defs of Preorder and PartialOrder are copied exactly from mathlib. Before the intro x, here's my tactic state infoview
image.png
and after the intro x, here's what it looks like instead
image.png

[Kevin Buzzard]

The person putting the CommSemiring structure on sets of sets yesterday was faced with this too (but they had about 15 goals, it was extremely confusing)

[Patrick Massot]

What’s happening?? This looks like a huge bug. It has nothing to do with the intro tactic. The tactic state before intro is already completely crazy. @Sebastian Ullrich do you understand what’s happening here?

[Patrick Massot]

The default value for lt_iff_le_not_le seems to completely mess up things.

[Sebastian Ullrich]

Yes, this looks like an autoparam bug

[Kevin Buzzard]

Aha, indeed nsmul will then be the culprit in the commring thread

[Eric Wieser]

Where is this thread?

[Kevin Buzzard]

It wasn't their main problem, they were trying to define a semiring structure on Set (Set X) and were mostly having unrelated problems but when I tried to fix them I was immediately totally confused. Sorry I've been on mobile all day and still am, you can search for recent messages from me, there won't be too many, I don't know how to search for messages from me on mobile

[Kyle Miller]

I need to do some experiments, but I think the bug here is how source position is being associated to the autoParam tactic. The tactic block needs a source position to be able to make errors appear somewhere sensible, and currently it's using the entire where block for that. That seems to cause the InfoView to think that the entire where block has goals, and so the autoParam goals appear no matter where you put your cursor.

I'm guessing that the reason the goal appears three times is that by intros; rfl, intros, and rfl each get the entire where block as their source positions.

[Kevin Buzzard]

FWIW the thread was here and when I tried to help I started with code below and at the sorry I had 15 goals :-/

import Mathlib.Data.Set.Basic
import Mathlib.Algebra.Ring.Hom.Defs

/-- Why(X) provenance is the double power set of X -/
def Why (X : Type) := Set (Set X)

instance Why.zero : Zero (Why X) where
  zero := (∅ : Set (Set X))

instance Why.instCommSemiring {X : Type} : CommSemiring (Why X) where
  add := Set.union
  add_assoc := Set.union_assoc
  zero_add := Set.empty_union
  add_zero := Set.union_empty
  add_comm := Set.union_comm
  mul := fun (S1 S2 : Set (Set X)) => { s | ∃ s1 ∈ S1, ∃ s2 ∈ S2, s = s1 ∪ s2}
  mul_comm := by
    intros A B; unfold HMul.hMul; unfold instHMul; unfold Mul.mul; simp
    apply Set.ext; intro x; rw [Set.mem_setOf_eq]; rw [Set.mem_setOf_eq]
    apply Iff.intro
    . rintro ⟨a1, ⟨a1_mem, ⟨b1, ⟨b1_mem, eq1⟩⟩⟩⟩; aesop
    . rintro ⟨b1, ⟨b1_mem, ⟨a1, ⟨a1_mem, eq1⟩⟩⟩⟩; aesop
  mul_assoc := by
    intros A B C; unfold HMul.hMul; unfold instHMul; unfold Mul.mul; simp
    apply Set.ext; intro x; rw [Set.mem_setOf_eq]; rw [Set.mem_setOf_eq]
    apply Iff.intro
    . rintro ⟨y, ⟨⟨a1, ⟨a1_mem, ⟨b1, ⟨b1_mem, eq1⟩⟩⟩⟩, ⟨c1, ⟨c1_mem, eq2⟩⟩⟩⟩
      exists a1; split_ands; exact a1_mem; exists (b1 ∪ c1)
      split_ands
      . exists b1; split_ands; exact b1_mem; exists c1
      . aesop
    . rintro ⟨a1, ⟨a1_mem, ⟨y, ⟨⟨b1, ⟨b1_mem, ⟨c1, ⟨c1_mem, eq1⟩⟩⟩⟩, eq2⟩⟩⟩⟩
      exists (a1 ∪ b1)
      split_ands
      . exists a1; split_ands; exact a1_mem
        exists b1
      . exists c1; split_ands; exact c1_mem; aesop
  zero_mul := by
    intro S; unfold HMul.hMul; unfold instHMul; unfold Mul.mul; simp
    apply Set.eq_empty_iff_forall_not_mem.mpr
    intro T; simp; aesop
  mul_zero := by
    intro S; unfold HMul.hMul; unfold instHMul; unfold Mul.mul; simp
    apply Set.eq_empty_iff_forall_not_mem.mpr
    intro T; simp; aesop
  one := Set.singleton ∅
  mul_one := by
    intros A; unfold HMul.hMul; unfold instHMul; unfold Mul.mul; simp
    apply Set.ext; intro x; rw [Set.mem_setOf_eq]; apply Iff.intro
    . rintro ⟨a, ⟨a_mem, ⟨e, ⟨e_mem, eq⟩⟩⟩⟩
      rw [Set.mem_singleton_iff.mp e_mem] at eq; aesop
    . intro x_mem; exists x; split_ands; exact x_mem; exists ∅; aesop
  one_mul := by
    intros A; sorry -- 15 goals

[Daniel Weber]

Is there an issue for this? Has anyone tried git bisecting this to find which version introduced this?

[Mauricio Collares]

This was caused by lean4#5835 (cc @Marc Huisinga):

2a02c121cfcb586fe64cfdf3a6b2a88d68c861e7 is the first bad commit
commit 2a02c121cfcb586fe64cfdf3a6b2a88d68c861e7 (HEAD)
Author: Marc Huisinga <mhuisi@protonmail.com>
Date:   Tue Oct 22 18:10:57 2024 +0200

    feat: structure auto-completion & partial `InfoTree`s

[Marc Huisinga]

Mauricio Collares said:

This was caused by lean4#5835 (cc Marc Huisinga). Would bisecting "inside the PR" be helpful?

Did you bisect on stage0 or stage1?

[Mauricio Collares]

stage1

[Marc Huisinga]

I'll look into it tomorrow

[Kyle Miller]

If you have some time @Mauricio Collares, would you mind bisecting it with curly brace notation? I think the root cause is an earlier PR of mine.

instance : PartialOrder Nat := {
  le := (· ≤ ·)
  le_refl := Nat.le_refl
  le_trans := fun a b c => Nat.le_trans
  le_antisymm := by
    intro x
}

[Kyle Miller]

In particular lean4#4926.

(I hope to take a look at this later today.)

[Mauricio Collares]

I only see one goal with curly brace notation, even in the most recent nightly.

[Kyle Miller]

Thanks

[Ruben Van de Velde]

lean4#6408 landed

[Bhavik Mehta]

Nice! Thank you, Marc!