Questions about defeq abuse

Stream: new members

[Luna]

I'm confused by what defeq absue means. My internal idea is that if you define

def SomeDefinition : Prop := ...

Then one would define an API around that object so that the user doesn't have to know the internal implementation details of SomeDefinition. So as a simple example, if I try to solve:

example {α : Type*} {p : α → Prop} {a : α} (ha : p a) : a ∈ {a | p a} := by
  sorry

I would look for a theorem that takes in ha and proves a ∈ {a | p a}. The closest thing to that is Set.mem_def but that comes with the following deprecation warning:

This lemma abuses the Set α := α → Prop defeq. If you think you need it you have already taken a wrong turn.

The only alternative I see others using is by exact ha but isn't that defeq abuse, since that requires the user to know how Set is defined under the hood?

[Aaron Liu]

docs#Set.mem_setOf

[Aaron Liu]

but in this case you can probably just exact ha

[Robin Arnez]

I like to define "defeq abuse" as "the type of a theorem doesn't type-check under reducible transparency".
For example Set.mem_def here has type ∀ {α : Type u} {a : α} {s : Set α}, a ∈ s ↔ s a as #print sig will tell you and

def test.{u} : Prop := by
  with_reducible exact ∀ {α : Type u} {a : α} {s : Set α}, a ∈ s ↔ s a

produces an error

[Ruben Van de Velde]

The issue with Set.mem_def is that it uses p a where p : Set _, but you have p : _ → Prop

[Ruben Van de Velde]

Aaron indeed has the correct lemma

[Ruben Van de Velde]

In this case, both rw? and simp?find docs#Set.mem_setOf_eq , which is fine as well. Annoyingly, apply? and exact? don't bother looking further than exact ha, which you indeed generally want to avoid

[Robin Arnez]

Ruben Van de Velde schrieb:

Annoyingly, apply? and exact? don't bother looking further than exact ha

Try with_reducible exact?

[Ruben Van de Velde]

Oh, thanks, I learned something! (That should be the default though)

[Robin Arnez]

I think exact ha is actually totally fine as a suggestion though; I wouldn't consider that defeq abuse in the same way that 1 + 2 = 3 by rfl isn't defeq abuse. In other words, if equalities that are part of the API hold definitionally, I feel like it's fine to use that fact (although there are exceptions). But if you have equalities that are considered implementation details (like Set a = a -> Prop) then we get to defeq abuse.

[Aaron Liu]

things I would not consider defeq abuse

• normalization of closed terms (although sometimes it gets stuck and sometimes it keeps reducing forever)
• defeqs like docs#Set.coe_comp_rangeFactorization which are part of the universal property
• structure projections from a definition like docs#finCongr
• certain definitions like docs#Filter.Tendsto and docs#Not for which other people unfold regularly without considering it to be defeq abuse

[Filippo A. E. Nuccio]

Although the above answers are certainly correct, let me propose a small example I sometimes use when teaching to explain my take on defeq. My focus is not really that the user should not know/look at the internal details, but rather that they should not matter: I play with structures instead of definitions, but the idea is the same. Consider the following structure (that you'll certainly recognise...)

import Mathlib

class Blob (α : Type) where
one : α
opBl : α → α → α
one_opBl (x : α) : opBl one x = x
opBl_one (x : α) : opBl x one = x
assoc (x y z : α) : opBl x (opBl y z) = opBl (opBl x y) z
inv : α → α
inv_cancel (x : α) : opBl x (inv x) = one
cancel_inv (x : α) : opBl (inv x) x = one

infixl:70 " ? " => Blob.opBl
local notation " u " => Blob.one

Then we can have the obvious, tautological results

open Blob

theorem Blob_inv_cancel (α : Type) [Blob α] (x : α) : x ? (inv x) = u := inv_cancel x

theorem Blob_cancel_inv (α : Type) [Blob α] (x : α) : ((inv x) ? x) = u := cancel_inv x

But it is well-known that we could as well decide to remove the final condition cancel_inv, because it can be deduced from the previous ones. So we can also simply define

import Mathlib

class Blob (α : Type) where
one : α
opBl : α → α → α
one_opBl (x : α) : opBl one x = x
opBl_one (x : α) : opBl x one = x
assoc (x y z : α) : opBl x (opBl y z) = opBl (opBl x y) z
inv : α → α
inv_cancel (x : α) : opBl x (inv x) = one

infixl:70 " ? " => Blob.opBl
local notation " u " => Blob.one

and obtain

open Blob

theorem Blob_inv_cancel (α : Type) [Blob α] (x : α) : x ? (inv x) = u := inv_cancel x

theorem Blob_cancel_inv (α : Type) [Blob α] (x : α) : ((inv x) ? x) = u := by
  calc
  (inv x) ? x = ((inv x) ? x) ? u := by rw [opBl_one]
            _ = ((inv x) ? x) ? ((inv x) ? inv (inv x)) := by rw [← inv_cancel]
            _ = (inv x) ? ((x ? (inv x)) ? inv (inv x)) := by rw [← assoc, ← assoc]
            _ = (inv x) ? (inv (inv x)) := by rw [inv_cancel, one_opBl]
            _ = u := by rw [inv_cancel]

Now, the point is that if you're writing a proof about Blob and you need (inv x) ? x = u, "avoiding defeq" means avoiding the call of the structure field cancel_inv, rather relying on the theorem Blob_cancel_inv: whose proof will be rfl or the small calc block according to your (internal) implementation of Blob. Since this implementation might change, but not its intrinsic/mathematical meaning, we'll always have the theorem Blob_cancel_inv irrespective of the implementation, for instance irrespective of cancel_inv being part of the structure. Following this hygiene makes your code more robust and less prone to rot due to internal changes.

[Luna]

Thank you everyone! This does make a lot more sense. I originally couldn't find Set.mem_setOf since it was in a different file than Set.mem_def and the doc for Set.mem_def (combined with my particular problem) made it seem as though one was not supposed to convert (ha : p a) to a ∈ {a | p a}.

And I didn't see that Set.mem_def uses the set s as though it were defined like s : A -> Propdue to my simplistic use case. I do see how that is defeq abuse now though.