Annoying simp + FunLike interaction

Stream: lean4

[Peter Nelson]

I'm encountering some problems where simp is definitionally rewriting data inside a dependent type in a way that breaks confluence when combined with FunLike.

It is fixed by changing a rfl proof to by exact rfl. As well as seeming hacky, this is not a feasible fix for my use case, because the relevant rfl proof is already in mathlib.

It is also fixed by not using FunLike and just going with toFun explicitly, which is undesirable.

Does anyone know another way to stop simp from screwing around inside the DFunLike.coe term?

import Mathlib

/-- A wrapper for a set -/
structure SetWrap where
  val : Set ℕ

/-- The union of two wrapped sets -/
def SetWrap.union (a b : SetWrap) : SetWrap := ⟨a.val ∪ b.val⟩

/-- A reasonable simp lemma with `rfl` as the proof. -/
@[simp]
lemma SetWrap.union_val (a b : SetWrap) : (a.union b).val = a.val ∪ b.val := rfl

/-- A sequence of subsets of a set `s` -/
structure SubsetSeq (s : Set ℕ) where
  toFun : ℕ → Set ℕ
  subset : ∀ i, toFun i ⊆ s

/-- `SubsetSeq` is `FunLike` -/
instance {s : Set ℕ} : FunLike (SubsetSeq s) ℕ (Set ℕ) where
  coe := SubsetSeq.toFun
  coe_injective' := by rintro ⟨f,h⟩ ⟨f', h'⟩; simp

/-- If `f` is a subset sequence arising from a `SetWrap`, then its terms are empty. -/
@[simp]
lemma foo {a : SetWrap} (f : SubsetSeq a.val) (i : ℕ) : f i = ∅ := sorry

/-- an easy lemma that follows directly from `foo` and should be proved by `simp`. -/
example {a b : SetWrap} {f : SubsetSeq (a.union b).val} {i : ℕ} : f i = ∅ := by
  /- The following `simp` succeeds with no visible change;
  it uses `SetWrap.union_val` to change the term `f i` from
  `@DFunLike.coe (SubsetSeq ((a.union b).val)) ℕ (fun x ↦ Set ℕ) instFunLikeSubsetSeqNatSet f i`
  to
  `@DFunLike.coe (SubsetSeq (a.val ∪ b.val)) ℕ (fun x ↦ Set ℕ) instFunLikeSubsetSeqNatSet f i`.
  This is not visible in the infoview without mouseover. -/
  simp -- succeeds with no visible change
  -- Now the next `simp` fails to resolve the goal using `foo`,
  -- because `f` does not match its argument.
  simp  -- fails

If the proof of SetWrap.union_val is changed from rfl to by exact rfl, then simp will resolve the above example using foo, because simp doesn't change the type of f.

[Aaron Liu]

so is the problem that foo isn't in simp-nf

[Peter Nelson]

In what way could foo by itself be more normalized? Using simp as the first line of the proof of foo fails.

[Peter Nelson]

(Of course foo is equivalent to a more normalized lemma with SubsetSeq s for arbitrary s, but that is an artefact of the MWE)

[Aaron Liu]

oh no nvm

[Aaron Liu]

it's definitely in simpNF

[Aaron Liu]

I think I need more context

[Peter Nelson]

(deleted)

[Peter Nelson]

The context is partitions of the ground sets of matroids.
First, independently of anything matroidy, for each s : Set a, I have a function-like type s.Bipartition that coerces to a function from Bool to Set a. (It encodes a partition of s into two parts.)

Then I have a structure Matroid a, which has a structure field E : Set a; this it the 'ground set' of a matroid.

One operation on matroids is the following : Matroid.delete (M : Matroid a) (D : Set a) : Matroid a. This satisfies (M.delete D).E = M.E \ D; this is a simp lemma whose proof is rfl.

Then I have a bunch of @[simp] lemmas foo1, foo2, ... about matroidal properties of bipartitions of the ground set of a matroid. They each take (P : M.E.Bipartition) as an argument.

The problem now is that if I have P : (M.delete D).E.Bipartition, then these simp lemmas will never work, because simp will first change (M.delete D).E to (M.E \ D) inside the FunLike coercion term.

[Aaron Liu]

uhhhhh

[Aaron Liu]

maybe make it not a dsimp lemma

[Aaron Liu]

or maybe noindex that part

[Peter Nelson]

It should really be a dsimp lemma in almost every other context, though. How does noindex work?

[Johan Commelin]

@Peter Nelson See #new members > ✔ What does `no_index` mean? @ 💬 for some explanation about no_index.

[Jakub Nowak]

Peter Nelson said:

The context is partitions of the ground sets of matroids.
First, independently of anything matroidy, for each s : Set a, I have a function-like type s.Bipartition that coerces to a function from Bool to Set a. (It encodes a partition of s into two parts.)

Then I have a structure Matroid a, which has a structure field E : Set a; this it the 'ground set' of a matroid.

