simp? creates wrong proof with user defined let-value

Stream: lean4

[Johannes Tantow]

Hi,
simp? adds user defined let-values to the simp set, if they occur in a hypothesis (I guess). Here is an example:

example : [].filter (fun _ => true) = ([] : List String) := by
  let t := 1+1+1
  have ht: t = 1 + 1 +1 := by simp [t]
  simp

Here it proposes to add t to the simp set, which is useless. If I remove the have, this no longer happens. This is not problematic in this example, but in a real use case I used this technique to mask some term in which I cant rewrite (see below) and therefore get there an error when using this directly to replace simp with simp only.

import Std.Data.Internal.List.Associative
import Std.Data.Internal.List.Defs

@[inline] def Option.pfilter (o : Option α) (p : (a : α) → a ∈ o → Bool) : Option α :=
  match o with
  | none => none
  | some a => bif p a rfl then o else none

theorem Option.pfilter_eq_none {α : Type _} {o : Option α} {p : (a : α) → a ∈ o → Bool} :
    o.pfilter p = none ↔ o = none ∨ ∃ (a : α) (ha : a ∈ o), p a ha = false := by
  sorry

theorem Option.pfilter_eq_some {α : Type _} {o : Option α} {p : (a : α) → a ∈ o → Bool}
    {a : α} (ha : a ∈ o) :
    o.pfilter p = some a ↔ p a ha = true := by
  sorry

@[congr]
theorem pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o')
    {f : (a : α) → a ∈ o → Bool} {g : (a : α) → a ∈ o' → Bool}
    (hf : ∀ a ha, f a (ho.trans ha) = g a ha) :
    o.pfilter f = o'.pfilter g := by
  sorry

namespace Std.Internal.List
variable {α : Type u} {β : α → Type v} {γ : α → Type w}

theorem containsKey_of_getKey?_eq_some [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a a' : α}
    (h : getKey? a l = some a') :
    containsKey a' l = true := by sorry

theorem getEntry?_filterMap [BEq α] [EquivBEq α]
    {f : (a : α) → β a → Option (γ a)}
    {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
    getEntry? k (l.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) =
      (getEntry? k l).bind fun p => (f p.1 p.2).map (⟨p.1, ·⟩) := by
  sorry

theorem List.getKey?_filterMap [BEq α] [LawfulBEq α]
    {f : (a : α) → β a→ Option (γ a)}
    {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) :
    getKey? k (l.filterMap fun p => (f p.1 p.2).map (fun x => (⟨p.1, x⟩ : (a : α) × γ a))) =
      (getKey? k l).pfilter (fun x h =>
      (f x (getValueCast x l (containsKey_of_getKey?_eq_some (Option.mem_iff.mp h)))).isSome) := by
  apply Eq.symm
  let t := ((getKey? k l).pfilter fun x h =>
    (f x (getValueCast x l (containsKey_of_getKey?_eq_some (Option.mem_iff.mp h)))).isSome)
  have ht: t = ((getKey? k l).pfilter fun x h =>
    (f x (getValueCast x l (containsKey_of_getKey?_eq_some (Option.mem_iff.mp h)))).isSome) := by
    simp [t]
  rw [← ht]
  simp [getKey?_eq_getEntry?, getEntry?_filterMap hl, Option.map_bind] --here the problem occurs.
  cases h : getEntry? k l with
  | none =>
    rw [ht]
    simp [Option.pfilter_eq_none, h, getKey?_eq_getEntry?]
  | some x =>
    rw [ht]
    have contains : containsKey k l = true := by
      simp [containsKey_eq_isSome_getEntry?, h]
    have := getKey?_eq_some contains
    rw [getEntry?_eq_getValueCast?, Option.map_eq_some'] at h
    rcases h with ⟨v, hv, hx⟩
    simp [← hx]
    cases h' : f k v with
    | none =>
      simp [Option.pfilter_eq_none, this]
      exists k
      exists rfl
      simp [getValueCast, hv, h']
    | some y =>
      simp
      rw [Option.pfilter_eq_some]
      simp [getValueCast, hv, h']
      apply this

[Bhavik Mehta]

I believe this is lean4#6655

[Jovan Gerbscheid]

I started an attempt to fix this at lean#7539