Anti-patterns in Lean

Stream: general

[Daniel Weber]

What are some examples of anti-patterns is Lean?
One example I can think of is using equality of types

[Jireh Loreaux]

1. defeq abuse (this is likely what you meant by "using equality of types"). That is, given a type X : Type, create a new type def Y : Type := X. Then prove theorems about elements of Y by allowing Lean to "see through" the definitional equality and using a theorem about terms of type X.
2. Using subtypes of subtypes. It's almost always a bad idea to start with a type X, some predicate p : X → Prop, create the subtype Y := { x // p x }, then take a predicate q : Y → Prop and create a subtype Z := { y // q y }. It's almost certainly better to use a predicate q' : X → Prop such that ∀ x, q' x ↔ ∃ hx : p x, q ⟨x, hx⟩ and create the subtype Z' := { x // q' x} instead.
3. Sets of sets. This is related to the previous one, but it is rarely the case that you actually want to consider s : Set X and t : Set ↥s; although it does happen occasionally. One of the issues is that if you have s s' : Set X with h : s = s' but h is not rfl (i.e., propeq but not defeq), then it's relatively hard to talk meaningfully about the equality of t : Set ↥s and t' : Set ↥s' and have it do anything useful for you. (Of course, you can say that Subtype.val '' t = Subtype.val '' t', but this probably doesn't buy you much.
4. Over-typing. This comes up a lot when you try to do things "precisely" or avoid junk values. For instance, we have docs#divp, but it is used relatively rarely compared to the usual /. I would argue that's because docs#divp is over-typed (i.e., too much information is required at the time the function is used); of course, there are always a few instances where this level of type safety is actually a good thing, but most of the time it isn't. The solution is often to embrace junk values, and use hypotheses in theorems to specify an input isn't junk. Another example could be the (over-typed) definition of Vector as an inductive definition, versus docs#Mathlib.Vector which is just a subtype of docs#List. Of course, there is a balance that needs to be struck here.
5. Not utilizing forgetful inheritance when designing class hierarchies. I'll just point to #mil for the explanation here. It's often easier at first to avoid forgetful inheritance, but it bites you later.
6. More generally, failing to make instances canonical, thereby ending up with non-defeq (or worse, non-propeq) diamonds. Again, it's natural to just declare an instance whenever you want it, but without careful thought you end up in this situation.
7. marking lemmas as simp because they are "obvious". This might be bad for a whole host of reasons (they have side conditions, they point in the wrong direction, they don't help reduce to a "normal form" even informally).

[Daniel Weber]

By equality of types I meant using HEq and cast

[Damiano Testa]

There was also a similar thread with more suggestions.