One operation on matroids is the following : Matroid.delete (M : Matroid a) (D : Set a) : Matroid a. This satisfies (M.delete D).E = M.E \ D; this is a simp lemma whose proof is rfl.

Then I have a bunch of @[simp] lemmas foo1, foo2, ... about matroidal properties of bipartitions of the ground set of a matroid. They each take (P : M.E.Bipartition) as an argument.

The problem now is that if I have P : (M.delete D).E.Bipartition, then these simp lemmas will never work, because simp will first change (M.delete D).E to (M.E \ D) inside the FunLike coercion term.

Does it matter that Set.Bipartition is FunLike? Wouldn't the same problem still occur even if it was just structure?

[Peter Nelson]

Jakub Nowak said:

Does it matter that Set.Bipartition is FunLike? Wouldn't the same problem still occur even if it was just structure?

If I understand you correctly, then no. The following works after the code above :

@[simp]
lemma foo' {a : SetWrap} (f : SubsetSeq a.val) (i : ℕ) : (f.toFun i = ∅) := by
  sorry

example {a b : SetWrap} {f : SubsetSeq (a.union b).val} {i : ℕ} : f.toFun i = ∅ := by
  simp

[Jakub Nowak]

Ah, I see. It's because simp is changing the type of f inside the term. Hmm, it's kinda defeq abuse. Maybe it's bug that simp does it in the first place?

[Peter Nelson]

Yes, the fact that FunLike and by exact rfl vs rfl change things suggests that some part of this behaviour is actually undesirable.

[Jakub Nowak]

The suggested no_index approach fixes the issue.

@[simp]
lemma foo {a : SetWrap} (f : SubsetSeq (no_index a.val)) (i : ℕ) : f i = ∅ := sorry

Though, it has a drawback of slowing down simp.

[Aaron Liu]

Jakub Nowak said:

Ah, I see. It's because simp is changing the type of f inside the term.

I don't think that's possible

[Aaron Liu]

Jakub Nowak said:

The suggested no_index approach fixes the issue.

@[simp]
lemma foo {a : SetWrap} (f : SubsetSeq (no_index a.val)) (i : ℕ) : f i = ∅ := sorry

Though, it has a drawback of slowing down simp.

I meant you should no_index the parts in the expression that are being changed hopefully retaining enough information to not slow down simp too much

[Peter Nelson]

Is this actually a bug?

[Matthew Ballard]

I think it is just sub-optimal design.

Does anyone want to argue against

attribute [reducible] DFunLike.coe

[Peter Nelson]

Design on my part, or of the interactions I’m fighting with? I don’t understand why FunLike should behave differently to a plain function.

[Matthew Ballard]

I think the totality of the design. Because DFunLike.coe is a projection to a field from a class it just doesn't "fade away" with simp. I could imagine that dsimp reduces it to the application of the underlying function it in this situation whether that is via some global setting or some particular local simp lemma.

[Jakub Nowak]

Aaron Liu said:

Jakub Nowak said:

Ah, I see. It's because simp is changing the type of f inside the term.

I don't think that's possible

I think it does, but using defeq of types.

[Jakub Nowak]

Aaron Liu said:

Jakub Nowak said:

The suggested no_index approach fixes the issue.

@[simp]
lemma foo {a : SetWrap} (f : SubsetSeq (no_index a.val)) (i : ℕ) : f i = ∅ := sorry

Though, it has a drawback of slowing down simp.

I meant you should no_index the parts in the expression that are being changed hopefully retaining enough information to not slow down simp too much

That's what I tried to do, what else could you do here? SetWrap.val (no_index a) won't work.

[Jakub Nowak]

And I has potential of slowing down simp quite a lot, because now it will try this lemma for every SubsetSeq, not just the ones using SetWrap. (It still needs some SetWrap in the context though).

[Aaron Liu]

I mean like doing @DFunLike.coe (SubsetSeq (no_index _)) (Nat → Set) _ f i

[Jakub Nowak]

I've tried, but this doesn't work.

[Aaron Liu]

oh no

[Jakub Nowak]

simp doesn't try foo, because the type of f doesn't match.

[Jakub Nowak]

And I don't think no_index in DFunLike instance, can stop simp from modifying the type.

[Jakub Nowak]

I still don't exactly understand why simp doesn't try foo without no_index. The type of f in the context didn't change. It only changed the type inside the goal term.

[Jakub Nowak]

I think simp shouldn't do this. If I wanted to change the type of f, I would do dsimp at f.

[Jakub Nowak]

Jakub Nowak said:

And I has potential of slowing down simp quite a lot, because now it will try this lemma for every SubsetSeq, not just the ones using SetWrap. (It still needs some SetWrap in the context though).

Oh, wow, it's even worse. It will not only try, but can even succeed in using this lemma for a different type:

import Mathlib

/-- A wrapper for a set -/
structure SetWrap where
  val : Set ℕ

/-- A sequence of subsets of a set `s` -/
structure SubsetSeq (s : Set ℕ) where
  toFun : ℕ → Set ℕ
  subset : ∀ i, toFun i ⊆ s

