Minimal examples of defeq abuse and defeq (non-abuse) use

Stream: new members

[Louis Cabarion]

For educational purposes, I'm putting together some simple and minimal examples that illustrate both defeq abuse (cases where relying on definitional equality becomes problematic) and safe uses of definitional equality, where such reliance is unproblematic.

1. What are some good examples (and non-examples) of defeq abuse?

2. Are there any tools, linters, or similar mechanisms that can help detect the presence (or absence) of defeq abuse?

3. Given a proof diff, what’s the recommended approach for identifying any defeq abuse introduced by the changes?

[Rado Kirov]

I would love to see those too. Is there a similar version of simp abuse?

[Louis Cabarion]

@Rado Kirov These are the simp guidelines.

As I understand them (please correct me if I'm wrong!):

• If a simp invocation closes the goal (i.e., it is a terminal simp), then using simp is recommended (using simp only […] is discouraged).
• If a simp does not close the goal (i.e., it is a non-terminal simp), then it should typically be replaced with a more specific simp only […], as identified using simp?.

[Michael Rothgang]

Isak Colboubrani said:

Rado Kirov These are the simp guidelines.

As I understand them (please correct me if I'm wrong!):

• If a simp invocation closes the goal (i.e., it is a terminal simp), then using simp is recommended (using simp only […] is discouraged).
• If a simp does not close the goal (i.e., it is a non-terminal simp), then it should typically be replaced with a more specific simp only […], as identified using simp?.

Looks alright to me. You can use mathlib's flexible linter (enable through set_option linter.flexible true) to detect one direction of this (namely, non-terminal simps).

[Ruben Van de Velde]

Don't have good examples right now, but-

1. It's fine to punch through a layer (typically no more than one at a time) of definitions while setting up the basic lemmas for that definition (so these should be right next to the definition)
2. It's typically not a good idea to rely on a definition as one step in a bigger proof or far away from the definition
3. There's a few definitions where, in practice, we make use of the definition anyway, even though the general rule would frown upon it (e.g. intro x hx to prove a subset, or treating Dvd.dvd as an exists)
4. There's a few red flags that make me double-check what's going on, like using erw, change, or rfl after rw/simp

[Jireh Loreaux]

Not examples, but my working definition of defeq abuse is here: #new members > Definitions of "defeq", "diamond" and "β/δ/η/ζ reductions" @ 💬

[Kenny Lau]

@Isak Colboubrani the biggest and most problematic defeq abuse I've seen and which is actually discussed about, is the various Lp norms on a space, which are introduced as type synonyms. As in, the sup norm and L2 norm on R^n, the underlying sets (i.e. types) are actually defeq

[Eric Paul]

Here's an example of the sort that I run into. By definition, αᵒᵈ is the same thing as α and so in the first definition of dual, it looks past this definition. But then the following proofs cannot be solved by simp. On the other hand, dual' respects the definition and so simp works. One way to avoid this is by writing seal OrderDual at the top of the file.

import Mathlib

variable [LinearOrder α] [LinearOrder β]

def dual (f : α ↪o β) : αᵒᵈ ↪o βᵒᵈ where
  toFun := f
  inj' := by simp [Function.Injective]
  map_rel_iff' := by simp

def dual' (f : α ↪o β) : αᵒᵈ ↪o βᵒᵈ where
  toFun := OrderDual.toDual ∘ f ∘ OrderDual.ofDual
  inj' := by simp [Function.Injective]
  map_rel_iff' := by simp