unfold vs dsimp

Stream: new members

[Kevin Cheung]

I know that the documentation discourages the use of Set.inter. But I would like to know why in the following dsimp works but unfold doesn't:

example : s ∩ u ⊆ u ∩ s := by
  dsimp [(· ∩ ·)]
  sorry

example : s ∩ u ⊆ u ∩ s := by
  unfold (· ∩ ·)
  sorry

In the second version, Lean complains about unexpected token '('. Is it simply a limitation of unfold that it cannot unfold operators?

[Timo Carlin-Burns]

I'm surprised either of those work. The only good way to unfold notation that I've learned is to define a custom lemma like docs#Set.inter_def which can be proved by rfl. It seems like simp has some special support for the · notation for defining functions.

import Mathlib.Data.Set.Basic

variable (s t : Set α)

-- This is the only one I would've expected to work. I thought `simp` and `unfold` only worked with declaration names.
example : s ∩ u ⊆ u ∩ s := by
  dsimp [Inter.inter] -- unfolds to `Set.inter`
  sorry

example : s ∩ u ⊆ u ∩ s := by
  dsimp [(Inter.inter · ·)] -- unfolds to `Set.inter`
  sorry

example : s ∩ u ⊆ u ∩ s := by
  dsimp [(· ∩ ·)] -- unfolds to `Set.inter`
  sorry

example : s ∩ u ⊆ u ∩ s := by
  dsimp [(fun x y => Inter.inter x y)] -- invalid 'simp', proposition expected
  sorry

example : s ∩ u ⊆ u ∩ s := by
  dsimp [(Inter.inter)] -- invalid 'simp', proposition expected
  sorry

example : s ∩ u ⊆ u ∩ s := by
  dsimp [((· ∩ ·))] -- invalid 'simp', proposition expected
  sorry

[Kevin Cheung]

Interesting. Replacing dsimp [Inter.inter] with unfold Inter.inter gives the goal instInterSet.1 s u ⊆ instInterSet.1 u s, not Set.inter s u ⊆ Set.inter u s. I am now utterly confused. Why instInterSet.1 here?

[Kyle Miller]

docs#Inter is a "notation typeclass" that provides the notation to whichever types implement the instance.

docs#Set.instInterSet is the instance for Set. When you unfold Inter.inter, you're seeing its definition, which is that it gets the definition from the instance.

[Kyle Miller]

If you do unfold_projs (mathlib tactic) it will unfold instInterSet.1 s

[Kyle Miller]

The limitation of unfold is that the syntax expects a sequence of identifiers

[Kevin Cheung]

So unfold cannot unfold operators?

[Kevin Cheung]

It seems that dsimp is more powerful than unfold. Are there reasons for using unfold but not dsimp?

[Kyle Miller]

It can, if you give it the underlying identifier. Here it's Inter.inter (you can check that by hovering over the notation)

[Kevin Cheung]

When I hover over ∩ , I saw only the following:

Set α

a ∩ b is the intersection of a and b.

Type ∩ using \i or \inter or \intersection or \cap

[Kevin Cheung]

Oh. I have to hover in the Infoview to see the Inter.inter

[Kyle Miller]

You can also "go to declaration" if you right click on it in the source

[Kevin Cheung]

Thanks for the tip! I was trying so hard looking into the documentation to see where intersection is defined.

[Timo Carlin-Burns]

Kyle, do you happen to know why (f · ·) is behaving differently from (fun x y => f x y) here? Is simp special casing the · syntax? Or does the · syntax have some eta-reduction built in?

[Kyle Miller]

Yeah, there's a special case for cdot syntax for simp (docs#Lean.Elab.Term.elabCDotFunctionAlias?)