fix(tactic/lint): simp_nf: do not ignore errors (#2266)

This PR fixes some bugs in the `simp_nf` linter.  Previously it ignored all errors (from failing tactics).  I've changed this so that errors from linters are handled centrally and reported as linter warnings.  The `simp_is_conditional` function was also broken.

As usual, new linters find new issues:

 1. Apparently Lean sometimes throws away simp lemmas.  leanprover-community/lean#163
 2. Some types define `has_coe` but have an incorrect `has_coe_to_fun`, causing the simplifier to loop `⇑f a = ⇑↑f a = ⇑f a`.  See the new library note:

Author: gebner

src/algebra/field.lean

@@ -234,9 +234,9 @@ section
 variables {β : Type*} [division_ring α] [division_ring β]
 variables (f : α → β) [is_ring_hom f] {x y : α}
 
-@[simp] lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 := (of f).map_ne_zero
+lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 := (of f).map_ne_zero
 
-@[simp] lemma map_eq_zero : f x = 0 ↔ x = 0 := (of f).map_eq_zero
+lemma map_eq_zero : f x = 0 ↔ x = 0 := (of f).map_eq_zero
 
 lemma map_inv : f x⁻¹ = (f x)⁻¹ := (of f).map_inv
 

src/category_theory/monoidal/functorial.lean

@@ -73,10 +73,12 @@ class lax_monoidal (F : C → D) [functorial.{v₁ v₂} F] :=
 
 restate_axiom lax_monoidal.μ_natural'
 attribute [simp] lax_monoidal.μ_natural
+
 restate_axiom lax_monoidal.left_unitality'
-attribute [simp] lax_monoidal.left_unitality
 restate_axiom lax_monoidal.right_unitality'
-attribute [simp] lax_monoidal.right_unitality
+-- The unitality axioms cannot be used as simp lemmas because they require
+-- higher-order matching to figure out the `F` and `X` from `F X`.
+
 restate_axiom lax_monoidal.associativity'
 attribute [simp] lax_monoidal.associativity
 

src/data/indicator_function.lean

@@ -38,7 +38,7 @@ variables [has_zero β] {s t : set α} {f g : α → β} {a : α}
 @[reducible]
 def indicator (s : set α) (f : α → β) : α → β := λ x, if x ∈ s then f x else 0
 
-@[simp] lemma indicator_apply (s : set α) (f : α → β) (a : α) :
+lemma indicator_apply (s : set α) (f : α → β) (a : α) :
   indicator s f a = if a ∈ s then f a else 0 := rfl
 
 @[simp] lemma indicator_of_mem (h : a ∈ s) (f : α → β) : indicator s f a = f a := if_pos h

src/data/set/basic.lean

@@ -287,7 +287,7 @@ not_nonempty_iff_eq_empty.2 rfl
 lemma eq_empty_or_nonempty (s : set α) : s = ∅ ∨ s.nonempty :=
 classical.by_cases or.inr (λ h, or.inl $ not_nonempty_iff_eq_empty.1 h)
 
-@[simp] theorem ne_empty_iff_nonempty : s ≠ ∅ ↔ s.nonempty :=
+theorem ne_empty_iff_nonempty : s ≠ ∅ ↔ s.nonempty :=
 (not_congr not_nonempty_iff_eq_empty.symm).trans classical.not_not
 
 theorem subset_eq_empty {s t : set α} (h : t ⊆ s) (e : s = ∅) : t = ∅ :=

src/linear_algebra/basic.lean

@@ -1358,7 +1358,7 @@ variables [module R M] [module R M₂] [module R M₃]
 include R
 
 instance : has_coe (M ≃ₗ[R] M₂) (M →ₗ[R] M₂) := ⟨to_linear_map⟩
-
+-- see Note [function coercion]
 instance : has_coe_to_fun (M ≃ₗ[R] M₂) := ⟨_, λ f, f.to_fun⟩
 
 @[simp] theorem coe_apply (e : M ≃ₗ[R] M₂) (b : M) : (e : M →ₗ[R] M₂) b = e b := rfl

src/logic/basic.lean

@@ -66,6 +66,33 @@ theorem coe_sort_coe_trans
   {α β γ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ]
   (x : α) : @coe_sort α _ x = @coe_sort β _ x := rfl
 
+/--
+Many structures such as bundled morphisms coerce to functions so that you can
+transparently apply them to arguments. For example, if `e : α ≃ β` and `a : α`
+then you can write `e a` and this is elaborated as `⇑e a`. This type of
+coercion is implemented using the `has_coe_to_fun`type class. There is one
+important consideration:
+
+If a type coerces to another type which in turn coerces to a function,
+then it **must** implement `has_coe_to_fun` directly:
+```lean
+structure sparkling_equiv (α β) extends α ≃ β
+
+-- if we add a `has_coe` instance,
+instance {α β} : has_coe (sparkling_equiv α β) (α ≃ β) :=
+⟨sparkling_equiv.to_equiv⟩
+
+-- then a `has_coe_to_fun` instance **must** be added as well:
+instance {α β} : has_coe_to_fun (sparkling_equiv α β) :=
+⟨λ _, α → β, λ f, f.to_equiv.to_fun⟩
+```
+
+(Rationale: if we do not declare the direct coercion, then `⇑e a` is not in
+simp-normal form. The lemma `coe_fn_coe_base` will unfold it to `⇑↑e a`. This
+often causes loops in the simplifier.)
+-/
+library_note "function coercion"
+
 @[simp] theorem coe_sort_coe_base
   {α β} [has_coe α β] [has_coe_to_sort β]
   (x : α) : @coe_sort α _ x = @coe_sort β _ x := rfl

src/order/order_iso.lean

@@ -206,8 +206,10 @@ def to_order_embedding (f : r ≃o s) : r ≼o s :=
 ⟨f.to_equiv.to_embedding, f.ord⟩
 
 instance : has_coe (r ≃o s) (r ≼o s) := ⟨to_order_embedding⟩
+-- see Note [function coercion]
+instance : has_coe_to_fun (r ≃o s) := ⟨λ _, α → β, λ f, f⟩
 
-theorem coe_coe_fn (f : r ≃o s) : ((f : r ≼o s) : α → β) = f := rfl
+@[simp] lemma coe_coe_fn (f : r ≃o s) : ((f : r ≼o s) : α → β) = f := rfl
 @[simp] lemma to_equiv_to_fun (f : r ≃o s) (x : α) : f.to_equiv.to_fun x = f x := rfl
 
 theorem ord' : ∀ (f : r ≃o s) {a b}, r a b ↔ s (f a) (f b)

src/set_theory/ordinal.lean

@@ -58,8 +58,6 @@ def of_iso (f : r ≃o s) : r ≼i s :=
   rcases f.2 _ _ h with ⟨a', rfl⟩, exact ⟨a', rfl⟩
 end⟩
 
-@[simp] theorem of_iso_apply (f : r ≃o s) (x : α) : (f : r ≼o s) x = f x := rfl
-
 @[simp] theorem refl_apply (x : α) : initial_seg.refl r x = x := rfl
 
 @[simp] theorem trans_apply (f : r ≼i s) (g : s ≼i t) (a : α) : (f.trans g) a = g (f a) := rfl
@@ -195,9 +193,7 @@ def lt_equiv {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ 
 ⟨@order_embedding.trans _ _ _ r s t f g, g f.top,
   begin
     intro x,
-    rw [←g.right_inv x],
-    simp only [order_iso.to_equiv_to_fun, coe_fn_coe_base, order_embedding.trans_apply],
-    rw [←order_iso.ord'' g, f.down', exists_congr],
+    rw [← g.right_inv x, order_iso.to_equiv_to_fun, ← order_iso.ord' g, f.down', exists_congr],
     intro y, exact ⟨congr_arg g, λ h, g.to_equiv.bijective.1 h⟩
   end⟩
 

src/tactic/core.lean

@@ -1437,6 +1437,18 @@ meta def finally {β} (tac : tactic α) (finalizer : tactic β) : tactic α :=
      | (result.exception msg p s') := (finalizer >> result.exception msg p) s'
      end
 
+/-- `decorate_error add_msg tac` prepends `add_msg` to an exception produced by `tac` -/
+meta def decorate_error (add_msg : string) (tac : tactic α) : tactic α | s :=
+match tac s with
+| result.exception msg p s :=
+  let msg (_ : unit) : format := match msg with
+    | some msg := add_msg ++ format.line ++ msg ()
+    | none := add_msg
+    end in
+  result.exception msg p s
+| ok := ok
+end
+
 /-- Applies tactic `t`. If it succeeds, revert the state, and return the value. If it fails,
   returns the error message. -/
 meta def retrieve_or_report_error {α : Type u} (t : tactic α) : tactic (α ⊕ string) :=

src/tactic/lint.lean

@@ -532,33 +532,50 @@ end
 private meta def simp_lhs (ty : expr): tactic expr :=
 prod.fst <$> simp_lhs_rhs ty
 
-/-- `simp_is_conditional ty` returns true iff the simp lemma with type `ty` is conditional. -/
-private meta def simp_is_conditional : expr → tactic bool | ty := do
+/--
+`simp_is_conditional_core ty` returns `none` if `ty` is a conditional simp
+lemma, and `some lhs` otherwise.
+-/
+private meta def simp_is_conditional_core : expr → tactic (option expr) | ty := do
 ty ← whnf ty transparency.semireducible,
 match ty with
-| `(¬ %%lhs) := pure ff
-| `(%%lhs = _) := pure ff
-| `(%%lhs ↔ _) := pure ff
-| (expr.pi n bi a b) :=
-  if bi ≠ binder_info.inst_implicit ∧ ¬ b.has_var then
-    pure tt
-  else do
-    l ← mk_local' n bi a,
-    simp_is_conditional (b.instantiate_var l)
-| ty := pure ff
+| `(¬ %%lhs) := pure lhs
+| `(%%lhs = _) := pure lhs
+| `(%%lhs ↔ _) := pure lhs
+| (expr.pi n bi a b) := do
+  l ← mk_local' n bi a,
+  some lhs ← simp_is_conditional_core (b.instantiate_var l) | pure none,
+  if bi ≠ binder_info.inst_implicit ∧
+      ¬ (lhs.abstract_local l.local_uniq_name).has_var then
+    pure none
+  else
+    pure lhs
+| ty := pure ty
 end
 
+/--
+`simp_is_conditional ty` returns true iff the simp lemma with type `ty` is conditional.
+-/
+private meta def simp_is_conditional (ty : expr) : tactic bool :=
+option.is_none <$> simp_is_conditional_core ty
+
 private meta def heuristic_simp_lemma_extraction (prf : expr) : tactic (list name) :=
 prf.list_constant.to_list.mfilter is_simp_lemma
 
+/-- Checks whether two expressions are equal for the simplifier. That is,
+they are reducibly-definitional equal, and they have the same head symbol. -/
+meta def is_simp_eq (a b : expr) : tactic bool :=
+if a.get_app_fn.const_name ≠ b.get_app_fn.const_name then pure ff else
+succeeds $ is_def_eq a b transparency.reducible
+
 /-- Reports declarations that are simp lemmas whose left-hand side is not in simp-normal form. -/
 meta def simp_nf_linter (timeout := 200000) (d : declaration) : tactic (option string) := do
 tt ← is_simp_lemma d.to_name | pure none,
 -- Sometimes, a definition is tagged @[simp] to add the equational lemmas to the simp set.
 -- In this case, ignore the declaration if it is not a valid simp lemma by itself.
 tt ← is_valid_simp_lemma_cnst d.to_name | pure none,
-(λ tac, tactic.try_for timeout tac <|> pure (some "timeout")) $ -- last resort
-(λ tac : tactic _, tac <|> pure none) $ -- tc resolution depth
+[] ← get_eqn_lemmas_for ff d.to_name | pure none,
+try_for timeout $
 retrieve $ do
 reset_instance_cache,
 g ← mk_meta_var d.type,
@@ -567,14 +584,16 @@ intros,
 (lhs, rhs) ← target >>= simp_lhs_rhs,
 sls ← simp_lemmas.mk_default,
 let sls' := sls.erase [d.to_name],
--- TODO: should we do something special about rfl-lemmas?
-(lhs', prf1) ← simplify sls [] lhs {fail_if_unchanged := ff},
+(lhs', prf1) ← decorate_error "simplify fails on left-hand side:" $
+  simplify sls [] lhs {fail_if_unchanged := ff},
 prf1_lems ← heuristic_simp_lemma_extraction prf1,
 if d.to_name ∈ prf1_lems then pure none else do
-(rhs', prf2) ← simplify sls [] rhs {fail_if_unchanged := ff},
-lhs'_eq_rhs' ← succeeds (is_def_eq lhs' rhs' transparency.reducible),
-lhs_in_nf ← succeeds (is_def_eq lhs' lhs transparency.reducible),
-if lhs'_eq_rhs' ∧ lhs'.get_app_fn.const_name = rhs'.get_app_fn.const_name then do
+is_cond ← simp_is_conditional d.type,
+(rhs', prf2) ← decorate_error "simplify fails on right-hand side:" $
+  simplify sls [] rhs {fail_if_unchanged := ff},
+lhs'_eq_rhs' ← is_simp_eq lhs' rhs',
+lhs_in_nf ← is_simp_eq lhs' lhs,
+if lhs'_eq_rhs' then do
   used_lemmas ← heuristic_simp_lemma_extraction (prf1 prf2),
   pure $ pure $ "simp can prove this:\n"
     ++ "  by simp only " ++ to_string used_lemmas ++ "\n"
@@ -589,6 +608,8 @@ else if ¬ lhs_in_nf then do
       ++ "to" ++ lhs'.group.indent 2 ++ format.line
       ++ "using " ++ (to_fmt prf1_lems).group.indent 2 ++ format.line
       ++ "Try to change the left-hand side to the simplified term!\n"
+else if ¬ is_cond ∧ lhs = lhs' then do
+  pure "Left-hand side does not simplify.\nYou need to debug this yourself using `set_option trace.simplify.rewrite true`"
 else
   pure none
 
@@ -705,8 +726,17 @@ checks.mmap $ λ ⟨linter_name, linter⟩, do
   let test_decls := if linter.auto_decls then all_decls else non_auto_decls,
   results ← test_decls.mfoldl (λ (results : rb_map name string) decl, do
     tt ← should_be_linted linter_name decl.to_name | pure results,
-    some linter_warning ← linter.test decl | pure results,
-    pure $ results.insert decl.to_name linter_warning) mk_rb_map,
+    s ← read,
+    let linter_warning : option string :=
+      match linter.test decl s with
+      | result.success w _ := w
+      | result.exception msg _ _ :=
+        some $ "LINTER FAILED:\n" ++ msg.elim "(no message)" (λ msg, to_string $ msg ())
+      end,
+    match linter_warning with
+    | some w := pure $ results.insert decl.to_name w
+    | none := pure results
+    end) mk_rb_map,
   pure (linter_name, linter, results)
 
 /-- Sorts a map with declaration keys as names by line number. -/