search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

Dangerous simp lemmas #118

Open gebner opened 2 years ago

gebner commented 2 years ago

We mark some lemmas as simp that were innocuous in Lean 3, but are dangerous now.

The typical case is that the lhs is reducible. For example, Lean 3 triggered only on inj_on applications, while Lean 4 tries to apply the lemma to everything (often causing nontermination):

attribute [-simp] Set.inj_on_empty Set.inj_on_singleton
digama0 commented 2 years ago

Can we backport remove these? It should not be too hard to write a lint for mathlib to detect them.

gebner commented 2 years ago

We could also remove reducible from set.inj_on.

digama0 commented 2 years ago

That would be another way to silence the lint, yes. (And I agree that's the way to go here.)