syntactic tautology linter

Stream: general

[Patrick Massot]

Could we get a linter checking that no lemma proves a syntactic equality? It seems dumb, but tricky type ascriptions or name clashes actually make them happen. For instance here we see:

@[simp] lemma coe_id : ⇑(id : E →ₗᵢ[R] E) = id := rfl

which looks like it's saying something about turning the identity linear isometry into a plain function. Fun challenge: figure out what's wrong here without using Lean.

The right hand side is not _root_.id, it's linear_isometry.id

You can check the statement is doing nothing with docs#tactic.interactive.guard_target_strict. The linter could test only refl lemmas if it's too slow.

[Eric Wieser]

Also docs#submodule.quotient.mk_eq_mk

[Alex J. Best]

I had a crack at this at branch#alexjbest/tautology-linter, it finds the two examples here and no others in those files, its running on mathlib now: https://github.com/leanprover-community/mathlib/runs/3393269351

[Alex J. Best]

Currently let expressions will confuse it in the sense that this linter won't flag def a below

def a : let b := 1 in b = b := sorry
def c : 1 = 1 := sorry
run_cmd (do get_decl `a >>= check_syn_eq >>= trace)

this should be easily fixable, it doesn't seem too common, but maybe some tactics produce terms like this.
It also might be better to check alpha equivalence instead as:

def a : (let b := 1 in b) = (let c:=1 in c) := sorry

wouldn't be flagged currently.

[Alex J. Best]

The results of the current version:

$ lean -j30 --run ./scripts/lint_mathlib.lean
/- Checking 81627 declarations (plus 80458 automatically generated ones) in mathlib -/

/- The `check_syn_eq` linter reports: -/
/- THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. -/
-- analysis\normed_space\affine_isometry.lean
#print affine_isometry.coe_id /- LHS equals RHS syntactically -/

-- analysis\normed_space\linear_isometry.lean
#print linear_isometry.coe_id /- LHS equals RHS syntactically -/

-- category_theory\sums\basic.lean
#print category_theory.sum_comp_inl /- LHS equals RHS syntactically -/
#print category_theory.sum_comp_inr /- LHS equals RHS syntactically -/

-- linear_algebra\basic.lean
#print submodule.quotient.mk_eq_mk /- LHS equals RHS syntactically -/

So you already found half of them it seems?

[Alex J. Best]

@Scott Morrison What do you think the corrected (i.e. not a tautology) form of docs#category_theory.sum_comp_inl should be, currently the type ascriptions in the source don't force the type you intended,

@[simp] lemma sum_comp_inl {P Q R : C} (f : (inl P : C ⊕ D) ⟶ inl Q) (g : inl Q ⟶ inl R) :
  (id (f ≫ g : inl P ⟶ inl R) : P ⟶ R) = (id f : P ⟶ Q) ≫ (id g : Q ⟶ R) := rfl

seems to work but looks weird, and not like a useful simp lemma anymore to me.

[Eric Wieser]

Instead of id, you probably want to eliminate the notation and put in some @s

[Eric Wieser]

In the same way as we often need @function.injective (A → B) (some_hom A B) coe_fn, and there is no way to spell that with casts alone

[Alex J. Best]

Ok that sounds like a better idea:

@[simp] lemma sum_comp_inl {P Q R : C} (f : (inl P : C ⊕ D) ⟶ inl Q) (g : inl Q ⟶ inl R) :
  @category_struct.comp _ _ (inl P) (inl Q) (inl R) f g =
  @category_struct.comp _ _ P Q R (f : P ⟶ Q) (g : Q ⟶ R) := rfl

[Alex J. Best]

Ok, any idea what docs#submodule.quotient.mk_eq_mk is meant to say?

[Alex J. Best]

Maybe:

@[simp] theorem mk_eq_mk {p : submodule R M} (x : M) : (@_root_.quotient.mk _ (quotient_rel p) x) = mk x := rfl

[Eric Wieser]

Definitely, but I don't think you even need the @ there

[Eric Wieser]

Just the _root_

[Alex J. Best]

It complains that it can't find the setoid instance in that case unfortunately, as the relation above is just a def