/-- `SubsetSeq` is `FunLike` -/
instance {s : Set ℕ} : FunLike (SubsetSeq s) ℕ (Set ℕ) where
  coe := SubsetSeq.toFun
  coe_injective' := by rintro ⟨f,h⟩ ⟨f', h'⟩; simp

/-- If `f` is a subset sequence arising from a `SetWrap`, then its terms are empty. -/
@[simp]
lemma foo {a : SetWrap} (f : SubsetSeq no_index a.val) (i : ℕ) : f i = ∅ := sorry

set_option pp.all true in
#discr_tree_simp_key foo

set_option trace.Meta.Tactic.simp.rewrite true in
example {a b : Set ℕ} {f : SubsetSeq (a ∪ b)} {i : ℕ} : f i = ∅ := by
  simp only [foo] -- succeeds

[Jakub Nowak]

@Peter Nelson This works:

import Mathlib

/-- A wrapper for a set -/
structure SetWrap where
  val : Set ℕ

/-- The union of two wrapped sets -/
def SetWrap.union (a b : SetWrap) : SetWrap := ⟨a.val ∪ b.val⟩

/-- A reasonable simp lemma with `rfl` as the proof. -/
@[simp]
lemma SetWrap.union_val (a b : SetWrap) : (a.union b).val = a.val ∪ b.val := rfl

/-- A sequence of subsets of a set `s` -/
structure SubsetSeq (s : Set ℕ) where
  toFun : ℕ → Set ℕ
  subset : ∀ i, toFun i ⊆ s

/-- `SubsetSeq` is `FunLike` -/
instance {s : Set ℕ} : FunLike (SubsetSeq s) ℕ (Set ℕ) where
  coe := SubsetSeq.toFun
  coe_injective' := by rintro ⟨f,h⟩ ⟨f', h'⟩; simp

/-- If `f` is a subset sequence arising from a `SetWrap`, then its terms are empty. -/
@[simp↓]
lemma foo {a : SetWrap} (f : SubsetSeq a.val) (i : ℕ) : f i = ∅ := sorry

/-- an easy lemma that follows directly from `foo` and should be proved by `simp`. -/
example {a b : SetWrap} {f : SubsetSeq (a.union b).val} {i : ℕ} : f i = ∅ := by
  simp -- succeeds

[Jakub Nowak]

Although, using @[simp↓] might cause failure in some other cases that one would expect to work. Maybe you could try @[simp↓, simp]?

[Jakub Nowak]

But it's a bit wacky solution. Ideally, we would want to apply simp to some argument subexpressions, but not all of them.

[Jovan Gerbscheid]

You could also try simp -dsimp?

[Jakub Nowak]

Isn't that a bug?

import Mathlib

/-- A wrapper for a set -/
structure SetWrap where
  val : Set ℕ

/-- A sequence of subsets of a set `s` -/
structure SubsetSeq (s : Set ℕ) where
  toFun : ℕ → Set ℕ
  subset : ∀ i, toFun i ⊆ s

/-- `SubsetSeq` is `FunLike` -/
instance {s : Set ℕ} : FunLike (SubsetSeq s) ℕ (Set ℕ) where
  coe := SubsetSeq.toFun
  coe_injective' := by rintro ⟨f,h⟩ ⟨f', h'⟩; simp

/-- If `f` is a subset sequence arising from a `SetWrap`, then its terms are empty. -/
@[simp]
axiom foo {a : SetWrap} (f : SubsetSeq no_index a.val) (i : ℕ) : f i = ∅

example {a b : Set ℕ} {f : SubsetSeq (a ∪ b)} {i : ℕ} : f i = ∅ := by
  simp -- succeeds

I've made an axiom for SetWrap. Yet, simp happily used it to prove example where there's no SetWrap.

[Jakub Nowak]

Ah, okay, somehow simp automatically used the one-argument constructor for SetWrap I think? This doesn't work, so I don't think there's soundness issue:

import Mathlib

/-- A wrapper for a set -/
structure SetWrap where
  val : Set ℕ
  impossible : False

/-- A sequence of subsets of a set `s` -/
structure SubsetSeq (s : Set ℕ) where
  toFun : ℕ → Set ℕ
  subset : ∀ i, toFun i ⊆ s

/-- `SubsetSeq` is `FunLike` -/
instance {s : Set ℕ} : FunLike (SubsetSeq s) ℕ (Set ℕ) where
  coe := SubsetSeq.toFun
  coe_injective' := by rintro ⟨f,h⟩ ⟨f', h'⟩; simp

/-- If `f` is a subset sequence arising from a `SetWrap`, then its terms are empty. -/
@[simp]
axiom foo {a : SetWrap} (f : SubsetSeq no_index a.val) (i : ℕ) : f i = ∅

example {a b : Set ℕ} {f : SubsetSeq (a ∪ b)} {i : ℕ} : f i = ∅ := by
  simp -- fails

[Peter Nelson]

still, simp is being quite a loose cannon...